Lecture 17: Synchronization Without Locks

What this lecture covers

The lecture asks whether mutual exclusion can be achieved using only ordinary loads and stores, without locks or special atomic instructions. It builds up the theory of sequential consistency, uses it to prove that Peterson's algorithm correctly enforces mutual exclusion between two threads, and then shows why that proof falls apart on real hardware, which reorders memory operations for performance.

This is a later lecture in MIT's performance engineering course, following earlier material on locks and mutual exclusion. After watching, you can reason formally about memory orderings using happens-before arguments, explain why modern processors don't implement sequential consistency, and understand how memory fences and compare-and-swap restore correctness for lock-free code.

Key ideas

• Sequential consistency: a memory model, defined by Leslie Lamport, where the result of an execution equals some interleaving of each processor's instructions in program order, with every load reading the most recent store in that global order.
• Happens-before relation: a linear ordering induced by an execution, used to reason formally about which store a given load must read; it's the basis for proofs about lock-free code.
• Peterson's algorithm: a two-thread mutual exclusion protocol built only from loads and stores, using a wants flag per thread and a shared turn variable, proven correct under sequential consistency by contradiction.
• Relaxed memory consistency: the model real processors use instead of sequential consistency; hardware and compilers may reorder instructions, most notably reordering an independent load ahead of a prior store.
• Total store order (x86): the specific relaxed model on x86, where loads aren't reordered with loads, stores aren't reordered with stores, stores aren't reordered before prior loads, but a load may move ahead of a prior store to a different address.
• Memory fence: an instruction (mfence, or atomic_thread_fence in C) that blocks reordering across it, needed to make algorithms like Peterson's correct on real hardware; variables must also be declared volatile so the compiler doesn't cache stale values.
• Compare-and-swap (CAS): an atomic instruction that updates a memory location only if it still holds an expected old value, letting you build lock-free algorithms; the Burns-Lynch theorem shows n-thread mutual exclusion needs linear space with only loads and stores, but constant space with something like CAS.
• Lock-free accumulation: using CAS to update a shared sum lets other threads keep progressing even if the operating system suspends the thread mid-update, unlike a lock, which stalls everyone until the descheduled thread resumes.

Walkthrough

Sequential consistency and the interleaving puzzle (1:01)

The lecture opens with two processors racing to write and read shared variables a and b. Students reason that both output registers can't end up 0, an argument that implicitly assumes sequential consistency. The lecture then states Lamport's formal definition: an execution is sequentially consistent if there's some interleaving of the processors' instructions, respecting each processor's own program order, in which every load returns the most recent store. Working through all six interleavings of the example confirms that under this model, both results being 0 is impossible.

Reasoning about mutual exclusion and Peterson's algorithm (15:25)

Before compare-and-swap or test-and-set existed, Dekker and Dijkstra showed mutual exclusion is achievable with only loads and stores under sequential consistency. The lecture presents Peterson's simplified version, illustrated with Alice and Bob competing to use a shared widget. Each thread sets its own wants flag and gives the turn to the other before spinning until it's safe to proceed.

Proving mutual exclusion with happens-before (21:37)

Rather than relying on intuition, the lecture proves Peterson's algorithm correct by contradiction: assuming both threads are in the critical section simultaneously, it chains together happens-before relationships from program order and the assumption that one thread wrote turn last. The chain forces a contradiction, showing the "losing" thread must still be spinning. The lecture notes this kind of reasoning is also what automated model checkers use to verify hardware cache protocols and security protocols.

Why real hardware breaks sequential consistency (34:03)

No modern processor implements sequential consistency; all use relaxed consistency for performance. The lecture explains the mechanism: stores go into a per-processor store buffer so the processor isn't stalled waiting on a slow memory system, while loads bypass the buffer (checking it associatively) to avoid stalling on latency. This causes loads to appear to execute before earlier stores to different addresses, which is exactly the reordering that would let both threads simultaneously believe they've won Peterson's algorithm.

x86's total store order and fixing the algorithm with fences (46:25)

The lecture details the total store order model x86 actually guarantees: loads keep their relative order, stores keep theirs, stores never move before an earlier load, but a load may move ahead of a prior store to a different address. To restore correctness in Peterson's algorithm, a memory fence must be inserted after setting turn, variables must be declared volatile, and compiler fences may be needed around the critical-section code itself.

Compare-and-swap and lock-free programming (1:06:01)

The lecture introduces CAS as the practical alternative to hand-rolled lock-free protocols, showing how it implements both a simple spinlock and a lock-free parallel-sum accumulator. In the CAS-based summation, each thread reads the current total, computes a new value, and only commits it if the total hasn't changed since; if the operating system preempts a thread mid-update, other threads simply keep retrying instead of blocking, unlike with a traditional lock. The lecture closes by naming the ABA problem as a known hazard with CAS-based algorithms.

Before you watch

• Be comfortable with locks and mutual exclusion, covered in the prior lecture in this course.
• Know what compare-and-swap and similar atomic instructions are meant to do at a high level.
• Some exposure to formal reasoning about program order or linear orders (such as from a discrete math course) will help with the proof section.

Check your understanding

1. Why is it possible, under sequential consistency, to reason that two racing writes-then-reads can never both observe 0?
2. In the proof that Peterson's algorithm is correct, what specific contradiction is reached, and what happens-before chain produces it?
3. Why does x86's total store order still allow a load to be reordered ahead of an earlier store, and why is that reordering dangerous for Peterson's algorithm?
4. What roles do a memory fence and the volatile keyword each play in fixing Peterson's algorithm on real hardware?
5. How does the CAS-based parallel-sum solution avoid the problem that arises when the operating system preempts a thread holding a lock?