CoTfW.inv+dsb-isb

Description

Here, Thread 0 writes a new mapping, and Thread 1 then sees this mapping with a translation-table walk, before overwriting it with another entry. Can this later write be coherence-before the original write?Our model forbids this, requiring that writes pass the point of coherence before being visible to translations.

Source

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

Execution Diagrams

Results

ETS CoTfW.inv+dsb-isb forbidden (0 of 2) 8392ms
strong CoTfW.inv+dsb-isb forbidden (0 of 2) 5572ms

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/CoTfW.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=.