14.2.4.7 Semantics Sufficient to Implement Locking

Suppose we have an exclusive lock (spinlock_t in the Linux kernel, pthread_mutex_t in pthreads code) that guards a number of variables (in other words, these variables are not accessed except from the lock's critical sections). The following properties must then hold true:

  1. A given CPU or thread must see all of its own loads and stores as if they had occurred in program order.
  2. The lock acquisitions and releases must appear to have executed in a single global order.14.2
  3. Suppose a given variable has not yet been stored to in a critical section that is currently executing. Then any load from a given variable performed in that critical section must see the last store to that variable from the last previous critical section that stored to it.

The difference between the last two properties is a bit subtle: the second requires that the lock acquisitions and releases occur in a well-defined order, while the third requires that the critical sections not ``bleed out'' far enough to cause difficulties for other critical section.

Why are these properties necessary?

Suppose the first property did not hold. Then the assertion in the following code might well fail!



a = 1;
b = 1 + a;
assert(b == 2);


Quick Quiz 14.7: How could the assertion b==2 on page [*] possibly fail? End Quick Quiz

Suppose that the second property did not hold. Then the following code might leak memory!



spin_lock(&mylock);
if (p == NULL)
  p = kmalloc(sizeof(*p), GFP_KERNEL);
spin_unlock(&mylock);


Quick Quiz 14.8: How could the code on page [*] possibly leak memory? End Quick Quiz

Suppose that the third property did not hold. Then the counter shown in the following code might well count backwards. This third property is crucial, as it cannot be strictly with pairwise memory barriers.



spin_lock(&mylock);
ctr = ctr + 1;
spin_unlock(&mylock);


Quick Quiz 14.9: How could the code on page [*] possibly count backwards? End Quick Quiz

If you are convinced that these rules are necessary, let's look at how they interact with a typical locking implementation.

Paul E. McKenney 2011-12-16