Intro

Casemate is a tool for testing systems software use of low-level hardware primitives.

Systems software must often perform low-level operations which interact with specific hardware mechanisms, such as cache and TLB maintenance, updating page tables, updates to the system configuration, and so on. Software must ensure that particular protocols are observed when doing such an operation, and failure to do so can result in loss of service or security guarantees.

On Arm, updates to page tables must follow a particular break-before-make protocol. Failure to do so leads to an unpredictable state which invalidates many of the security guarantees a hypervisor or operating system, or other such isolation kernel, seek to provide. Casemate is powered by the Casemate model, which encodes a number of such protocols to monitor and validate that systems software is correctly following the protocols and to call out violations when they occur.

Casemate has two modes of operation:

  • Online: as a library (casemate-lib), Casemate can run with the code monitoring accesses and reporting failures at runtime.

  • Offline: as an external tool (casemate-check), Casemate can check a log file for violations.

Casemate currently supports Arm-A, and the following page table protocols:

  • Updating page tables with break-before-make. (For both Stage 1 and Stage 2).

  • Allocation, zeroing, freeing, and re-use of page tables.

  • Context switching between different page tables.

  • Thread-local address spaces.

The Casemate model

The Casemate model tracks each location with a finite state machine which encodes the protocol that the location should be following, e.g. break-before-make. This automaton takes steps on each operation: page table write, TLB maintenace, system register update, and barrier. When an operation that is not supported by the current state of that location takes place, the Casemate model indicates a violation of the protocol, and Casemate reports an error to the user.

The Casemate top-level automaton tracks, for each potential page table location, whether it is clean. Unclean locations then require the proper TLB maintenance.

toplevelautomaton

The protocol is hierarchical: globally, we track whether each page table location has been cleaned enough since previous TLBs to now be writeable; individually, each thread must follow a sub-protocol to perform the necessary cleaning to transition the global state from unclean to clean.

The Casemate cleaning sub-protocol requires a single thread to perform all the necessary cleaning with the correct barriers, to ensure that the location is seen as clean globally.

subautomaton

To ensure that the automata do not miss transitions due to racy concurrent accesses, the Casemate model can, optionally, check data race freedom over the page tables (at a per-tree granularity), reporting a violation if two threads try to access the same page table tree at the same time.

Casemate-Check: CLI and Usage

casemate-check takes a log file and performs an offline check for protcol violations.

Usage

Usage: casemate-check FILE [OPTIONS]

General options:

  • -h | --help prints help text.

  • -q makes the tool quiet, with no output.

  • --color enable ANSI escape color codes

  • -a | --no-color force ascii-only, no ANSI escape color codes

Model options:

  • -R | --racy do not check locks/synchronisation are respected

  • -C | --dry-run do not run checks

Output options:

  • -c condensed trace format

  • -p | --print print state out at each step

  • -t | --trace print trace record for each step

  • -T | --no-trace do not print trace record for each step

  • -d | --diff show diffs of state

  • -U | --all show all (including unclean) locations in states/diffs

  • -W<addr> watch this address

Other:

  • -D | --debug debug mode

Example usage

The following is a log file generated by the good_bbm example, and can be generated by running the associated code (see the examples README).

