C lru_add_drain_all (* * x is a pagevec counter * y is @lru_drain_gen * z is @lock *) { } P0(int *x) { // mark pagevec for draining WRITE_ONCE(*x, 1); } P1(int *x, int *y, int *z) { int rx; int rz; // mutex_lock(&lock); rz = cmpxchg_acquire(z, 0, 1); if (rz == 0) { // WRITE_ONCE(lru_drain_gen, lru_drain_gen + 1); WRITE_ONCE(*y, 1); // guarantee lru_drain_gen store before loading pagevec smp_mb(); // if (pagevec_count(...)) rx = READ_ONCE(*x); // mutex_unlock(&lock); rz = cmpxchg_release(z, 1, 2); } } P2(int *x, int *y, int *z) { int rx; int ry1; int ry2; int rz; // the pagevec counter as visible now to this CPU rx = READ_ONCE(*x); // guarantee pagevec store before loading lru_drain_gen smp_mb(); // this_gen = READ_ONCE(lru_drain_gen); smp_rmb(); ry1 = smp_load_acquire(y); // mutex_lock(&lock) - acquired after P1 rz = cmpxchg_acquire(z, 2, 3); if (rz == 2) { // if (unlikely(this_gen != lru_drain_gen)) ry2 = READ_ONCE(*y); } } locations [x; y; z] exists (1:rx=0 /\ 2:rx=1 /\ 2:ry1=0 /\ 2:ry2=1)