ROT.inv+dsb

Description

In this ROT test (“reorder translation”), Thread 0 writes to the leaf entry of a fresh (unused) translation-table, and then replaces an (initially invalid) leaf higher in the table with a new table entry which points to the freshly created table.Thread 1 then tries to load an address that would use this new freshly made entry. If the individual accesses during the translation-table-walk are allowed to re-order, then it would be possible for Thread 1 to see the updated table but still see the old leaf entry.This must be forbidden, requiring that the translation-table-walk happens ‘in-order’ and the ordering on Thread 0 ensures the two writes are visible to the walker in that order.The exception handler code records which translation level caused the exception.

Source

[download toml source]

Page table setup	Code
`physical pa1; intermediate ipa1; assert pa1 == ipa1; ipa1 \|-> pa1; s1table new_table 0x280000 { x \|-> invalid; x ?-> ipa1; }; identity 0x283000 with default; x \|-> invalid at level 2; x ?-> table(0x283000) at level 2; identity 0x1000 with code;`
	Thread 0
	`{R0=mkdesc3(oa=ipa1), R1=pte3(x, new_table), R2=mkdesc2(table=extz(0x283000, 64)), R3=pte2(x, page_table_base), PSTATE.EL=0b01}`
	`STR X0,[X1] DSB SY STR X2,[X3]`
	Thread 1
	`{R1=x, VBAR_EL1=extz(0x1000, 64)}`
	`LDR X0,[X1]`
	thread_1_el1_handler
	`MRS X14,ESR_EL1 AND X14,X14,#0b111 CMP X14,#0b111 MOV X17,#1 MOV X18,#2 // if ESR_EL1.ISS.DFSC == Translation Level 3 then x2 = 1 else x2 = 2 CSEL X0,X17,X18,eq`
Final State
`1:X0=1`

Execution Diagrams

Results¶

ETS	ROT.inv+dsb forbidden (0 of 3) 3202ms
strong	ROT.inv+dsb forbidden (0 of 3) 2805ms

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/ROT.inv+dsb.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=.