CoTTf.inv+dsb-isb

Description

Here, Thread 0 makes a new mapping, and Thread 1 observes that new mapping by performing a translation using it, and then later tries to load that same location. If the first read is translated using the new entry, then the second one is not allowed to fault.Note this test’s handler writes to X2, so the test saves it into X0 after the first load.This suggests a kind of translation→translation coherence. In general, you do observe such coherence when TLB-misses (and therefore walks in memory) occur. However, the CoTfT+dsb-isb test (later in this document) shows that this is not guaranteed for all translations.

Source

[download toml source]
Page table setup Code
physical pa1; x |-> invalid; x ?-> pa1; y |-> pa1; *pa1 = 1; identity 0x1000 with code;
Thread 0
{R0=desc3(y, page_table_base), R1=pte3(x, page_table_base)}
STR X0,[X1]
Thread 1
{R1=x, R3=x, VBAR_EL1=extz(0x1000, 64), PSTATE.SP=0b0, PSTATE.EL=0b00}
LDR X2,[X1] MOV X0,X2 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 CoTTf.inv+dsb-isb forbidden (0 of 4) 26198ms
strong CoTTf.inv+dsb-isb forbidden (0 of 4) 21525ms

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/CoTTf.inv+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=.