11.4History and Further Reading

book p. 267 · ~6 min read

  • ProtoGen
  • TriCheck
  • RTLCheck
  • correct-by-construction
  • parameterized verification

The history of this chapter’s ideas begins where the book’s formal story began: in the same paper that defined SC, Lamport also gave its first operational specification — a variant of, and semantically equivalent to, §11.1’s Spec1. The delicious detail: that very first SC spec employed a linearizable memory system — a decade before Herlihy and Wing formalized linearizability. The first operational SC spec built on a consistency-directed (non-linearizable) protocol came from Afek et al.’s lazy caching (§10.3’s family patriarch), and Shasha and Snir provided the first axiomatic specification of SC.

The 1990s and early 2000s brought a wave of formal coherence-protocol verification — against invariants like SWMR and against full memory models (Pong and Dubois survey the era). Landmarks: Park and Dill abstracted and verified the FLASH multiprocessor’s protocol with a theorem prover; Qadeer showed that verifying against SC is undecidable in general, yet tractable for most practical protocols; Chatterjee et al. automatically verified a pipeline combined with a coherence protocol against an operational weak-memory spec in a model checker.

Since then, the field has attacked the verification bottleneck from three directions:

Design for verification

If parameterized proofs are hard, design protocols that make them easy: PVCoherence shapes flat protocols for straightforward parameterized verification; fractal coherence makes the protocol self-similar so verifying a small instance verifies them all.

Correct by construction

TRANSIT and verC3 use program synthesis to auto-complete partial protocol implementations. ProtoGen goes furthest: feed it an atomic protocol with only stable states — the shape of chapter 10’s tables — and it generates the complete concurrent protocol, transient states and all. The states chapters 7–8 taught you to dread, machine-derived.

Full-stack validation

Consistency spans languages to logic gates. TriCheck validates that HLL, compiler, ISA, and microarchitecture jointly satisfy the language-level model (per litmus suite); RTLCheck validates that the actual RTL implements the microarchitectural consistency spec.

The authors close the book with proper humility: this chapter — like the book itself — has “but scratched the surface” of a topic that, despite its long history, keeps producing exciting new results. Between PTX’s formalization, industrial-strength model checking, and correct-by-construction synthesis, the machinery for getting consistency and coherence right has never been better — and the subtlety that filled these eleven chapters is exactly why it’s needed.

Check yourself: history of specification and validation

1.What is historically remarkable about the operational specification in Lamport's original SC paper?

2.ProtoGen's correct-by-construction promise: what do you give it and what do you get back?

3.TriCheck and RTLCheck extend validation beyond the microarchitecture-vs-architecture question. Which layers does each cover?

