…
C C-ManfredSpraul-L1G1xchgnr.litmus
(* Expected result: Sometimes. Need acquire-load of nfcla! *)
{
}
P0(int *nfcla, int *gbl, int *gbl_held, int *lcl, int *lcl_held)
{
int r1; int r2;
int r10;
int r11=0; int r12=0;
/* Acquire local lock. */
r10 = xchg_acquire(lcl, 1);
r1 = READ_ONCE(*nfcla);
if (r1) {
smp_store_release(lcl, 0);
r11 = xchg_acquire(gbl, 1);
r12 = xchg_acquire(lcl, 1);
smp_store_release(gbl, 0);
}
r2 = READ_ONCE(*gbl_held);
WRITE_ONCE(*lcl_held, 1);
WRITE_ONCE(*lcl_held, 0);
smp_store_release(lcl, 0);
}
P1(int *nfcla, int *gbl, int *gbl_held, int *lcl, int *lcl_held)
{
int r10; int r11; int r2;
/* Acquire global lock. */
r10 = xchg_acquire(gbl, 1);
WRITE_ONCE(*nfcla, 1);
r11 = xchg_acquire(lcl, 1);
smp_store_release(lcl, 0);
r2 = READ_ONCE(*lcl_held);
WRITE_ONCE(*gbl_held, 1);
WRITE_ONCE(*gbl_held, 0);
smp_store_release(nfcla, 0);
smp_store_release(gbl, 0);
}
Observed
1:r2=0; 1:r11=0; 1:r10=0; 0:r2=1; 0:r12=0; 0:r11=0; 0:r10=1;
and 1:r2=0; 1:r11=0; 1:r10=0; 0:r2=1; 0:r12=0; 0:r11=0; 0:r10=0;