RSW.alias

Description

If two reads from different VAs which translate to the same PA read from the same write, they can be re-ordered with respect to program-order.

Source

[download toml source]
Page table setup Code
physical pa1 pa2 pa3; w |-> pa1; x |-> pa1; y |-> pa2; z |-> pa3; *pa1 = 0; *pa2 = 0; *pa3 = 0;
Thread 0
{R0=extz(0b1, 64), R1=z, R2=extz(0b1, 64), R3=y, PSTATE.SP=0b0, PSTATE.EL=0b00}
STR X0,[X1] DMB SY STR X2,[X3]
Thread 1
{R1=y, R4=w, R6=x, R9=z, PSTATE.SP=0b0, PSTATE.EL=0b00}
LDR X0,[X1] EOR X2,X0,X0 LDR X3,[X4,X2] LDR X5,[X6] EOR X7,X5,X5 LDR X8,[X9,X7]
Final State
1:X0=1 & 1:X8=0

Execution Diagrams

Results

ETS RSW.alias allowed (1 of 1) 2609ms
strong RSW.alias allowed (1 of 1) 2765ms

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/RSW.alias.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=.