Re: [PATCH] workqueue(9): Allow requeueing
Taylor R Campbell <[email protected]> Sat, 30 May 2026 21:51:22 +0000
| Newsgroups | gmane.os.netbsd.devel.kernel |
|---|---|
| Message-ID | <[email protected]> |
> Date: Sat, 30 May 2026 21:07:25 +0000 > From: Taylor R Campbell <[email protected]> > > [*] 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!
samecas-dmbstld.litmus
(text/plain, 851 B)
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)
samecas-casl.litmus
(text/plain, 812 B)
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)