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

[James Houghton]

On Mon, Aug 17, 2026 at 10:34 AM Catalin Marinas
<catalin.marinas@xxxxxxx> wrote:
>
> Hi James,

Hi Catalin, thanks for your feedback on this series!

> 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 agree; it would be nice if the BBM rules were more explicit about
PTEs with AF=0.

The question I find myself wanting an answer to is: "is there ever a
case where a TLBI must be issued for a guaranteed-uncached TTD before
it can be modified?"

I'm pretty convinced that, for Page->Page, there are no such cases
(but I can't really say for sure).

For Block->Table, it's certainly more plausible for there to be such
cases, like your comment on patch 12[1].

[1] https://lore.kernel.org/linux-mm/aoSJcAFMNJ1nPl2H@xxxxxxx/

> 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?).

I should have clarified that the exists clause in this case should
always be negative. So I read it is:

"It should never be the case that: the CAS succeeds AND (P1 takes a
fault OR P1 reads a bogus value)."

It's really useful for HVO not to introduce a window where Linux (e.g.
get_page_unless_zero() callers) might take a fault on the vmemmap;
this is what the fault(P1) part of the clause is conveying (even if it
is obvious). This is actually the main point of the test: to verify we
don't take a fault. The bogus value part is just kind of a sanity
check.

I don't think fault() captures TLB conflict aborts. The lack of a BBM
warning is supposed to indicate that the litmus test has followed BBM
rules properly => TLB conflict aborts should not occur.

>
> 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).

Changing P1 to:

LDR X2,[X1];
LDR X3,[X1];

and using the exists clause:

0:X5=0:X4 /\ (fault(P1:L0) \/ (1:X3=1 /\ 1:X2=2))

remains always false => P1 never reads in reverse order.

    Test TTDFaultlessUpdateRAR Allowed
    States 3
    0:X4=(oa:PA(x)); 0:X5=(oa:PA(x)); 1:X2=1; 1:X3=1;  ~Fault(P1:L0);
    0:X4=(oa:PA(x)); 0:X5=(oa:PA(x)); 1:X2=1; 1:X3=2;  ~Fault(P1:L0);
    0:X4=(oa:PA(x)); 0:X5=(oa:PA(x)); 1:X2=2; 1:X3=2;  ~Fault(P1:L0);
    No
    Witnesses
    Positive: 0 Negative: 140
    Flag Maintenance-scope-for-DSB-ST-is-deprecated

I've tried to write more interesting tests than this, but I can't get
any of them to run in any reasonable amount of time. (This test with
P1 doing two reads took 2.5 minutes.)

Here's one that I was trying:

  AArch64 TTDFaultlessUpdateRAR2
  Variant=vmsa
  TTHM=HA
  {
   uint64_t x=0;
   uint64_t y=2;
   [PTE(x)]=(oa:PA(x), af:0);
   0:X0=PTE(x);
   1:X1=x; 2:X1=x;
   2:X2=1;
   pteval_t 0:X2=(oa:PA(x), af:0);
   pteval_t 0:X3=(oa:PA(y), af:0);
   pteval_t 0:X4=(oa:PA(x), af:1);
  }
   P0                | P1             | P2             ;
   MOV X6,X2         | LDR X2,[X1]    | STR X2,[X1]    ;
   CAS X2,X3,[X0]    | LDR X3,[X1]    |                ;
   MOV X7,X3         |                |                ;
   CAS X3,X4,[X0]    |                |                ;
                     |                |                ;
                     |                |                ;
  exists
    0:X6=0:X2 /\ (* First CAS must succeed *)
    0:X7=0:X3 /\ (* Second CAS must succeed *)
    (1:X2=2 \/ 1:X3=2 \/ (1:X3=0 /\ 1:X2=1))

Let me know if you have any more specific ideas about tests to try.

Thanks!