5.8.1 How do relaxed models relate to each other, TSO, and SC?
Recall §4.6’s vocabulary: Y is strictly more relaxed strictly more relaxed Model Y is strictly more relaxed (weaker) than X iff every X execution is a Y execution but not vice versa; models can also be incomparable. defined in Chapter 4 — open in glossary than X if all X executions are Y executions but not vice versa; two models are incomparable if each allows executions the other precludes. Figure 5.5 repeats chapter 4’s Venn diagram with names filled in — Power replaces MC1, while MC2 could be Alpha, ARM, RMO, or XC:
Figure 5.5 (recreated): comparing memory consistency models.
The known relations:
- Power is more relaxed than TSO, which is more relaxed than SC.
- Alpha, ARM, RMO, and XC are each more relaxed than TSO, which is more relaxed than SC.
- Power vs. Alpha/ARM/RMO/XC is assumed incomparable — until someone proves one more relaxed than the other, or the two equivalent.
Mador-Haim et al. developed an automated technique for comparing memory models — including SC, TSO, and RMO — but did not consider ARM or Power. ARM and Power may be equivalent, but we await a proof.
The chapter’s models, side by side
The book stops short of a Power ordering table; this matrix collects what chapters 3–5 did establish. Click cells and model names:
| Property | |||||
|---|---|---|---|---|---|
| Load → Load (different addresses) | |||||
| Load → Store (different addresses) | |||||
| Store → Store (different addresses) | |||||
| Store → Load (different addresses) | |||||
| Same-address L→L / L→S / S→S | |||||
| Dependency-induced ordering | |||||
| Total global memory order | |||||
| Write atomicity | |||||
| Ordering toolkit |
✓ enforced / holds · – relaxed / absent · ◐ conditional — click for when · ? not specified
Click any cell for its explanation, or a model name for a summary.
5.8.2 How good are relaxed models?
Against the 4Ps the 4ps Programmability, Performance, Portability, Precision: criteria for a good memory consistency model. defined in Chapter 4 — open in glossary of §4.6:
- Programmability — acceptable for those who use SC for DRF; deeply understanding a relaxed model (as compiler and runtime authors must) is difficult.
- Performance — relaxed models can beat TSO, but the difference is smaller for many-core microarchitectures.
- Portability — manageable while staying within SC for DRF; pushing the limits of relaxed models, especially incomparable ones, is hard.
- Precision — many relaxed models are only informally defined, and the formal definitions that exist tend to be obtuse.
The bottom line is that … there is no simple bottom line.
Check yourself
1.Figure 5.5 updates chapter 4's Venn diagram. How do the models relate?
2.Why does the book say Power is "ASSUMED" incomparable to Alpha, ARM, RMO, and XC — and where do ARM and Power stand?
3.How do relaxed models score on the 4Ps?
4.Using the comparison matrix: which single property separates Power from EVERY other model in this chapter's lineup (SC, TSO, XC, RVWMO)?