MP.RT.EL1+dsb-shootdown-dsb+dsb-isb

Description

forbidA broadcast TLBI can be emulated by performing a thread-local TLBI on each core, with sufficient synchronization between them.In the following test, we take MP.RT.EL1+dsb-tlbiis-dsb+dsb-isb and split the broadcast TLBI over many threads. Thread 0 ‘breaks’ the location and then sends messages to each core requesting it perform the TLB maintenance locally.Note that to correctly emulate the behaviour of the broadcast TLBI, each core must perform an ISB (or other context-synchronizing event) to get the pipeline effects of the TLBI. This requirement is slightly stronger than the TLBI semantics, also flushing unrelated accesses.201ex

Source

[download toml source]
Page table setup Code
physical pa1 pa2 pa3; x |-> pa1; x ?-> invalid; y |-> pa2; *pa2 = 0; f |-> pa3; *pa3 = 0; identity 0x1000 with code;
Thread 0
{R0=extz(0b0, 64), R1=pte3(x, page_table_base), R2=extz(0b1, 64), R3=y, R4=extz(0b1, 64), R5=f, PSTATE.EL=0b01}
STR X0,[X1] DSB SY STR X4,[X5] LDR X6,[X5] DSB SY STR X2,[X3]
Thread 1
{R1=y, R3=x, VBAR_EL1=extz(0x1000, 64), R5=f, R6=extz(page(x), 64), R7=extz(0b10, 64), PSTATE.SP=0b0, PSTATE.EL=0b00}
LDR X4,[X5] SVC #0 STR X7,[X5] LDR X0,[X1] DSB SY ISB LDR X2,[X3]
thread1_el1_handler
MRS X9,ESR_EL1 LSR X9,X9,#26 SUB X9,X9,#0b010101 CBNZ X9,1f 0: DSB SY TLBI VAE1,X6 DSB SY ISB ERET 1: MOV X2,#1 MRS X13,ELR_EL1 ADD X13,X13,#4 MSR ELR_EL1,X13 ERET
Final State
1:X4 = 1 & 0:X6 = 2 & 1:X0 = 1 & 1:X2=0

Execution Diagrams

Results

ETS MP.RT.EL1+dsb-shootdown-dsb+dsb-isb forbidden (0 of 2) 49466ms
strong MP.RT.EL1+dsb-shootdown-dsb+dsb-isb forbidden (0 of 2) 765865ms

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.RT.EL1+dsb-shootdown-dsb+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=.