CoWW.alias

Description

Should the coherence-order of writes respect program-order in the same thread even if they are to different VAs?Our model says yes, and forbids the following CoWW.alias test.

Source

[download toml source]
Page table setup Code
physical pa1; x |-> pa1; y |-> pa1; *pa1 = 0;
Thread 0
{R0=extz(0b01, 64), R1=x, R2=extz(0b10, 64), R3=y, PSTATE.SP=0b0, PSTATE.EL=0b00}
STR X0,[X1] STR X2,[X3]
Final State
*x=1

Execution Diagrams

Results

ETS CoWW.alias forbidden (0 of 1) 849ms
strong CoWW.alias forbidden (0 of 1) 822ms

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