MP.BBM1+dsb-tlbiis-dsb-dsb+dsb-isb

Description

In this test, Thread 0 break-before-makes a new mapping, and then synchronises with Thread 1 with a message pass.While this is a slightly unusual setup, as one would mostly expect break-before-make to happen concurrently with the other thread, rather than be synchronised-before it, this is still an interesting test to explore the architecture.Arm forbid both the translation-fault and the translation with the old entry.2

Source

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

Execution Diagrams

Results

ETS MP.BBM1+dsb-tlbiis-dsb-dsb+dsb-isb error (0 of 3) 182456ms
strong MP.BBM1+dsb-tlbiis-dsb-dsb+dsb-isb forbidden (0 of 3) 116116ms

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/MP.BBM1+dsb-tlbiis-dsb-dsb+dsb-isb.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=.