$ cat example.log
(mem-init (id 0) (tid 0) (address 0xaaaadce53000) (size 0x1000) (src "examples/tests/good_bbm.c:25"))
(mem-init (id 1) (tid 0) (address 0xaaaadce54000) (size 0x1000) (src "examples/tests/good_bbm.c:26"))
(mem-init (id 2) (tid 0) (address 0xaaaadce55000) (size 0x1000) (src "examples/tests/good_bbm.c:27"))
(hint (id 3) (tid 0) (kind set_root_lock) (location 0xaaaadce53000) (value 0xaaaadce56000) (src "examples/tests/good_bbm.c:28"))
(hint (id 4) (tid 0) (kind set_owner_root) (location 0xaaaadce54000) (value 0xaaaadce53000) (src "examples/tests/good_bbm.c:29"))
(hint (id 5) (tid 0) (kind set_owner_root) (location 0xaaaadce55000) (value 0xaaaadce53000) (src "examples/tests/good_bbm.c:30"))
(mem-write (id 6) (tid 0) (mem-order plain) (address 0xaaaadce53000) (value 0xaaaadce54003) (src "examples/tests/good_bbm.c:33"))
(sysreg-write (id 7) (tid 0) (sysreg vttbr_el2) (value 0xaaaadce53000) (src "examples/tests/good_bbm.c:36"))
(lock (id 8) (tid 0) (address 0xaaaadce56000) (src "examples/tests/good_bbm.c:38"))
(mem-write (id 9) (tid 0) (mem-order plain) (address 0xaaaadce53000) (value 0x0) (src "examples/tests/good_bbm.c:39"))
(barrier (id 10) (tid 0) dsb (kind ish) (src "examples/tests/good_bbm.c:40"))
(tlbi (id 11) (tid 0) ipas2e1is (addr 0x0) (level 0x3) (src "examples/tests/good_bbm.c:41"))
(barrier (id 12) (tid 0) dsb (kind ish) (src "examples/tests/good_bbm.c:42"))
(tlbi (id 13) (tid 0) vmalle1is (src "examples/tests/good_bbm.c:43"))
(barrier (id 14) (tid 0) dsb (kind ish) (src "examples/tests/good_bbm.c:44"))
(mem-write (id 15) (tid 0) (mem-order plain) (address 0xaaaadce53000) (value 0xaaaadce55003) (src "examples/tests/good_bbm.c:45"))
(unlock (id 16) (tid 0) (address 0xaaaadce56000) (src "examples/tests/good_bbm.c:46"))

casemate-check can be used to check this log for violations:

$ ./casemate-check examples/expected/good_bbm.log
[...]
casemate-check: log checked successfully.

Checking racy executions

Here is a log from a racy execution

$ cat bad_race.log
(mem-init (id 0) (tid 0) (address 0xaaaad7824000) (size 0x1000) (src "examples/tests/bad_race.c:34"))
(hint (id 1) (tid 0) (kind set_root_lock) (location 0xaaaad7824000) (value 0xaaaad7825000) (src "examples/tests/bad_race.c:35"))
(sysreg-write (id 2) (tid 0) (sysreg vttbr_el2) (value 0xaaaad7824000) (src "examples/tests/bad_race.c:38"))
(mem-write (id 4) (tid 1) (mem-order release) (address 0xaaaad7824008) (value 0x1) (src "examples/tests/bad_race.c:24"))
(mem-write (id 3) (tid 2) (mem-order release) (address 0xaaaad7824008) (value 0x1) (src "examples/tests/bad_race.c:24"))

Note the two concurrently writes from threads 1 and 2 to the same location without sufficient locking. Running this with casemate-check reports an error, that the concurrent accesses are not locked.

One can disable race detection with the -R flag. Full break-before-make checking is done on the trace, but does not guarantee that there are no data races on the locations.

$ ./casemate-check bad_race.log
[...]
! must write to pte while holding owner lock

$ ./casemate-check -R bad_race.log
[...]
casemate-check: log checked successfully.

Printing model state

By default, casemate-check prints out the trace as it goes. More information can be seen by supplying the -p or -d options.

-p prints out the Casemate model state at each step. By default, this is only for the unclean locations. All locations can be seen by printing unclean (-pU).

More often it is more useful to show just the change to the state on each step. This can be achieved by passing -d to produce diffs.

