C C-ManfredSpraul-L1G2xchg.litmus (* Expected result: Never. *) { } 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 = smp_load_acquire(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(gbl, 0); } P2(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(gbl, 0); } Observed 2:r2=1; 2:r11=0; 2:r10=0; 1:r2=0; 1:r11=0; 1:r10=1; 0:r2=1; 0:r12=1; 0:r11=1; 0:r10=1; and 2:r2=1; 2:r11=0; 2:r10=0; 1:r2=1; 1:r11=0; 1:r10=1; 0:r2=0; 0:r12=1; 0:r11=1; 0:r10=1; and 2:r2=0; 2:r11=0; 2:r10=0; 1:r2=1; 1:r11=0; 1:r10=1; 0:r2=0; 0:r12=1; 0:r11=1; 0:r10=1; and 2:r2=1; 2:r11=0; 2:r10=0; 1:r2=0; 1:r11=0; 1:r10=1; 0:r2=0; 0:r12=1; 0:r11=1; 0:r10=1; and 2:r2=1; 2:r11=0; 2:r10=1; 1:r2=1; 1:r11=0; 1:r10=0; 0:r2=0; 0:r12=1; 0:r11=1; 0:r10=1; and 2:r2=0; 2:r11=0; 2:r10=1; 1:r2=1; 1:r11=0; 1:r10=0; 0:r2=0; 0:r12=1; 0:r11=1; 0:r10=1; and 2:r2=0; 2:r11=0; 2:r10=0; 1:r2=1; 1:r11=0; 1:r10=0; 0:r2=0; 0:r12=1; 0:r11=1; 0:r10=1; and 2:r2=1; 2:r11=0; 2:r10=1; 1:r2=0; 1:r11=0; 1:r10=0; 0:r2=0; 0:r12=1; 0:r11=1; 0:r10=1; and 2:r2=1; 2:r11=0; 2:r10=0; 1:r2=0; 1:r11=0; 1:r10=0; 0:r2=0; 0:r12=1; 0:r11=1; 0:r10=1; and 2:r2=0; 2:r11=0; 2:r10=0; 1:r2=1; 1:r11=1; 1:r10=1; 0:r2=1; 0:r12=0; 0:r11=1; 0:r10=1; and 2:r2=1; 2:r11=0; 2:r10=0; 1:r2=0; 1:r11=1; 1:r10=1; 0:r2=1; 0:r12=0; 0:r11=1; 0:r10=1; and 2:r2=0; 2:r11=0; 2:r10=0; 1:r2=1; 1:r11=0; 1:r10=1; 0:r2=1; 0:r12=0; 0:r11=1; 0:r10=1; and 2:r2=1; 2:r11=0; 2:r10=0; 1:r2=0; 1:r11=0; 1:r10=1; 0:r2=1; 0:r12=0; 0:r11=1; 0:r10=1; and 2:r2=1; 2:r11=1; 2:r10=1; 1:r2=0; 1:r11=0; 1:r10=0; 0:r2=1; 0:r12=0; 0:r11=1; 0:r10=1; and 2:r2=1; 2:r11=0; 2:r10=1; 1:r2=0; 1:r11=0; 1:r10=0; 0:r2=1; 0:r12=0; 0:r11=1; 0:r10=1; and 2:r2=1; 2:r11=0; 2:r10=0; 1:r2=0; 1:r11=0; 1:r10=0; 0:r2=1; 0:r12=0; 0:r11=1; 0:r10=1; and 2:r2=1; 2:r11=1; 2:r10=0; 1:r2=1; 1:r11=0; 1:r10=1; 0:r2=0; 0:r12=0; 0:r11=1; 0:r10=1; and 2:r2=0; 2:r11=1; 2:r10=0; 1:r2=1; 1:r11=0; 1:r10=1; 0:r2=0; 0:r12=0; 0:r11=1; 0:r10=1; and 2:r2=1; 2:r11=0; 2:r10=0; 1:r2=1; 1:r11=0; 1:r10=1; 0:r2=0; 0:r12=0; 0:r11=1; 0:r10=1; and 2:r2=1; 2:r11=0; 2:r10=1; 1:r2=1; 1:r11=1; 1:r10=0; 0:r2=0; 0:r12=0; 0:r11=1; 0:r10=1; and 2:r2=0; 2:r11=0; 2:r10=1; 1:r2=1; 1:r11=1; 1:r10=0; 0:r2=0; 0:r12=0; 0:r11=1; 0:r10=1; and 2:r2=1; 2:r11=0; 2:r10=0; 1:r2=1; 1:r11=1; 1:r10=0; 0:r2=0; 0:r12=0; 0:r11=1; 0:r10=1; and 2:r2=1; 2:r11=0; 2:r10=1; 1:r2=0; 1:r11=1; 1:r10=0; 0:r2=0; 0:r12=0; 0:r11=1; 0:r10=1; and 2:r2=1; 2:r11=0; 2:r10=0; 1:r2=0; 1:r11=1; 1:r10=0; 0:r2=0; 0:r12=0; 0:r11=1; 0:r10=1; and 2:r2=1; 2:r11=0; 2:r10=1; 1:r2=1; 1:r11=0; 1:r10=0; 0:r2=0; 0:r12=0; 0:r11=1; 0:r10=1; and 2:r2=0; 2:r11=0; 2:r10=1; 1:r2=1; 1:r11=0; 1:r10=0; 0:r2=0; 0:r12=0; 0:r11=1; 0:r10=1; and 2:r2=0; 2:r11=0; 2:r10=0; 1:r2=1; 1:r11=0; 1:r10=1; 0:r2=0; 0:r12=1; 0:r11=0; 0:r10=1; and 2:r2=1; 2:r11=0; 2:r10=0; 1:r2=0; 1:r11=0; 1:r10=1; 0:r2=0; 0:r12=1; 0:r11=0; 0:r10=1; and 2:r2=0; 2:r11=0; 2:r10=1; 1:r2=1; 1:r11=0; 1:r10=0; 0:r2=0; 0:r12=1; 0:r11=0; 0:r10=1; and 2:r2=0; 2:r11=1; 2:r10=0; 1:r2=0; 1:r11=0; 1:r10=1; 0:r2=1; 0:r12=0; 0:r11=0; 0:r10=1; and 2:r2=0; 2:r11=0; 2:r10=0; 1:r2=0; 1:r11=1; 1:r10=0; 0:r2=1; 0:r12=0; 0:r11=0; 0:r10=1; and 2:r2=1; 2:r11=0; 2:r10=0; 1:r2=0; 1:r11=1; 1:r10=1; 0:r2=0; 0:r12=0; 0:r11=0; 0:r10=1; and 2:r2=1; 2:r11=1; 2:r10=0; 1:r2=0; 1:r11=0; 1:r10=1; 0:r2=0; 0:r12=0; 0:r11=0; 0:r10=1; and 2:r2=0; 2:r11=0; 2:r10=1; 1:r2=1; 1:r11=1; 1:r10=0; 0:r2=0; 0:r12=0; 0:r11=0; 0:r10=1; and 2:r2=0; 2:r11=1; 2:r10=1; 1:r2=1; 1:r11=0; 1:r10=0; 0:r2=0; 0:r12=0; 0:r11=0; 0:r10=1; and 2:r2=0; 2:r11=0; 2:r10=1; 1:r2=1; 1:r11=0; 1:r10=0; 0:r2=0; 0:r12=0; 0:r11=0; 0:r10=1; and 2:r2=0; 2:r11=0; 2:r10=0; 1:r2=1; 1:r11=1; 1:r10=1; 0:r2=1; 0:r12=1; 0:r11=1; 0:r10=0; and 2:r2=1; 2:r11=0; 2:r10=0; 1:r2=0; 1:r11=1; 1:r10=1; 0:r2=1; 0:r12=1; 0:r11=1; 0:r10=0; and 2:r2=0; 2:r11=1; 2:r10=0; 1:r2=1; 1:r11=0; 1:r10=1; 0:r2=1; 0:r12=1; 0:r11=1; 0:r10=0; and 2:r2=0; 2:r11=0; 2:r10=0; 1:r2=1; 1:r11=0; 1:r10=1; 0:r2=1; 0:r12=1; 0:r11=1; 0:r10=0; and 2:r2=1; 2:r11=1; 2:r10=0; 1:r2=0; 1:r11=0; 1:r10=1; 0:r2=1; 0:r12=1; 0:r11=1; 0:r10=0; and 2:r2=1; 2:r11=0; 2:r10=0; 1:r2=0; 1:r11=0; 1:r10=1; 0:r2=1; 0:r12=1; 0:r11=1; 0:r10=0; and 2:r2=0; 2:r11=0; 2:r10=1; 1:r2=1; 1:r11=1; 1:r10=0; 0:r2=1; 0:r12=1; 0:r11=1; 0:r10=0; and 2:r2=1; 2:r11=0; 2:r10=1; 1:r2=0; 1:r11=1; 1:r10=0; 0:r2=1; 0:r12=1; 0:r11=1; 0:r10=0; and 2:r2=0; 2:r11=1; 2:r10=1; 1:r2=1; 1:r11=0; 1:r10=0; 0:r2=1; 0:r12=1; 0:r11=1; 0:r10=0; and 2:r2=0; 2:r11=0; 2:r10=1; 1:r2=1; 1:r11=0; 1:r10=0; 0:r2=1; 0:r12=1; 0:r11=1; 0:r10=0; and 2:r2=1; 2:r11=1; 2:r10=1; 1:r2=0; 1:r11=0; 1:r10=0; 0:r2=1; 0:r12=1; 0:r11=1; 0:r10=0; and 2:r2=1; 2:r11=0; 2:r10=1; 1:r2=0; 1:r11=0; 1:r10=0; 0:r2=1; 0:r12=1; 0:r11=1; 0:r10=0; and 2:r2=1; 2:r11=0; 2:r10=0; 1:r2=0; 1:r11=0; 1:r10=0; 0:r2=1; 0:r12=1; 0:r11=1; 0:r10=0; and 2:r2=1; 2:r11=0; 2:r10=0; 1:r2=0; 1:r11=1; 1:r10=1; 0:r2=0; 0:r12=1; 0:r11=1; 0:r10=0; and 2:r2=1; 2:r11=1; 2:r10=0; 1:r2=1; 1:r11=0; 1:r10=1; 0:r2=0; 0:r12=1; 0:r11=1; 0:r10=0; and 2:r2=1; 2:r11=0; 2:r10=0; 1:r2=1; 1:r11=0; 1:r10=1; 0:r2=0; 0:r12=1; 0:r11=1; 0:r10=0; and 2:r2=0; 2:r11=0; 2:r10=1; 1:r2=1; 1:r11=1; 1:r10=0; 0:r2=0; 0:r12=1; 0:r11=1; 0:r10=0; and 2:r2=1; 2:r11=0; 2:r10=0; 1:r2=0; 1:r11=1; 1:r10=0; 0:r2=0; 0:r12=1; 0:r11=1; 0:r10=0; and 2:r2=1; 2:r11=1; 2:r10=1; 1:r2=1; 1:r11=0; 1:r10=0; 0:r2=0; 0:r12=1; 0:r11=1; 0:r10=0; and 2:r2=0; 2:r11=1; 2:r10=1; 1:r2=1; 1:r11=0; 1:r10=0; 0:r2=0; 0:r12=1; 0:r11=1; 0:r10=0; and 2:r2=1; 2:r11=0; 2:r10=1; 1:r2=1; 1:r11=0; 1:r10=0; 0:r2=0; 0:r12=1; 0:r11=1; 0:r10=0; and 2:r2=1; 2:r11=1; 2:r10=0; 1:r2=1; 1:r11=0; 1:r10=0; 0:r2=0; 0:r12=1; 0:r11=1; 0:r10=0; and 2:r2=0; 2:r11=1; 2:r10=0; 1:r2=1; 1:r11=0; 1:r10=0; 0:r2=0; 0:r12=1; 0:r11=1; 0:r10=0; and 2:r2=1; 2:r11=1; 2:r10=1; 1:r2=0; 1:r11=0; 1:r10=0; 0:r2=0; 0:r12=1; 0:r11=1; 0:r10=0; and 2:r2=1; 2:r11=1; 2:r10=0; 1:r2=0; 1:r11=0; 1:r10=0; 0:r2=0; 0:r12=1; 0:r11=1; 0:r10=0; and 2:r2=0; 2:r11=1; 2:r10=0; 1:r2=1; 1:r11=1; 1:r10=1; 0:r2=1; 0:r12=0; 0:r11=1; 0:r10=0; and 2:r2=0; 2:r11=0; 2:r10=0; 1:r2=1; 1:r11=1; 1:r10=1; 0:r2=1; 0:r12=0; 0:r11=1; 0:r10=0; and 2:r2=1; 2:r11=1; 2:r10=0; 1:r2=0; 1:r11=1; 1:r10=1; 0:r2=1; 0:r12=0; 0:r11=1; 0:r10=0; and 2:r2=1; 2:r11=0; 2:r10=0; 1:r2=0; 1:r11=1; 1:r10=1; 0:r2=1; 0:r12=0; 0:r11=1; 0:r10=0; and 2:r2=0; 2:r11=1; 2:r10=0; 1:r2=1; 1:r11=0; 1:r10=1; 0:r2=1; 0:r12=0; 0:r11=1; 0:r10=0; and 2:r2=0; 2:r11=0; 2:r10=0; 1:r2=1; 1:r11=0; 1:r10=1; 0:r2=1; 0:r12=0; 0:r11=1; 0:r10=0; and 2:r2=1; 2:r11=1; 2:r10=0; 1:r2=0; 1:r11=0; 1:r10=1; 0:r2=1; 0:r12=0; 0:r11=1; 0:r10=0; and 2:r2=0; 2:r11=1; 2:r10=1; 1:r2=1; 1:r11=1; 1:r10=0; 0:r2=1; 0:r12=0; 0:r11=1; 0:r10=0; and 2:r2=0; 2:r11=0; 2:r10=1; 1:r2=1; 1:r11=1; 1:r10=0; 0:r2=1; 0:r12=0; 0:r11=1; 0:r10=0; and 2:r2=1; 2:r11=1; 2:r10=1; 1:r2=0; 1:r11=1; 1:r10=0; 0:r2=1; 0:r12=0; 0:r11=1; 0:r10=0; and 2:r2=1; 2:r11=0; 2:r10=1; 1:r2=0; 1:r11=1; 1:r10=0; 0:r2=1; 0:r12=0; 0:r11=1; 0:r10=0; and 2:r2=1; 2:r11=1; 2:r10=0; 1:r2=0; 1:r11=1; 1:r10=0; 0:r2=1; 0:r12=0; 0:r11=1; 0:r10=0; and 2:r2=1; 2:r11=0; 2:r10=0; 1:r2=0; 1:r11=1; 1:r10=0; 0:r2=1; 0:r12=0; 0:r11=1; 0:r10=0; and 2:r2=0; 2:r11=1; 2:r10=1; 1:r2=1; 1:r11=0; 1:r10=0; 0:r2=1; 0:r12=0; 0:r11=1; 0:r10=0; and 2:r2=0; 2:r11=1; 2:r10=0; 1:r2=1; 1:r11=0; 1:r10=0; 0:r2=1; 0:r12=0; 0:r11=1; 0:r10=0; and 2:r2=1; 2:r11=1; 2:r10=1; 1:r2=0; 1:r11=0; 1:r10=0; 0:r2=1; 0:r12=0; 0:r11=1; 0:r10=0; and 2:r2=0; 2:r11=0; 2:r10=0; 1:r2=1; 1:r11=0; 1:r10=1; 0:r2=0; 0:r12=0; 0:r11=1; 0:r10=0; and 2:r2=1; 2:r11=1; 2:r10=0; 1:r2=1; 1:r11=1; 1:r10=0; 0:r2=0; 0:r12=0; 0:r11=1; 0:r10=0; and 2:r2=1; 2:r11=0; 2:r10=0; 1:r2=1; 1:r11=1; 1:r10=0; 0:r2=0; 0:r12=0; 0:r11=1; 0:r10=0; and 2:r2=1; 2:r11=0; 2:r10=0; 1:r2=0; 1:r11=1; 1:r10=0; 0:r2=0; 0:r12=0; 0:r11=1; 0:r10=0; and 2:r2=0; 2:r11=0; 2:r10=1; 1:r2=1; 1:r11=0; 1:r10=0; 0:r2=0; 0:r12=0; 0:r11=1; 0:r10=0; and 2:r2=1; 2:r11=1; 2:r10=0; 1:r2=1; 1:r11=0; 1:r10=0; 0:r2=0; 0:r12=0; 0:r11=1; 0:r10=0; and 2:r2=1; 2:r11=0; 2:r10=0; 1:r2=0; 1:r11=1; 1:r10=1; 0:r2=0; 0:r12=1; 0:r11=0; 0:r10=0; and 2:r2=1; 2:r11=0; 2:r10=0; 1:r2=0; 1:r11=0; 1:r10=1; 0:r2=0; 0:r12=1; 0:r11=0; 0:r10=0; and 2:r2=0; 2:r11=1; 2:r10=1; 1:r2=1; 1:r11=0; 1:r10=0; 0:r2=0; 0:r12=1; 0:r11=0; 0:r10=0; and 2:r2=0; 2:r11=0; 2:r10=1; 1:r2=1; 1:r11=0; 1:r10=0; 0:r2=0; 0:r12=1; 0:r11=0; 0:r10=0; and 2:r2=0; 2:r11=1; 2:r10=0; 1:r2=1; 1:r11=1; 1:r10=1; 0:r2=1; 0:r12=0; 0:r11=0; 0:r10=0; and 2:r2=1; 2:r11=1; 2:r10=0; 1:r2=0; 1:r11=1; 1:r10=1; 0:r2=1; 0:r12=0; 0:r11=0; 0:r10=0; and 2:r2=1; 2:r11=0; 2:r10=0; 1:r2=0; 1:r11=1; 1:r10=1; 0:r2=1; 0:r12=0; 0:r11=0; 0:r10=0; and 2:r2=0; 2:r11=1; 2:r10=0; 1:r2=1; 1:r11=0; 1:r10=1; 0:r2=1; 0:r12=0; 0:r11=0; 0:r10=0; and 2:r2=0; 2:r11=1; 2:r10=1; 1:r2=1; 1:r11=1; 1:r10=0; 0:r2=1; 0:r12=0; 0:r11=0; 0:r10=0; and 2:r2=1; 2:r11=1; 2:r10=1; 1:r2=0; 1:r11=1; 1:r10=0; 0:r2=1; 0:r12=0; 0:r11=0; 0:r10=0; and 2:r2=1; 2:r11=0; 2:r10=1; 1:r2=0; 1:r11=1; 1:r10=0; 0:r2=1; 0:r12=0; 0:r11=0; 0:r10=0; and 2:r2=1; 2:r11=0; 2:r10=0; 1:r2=0; 1:r11=1; 1:r10=0; 0:r2=1; 0:r12=0; 0:r11=0; 0:r10=0; and 2:r2=0; 2:r11=1; 2:r10=1; 1:r2=1; 1:r11=0; 1:r10=0; 0:r2=1; 0:r12=0; 0:r11=0; 0:r10=0; and 2:r2=0; 2:r11=1; 2:r10=0; 1:r2=1; 1:r11=0; 1:r10=0; 0:r2=1; 0:r12=0; 0:r11=0; 0:r10=0; and 2:r2=1; 2:r11=0; 2:r10=0; 1:r2=0; 1:r11=0; 1:r10=1; 0:r2=0; 0:r12=0; 0:r11=0; 0:r10=0; and 2:r2=0; 2:r11=0; 2:r10=1; 1:r2=1; 1:r11=0; 1:r10=0; 0:r2=0; 0:r12=0; 0:r11=0; 0:r10=0;