Two models on one picture
With two memory consistency models in hand, we can finally compare. How do SC, TSO total store order (tso) SC minus the Store→Load ordering rule: legalizes per-core FIFO write buffers; the SPARC/x86 memory model. defined in Chapter 4 — open in glossary , and the rest relate?
- Executions. SC executions are a proper subset of TSO executions: every SC execution is a TSO execution, while some TSO executions — Dekker’s (0, 0) from §4.2 — are TSO executions and not SC executions. That is the Venn diagram of Figure 4.5a.
- Implementations. Implementations follow the same rule: SC implementations are a proper subset of TSO implementations — an SC implementation produces only SC executions, all of which TSO also permits; it simply never uses the extra latitude. Figure 4.5b is the same picture as 4.5a.
Figure 4.5: comparing memory consistency models. The stronger the model, the smaller its region: SC sits inside TSO; TSO sits inside the incomparable, more relaxed models MC1 and MC2.
Relaxed, weaker, incomparable
The Venn picture generalizes into vocabulary the rest of the book leans on:
As Figure 4.5 depicts, TSO is more relaxed than SC but less relaxed than models MC1 and MC2 — which are incomparable with each other: each allows executions the other forbids. Who are MC1 and MC2? The next chapter supplies candidates (§5.8), including a case study of the IBM Power memory consistency model (§5.6).
What is a good memory consistency model?
Comparing models begs the question of what good looks like. A good model should possess Sarita Adve’s 3Ps, plus the book’s fourth — the 4Ps the 4ps Programmability, Performance, Portability, Precision: criteria for a good memory consistency model. defined in Chapter 4 — open in glossary :
Programmability
Writing multithreaded programs should be (relatively) easy. The model should be intuitive even to users who haven’t read the details — yet precise enough that experts can push the envelope of what’s allowed.
Performance
The model should facilitate high-performance implementations at reasonable power and cost, giving implementors broad latitude in options.
Portability
A good model is adopted widely — or at least offers backward compatibility or the ability to translate among models.
Precision the book’s addition
The model should be precisely defined, usually with mathematics. Natural languages are too ambiguous for experts to push the envelope of what is allowed.
How good are SC and TSO?
Scoring both models against the 4Ps:
| SC | TSO | |
|---|---|---|
| Programmability | The most intuitive model | Close behind — acts like SC for common idioms, but subtle non-SC executions can bite programmers and tool authors |
| Performance | Needs speculation (§3.8) to keep pace | Better than SC on simple cores; the difference shrinks with speculation |
| Portability | Widely understood | Widely adopted |
| Precision | Formally defined | Formally defined (§4.3) |
The bottom line: SC and TSO are pretty close — especially compared with the more complex and more relaxed memory consistency models of the next chapter.
Check yourself
1.What is the relationship between SC executions and TSO executions?
2.Why is every SC implementation automatically a TSO implementation?
3.Figure 4.5 shows models MC1 and MC2 as INCOMPARABLE. What does that mean?
4.Which P did the book's authors add to Sarita Adve's 3Ps for judging memory models?
5.Which statement matches the book's 4Ps scorecard for SC vs. TSO?
Chapter 4 references
- S. V. Adve. Designing memory consistency models for shared-memory multiprocessors. Ph.D. thesis, University of Wisconsin–Madison, 1993.
- W. W. Collier. Reasoning About Parallel Architectures. Prentice-Hall, 1990.
- Y. Duan, A. Muzahid, and J. Torrellas. WeeFence: Toward making fences free in TSO. ISCA, 2013.
- Y. Duan, N. Honarmand, and J. Torrellas. Asymmetric memory fences: Optimizing both performance and implementability. ASPLOS, 2015.
- K. Gharachorloo, D. Lenoski, J. Laudon, P. Gibbons, A. Gupta, and J. Hennessy. Memory consistency and event ordering in scalable shared-memory. ISCA, 1990.
- K. Gharachorloo, M. Sharma, S. Steely, and S. Van Doren. Architecture and design of AlphaServer GS320. ASPLOS, 2000.
- J. R. Goodman. Cache consistency and sequential consistency. TR 1006, University of Wisconsin–Madison, 1991.
- C. Lin, V. Nagarajan, and R. Gupta. Efficient sequential consistency using conditional fences. PACT, 2010.
- S. Owens, S. Sarkar, and P. Sewell. A better x86 memory model: x86-TSO. TPHOLs, 2009.
- B. Rajaram, V. Nagarajan, S. Sarkar, and M. Elver. Fast RMWs for TSO: Semantics and implementation. PLDI, 2013.
- A. Ros, T. E. Carlson, M. Alipour, and S. Kaxiras. Non-speculative load-load reordering in TSO. ISCA, 2017.
- A. Ros and S. Kaxiras. The superfluous load queue. MICRO, 2018.
- A. Ros and S. Kaxiras. Non-speculative store coalescing in total store order. ISCA, 2018.
- S. Sarkar, P. Sewell, F. Z. Nardelli, S. Owens, T. Ridge, T. Braibant, M. O. Myreen, and J. Alglave. The semantics of x86-CC multiprocessor machine code. POPL, 2009.
- P. Sewell, S. Sarkar, S. Owens, F. Z. Nardelli, and M. O. Myreen. x86-TSO: A rigorous and usable programmer’s model for x86 multiprocessors. CACM, July 2010.
- P. Sindhu, J.-M. Frailong, and M. Ceklov. Formal specification of memory models. TR CSL-91-11, Xerox PARC, 1991.