CoWTf.inv+po

Description

If a thread writes to a page table entry initially containing an invalid descriptor, and the translation of the address of the next instruction uses the page table entry, then the translate is allowed to see the old, invalid descriptor.To detect this, we install a handler for synchronous aborts which writes 0 to X2 before incrementing the ELR to the next instruction address and performing an exception-return.If the final state sees X2=1, then we know the load read-from the new physical location, but if it saw X2=0, then it must have been caused by a translation-fault.The role of y in this litmus test is to make it possible to succinctly describe the new descriptor for x.

Source

[download toml source]
Page table setup Code
physical pa1; x |-> invalid; x ?-> pa1; y |-> pa1; *pa1 = 1; identity 0x1000 with code;
Thread 0
{R0=desc3(y, page_table_base), R1=pte3(x, page_table_base), R3=x, VBAR_EL1=extz(0x1000, 64), PSTATE.SP=0b0}
STR X0,[X1] LDR X2,[X3]
thread0_el1_handler
MOV X2,#0 MRS X20,ELR_EL1 ADD X20,X20,#4 MSR ELR_EL1,X20 ERET
Final State
0:X2 = 0

Execution Diagrams

Results

ETS CoWTf.inv+po allowed (1 of 2) 4160ms
strong CoWTf.inv+po allowed (1 of 2) 4112ms

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/CoWTf.inv+po.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=.