$ ./casemate-check ./examples/expected/good_bbm.log -d
(mem-init (id 0) (tid 0) (address 0xaaaadce53000) (size 0x1000) (src ""examples/tests/good_bbm.c:25":0"))
<identical>
(mem-init (id 1) (tid 0) (address 0xaaaadce54000) (size 0x1000) (src ""examples/tests/good_bbm.c:26":0"))
<identical>
(mem-init (id 2) (tid 0) (address 0xaaaadce55000) (size 0x1000) (src ""examples/tests/good_bbm.c:27":0"))
<identical>
(hint (id 3) (tid 0) (kind set_root_lock) (location 0xaaaadce53000) (value 0xaaaadce56000) (src ""examples/tests/good_bbm.c:28":0"))
<identical>
(hint (id 4) (tid 0) (kind set_owner_root) (location 0xaaaadce54000) (value 0xaaaadce53000) (src ""examples/tests/good_bbm.c:29":0"))
<identical>
(hint (id 5) (tid 0) (kind set_owner_root) (location 0xaaaadce55000) (value 0xaaaadce53000) (src ""examples/tests/good_bbm.c:30":0"))
<identical>
(mem-write (id 6) (tid 0) (mem-order plain) (address 0xaaaadce53000) (value 0xaaaadce54003) (src ""examples/tests/good_bbm.c:33":0"))
<identical>
(sysreg-write (id 7) (tid 0) (sysreg vttbr_el2) (value 0xaaaadce53000) (src ""examples/tests/good_bbm.c:36":0"))
<identical>
(lock (id 8) (tid 0) (address 0xaaaadce56000) (src ""examples/tests/good_bbm.c:38":0"))
<identical>
(mem-write (id 9) (tid 0) (mem-order plain) (address 0xaaaadce53000) (value 0x0) (src ""examples/tests/good_bbm.c:39":0"))
mem:
    -*[  0xaaaadce53000]=    aaaadce54003 (pte_st:V       root:  0xaaaadce53000, range:               0-      8000000000)
    +*[  0xaaaadce53000]=               0 (pte_st:IU n  0 root:  0xaaaadce53000, range:               0-      8000000000)
(barrier (id 10) (tid 0) dsb (kind ish) (src ""examples/tests/good_bbm.c:40":0"))
mem:
    -*[  0xaaaadce53000]=               0 (pte_st:IU n  0 root:  0xaaaadce53000, range:               0-      8000000000)
    +*[  0xaaaadce53000]=               0 (pte_st:IU d  0 root:  0xaaaadce53000, range:               0-      8000000000)
(tlbi (id 11) (tid 0) ipas2e1is (addr 0x0) (level 0x0) (src ""examples/tests/good_bbm.c:41":0"))
mem:
    -*[  0xaaaadce53000]=               0 (pte_st:IU d  0 root:  0xaaaadce53000, range:               0-      8000000000)
    +*[  0xaaaadce53000]=               0 (pte_st:IU ti 0 root:  0xaaaadce53000, range:               0-      8000000000)
(barrier (id 12) (tid 0) dsb (kind ish) (src ""examples/tests/good_bbm.c:42":0"))
mem:
    -*[  0xaaaadce53000]=               0 (pte_st:IU ti 0 root:  0xaaaadce53000, range:               0-      8000000000)
    +*[  0xaaaadce53000]=               0 (pte_st:IU td 0 root:  0xaaaadce53000, range:               0-      8000000000)
(tlbi (id 13) (tid 0) vmalle1is (src ""examples/tests/good_bbm.c:43":0"))
mem:
    -*[  0xaaaadce53000]=               0 (pte_st:IU td 0 root:  0xaaaadce53000, range:               0-      8000000000)
    +*[  0xaaaadce53000]=               0 (pte_st:IU ta 0 root:  0xaaaadce53000, range:               0-      8000000000)
(barrier (id 14) (tid 0) dsb (kind ish) (src ""examples/tests/good_bbm.c:44":0"))
mem:
    -*[  0xaaaadce53000]=               0 (pte_st:IU ta 0 root:  0xaaaadce53000, range:               0-      8000000000)
    +*[  0xaaaadce53000]=               0 (pte_st:I     0 root:  0xaaaadce53000, range:               0-      8000000000)
(mem-write (id 15) (tid 0) (mem-order plain) (address 0xaaaadce53000) (value 0xaaaadce55003) (src ""examples/tests/good_bbm.c:45":0"))
<identical>
(unlock (id 16) (tid 0) (address 0xaaaadce56000) (src ""examples/tests/good_bbm.c:46":0"))
<identical>
casemate-check: log checked successfully.

