MP.RTf.inv+dmbs

Description

(forbid with ETS)The DSB; ISB is required for the base architecture, as illustrated by the this test.However, if the implementation has the ETS optional feature (“Enhanced Translation Synchronization”), then this test is forbidden. This is because ETS ensures that a translation-table-walk which results in a translation-fault (that is, one that reads an invalid entry) is ordered-after any memory event which would be ordered-before the read/write of any load/store (as appropriate) in the place of the instruction which generated the translation-fault.

Source

[download toml source]
Page table setup Code
physical pa1 pa2; x |-> invalid; x ?-> pa1; z |-> pa1; *pa1 = 1; y |-> pa2; identity 0x1000 with code;
Thread 0
{R0=desc3(z, page_table_base), R1=pte3(x, page_table_base), R2=extz(0b1, 64), R3=y}
STR X0,[X1] DMB ST STR X2,[X3]
Thread 1
{R1=y, R3=x, VBAR_EL1=extz(0x1000, 64), PSTATE.SP=0b0, PSTATE.EL=0b00}
LDR X0,[X1] DMB SY 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.RTf.inv+dmbs forbidden (0 of 2) 3681ms
strong MP.RTf.inv+dmbs allowed (1 of 2) 5896ms

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.RTf.inv+dmbs.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=.