skip to main content
10.1145/2676726.2676984acmconferencesArticle/Chapter ViewAbstractPublication PagespoplConference Proceedingsconference-collections
research-article

A Calculus for Relaxed Memory

Published: 14 January 2015 Publication History

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 specified requirements, RMC is designed to be strictly more relaxed than existing architectures. It employs an aggressively nondeterministic semantics for expressions, in which actions can be executed in nearly any order, and a store semantics that generalizes Sarkar et al.'s and Alglave et al.'s models of the Power architecture. We establish several results for RMC, including sequential consistency for two programming disciplines, and an appropriate notion of type safety. All our results are formalized in Coq.

Supplementary Material

MPG File (p623-sidebyside.mpg)

References

[1]
S. Adve and K. Gharachorloo. Shared memory consistency models: A tutorial. IEEE Computer, 1995.
[2]
J. Alglave. A Shared Memory Poetics. PhD thesis, Université Paris VII, Nov. 2010.
[3]
J. Alglave. A formal hierarchy of weak memory models. Formal Methods in System Design, 41: 178--210, 2012.
[4]
J. Alglave, L. Maranget, S. Sarkar, and P. Sewell. Fences in weak memory models. In Twenty-Second International Conference on Computer Aided Verification, 2010.
[5]
J. Alglave, L. Maranget, and M. Tautschnig. Herding cats: Modelling, simulation, testing, and data-mining for weak memory. ACM Transactions on Programming Languages and Systems, 2014. To appear.
[6]
M. Batty and P. Sewell. The thin-air problem. Working note, available at http://www.cl.cam.ac.uk/ pes20/cpp/notes42.html, Feb. 2014.
[7]
M. Batty, S. Owens, S. Sarkar, P. Sewell, and T. Weber. Mathematizing C
[8]
concurrency: The post-Rapperswil model. Technical Report N3132, ISO IEC JTC1/SC22/WG21, Aug. 2010. Available electronically at www.open-std.org/jtc1/sc22/wg21/docs/papers/2010/n3132.pdf.
[9]
M. Batty, S. Owens, S. Sarkar, P. Sewell, and T. Weber. Mathematizing C
[10]
concurrency. In Thirty-Eighth ACM Symposium on Principles of Programming Languages, Austin, Texas, Jan. 2011.
[11]
M. Batty, K. Memarian, S. Owens, S. Sarkar, and P. Sewell. Clarifying and compiling C/C
[12]
concurrency: from C
[13]
11 to POWER. In Thirty-Ninth ACM Symposium on Principles of Programming Languages, Philadelphia, Pennsylvania, Jan. 2012.
[14]
M. Batty, M. Dodds, and A. Gotsman. Library abstraction for C/C
[15]
concurrency. In Fortieth ACM Symposium on Principles of Programming Languages, Rome, Italy, Jan. 2013.
[16]
H.-J. Boehm and S. V. Adve. Foundations of the C
[17]
concurrency memory model. In 2008 SIGPLAN Conference on Programming Language Design and Implementation, Tucson, Arizona, June 2008.
[18]
K. Crary and M. J. Sullivan. A calculus for relaxed memory. Technical Report Carnegie Mellon University-CS-14--139, Carnegie Mellon University, School of Computer Science, 2014.
[19]
R. Grisenthwaite. ARM barrier litmus tests and cookbook. http://infocenter.arm.com/help/topic/com.arm.doc.genc007826/Barrier_Litmus_Tests_and_Cookbook_A08.pdf, 2009.
[20]
D. Howells and P. E. McKenney. Circular buffers. https://www.kernel.org/doc/Documentation/circular-buffers.txt.
[21]
IBM. Power ISA™ version 2.06 revision B, 2010.
[22]
R. Jagadeesan, C. Pitcher, and J. Riely. Generative operational semantics for relaxed memory models. In Nineteenth European Symposium on Programming, 2010.
[23]
L. Lamport. How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Transactions on Computers, C-28 (9), Sept. 1979.
[24]
J. Manson, W. Pugh, and S. V. Adve. The Java memory model. In Thirty-Second ACM Symposium on Principles of Programming Languages, Long Beach, California, Jan. 2005.
[25]
J. Polakow. Ordered Linear Logic and Applications. PhD thesis, Carnegie Mellon University, School of Computer Science, Pittsburgh, Pennsylvania, Aug. 2001.
[26]
J. C. Reynolds. Types, abstraction and parametric polymorphism. In Information Processing '83, pages 513--523. North-Holland, 1983. Proceedings of the IFIP 9th World Computer Congress.
[27]
Sarkar, Sewell, Alglave, and Maranget}sarkar
[28]
:leapfrog-codeS. Sarkar, P. Sewell, J. Alglave, and L. Maranget. ppcmem executable model (ARM version). Unpublished code, 2011\natexlaba.
[29]
Sarkar, Sewell, Alglave, Maranget, and Williams}sarkar
[30]
:powerS. Sarkar, P. Sewell, J. Alglave, L. Maranget, and D. Williams. Understanding POWER multiprocessors. In 2011 SIGPLAN Conference on Programming Language Design and Implementation, San Jose, California, June 2011\natexlabb.
[31]
P. Sewell, S. Sarkar, S. Owens, F. Z. Nardelli, and M. O. Myreen. x86-TSO: A rigorous and usable programmer's model for x86 multiprocessors. Communications of the ACM, 53 (7), July 2010.
[32]
A. K. Wright and M. Felleisen. A syntactic approach to type soundness. Information and Computation, 115: 38--94, 1994.

