CoRpteT.EL1+dsb-tlbi-dsb-isb

Description

In order to forbid the case in the previous test, an extra TLBI (with correct synchronization) must be inserted to remove those cached entries before trying to load the possibly-unmapped location.

Source

[download toml source]
Page table setup Code
physical pa1; intermediate ipa1; x |-> pa1; x ?-> invalid; identity 0x1000 with code; *pa1 = 0;
Thread 0
{R0=extz(0b0, 64), R1=pte3(x, page_table_base)}
STR X0,[X1]
Thread 1
{R1=pte3(x, page_table_base), R3=x, R4=extz(page(x), 64), VBAR_EL1=extz(0x1000, 64), PSTATE.EL=0b01}
LDR X0,[X1] DSB SY TLBI VAE1,X4 DSB SY ISB LDR X2,[X3]
thread1_el1_handler
MOV X2,#1 MRS X13,ELR_EL1 ADD X13,X13,#4 MSR ELR_EL1,X13 ERET
Final State
1:X0=0 & 1:X2=0

Execution Diagrams

Results

ETS CoRpteT.EL1+dsb-tlbi-dsb-isb forbidden (0 of 2) 28345ms
strong CoRpteT.EL1+dsb-tlbi-dsb-isb forbidden (0 of 2) 53579ms

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/CoRpteT.EL1+dsb-tlbi-dsb-isb.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=.