Relaxed-Memory Concurrency and Verified Compilation

In this paper, the authors 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.

Provided by: Association for Computing Machinery Topic: Data Centers Date Added: Jan 2011 Format: PDF

Find By Topic