Page table setup | Code |
---|---|
physical pa1;
x |-> pa1;
x ?-> invalid;
identity 0x1000 with code;
|
|
Thread 0 | |
{R0=extz(0b0, 64), R1=pte3(x, page_table_base), R3=x, R4=asid(0x1), VBAR_EL1=extz(0x1000, 64), TTBR0_EL1=ttbr(asid=0x0001, base=page_table_base), PSTATE.EL=0b01, SPSR_EL1=extz(0b00000, 64), ELR_EL1=L0:}
|
|
STR X0,[X1]
DSB SY
TLBI ASIDE1IS,X4
DSB SY
ERET
L0:
LDR X2,[X3]
|
|
thread0_el1_handler | |
MOV X2,#1
MRS X13,ELR_EL1
ADD X13,X13,#4
MSR ELR_EL1,X13
ERET
|
|
Final State | |
0:X2 = 0 |
ETS | CoWinvTa1.1+dsb-tlbiasidis-dsb-eret forbidden (0 of 2) 99884ms |
strong | CoWinvTa1.1+dsb-tlbiasidis-dsb-eret forbidden (0 of 2) 7638ms |
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/CoWinvTa1.1+dsb-tlbiasidis-dsb-eret.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=.