We can see that the first write to 0xaaaadce53000 transitions that location’s state from valid (V) to invalid-but-unclean (IU) with no synchronisation (n). The following DSB on the same thread transitions the state to invalid-unclean but with DSB synchronisation (IU d). The subsequent TLBI-IPA transitions the per-thread state to invalid-unclean but with TLB maintenance but no synchronisation (IU ti). Then the DSB moves the per-thread state to invalid-unclean, with synchronised TLB maintenance (IU td), before the final TLBI-ALL puts the state in the IU ta state representing the fully-cleaned (but not yet globally synchronised) TLB maintenance. The final DSB then transitions the global state from invalid-unclean with some thread-local state to a new global invalid-clean state (I).

State format

The format of locations printed by -p and -d are compact representations of the state machine.

Each location is printed as

<UNCLEAN MARK ?>[<ADDRESS>]=<VALUE> (pte_st:<STATE> root: <PAGETABLE ROOT ADDRESS> range: <IA RANGE>)

Where:

  • <UNCLEAN MARK> is either empty or a single * if the location is unclean.

  • <STATE> is the top-level automata state, one of:

    • V for valid; **IU <ukind> <old value> for invalid-but-unclean values, where ukind is the per-thread automata state (see below);

    • or I <old value> for invalid-and-clean locations.

  • <IA RANGE> is the range of input addresses (virtual, or intermediate-physical) that this page table entry maps.

  • <ukind> is the per-thread pte state, for the thread that invalidated the entry, and is one of:

    • n for no synchronisation;

    • d for a single DSB without any TLB maintenance;

    • ti for having done a TLBI-by-IPA for this pte’s range, but not yet synchronised;

    • td for the TLBI-by-IPA which has been synchronised (by a DSB);

    • ta for having been TLBI-by-VA or TLBI-ALL cleaned.

Note that the per-thread pte states do not include the trailing DSB as that transitions the global automata state not the per-thread one.

Watching locations

On a large trace, even simple diffs may be too noisy. It is possible to tell the Casemate model to 'watch' only particular locations, and print out only transitions which touch them.

For example, watching location 0xaaaadce55000 (the new child page) in the above trace we get prints only for two transitions: the first initialises it; the other is not a transition to that location but to its parent which affects the state of the child, so is also counted in the watch. In this case the global pte state of that particular location is unchanged, so the diffs are empty.

./casemate-check ./examples/expected/good_bbm.log -d -W0xaaaadce55000
(mem-init (id 2) (tid 0) (address 0xaaaadce55000) (size 0x1000) (src ""examples/tests/good_bbm.c:27":0"))
<identical>
(mem-write (id 15) (tid 0) (mem-order plain) (address 0xaaaadce53000) (value 0xaaaadce55003) (src ""examples/tests/good_bbm.c:45":0"))
<identical>
casemate-check: log checked successfully.

This only affects the printing, the full model is simulated and checks still performed for all locations.

Casemate-Lib: Usage

Casemate can be compiled as a standalone library, which can be linked into systems software, in order to:

  • Generate casemate-check-compatible logs.

  • Simulate the Casemate model and report violations at runtime.

Compiling, linking, and the Ghost driver

Running make at the top-level should produce a src/lib/casemate.o object file and src/lib/casemate.h header. These are what casemate-check use to drive the model, but could be used by a third-party build process to link casemate into a pre-existing system. Alternatively, one can build casemate directly in that toolchain, for example see src/lib/Makefile.linux for a Makefile which can be included from the Linux build system to include Casemate in the Linux kernel.

Once Casemate is available, the user needs call two initialisation functions:

  • initialise_casemate_model passing some memory for Casemate to use to store the model state, and the initial model configuration options; and

  • initialise_ghost_driver which provides Casemate a set of callbacks for performing side-effects in the system.