3 questions
Chapter 11 references (38)
  1. Linux Kernel mailing list: Spin unlock optimization. lists.gt.net/engine?post=105365;list=linux
  2. M. Abadi and L. Lamport. The existence of refinement mappings. Theoretical Computer Science, 82(2):253–284, 1991.
  3. Y. Afek, G. M. Brown, and M. Merritt. Lazy caching. ACM TOPLAS, 15(1):182–205, 1993.
  4. J. Alglave, L. Maranget, and M. Tautschnig. Herding cats: Modelling, simulation, testing, and data mining for weak memory. ACM TOPLAS, 36(2), 2014.
  5. C. J. Banks, M. Elver, R. Hoffmann, S. Sarkar, P. Jackson, and V. Nagarajan. Verification of a lazy cache coherence protocol against a weak memory model. In FMCAD, pp. 60–67, 2017.
  6. A. Biere, A. Cimatti, E. M. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In TACAS, pp. 193–207, 1999.
  7. J. R. Burch, E. M. Clarke, K. L. McMillan, and D. L. Dill. Sequential circuit verification using symbolic model checking. In DAC, pp. 46–51, 1990.
  8. P. Chatterjee, H. Sivaraj, and G. Gopalakrishnan. Shared memory consistency protocol verification against weak memory models: Refinement via model-checking. In CAV, pp. 123–136, 2002.
  9. K. Chen, S. Malik, and P. Patra. Runtime validation of memory ordering using constraint graph checking. In HPCA-14, pp. 415–426, 2008.
  10. J. Choi, M. Vijayaraghavan, B. Sherman, A. Chlipala, and Arvind. Kami: A platform for high-level parametric hardware specification and its modular verification. PACMPL, 1(ICFP), 2017.
  11. C. Chou, P. K. Mannava, and S. Park. A simple method for parameterized verification of cache coherence protocols. In FMCAD, pp. 382–398, 2004.
  12. D. L. Dill. The Murphi verification system. In CAV, pp. 390–393, 1996.
  13. M. Elver, C. J. Banks, P. Jackson, and V. Nagarajan. VerC3: A library for explicit state synthesis of concurrent systems. In DATE, pp. 1381–1386, 2018.
  14. M. Elver and V. Nagarajan. McVerSi: A test generation framework for fast memory consistency verification in simulation. In HPCA, pp. 618–630, 2016.
  15. S. Hangal, D. Vahia, C. Manovit, J. J. Lu, and S. Narayanan. TSOtool: A program for verifying memory systems using the memory consistency model. In ISCA, pp. 114–123, 2004.
  16. M. Herlihy and J. M. Wing. Linearizability: A correctness condition for concurrent objects. ACM TOPLAS, 12(3):463–492, 1990.
  17. R. Jhala and K. L. McMillan. Microarchitecture verification by compositional model checking. In CAV, pp. 396–410, 2001.
  18. L. Lamport. Time, clocks, and the ordering of events in a distributed system. CACM, 21(7):558–565, 1978.
  19. D. Lee and V. Bertacco. MTraceCheck: Validating non-deterministic behavior of memory consistency models in post-silicon validation. In ISCA, pp. 201–213, 2017.
  20. D. Lustig, M. Pellauer, and M. Martonosi. PipeCheck: Specifying and verifying microarchitectural enforcement of memory consistency models. In MICRO, pp. 635–646, 2014.
  21. D. Lustig, G. Sethi, M. Martonosi, and A. Bhattacharjee. COATCheck: Verifying memory ordering at the hardware-OS interface. In ASPLOS, pp. 233–247, 2016.
  22. Y. A. Manerkar, D. Lustig, M. Martonosi, and A. Gupta. PipeProof: Automated memory consistency proofs for microarchitectural specifications. In MICRO, pp. 788–801, 2018.
  23. Y. A. Manerkar, D. Lustig, M. Martonosi, and M. Pellauer. RTLCheck: Verifying the memory consistency of RTL designs. In MICRO, pp. 463–476, 2017.
  24. Y. A. Manerkar, D. Lustig, M. Pellauer, and M. Martonosi. CCICheck: Using hb graphs to verify the coherence-consistency interface. In MICRO, pp. 26–37, 2015.
  25. A. Meixner and D. J. Sorin. Dynamic verification of sequential consistency. In ISCA, pp. 26–37, 2005.
  26. A. Meixner and D. J. Sorin. Dynamic verification of memory consistency in cache-coherent multithreaded computer architectures. In DSN, pp. 73–82, 2006.
  27. R. Milner. An algebraic definition of simulation between programs. In IJCAI, pp. 481–489, 1971.
  28. N. Oswald, V. Nagarajan, and D. J. Sorin. ProtoGen: Automatically generating directory cache coherence protocols from atomic specifications. In ISCA, pp. 247–260, 2018.
  29. S. Park and D. L. Dill. Verification of FLASH cache coherence protocol by aggregation of distributed transactions. In SPAA, pp. 288–296, 1996.
  30. M. Plakal, D. J. Sorin, A. Condon, and M. D. Hill. Lamport clocks: Verifying a directory cache-coherence protocol. In SPAA, pp. 67–76, 1998.
  31. A. Pnueli. The temporal logic of programs. In FOCS, pp. 46–57, 1977.
  32. F. Pong and M. Dubois. Verification techniques for cache coherence protocols. ACM Computing Surveys, 29(1):82–126, 1997.
  33. S. Qadeer. Verifying sequential consistency on shared-memory multiprocessors by model checking. IEEE TPDS, 14(8):730–741, 2003.
  34. D. E. Shasha and M. Snir. Efficient and correct execution of parallel programs that share memory. ACM TOPLAS, 10(2):282–312, 1988.
  35. C. Trippel, Y. A. Manerkar, D. Lustig, M. Pellauer, and M. Martonosi. TriCheck: Memory model verification at the trisection of software, hardware, and ISA. In ASPLOS, pp. 119–133, 2017.
  36. A. Udupa, A. Raghavan, J. V. Deshmukh, S. Mador-Haim, M. M. K. Martin, and R. Alur. TRANSIT: Specifying protocols with concolic snippets. In PLDI, pp. 287–296, 2013.
  37. M. Zhang, J. D. Bingham, J. Erickson, and D. J. Sorin. PVCoherence: Designing flat coherence protocols for scalable verification. In HPCA, pp. 392–403, 2014.
  38. M. Zhang, A. R. Lebeck, and D. J. Sorin. Fractal coherence: Scalably verifiable cache coherence. In MICRO, pp. 471–482, 2010.