MP.RTf.inv.EL1+dsb-tlbiis-dsb+dmb

Description

A fault inherits the order that the corresponding memory access would have had if it had not faulted. (With ETS, its translates also inherit the order, making this test forbidden more directly.) Moreover, the pipeline effect of the broadcast TLBI enforces that a memory access and its translate-reads are ‘atomically’ ordered with respect to the TLBI: they are either both ordered-before it, or both ordered-after it. Therefore, because the counterfactual load of x in Thread 1 is ordered after the load of the flag y by the DMB SY, the translate is also ordered after it. Therefore, if Thread 1 sees that the flag y is set to 1, then the translate is guaranteed to translate-read something at least as new as the new, valid mapping that Thread 0 wrote.

Source

[download toml source]

Page table setup	Code
`physical pa1 pa2; x \|-> invalid; x ?-> pa1; z \|-> pa1; *pa1 = 1; y \|-> pa2; identity 0x1000 with code;`
	Thread 0
	`{R0=desc3(z, page_table_base), R1=pte3(x, page_table_base), R2=extz(0b1, 64), R3=y, R4=extz(page(x), 64), PSTATE.EL=0b01}`
	`STR X0,[X1] DSB SY TLBI VAE1IS,X4 DSB SY STR X2,[X3]`
	Thread 1
	`{R1=y, R3=x, VBAR_EL1=extz(0x1000, 64), PSTATE.SP=0b0, PSTATE.EL=0b00}`
	`LDR X0,[X1] DMB SY LDR X2,[X3]`
	thread1_el1_handler
	`MOV X2,#0 MRS X13,ELR_EL1 ADD X13,X13,#4 MSR ELR_EL1,X13 ERET`
Final State
`1:X0 = 1 & 1:X2=0`

Execution Diagrams

Results¶

ETS	MP.RTf.inv.EL1+dsb-tlbiis-dsb+dmb forbidden (0 of 2) 5294ms
strong	MP.RTf.inv.EL1+dsb-tlbiis-dsb+dmb forbidden (0 of 2) 10762ms

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/MP.RTf.inv.EL1+dsb-tlbiis-dsb+dmb.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=.