Cited By

View all
  • (2024)An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: The AxSL LogicProceedings of the ACM on Programming Languages10.1145/36328638:POPL(604-637)Online publication date: 5-Jan-2024
  • (2021)Distributed causal memory: modular specification and verification in higher-order distributed separation logicProceedings of the ACM on Programming Languages10.1145/34343235:POPL(1-29)Online publication date: 4-Jan-2021
  • (2021)A Survey of Programming Language Memory ModelsProgramming and Computing Software10.1134/S036176882106005047:6(439-456)Online publication date: 3-Dec-2021
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences
POPL '15: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
January 2015
716 pages
ISBN:9781450333009
DOI:10.1145/2676726
  • cover image ACM SIGPLAN Notices
    ACM SIGPLAN Notices  Volume 50, Issue 1
    POPL '15
    January 2015
    682 pages
    ISSN:0362-1340
    EISSN:1558-1160
    DOI:10.1145/2775051
    • Editor:
    • Andy Gill
    Issue’s Table of Contents
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

In-Cooperation

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 14 January 2015

Permissions

Request permissions for this article.

Check for updates

Author Tag

  1. relaxed memory concurrency

Qualifiers

  • Research-article

Conference

POPL '15
Sponsor:

Acceptance Rates

POPL '15 Paper Acceptance Rate 52 of 227 submissions, 23%;
Overall Acceptance Rate 860 of 4,328 submissions, 20%

Upcoming Conference

POPL '26

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)7
  • Downloads (Last 6 weeks)0
Reflects downloads up to 19 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2024)An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: The AxSL LogicProceedings of the ACM on Programming Languages10.1145/36328638:POPL(604-637)Online publication date: 5-Jan-2024
  • (2021)Distributed causal memory: modular specification and verification in higher-order distributed separation logicProceedings of the ACM on Programming Languages10.1145/34343235:POPL(1-29)Online publication date: 4-Jan-2021
  • (2021)A Survey of Programming Language Memory ModelsProgramming and Computing Software10.1134/S036176882106005047:6(439-456)Online publication date: 3-Dec-2021
  • (2021)Global Analysis of C Concurrency in High-Level SynthesisIEEE Transactions on Very Large Scale Integration (VLSI) Systems10.1109/TVLSI.2020.302611229:1(24-37)Online publication date: Jan-2021
  • (2019)A formalization of Java’s concurrent access modesProceedings of the ACM on Programming Languages10.1145/33605683:OOPSLA(1-28)Online publication date: 10-Oct-2019
  • (2017)A promising semantics for relaxed-memory concurrencyACM SIGPLAN Notices10.1145/3093333.300985052:1(175-189)Online publication date: 1-Jan-2017
  • (2017)A promising semantics for relaxed-memory concurrencyProceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages10.1145/3009837.3009850(175-189)Online publication date: 1-Jan-2017
  • (2017)A general model checking framework for various memory consistency modelsInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-016-0429-y19:5(623-647)Online publication date: 1-Oct-2017
  • (2017)A Formal Model of Parallel Execution on Multicore Architectures with Multilevel CachesFormal Aspects of Component Software10.1007/978-3-319-68034-7_4(58-77)Online publication date: 14-Sep-2017
  • (2017)Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming LanguagesundefinedOnline publication date: 1-Jan-2017
  • Show More Cited By

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media