research-article

Relaxed memory models: an operational approach

Authors:

Gérard Boudol,

Gustavo PetriAuthors Info & Claims

POPL '09: Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Pages 392 - 403

https://doi.org/10.1145/1480881.1480930

Published: 21 January 2009 Publication History

Abstract

Memory models define an interface between programs written in some language and their implementation, determining which behaviour the memory (and thus a program) is allowed to have in a given model. A minimal guarantee memory models should provide to the programmer is that well-synchronized, that is, data-race free code has a standard semantics. Traditionally, memory models are defined axiomatically, setting constraints on the order in which memory operations are allowed to occur, and the programming language semantics is implicit as determining some of these constraints. In this work we propose a new approach to formalizing a memory model in which the model itself is part of a weak operational semantics for a (possibly concurrent) programming language. We formalize in this way a model that allows write operations to the store to be buffered. This enables us to derive the ordering constraints from the weak semantics of programs, and to prove, at the programming language level, that the weak semantics implements the usual interleaving semantics for data-race free programs, hence in particular that it implements the usual semantics for sequential code.

References

[1]

M. Abadi, A. Birrell, T. Harris, M. Isard, Semantics of transactional memory and automatic mutual exclusion POPL'08 (2008) 63--74.

Digital Library

[2]

S. V. Adve, Designing Memory Consistency Models for Shared-Memory Multiprocessors PhD Thesis, Univ. of Wisconsin (1993).

Digital Library

[3]

S. A. Adve, K. Gharachorloo, Shared memory consistency models: a tutorial IEEE Computer Vol. 29 No. 12 (1996)66--76.

Digital Library

[4]

S. Adve, M. D. Hill, Weak ordering -- A new definition ISCA'90 1990 2--14.

Digital Library

[5]

D. Aspinall, J. Ševčík, Formalising Java's data race free guarantee TPHOLs'07, Lecture Notes in Comput. Sci. 4732 (2007) 22--37.

Digital Library

[6]

D. Aspinall, J. Ševčík, Java memory model examples: good, bad and ugly VAMP'07 (2007).

[7]

G. Berry, J.-J. Lévy, Minimal and optimal computations of recursive programs J. of ACM 26 (1979) 148--175

Digital Library

[8]

H.-J. Boehm, S. V. Adve, Foundations of the C concurrency model PLDI'08 (2008) 68--78.

Digital Library

[9]

C. Blundell, E. C. Lewis, M. M. K. Martin, Subtleties of transactional memory atomicity semantics IEEE Comput. Architecture Letters Vol. 5 No. 2 (2006).

Digital Library

[10]

G. Boudol, Atomic actions INRIA Res. Rep. 1026 and EATCS Bull. 38 (1989) 136--144

[11]

G. Boudol, I. Castellani, A non-interleaving semantics for CCS based on proved transitions Fundamenta Informaticae XI (1988) 433--452

[12]

G. Boudol, I. Castellani, Flow models of distributed computations: three equivalent semantics for CCS Information and Computation Vol. 114 No. 2 (1994) 247--314.

Digital Library

[13]

P. Cenciarelli, A. Knapp, B. Reus, M. Wirsing, An event-based structural operational semantics of multi-threaded Javain Formal Syntax and Semantics of JAVA, Lecture Notes in Comput. Sci. 1523 (1999) 157--200

Digital Library

[14]

P. Cenciarelli, A. Knapp, E. Sibilio, The Java memory model: operationally, denotationally, axiomatically ESOP'07, Lecture Notes in Comput. Sci. 4421 (2007) 331--346.

Digital Library

[15]

M. Dubois, Ch. Scheurich, F. Briggs, Memory access buffering in multiprocessors ISCA'86 (1986) 434--442.

Digital Library

[16]

L. Effinger-Dean, M. Kehrt, D. Grossman, Transactional events for MLICFP'08 (2008) 103--114.

Digital Library

[17]

G. R. Gao, V. Sarkar, Location consistency -- a new memory model and cache consistency protocol IEEE Trans. on Computers Vol. 49 No. 8 (2000) 798--813.

Digital Library

[18]

G. R. Gao, V. Sarkar, On the importance of an end-to-end view of memory consistency in future computer systems ISHPC'97, Lecture Notes in Comput. Sci. 1336 (1997) 30--41.

