Re: [PATCH 00/18] Another attempt at HVO support on arm64

[Catalin Marinas]

Hi James,

On Wed, Jul 08, 2026 at 03:11:10AM +0000, James Houghton wrote:
> The following Herd litmus test demonstrates the PTE update routine:
> 
>   AArch64 TTDFaultlessUpdate
>   Variant=vmsa
>   TTHM=HA
>   {
>    uint64_t x=1;
>    uint64_t y=2;
>    [PTE(x)]=(oa:PA(x), af:1);
>    0:X0=PTE(x); 1:X0=PTE(x);
>    0:X1=x; 1:X1=x;
>    pteval_t 0:X2=(oa:PA(x), af:0);
>    pteval_t 0:X3=(oa:PA(y), af:1);
>   }
>    P0                | P1             ;
>    LDR X4,[X0]       | L0:            ;
>    MOV X5,X4         | LDR X2,[X1]    ;
>    CAS X4,X2,[X0]    |                ;
>    DSB ISHST         |                ;
>    LSR X9,X1,#12     |                ;
>    TLBI VAALE1IS,X9  |                ;
>    DSB ISH           |                ;
>    ISB               |                ;
>    CAS X2,X3,[X0]    |                ;
>   exists
>     0:X5=0:X4 /\ (* First CAS must succeed *)
>     (fault(P1:L0) \/ ~(1:X2=2 \/ 1:X2=1))
> 
>   (* This test should not violate BBM requirements. *)

We definitely need a clear statement in the Arm ARM around this. As
already raised in this thread, we can assume that AF=0 entries won't be
cached in TLB but there's more to the BBM rules. For the dirty bit, we
have R_SGJBL, we might need something similar for AF in addition to the
BBM rules update. In theory, I think your approach works but we need the
memory model experts confirmation and the Arm ARM updated.

I'm not entirely clear what the above litmus test guarantees other than
not giving a warning. On P1, X2 can be either 1 or 2, otherwise fault
but that won't happen with HA. I'd rather have something in the 'exists'
rule explicitly (like a TLB conflict abort; not supported AFAIK but
maybe that's what fault(P1) was meant to show?).

In addition to the above test, I wonder whether we could have P1 do two
consecutive reads from [X1] and check the read values. Maybe go through
a third mapping, OA(z) with AF=0 after the TLBI or just start with AF=0
on x. Basically any other tests for coherency like read-after-read etc.,
check that the behaviour is preserved through AF=0 just like going
through valid=0 with BBM (that's something that should eventually be
runnable on actual hardware to validate where we won't have a BBM
warning message).

-- 
Catalin