/* An example Casemate initialisation procedure */
void initialise_casemate(u64 phys_memory_start, u64 phys_memory_size)
{
	struct casemate_options opts = CASEMATE_DEFAULT_OPTS;
	void *state_addr = malloc(sizeof(struct casemate_model_state)); // or 2x that if enabling diffing.
	initialise_casemate_model(&opts, phys_memory_start, phys_memory_size, state_addr, sizeof(struct casemate_model_state));

	struct ghost_driver sm_driver = {
		.read_physmem = NULL,
		.read_sysreg = read_sysreg_callback,
		...
	};
	initialise_ghost_driver(&sm_driver);

	u64 pgtable_root = EXTRACT_ROOT(read_sysreg(ttbr0_el2));

	/* Initialise the currently loaded pagetable's memory */
	FOREACH_PGTABLE_NODE(table, pgtable_root) {
		casemate_model_step_init(table, 4096);
		FOREACH_ENTRY(entry, table) {
			casemate_model_step_write(WMO_plain, virt_to_phys(entry), *entry);
		}
	}

	/* tell the model it's owned by this lock and currently loaded */
	casemate_model_step_hint(GHOST_HINT_SET_ROOT_LOCK, pgtable_root, virt_to_phys(pgtable_lock));
	casemate_model_step_msr(SYSREG_TTBR_EL2, pgtable_root);
}

Casemate Model initialisation and configuration

An example configuration

(struct casemate_options){
  .enable_tracing = true,
  .enable_checking = true,
  .track_watchpoints = false,
  .log_opts = (struct casemate_log_options){
		.log_format_version = 1,
		.condensed_format = false,
	},
  .check_opts = (struct casemate_checker_options){
		.promote_DSB_nsh = false,
		.promote_TLBI_nsh = false,
		.promote_TLBI_by_id = false,
		.check_synchronisation = true,
		.enable_printing = false,
		.print_opts = CM_PRINT_DIFF_TO_STATE_ON_STEP | CM_PRINT_ONLY_UNCLEAN,
	},
  .enable_safety_checks = false,
}

See the full configuration datatype definition at github.com/rems-project/casemate/blob/main/src/lib/include/casemate-in/casemate-config.in.h.

The options should be passed to initialise_casemate_model, which takes a snapshot. Options cannot currently be changed after initialisation.

Ghost driver

Whenever the Casemate model needs to perform an operation with or as a side-effect, e.g. reading physical memory, printing a log record, or reporting a violation, it does so through a generic ghost driver that the user initialises as a struct-of-function-pointers.

An exmple driver from casemate-check is given below:

u64 __read_sysreg_cb(enum ghost_sysreg_kind sysreg)
{
	/* perform side-effect of reading system register */
}

void __abort_cb(const char *msg)
{
	exit(1);
}

/* callbacks for printing to string buffers
 * since Casemate cannot use printf/malloc it is all driven by the driver */
struct _string_buffer {
	char *buf;
	int n;
};

int __sprintf_cb(void* arg, const char *format, va_list ap)
{
	int ret;
	if (arg != NULL) {
		struct _string_buffer *buf = arg;
		ret = vsnprintf(buf->buf, buf->n, format, ap);
		if (ret < 0)
			return ret;
		buf->buf += ret;
		buf->n -= ret;
		return 0;
	} else {
		ret = vprintf(format, ap);
		if (ret < 0)
			return ret;
		return 0;
	}
}

void *__malloc_stringbuf_cb(char* arg, u64 n)
{
	struct _string_buffer *buf = malloc(sizeof(struct _string_buffer));
	buf->buf = arg;
	buf->n = n;
	return buf;
}

void __free_stringbuf_cb(void *buf)
{
	free(buf);
}

/* logs a transition record */
void __trace_cb(const char *record)
{
	printf("%s\n", record);
}

/* casemate-check driver */
struct ghost_driver sm_driver = {
  .read_physmem = NULL,  /* casemate-check never reads real memory */
  .read_sysreg = __read_sysreg_cb,
  .abort = __abort_cb,
  .print = __sprintf_cb,
  .sprint_create_buffer = __malloc_stringbuf_cb,
  .sprint_destroy_buffer = __free_stringbuf_cb,
  .trace = __trace_cb,
};

See the full casemate-check driver definition at github.com/rems-project/casemate/blob/main/src/casemate-check-c/src/driver.c.

Generating logs

Ensure enable_tracing is true in the configuration, and an appropriate trace callback is defined in the driver, then stepping the model will output properly formatted trace records.

Configuring for runtime checks

Ensure enable_checking is true in the configuration, then Stepping the model will perform checks, and report violations via the abort callback in the driver.

Stepping the model