Digital Library

[19]

K. Gharachorloo, D. Lenoski, J. Laudon, P. Gibbons, A. Gupta, J. Hennessy, Memory consistency and event ordering in scalable shared-memory multiprocessors ACM SIGARCH Computer Architecture News Vol. 18 No. 3a (1990) 15--26.

Digital Library

[20]

P. B. Gibbons, M. Merritt, K. Gharachorloo, Proving sequential consistency of high-performance shared memories ACM Symp. on Parallel Algorithms and Architectures (1991) 292--303.

Digital Library

[21]

J. R. Goodman, Cache consistency and sequential consistency Techn. Rep. TR-1006, University of Wisconsin (1991).

[22]

D. Grossman, J. Manson, W. Pugh, What do high-level memory models mean for transactions? MSPC'06 (2006) 62--69.

Digital Library

[23]

A. Hobor, A. W. Appel, F. Zappa Nardelli, Oracle semantics for concurrent separation logic ESOP'08, Lecture Notes in Comput. Sci. 4960 (2008) 353--360.

Digital Library

[24]

Intel Corp. Intel 64 architecture memory ordering white paper (2007).

[25]

M. Huisman, G. Petri, The Java memory model: a formal explanation VAMP'07 (2007).

[26]

L. Lamport, Time, clocks, and the ordering of events in a distributed system CACM Vol. 21 No. 7 (1978) 558--565.

Digital Library

[27]

L. Lamport, How to make a multiprocessor computer that correctly executes multiprocess programs IEEE Trans. on Computers Vol. 28 No. 9 (1979) 690--691.

Digital Library

[28]

J.-J. Lévy, Optimal reductions in the lambda calculusin To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism (J. P. Seldin, J. R. Hindley, Eds), Academic Press (1980) 159--191.

[29]

J. Manson, W. Pugh, S. A. Adve, The Java memory model POPL'05 (2005) 378--391

Digital Library

[30]

K. F. Moore, D. Grossman, High-level small-step operational semantics for transactions POPL'08 (2008) 51--62.

Digital Library

[31]

J. C. Reynolds, Toward a grainless semantics for shared-variable concurrency FST-TCS'04, Lecture Notes in Comput. Sci. 3328 (2004) 35--48

Digital Library

[32]

V. Saraswat, R. Jagadeesan, M. Michael, C. von Praun, A theory of memory models PPOPP'07 (2007) 161--172.

Digital Library

[33]

X. Shen, Arvind, L. Rudolph, Commit-reconcile & fences (CRF): a new memory model for architects and compiler writers ISCA'99 (1999) 150--161.

Digital Library

[34]

R. C. Steinke, G. J. Nutt, A unified theory of shared memory consistency JACM Vol. 51 No. 5 (2004) 800--849.

Digital Library

Cited By

Abdulla PAtig MGodbole AKrishna SVahanwala M(2023)Overcoming Memory Weakness with Unified FairnessComputer Aided Verification10.1007/978-3-031-37706-8_10(184-205)Online publication date: 17-Jul-2023
https://dl.acm.org/doi/10.1007/978-3-031-37706-8_10
Abdulla PAtig MBouajjani ANarayan Kumar KSaivasan P(2022)Verifying Reachability for TSO Programs with Dynamic Thread CreationNetworked Systems10.1007/978-3-031-17436-0_19(283-300)Online publication date: 28-Sep-2022
https://doi.org/10.1007/978-3-031-17436-0_19
Melliès PStefanesco L(2018)An Asynchronous Soundness Theorem for Concurrent Separation LogicProceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3209108.3209116(699-708)Online publication date: 9-Jul-2018
https://dl.acm.org/doi/10.1145/3209108.3209116
Show More Cited By

Index Terms

Relaxed memory models: an operational approach
1. Software and its engineering
  1. Software notations and tools
    1. Compilers
2. Theory of computation
  1. Semantics and reasoning
    1. Program semantics

Recommendations

A promising semantics for relaxed-memory concurrency
POPL '17: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages

Despite many years of research, it has proven very difficult to develop a memory model for concurrent programming languages that adequately balances the conflicting desiderata of programmers, compilers, and hardware. In this paper, we propose the first ...
Relaxed memory models: an operational approach
POPL '09

