Page table setup | Code |
---|---|
physical pa1 pa2;
x |-> invalid;
x ?-> pa1;
y |-> invalid;
y ?-> pa2;
*pa1 = 1;
*pa2 = 1;
identity 0x1000 with code;
identity 0x2000 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=mkdesc3(oa=pa2), R3=pte3(y, page_table_base), VBAR_EL1=extz(0x1000, 64), PSTATE.EL=0b00, PSTATE.SP=0b0, __isla_monomorphize_writes=true}
|
|
MOV X0,#0
LDR X0,[X1]
EOR X4,X0,X0
STR X2,[X3,X4]
|
|
Thread 2 | |
{R1=y, R3=x, VBAR_EL1=extz(0x2000, 64), PSTATE.SP=0b0, PSTATE.EL=0b00}
|
|
MOV X0,#0
LDR X0,[X1]
EOR X4,X0,X0
MOV X2,#0
LDR X2,[X3,X4]
|
|
thread1_el1_handler | |
MRS X13,ELR_EL1
ADD X13,X13,#4
MSR ELR_EL1,X13
ERET
|
|
thread2_el1_handler | |
MRS X13,ELR_EL1
ADD X13,X13,#4
MSR ELR_EL1,X13
ERET
|
|
Final State | |
1:X0=1 & 2:X0=1 & 2:X2=0 |
ETS | WRC.TTTf.inv+addrs forbidden (0 of 8) 23959ms |
strong | WRC.TTTf.inv+addrs forbidden (0 of 8) 31851ms |
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/WRC.TTTf.inv+addrs.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=.