Once initialised the Casemate model is ready to begin taking steps immediately.

The model transitions are broadly separated into three categories:

  • hardware steps, for individual accesses and instructions.

  • abstract steps, for C-level abstract actions (e.g. variable initialisation and memset).

  • hints, for providing out-of-band ownership information.

See the full transition interface at github.com/rems-project/casemate/blob/main/src/lib/include/casemate-in/casemate-helpers.in.h.

Hardware steps

  • casemate_model_step_write(MEMORY_ORDER, LOC, VAL)

  • casemate_model_step_read(LOC, VAL)

Reads do not transition the state, but check the value is consistent with the current state. In this way, they behave as a sanity check.

  • casemate_model_step_dsb(DxB_KIND)

  • casemate_model_step_isb()

  • casemate_model_step_tlbi1(TLBI_KIND)

  • casemate_model_step_tlbi3(TLBI_KIND, PAGE_NUMBER, LEVEL_HINT)

  • casemate_model_step_msr(SYSREG_KIND, VAL)

Abstract steps

  • casemate_model_step_init(LOC, SIZE) - Zero initialise a region.

  • casemate_model_step_memset(LOC, VAL, SIZE)

  • casemate_model_step_lock(LOC) and casemate_model_step_unlock(LOC) for acquiring/releasing a lock.

Hint steps

There is only one hint transition:

  • casemate_model_step_hint(HINT_KIND, LOC, VAL), where HINT_KIND is one of:

    • GHOST_HINT_SET_ROOT_LOCK to associate a pagetable root with a particular lock.

    • GHOST_HINT_SET_OWNER_ROOT to associate a pagetable location with a particular tree.

    • GHOST_HINT_RELEASE_TABLE to remove association of a page table and its children with its parents.

    • GHOST_HINT_SET_PTE_THREAD_OWNER to mark a particular location as thread-local.

See the full transition datatype definitions at github.com/rems-project/casemate/blob/main/src/lib/include/casemate-in/casemate-transitions.in.h.

Casemate trace format

The offline trace checker consumes traces from a runtime execution, and performs the break-before-make dynamic check on those traces.

The traces are a sequence of records, where each record is a trace event tagged with a sequence ID and an originating thread ID:

SEQ = "(", "id", int, ")";
TID = "(", "thread", int, ")";
SRC = "(", "src", (string | int), ")"

TRANSITION =
    MEM-WRITE
  | MEM-READ
  | MEM-INIT
  | MEM-SET
  | BARRIER
  | TLBI
  | SYSREG
  | HINT
  | LOCK
  ;

RECORD(t: TRANSITION) =
    "(", t[0], SEQ, TID, t[1..], SRC?, ")"
  ;

Records are s-exps which start with the name of the transition, followed by the sequence and thread IDs, then the remainin fields, with the source location in final position.

The source location is optional, and is either a string containing the source line or an integer key into an externally defined map from tracepoint to source location.

transitions

mem-write

A write to potentially-pagetable memory.

MEM-WRITE =
    "mem-write",
         "(", "mem-order", ( "PLAIN" | "RELEASE" ), ")",
         "(", "address", u64, ")",
         "(", "value", u64, ")";

mem-read

A read of potentially-pagetable memory.

MEM-READ =
    "mem-read",
         "(", "address", u64, ")",
         "(", "value", u64, ")";

mem-init

Zero initialise memory.

MEM-INIT =
    "mem-init",
         "(", "address", u64, ")",
         "(", "size", u64, ")";

mem-set

Wide memory write. Writes value to every byte of the given region.

address must be aligned on an 8-byte boundary, and size a multiple of 8.

equvialent to efficiently performing a sequence of WRITE-MEM transitions.

MEM-SET =
    "mem-set",
         "(", "address", u64, ")",
         "(", "size", u64, ")",
         "(", "value", u8, ")";

barrier

Barriers/fences.

BARRIER =
    "barrier", BARRIER-KIND;

DxB-KIND =
    "ish"
  | "ishst"
  | "nsh"
  | "sy"
  ;

BARRIER-DSB =
    "dsb",
      "(", "kind", DxB-KIND, ")"

