publication . Article . Conference object . 2015

A Calculus for Relaxed Memory

Name: A Calculus for Relaxed Memory
Keywords: Software, Computer Graphics and Computer-Aided Design

Michael J. Sullivan; Karl Crary;

Open Access

Published: 11 May 2015 Journal: ACM SIGPLAN Notices, volume 50, pages 623-636 (issn: 0362-1340, eissn: 1558-1160,

Publisher: Association for Computing Machinery (ACM)

Summary

Abstract

We propose a new approach to programming multi-core, relaxed-memory architectures in imperative, portable programming languages. Our memory model is based on explicit, programmer-specified requirements for order of execution and the visibility of writes. The compiler then realizes those requirements in the most efficient manner it can. This is in contrast to existing memory models, which---if they allow programmer control over synchronization at all---are based on inferring the execution and visibility consequences of synchronization operations or annotations in the code. We formalize our memory model in a core calculus called RMC\@. Outside of the programmer's ...

doi: 10.1145/2775051.2676984 , 10.1145/2676726.2676984

Subjects

free text keywords: Software, Computer Graphics and Computer-Aided Design, Expression (mathematics), Sequential consistency, Compiler, computer.software_genre, computer, Computer science, Programmer, Semantics, Type safety, Programming language, Memory model, Calculus, Nondeterministic algorithm

Related Organizations