Re: [PATCH] workqueue(9): Allow requeueing

[Taylor R Campbell <riastradh%NetBSD.org@localhost>]

> Date: Sat, 30 May 2026 21:07:25 +0000
> From: Taylor R Campbell <riastradh%NetBSD.org@localhost>
> 
> [*] Curiously, if you change  CAS W3,W3,[X0]  to  LDR W3,[X0]  rather
>     than deleting it altogether then herd7 still can't find
>     counterexamples.  But the proof of correctness that I sketched in
>     the comments fundamentally relies on having a store operation to
>     advance from one version of an object to the next version (even if
>     it has the same value!), and makes no sense with a load operation.
>     It's possible I'm missing something here or holding it wrong!

I played around a little more, and it turns out CAS vs LDR does make a
difference between working and broken, if the membar_release barrier
is relaxed from DMB ISH to DMB ISHST in P0.

DMB ISHST technically isn't enough for membar_release in general --
but it's enough for this case because the only thing we have to order
is the store x=1 before the conditional store atomic_cas(&flag, 1, 1).

Similarly, if I omit the DMB altogether in P0, CASL vs LDR does make a
difference between working and broken.  And CASL a correct
implementation of membar_release(); atomic_cas().

So I no longer think I'm missing anything or holding it wrong -- even
if it is really counterintuitive that atomic_cas(&flag, 1, 1) could
make a difference in correctness!

AArch64 MP
{
int flag=1;
int x=0;
0:X0=flag; 0:X1=x;
1:X0=flag; 1:X1=x;
}
 P0               | P1               ;
 MOV W6,#0        | MOV W6,#0        ;
 MOV W7,#0        | SWP WZR,W3,[X0]  ;
 MOV W4,#1        | CBZ W3,L10       ;
 STR W4,[X1]      | DMB ISHLD        ;
 MOV W3,#0        | LDR W6,[X1]      ;
 CAS W3,W4,[X0]   |L10:              ;
 CBNZ W3,L00      |                  ;
 MOV W6,#1        |                  ;
 B L09            |                  ;
L00:              |                  ;
 DMB ISHST        |                  ;
 MOV W3,#1        |                  ;
 CAS W3,W3,[X0]   |                  ;
 CBZ W3,L08       |                  ;
 B L09            |                  ;
L08:              |                  ;
 MOV W7,#1        |                  ;
L09:              |                  ;
exists
(0:X6=0 /\ 0:X7=0 /\ 1:X6=0)

AArch64 MP
{
int flag=1;
int x=0;
0:X0=flag; 0:X1=x;
1:X0=flag; 1:X1=x;
}
 P0               | P1               ;
 MOV W6,#0        | MOV W6,#0        ;
 MOV W7,#0        | SWP WZR,W3,[X0]  ;
 MOV W4,#1        | CBZ W3,L10       ;
 STR W4,[X1]      | DMB ISHLD        ;
 MOV W3,#0        | LDR W6,[X1]      ;
 CAS W3,W4,[X0]   |L10:              ;
 CBNZ W3,L00      |                  ;
 MOV W6,#1        |                  ;
 B L09            |                  ;
L00:              |                  ;
 MOV W3,#1        |                  ;
 CASL W3,W3,[X0]  |                  ;
 CBZ W3,L08       |                  ;
 B L09            |                  ;
L08:              |                  ;
 MOV W7,#1        |                  ;
L09:              |                  ;
exists
(0:X6=0 /\ 0:X7=0 /\ 1:X6=0)