Memory Consistency Model

Sequential Consistency

Sequential consistency is the memory model in which all processors appear to execute operations in some single interleaved order, with each thread’s operations in program order. Covered in ECE459 L15.

Why is it the "safe default"?

It is the strictest ordering Rust offers, so reasoning about concurrent code reduces to reasoning about interleavings. “Use sequential consistency and you won’t get surprises.”

Leslie Lamport’s original statement:

the result of any execution is the same as if the operations of all the processors were executed in some sequential order, and the operations of each individual processor appear in this sequence in the order specified by its program.

Simple description:

  • each thread induces an execution trace
  • at any point the program has executed some prefix of each thread’s trace

L15 example (variables initialized to 0):

T1: x = 1; r1 = y;
T2: y = 1; r2 = x;

Under SC, every execution corresponds to some prefix of both threads. Weaker models allow r1 == 0 && r2 == 0.

Cost

Lamport’s lunch analogy: getting a few people to agree on where to go is hard; getting them to agree on the order events happened is harder. Threads cannot negotiate, so SC implementations insert fences that slow execution.

In Rust, Ordering::SeqCst is the strictest ordering and the course default. The compiler inserts the fences required to maintain SC.