BBM+dsb-tlbiis-dsb

Description

This is the smallest example of a safe change of output address mapping, using the ‘break-before-make’ (BBM) pattern.Thread 1 loads a fixed VA, and Thread 0 tries to re-map that VA from the initial PA to a new one.To do this safely, Arm prescribe a “break-before-make” sequence to ensure that the other threads will not ever see both the new and old mappings at the same time. Instead, the mapping must be ‘broken’ (unmapped) and cleaned between the two states.This test is the minimum required to correctly change OA (“output address”) for a given mapping.

Source

[download toml source]
Page table setup Code
physical pa1 pa2; x |-> pa1; x ?-> invalid; x ?-> pa2; identity 0x1000 with code; *pa2 = 2;
Thread 0
{R0=extz(0b0, 64), R1=pte3(x, page_table_base), R2=mkdesc3(oa=pa2), R4=extz(0b1, 64), R6=extz(page(x), 64), PSTATE.EL=0b01}
STR X0,[X1] DSB SY TLBI VAE1IS,X6 DSB SY STR X2,[X1]
Thread 1
{R1=x, VBAR_EL1=extz(0x1000, 64), PSTATE.SP=0b0, PSTATE.EL=0b00}
LDR X0,[X1]
thread1_el1_handler
MOV X0,#1 MRS X13,ELR_EL1 ADD X13,X13,#4 MSR ELR_EL1,X13 ERET
Final State
1:X0=0

Execution Diagrams

Results

ETS BBM+dsb-tlbiis-dsb allowed (1 of 3) 19328ms
strong BBM+dsb-tlbiis-dsb allowed (1 of 3) 12702ms

Command-line invocation

isla-axiomatic --arch=/path/to/rems-project/isla-snapshots/aarch64.ir --config=/path/to/rems-project/isla/configs/aarch64_mmu_on.toml --footprint-config=/path/to/rems-project/isla/configs/aarch64.toml --model=/path/to/rems-project/systems-isla-tests/models/aarch64_mmu_strong_ETS.cat --armv8-page-tables --check-sat-using "(then dt2bv qe simplify solve-eqs bv)" --remove-uninteresting safe --dot . -t /path/to/litmus-tests/litmus-tests-armv8a-system-vmsa/tests/pgtable/HAND/BBM+dsb-tlbiis-dsb.litmus.toml

To generate diagrams we use model aarch64_mmu_no_axioms.cat to get diagrams of forbidden executions. To generate LaTeX sources of each test, pass --latex=.