Memory models define an interface between programs written in some language and their implementation, determining which behaviour the memory (and thus a program) is allowed to have in a given model. A minimal guarantee memory models should provide to ...
Specifying Java thread semantics using a uniform memory model
JGI '02: Proceedings of the 2002 joint ACM-ISCOPE conference on Java Grande

Standardized language level support for threads is one of the most important features of Java. However, defining the Java Memory Model (JMM) has turned out to be a major challenge. Several models produced to date are not as easily comprehensible and ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

POPL '09: Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

January 2009

464 pages

ISBN:9781605583792

DOI:10.1145/1480881

General Chair:
Zhong Shao
Yale University, USA
,
Program Chair:
Benjamin C. Pierce
University of Pennsylvania, USA

ACM SIGPLAN Notices Volume 44, Issue 1
POPL '09
January 2009
453 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/1594834
Issue’s Table of Contents

Copyright © 2009 ACM.

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

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 21 January 2009

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

POPL09

Sponsor:

POPL09: The 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

January 21 - 23, 2009

GA, Savannah, USA

Acceptance Rates

Overall Acceptance Rate 860 of 4,328 submissions, 20%

Upcoming Conference

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

69
Total Citations
View Citations
862
Total Downloads

Downloads (Last 12 months)19
Downloads (Last 6 weeks)4

Reflects downloads up to 12 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Abdulla PAtig MGodbole AKrishna SVahanwala M(2023)Overcoming Memory Weakness with Unified FairnessComputer Aided Verification10.1007/978-3-031-37706-8_10(184-205)Online publication date: 17-Jul-2023
https://dl.acm.org/doi/10.1007/978-3-031-37706-8_10
Abdulla PAtig MBouajjani ANarayan Kumar KSaivasan P(2022)Verifying Reachability for TSO Programs with Dynamic Thread CreationNetworked Systems10.1007/978-3-031-17436-0_19(283-300)Online publication date: 28-Sep-2022
https://doi.org/10.1007/978-3-031-17436-0_19
Melliès PStefanesco L(2018)An Asynchronous Soundness Theorem for Concurrent Separation LogicProceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3209108.3209116(699-708)Online publication date: 9-Jul-2018
https://dl.acm.org/doi/10.1145/3209108.3209116
Abe TMaeda T(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
https://dl.acm.org/doi/10.1007/s10009-016-0429-y
Prasad S(2016)Program Execution on Reconfigurable Multicore ArchitecturesElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.211.9211(83-91)Online publication date: 17-Jun-2016
https://doi.org/10.4204/EPTCS.211.9
Zakkak FPratikakis PZheng YBinder WTůma P(2016)DiSquawkProceedings of the 13th International Conference on Principles and Practices of Programming on the Java Platform: Virtual Machines, Languages, and Tools10.1145/2972206.2972212(1-12)Online publication date: 29-Aug-2016
https://dl.acm.org/doi/10.1145/2972206.2972212
Blanchard AKosmatov NLemerre MLoulergue F(2015)A Case Study on Formal Verification of the Anaxagoros Hypervisor Paging System with Frama-CFormal Methods for Industrial Critical Systems10.1007/978-3-319-19458-5_2(15-30)Online publication date: 2015
https://doi.org/10.1007/978-3-319-19458-5_2
Abe TMaeda TMalony AHammond J(2014)Optimization of a General Model Checking Framework for Various Memory Consistency ModelsProceedings of the 8th International Conference on Partitioned Global Address Space Programming Models10.1145/2676870.2676878(1-10)Online publication date: 6-Oct-2014
https://dl.acm.org/doi/10.1145/2676870.2676878
Alglave JMaranget LTautschnig M(2014)Herding CatsACM Transactions on Programming Languages and Systems10.1145/262775236:2(1-74)Online publication date: 1-Jul-2014
https://dl.acm.org/doi/10.1145/2627752
Lochbihler A(2014)Making the java memory model safeACM Transactions on Programming Languages and Systems10.1145/251819135:4(1-65)Online publication date: 3-Jan-2014
https://dl.acm.org/doi/10.1145/2518191
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Table of Conten