BARRIER-KIND =
    "isb" | BARRIER-DSB;

TLBIs

TLBI =
    "tlbi",
         (TLBI-OP-ALL | TLBI-OP-ADDR);

TLBI-OP-ALL =
    "vmalls12e1"
  | "vmalls12e1is"
  | "vmalle1is"
  | "alle1is"
  | ...
  ;

TLBI-OP-ADDR-KIND =
    "vae2"
  | "vae2is"
  | "ipas2e1is"
  | ...
  ;

TLBI-OP-ADDR =
    TLBI-OP-ADDR-KIND,
      "(", "addr", u64, ")",
      "(", "level", u64, ")"
  ;

MSR (SysReg Write)

SYSREG =
    "sysreg-write"
        "(", "sysreg", ( "vttbr_el2" | "ttbr0_el2" ), ")",
        "(", "value", u64, ")"
  ;

HINTs

Hint transitions update purely logical state, associating pagetables with locks and so on.

HINT_KIND =
      "set_root_lock"
    | "set_owner_root"
    | "release_table"
    | "set_pte_thread_owner"
    ;

HINT =
    "hint",
         "(", "kind", HINT_KIND, ")",
         "(", "location", u64, ")",
         "(", "value", u64, ")";

LOCKs

Acquire/release of a pagetable-owning lock.

LOCK =
    ("lock" | "unlock"),
         "(", "address", u64, ")"

Example trace

(mem-init
  (id 0)
  (tid 0)
  (address 0xaaaaaf200000)
  (size 0x1000)
  (src "test04_bad_bbm_missing_tlbi.c:29"))
(mem-init
  (id 1)
  (tid 0)
  (address 0xaaaaaf201000)
  (size 0x1000)
  (src "test04_bad_bbm_missing_tlbi.c:30"))
(hint
  (id 2)
  (tid 0)
  (kind set_root_lock)
  (location 0xaaaaaf200000)
  (value 0xaaaaaf203000)
  (src "test04_bad_bbm_missing_tlbi.c:31"))
(hint
  (id 3)
  (tid 0)
  (kind set_owner_root)
  (location 0xaaaaaf201000)
  (value 0xaaaaaf200000)
  (src "test04_bad_bbm_missing_tlbi.c:32"))
(hint
  (id 4)
  (tid 0)
  (kind set_owner_root)
  (location 0xaaaaaf202000)
  (value 0xaaaaaf200000)
  (src "test04_bad_bbm_missing_tlbi.c:33"))
(mem-write
  (id 5)
  (tid 0)
  (mem-order plain)
  (address 0xaaaaaf200000)
  (value 0xaaaaaf201003)
  (src "test04_bad_bbm_missing_tlbi.c:36"))
(msr
  (id 6)
  (tid 0)
  (sysreg vttbr_el2)
  (value 0xaaaaaf200000)
  (src "test04_bad_bbm_missing_tlbi.c:39"))
(lock
  (id 7)
  (tid 0)
  (address 0xaaaaaf203000)
  (src "test04_bad_bbm_missing_tlbi.c:41"))
(mem-write
  (id 8)
  (tid 0)
  (mem-order plain)
  (address 0xaaaaaf200000)
  (value 0x0)
  (src "test04_bad_bbm_missing_tlbi.c:42"))
(barrier
  (id 9)
  (tid 0)
  dsb (kind ish)
  (src "test04_bad_bbm_missing_tlbi.c:43"))
(barrier
  (id 10)
  (tid 0)
  dsb (kind ish)
  (src "test04_bad_bbm_missing_tlbi.c:44"))
(mem-write
  (id 11)
  (tid 0)
  (mem-order plain)
  (address 0xaaaaaf200000)
  (value 0xaaaaaf202003)
  (src "test04_bad_bbm_missing_tlbi.c:45"))

Arguments can be also be given positionally for more compressed traces:

(mem-write 1 1 "src" release 42 93)
(lock 2 1 "src" 42)
(msr 3 1 "src" TTBR_EL2 93)
(barrier 4 1 "src" DSB ISH)
(hint 5 1 "src" SET_PTE_THREAD_OWNER 42 93)

References