| 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(0x1, 64), R1=z, R2=extz(0x1, 64), R3=y}
|
|
STR X0,[X1]
DMB SY
STR X2,[X3]
|
|
| Thread 1 | |
{R1=y, R2=extz(0x1, 64), R3=x, R5=w, R7=z}
|
|
LDR X0,[X1]
CBNZ X0,L0
L0:
STR X2,[X3]
LDR X4,[X5]
EOR X8,X4,X4
LDR X6,[X7,X8]
|
|
| Final State | |
1:X0 = 1 & 1:X4 = 1 & 1:X6 = 0 |
|
| ETS | PPOCA.alias allowed (1 of 2) 4932ms |
| strong | PPOCA.alias allowed (1 of 2) 4744ms |
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/PPOCA.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=.