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.
Supplemental Material
- S. V. Adve and K. Gharachorloo. Shared memory consistency models: A tutorial. IEEE Computer, 29(12):66--76, 1996. Google ScholarDigital Library
- J. Alglave, L. Maranget, S. Sarkar, and P. Sewell. Fences in weak memory models. In Proc. CAV, 2010. Google ScholarDigital Library
- P. Becker, editor. Programming Languages -- C++. Final Committee Draft. 2010. ISO/IEC JTC1 SC22 WG21 N3092.Google Scholar
- N. Benton and C.K Hur. Biorthogonality, step-indexing and compiler correctness. In Proc. ICFP, 2009. Google ScholarDigital Library
- Sandrine Blazy and Xavier Leroy. Mechanized semantics for the Clight subset of the C language. Journal of Automated Reasoning, 43(3):263--288, 2009.Google ScholarCross Ref
- H.-J. Boehm. Threads cannot be implemented as a library. In Proc. PLDI, pages 261--268, 2005. Google ScholarDigital Library
- M. Batty, S. Owens, S. Sarkar, P. Sewell, and T.Weber. Mathematizing C++ concurrency. In Proc. POPL, 2011. Google ScholarDigital Library
- Programming languages -- C (committee draft, WG14 N1494, ISO/IEC 9899:201x). http://www.open-std.org/jtc1/sc22/wg14/www/docs/PostColorado.htm.Google Scholar
- A. Chlipala. A verified compiler for an impure functional language. In Proc. POPL, 2010. Google ScholarDigital Library
- P. Cenciarelli, A. Knapp, and E. Sibilio. The Java memory model: Operationally, denotationally, axiomatically. In Proc. ESOP, 2007. Google ScholarDigital Library
- The Compcert verified compiler, v. 1.5. http://compcert.inria.fr/release/compcert-1.5.tgz, August 2009.Google Scholar
- The Coq proof assistant. http://coq.inria.fr/.Google Scholar
- Keir Fraser. Practical Lock Freedom. PhD thesis, 2003. Also available as Tech. Report UCAM-CL-TR-639.Google Scholar
- G. Gonthier and A.Mahboubi. A small scale reflection extension for the coq system. Technical report, 2007.Google Scholar
- A. Hobor, A.W. Appel, and F. Zappa Nardelli. Oracle semantics for concurrent separation logic. In Proc. ESOP, 2008. Google ScholarDigital Library
- L. Lamport. How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Comput., C-28(9):690--691, 1979. Google ScholarDigital Library
- D. Lea. Concurrent Programming in Java. Second Edition: Design Principles and Patterns. 1999. Google ScholarDigital Library
- Xavier Leroy. Formal verification of a realistic compiler. Communications of the ACM, 52(7):107--115, 2009. Google ScholarDigital Library
- Xavier Leroy. A formally verified compiler back-end. Journal of Automated Reasoning, 43(4):363--446, 2009. Google ScholarDigital Library
- 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.Google Scholar
- A. Lochbihler. Verifying a compiler for Java threads. In Proc. ESOP'10, 2010. Google ScholarDigital Library
- R. Milner. Communication and Concurrency. Prentice Hall International, 1989. Google ScholarDigital Library
- J. Manson, W. Pugh, and S.V. Adve. The Java memory model. In Proc. POPL, 2005. Google ScholarDigital Library
- M. O. Myreen. Verified just-in-time compiler on x86. In Proc. POPL, 2010. Google ScholarDigital Library
- S. Owens, S. Sarkar, and P. Sewell. A better x86 memory model: x86-TSO. In Proc. TPHOLs, 2009. Google ScholarDigital Library
- S. Owens. Reasoning about the implementation of concurrency abstractions on x86-TSO. In Proc. ECOOP, 2010. Google ScholarDigital Library
- W. Pugh. The Java memory model is fatally flawed. Concurrency - Practice and Experience, 12(6), 2000.Google Scholar
- J. Ševçík and D. Aspinall. On validity of program transformations in the Java memory model. In ECOOP, 2008. Google ScholarDigital Library
- P. Sewell. On implementations and semantics of a concurrent programming language. In Proc. CONCUR, July 1997. Google ScholarDigital Library
- The SPARC architecture manual, v. 9. http://dev elopers.sun.com/solaris/articles/sparcv9.pdf. Google ScholarDigital Library
- The SPARC Architecture Manual, V. 8. SPARC International, Inc., 1992. Revision SAV080SI9308. http://www.sparc.org/standards/V8.pdf. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- E. Torlak, M. Vaziri, and J. Dolby. MemSAT: checking axiomatic specifications of memory models. In PLDI, 2010. Google ScholarDigital Library
Index Terms
- Relaxed-memory concurrency and verified compilation
Recommendations
Clarifying and compiling C/C++ concurrency: from C++11 to POWER
POPL '12: Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languagesThe upcoming C and C++ revised standards add concurrency to the languages, for the first time, in the form of a subtle *relaxed memory model* (the *C++11 model*). This aims to permit compiler optimisation and to accommodate the differing relaxed-memory ...
CompCertTSO: A Verified Compiler for Relaxed-Memory Concurrency
In this article, we consider the semantic design and verified compilation of a C-like programming language for concurrent shared-memory computation on x86 multiprocessors. The design of such a language is made surprisingly subtle by several factors: the ...
Relaxed-memory concurrency and verified compilation
POPL '11In 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: ...
Comments