| Page table setup | Code |
|---|---|
physical pa1 pa2 pa3 pa4;
x |-> pa1;
y |-> pa2;
u |-> invalid;
u ?-> pa2;
v |-> invalid;
v ?-> pa1;
identity 0x1000 with code;
identity 0x2000 with code;
|
|
| Thread 0 | |
{R1=x, R3=desc3(y, page_table_base), R4=pte3(u, page_table_base), R5=extz(0b1, 64), R6=u, R7=extz(0b1, 64), VBAR_EL1=extz(0x1000, 64)}
|
|
LDR X0,[X1]
EOR X2,X0,X0
ORR X3,X3,X2
STR X3,[X4]
STR X5,[X6]
|
|
| Thread 1 | |
{R1=y, R3=desc3(x, page_table_base), R4=pte3(v, page_table_base), R5=extz(0b1, 64), R6=v, R7=extz(0b1, 64), VBAR_EL1=extz(0x2000, 64)}
|
|
LDR X0,[X1]
EOR X2,X0,X0
ORR X3,X3,X2
STR X3,[X4]
STR X5,[X6]
|
|
| thread1_el0_handler | |
MOV X7,#0
MRS X13,ELR_EL1
ADD X13,X13,#4
MSR ELR_EL1,X13
ERET
|
|
| thread1_el1_handler | |
MOV X7,#0
MRS X13,ELR_EL1
ADD X13,X13,#4
MSR ELR_EL1,X13
ERET
|
|
| Final State | |
0:X0 = 1 & 0:X7 = 1 & 1:X0 = 1 & 1:X7 = 1 |
|
| ETS | LB+data-trfis forbidden (0 of 4) 18056ms |
| strong | LB+data-trfis forbidden (0 of 4) 26579ms |
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/LB+data-trfis.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=.