Relaxed-memory concurrency and verified compilation

ABSTRACT

In this paper, we consider the semantic design and verified compilation of a C-like programming language for concurrent shared-memory computation above x86 multiprocessors. The design of such a language is made surprisingly subtle by several factors: the relaxed-memory behaviour of the hardware, the effects of compiler optimisation on concurrent code, the need to support high-performance concurrent algorithms, and the desire for a reasonably simple programming model. In turn, this complexity makes verified (or verifying) compilation both essential and challenging.

We define a concurrent relaxed-memory semantics for ClightTSO, an extension of CompCert's Clight in which the processor's memory model is exposed for high-performance code. We discuss a strategy for verifying compilation from ClightTSO to x86, which we validate with correctness proofs (building on CompCert) for the most interesting compiler phases.

References

1. S. V. Adve and K. Gharachorloo. Shared memory consistency models: A tutorial. IEEE Computer, 29(12):66--76, 1996.
2. J. Alglave, L. Maranget, S. Sarkar, and P. Sewell. Fences in weak memory models. In Proc. CAV, 2010.
3. P. Becker, editor. Programming Languages -- C++. Final Committee Draft. 2010. ISO/IEC JTC1 SC22 WG21 N3092.
4. N. Benton and C.K Hur. Biorthogonality, step-indexing and compiler correctness. In Proc. ICFP, 2009.
5. Sandrine Blazy and Xavier Leroy. Mechanized semantics for the Clight subset of the C language. Journal of Automated Reasoning, 43(3):263--288, 2009.
6. H.-J. Boehm. Threads cannot be implemented as a library. In Proc. PLDI, pages 261--268, 2005.
7. M. Batty, S. Owens, S. Sarkar, P. Sewell, and T.Weber. Mathematizing C++ concurrency. In Proc. POPL, 2011.
8. Programming languages -- C (committee draft, WG14 N1494, ISO/IEC 9899:201x). http://www.open-std.org/jtc1/sc22/wg14/www/docs/PostColorado.htm.
9. A. Chlipala. A verified compiler for an impure functional language. In Proc. POPL, 2010.
10. P. Cenciarelli, A. Knapp, and E. Sibilio. The Java memory model: Operationally, denotationally, axiomatically. In Proc. ESOP, 2007.
11. The Compcert verified compiler, v. 1.5. http://compcert.inria.fr/release/compcert-1.5.tgz, August 2009.
12. The Coq proof assistant. http://coq.inria.fr/.
13. Keir Fraser. Practical Lock Freedom. PhD thesis, 2003. Also available as Tech. Report UCAM-CL-TR-639.
14. G. Gonthier and A.Mahboubi. A small scale reflection extension for the coq system. Technical report, 2007.
15. A. Hobor, A.W. Appel, and F. Zappa Nardelli. Oracle semantics for concurrent separation logic. In Proc. ESOP, 2008.
16. L. Lamport. How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Comput., C-28(9):690--691, 1979.
17. D. Lea. Concurrent Programming in Java. Second Edition: Design Principles and Patterns. 1999.
18. Xavier Leroy. Formal verification of a realistic compiler. Communications of the ACM, 52(7):107--115, 2009.
19. Xavier Leroy. A formally verified compiler back-end. Journal of Automated Reasoning, 43(4):363--446, 2009.
20. 1999. Linux Kernel mailing list, thread "spin unlock optimization(i386)", 119 messages, Nov. 20-Dec. 7th, http://www.gossamer-threads.com/lists/engine? post=105365;list=linux. Accessed 2009/11/18.
21. A. Lochbihler. Verifying a compiler for Java threads. In Proc. ESOP'10, 2010.
22. R. Milner. Communication and Concurrency. Prentice Hall International, 1989.
23. J. Manson, W. Pugh, and S.V. Adve. The Java memory model. In Proc. POPL, 2005.
24. M. O. Myreen. Verified just-in-time compiler on x86. In Proc. POPL, 2010.
25. S. Owens, S. Sarkar, and P. Sewell. A better x86 memory model: x86-TSO. In Proc. TPHOLs, 2009.
26. S. Owens. Reasoning about the implementation of concurrency abstractions on x86-TSO. In Proc. ECOOP, 2010.
27. W. Pugh. The Java memory model is fatally flawed. Concurrency - Practice and Experience, 12(6), 2000.
28. J. Ševçík and D. Aspinall. On validity of program transformations in the Java memory model. In ECOOP, 2008.
29. P. Sewell. On implementations and semantics of a concurrent programming language. In Proc. CONCUR, July 1997.
30. The SPARC architecture manual, v. 9. http://dev elopers.sun.com/solaris/articles/sparcv9.pdf.
31. The SPARC Architecture Manual, V. 8. SPARC International, Inc., 1992. Revision SAV080SI9308. http://www.sparc.org/standards/V8.pdf.
32. P. Sewell, S. Sarkar, S. Owens, F. Zappa Nardelli, and M. O. Myreen. x86-TSO: A rigorous and usable programmer's model for x86 multiprocessors. C. ACM, 53(7):89--97, 2010.
33. S. Sarkar, P. Sewell, F. Zappa Nardelli, S. Owens, T. Ridge, T. Braibant, M. Myreen, and J. Alglave. The semantics of x86-CC multiprocessor machine code. In Proc. POPL, 2009.
34. P. Sewell, F. Zappa Nardelli, S. Owens, G. Peskine, T. Ridge, S. Sarkar, and R. StrniŠa. Ott: Effective tool support for the working semanticist. J. Funct. Program., 20(1):71--122, 2010.
35. E. Torlak, M. Vaziri, and J. Dolby. MemSAT: checking axiomatic specifications of memory models. In PLDI, 2010.

Index Terms

• Computer systems organization

  • Architectures

    • Parallel architectures

      • Multiple instruction, multiple data

• Computing methodologies

  • Concurrent computing methodologies

    • Concurrent programming languages

• Software and its engineering

  • Software notations and tools

    • General programming languages

      • Language types

        • Concurrent programming languages

• Theory of computation

  • Logic

  • Semantics and reasoning

    • Program reasoning