research-article

Plan B: a buffered memory model for Java

Authors:

Delphine Demange,

Vincent Laporte,

Suresh Jagannathan,

David Pichardie,

Jan VitekAuthors Info & Claims

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

Pages 329 - 342

https://doi.org/10.1145/2429069.2429110

Published: 23 January 2013 Publication History

Abstract

Recent advances in verification have made it possible to envision trusted implementations of real-world languages. Java with its type-safety and fully specified semantics would appear to be an ideal candidate; yet, the complexity of the translation steps used in production virtual machines have made it a challenging target for verifying compiler technology. One of Java's key innovations, its memory model, poses significant obstacles to such an endeavor. The Java Memory Model is an ambitious attempt at specifying the behavior of multithreaded programs in a portable, hardware agnostic, way. While experts have an intuitive grasp of the properties that the model should enjoy, the specification is complex and not well-suited for integration within a verifying compiler infrastructure. Moreover, the specification is given in an axiomatic style that is distant from the intuitive reordering-based reasonings traditionally used to justify or rule out behaviors, and ill suited to the kind of operational reasoning one would expect to employ in a compiler. This paper takes a step back, and introduces a Buffered Memory Model (BMM) for Java. We choose a pragmatic point in the design space sacrificing generality in favor of a model that is fully characterized in terms of the reorderings it allows, amenable to formal reasoning, and which can be efficiently applied to a specific hardware family, namely x86 multiprocessors. Although the BMM restricts the reorderings compilers are allowed to perform, it serves as the key enabling device to achieving a verification pathway from bytecode to machine instructions. Despite its restrictions, we show that it is backwards compatible with the Java Memory Model and that it does not cripple performance on TSO architectures.

Supplementary Material

JPG File (r1d2_talk8.jpg)

Download
10.71 KB

MP4 File (r1d2_talk8.mp4)

Download
208.71 MB

References

[1]

S. V. Adve and K. Gharachorloo. Shared memory consistency models: A tutorial. Computer, 29(12), 1996.

Digital Library

[2]

S. V. Adve and M. Hill. A Unified Formalization of Four Shared-Memory Models. Par. and Distr. Systems, IEEE Transactions on, 1993.

Digital Library

[3]

J. Alglave, L. Maranget, S. Sarkar, and P. Sewell. Fences in Weak Memory Models. In Proc. of CAV, 2010.

Digital Library

[4]

D. Aspinall and J. Sevc1k. Java Memory Model Examples: Good, Bad and Ugly. In Proc. of VAMP, 2007.

[5]

D. Aspinall and J. Sevc1k. Formalising Java's Data Race Free Guarantee. In Proc. of TPHOLs, 2007.

Digital Library

[6]

H.-J. Boehm and S. V. Adve. Foundations of the C++ concurrency memory model. SIGPLAN Not., 43, 2008.

Digital Library

[7]

G. Boudol and G. Petri. Relaxed Memory Models: an Operational Approach. In Proc. of POPL, 2009.

Digital Library

[8]

G. Boudol and G. Petri. A Theory of Speculative Computation. In Proc. of ESOP, 2010.

Digital Library

[9]

S. Burckhardt, M. Musuvathi, and V. Singh. Verifying Local Transformations on Relaxed Memory Models. In Proc. of CC, 2010.

Digital Library

[10]

P. Cenciarelli, A. Knapp, and E. Sibilio. The Java Memory Model: Operationally, denotationally, axiomatically. In Proc. of ESOP, 2007.

Digital Library

[11]

B. Goetz, T. Peierls, J. Bloch, J. Bowbeer, D. Holmes, and D. Lea. Java Concurrency in Practice. Addison-Wesley Longman, 2006.

Digital Library

[12]

T. Henties, J. Hunt, D. Locke, K. Nilsen, M. Schoeberl, and J. Vitek. Java for safety-critical applications. In SafeCert, 2009.

[13]

L. Higham, J. Kawash, and N. Verwaaland. Defining and Comparing Memory Consistency Models. In Proc. of PDCS, 1997.

[14]

L. Hubert, T. Jensen, V. Monfort, and D. Pichardie. Enforcing Secure Object Initialization in Java. In Proc. of ESORICS, 2010.

Digital Library

[15]

M. Huisman and G. Petri. The Java Memory Model: a Formal Explanation. In Proc. of VAMP, 2007.

[16]

R. Jagadeesan, C. Pitcher, and J. Riely. Generative Operational Semantics for Relaxed Memory Models. In Proc. of ESOP, 2010.

Digital Library

[17]

K. Kawachiya, A. Koseki, and T. Onodera. Lock Reservation: Java Locks can Mostly doWithout Atomic Operations. In Proc. of OOPSLA, 2002.

Digital Library

[18]

G. Klein and T. Nipkow. A Machine-Checked Model for a Java-like Language, Virtual Machine, and Compiler. ACM Trans. Program. Lang. Syst., 28(4), 2006.

Digital Library

[19]

L. Lamport. Time, Clocks, and the Ordering of Events in a Distributed System. Commun. ACM, 21(7), 1978.

Digital Library

[20]

X. Leroy. A Formally Verified Compiler Back-end. J. Autom. Reasoning, 43(4), 2009.

Digital Library

[21]

A. Lochbihler. Java and the Java memory Model -- a Unified, Machine-Checked Formalisation. In Proc. of ESOP, 2012.

Digital Library

[22]

J. Manson, W. Pugh, and S. V. Adve. The Java Memory Model. In Proc. of POPL, 2005.

Digital Library

[23]

D. Marino, A. Singh, T. D. Millstein, M. Musuvathi, and S. Narayanasamy. A Case for an SC-Preserving Compiler. In Proc. of PLDI, 2011.

Digital Library

[24]

A. Mine. Static Analysis of Run-Time Errors in Embedded Critical Parallel C Programs. In Proc. of ESOP, 2011.

Digital Library

[25]

S. Owens, S. Sarkar, and P. Sewell. A Better x86 Memory Model: x86-TSO. In Proc. of TPHOLs, 2009.

Digital Library

[26]

F. Pizlo, L. Ziarek, E. Blanton, P. Maj, and J. Vitek. High-level Programming of Embedded Hard Real-Time Devices. In Proc. of EuroSys, 2010.

Digital Library

[27]

W. Pugh. The Initialization On Demand Holder idiom, 2004. http://www.cs.umd.edu/~pugh/java/memoryModel/jsr-133-faq.html#dcl.

[28]

W. Pugh. Causality test cases for the Java Memory Model, 2004. http://www.cs.umd.edu/~pugh/java/memoryModel/CausalityTestCases.html.

[29]

K. Russell and D. Detlefs. Eliminating Synchronization-Related Atomic Operations with Biased Locking and Bulk Rebiasing. In Proc. of OOPSLA, 2006.

Digital Library

[30]

S. Sarkar, P. Sewell, F. Z. Nardelli, S. Owens, T. Ridge, T. Braibant, M. O. Myreen, and J. Alglave. The Semantics of x86-CC Multiprocessor Machine Code. In Proc. of POPL, 2009.

Digital Library

[31]

S. Sarkar, P. Sewell, J. Alglave, L. Maranget, and D. Williams. Understanding Power Multiprocessors. In Proc. of PLDI, 2011.

Digital Library

[32]

J. Sevc1k. Program Transformations in Weak Memory Models. PhD thesis, The University of Edinburgh, 2009.

[33]

J. Sevc1k. Safe optimisations for shared-memory concurrent programs. In Proc. of PLDI, 2011.

Digital Library

[34]

J. Sevc1k and D. Aspinall. On Validity of Program Transformations in the Java Memory Model. In Proc. of ECOOP, 2008.

Digital Library

[35]

J. Sevc1k, V. Vafeiadis, F. Z. Nardelli, S. Jagannathan, and P. Sewell. Relaxed-memory Concurrency and Verified Compilation. In Proc. of POPL, 2011.

Digital Library

[36]

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. Commun. ACM, 53(7), 2010.

Digital Library

[37]

E. Torlak, M. Vaziri, and J. Dolby. MemSAT: Checking Axiomatic Specifications of Memory Models. In Proc. of PLDI, 2010.

Digital Library

[38]

V. Vafeiadis and F. Z. Nardelli. Verifying fence elimination optimisations. In Proc. of SAS, 2011.

Digital Library

Cited By

Xiao LZhu H(2022)UTP semantics for the MCA ARMv8 architectureJournal of Systems Architecture: the EUROMICRO Journal10.1016/j.sysarc.2022.102438125:COnline publication date: 18-May-2022
https://dl.acm.org/doi/10.1016/j.sysarc.2022.102438
Liu LMillstein TMusuvathi M(2021)Safe-by-default Concurrency for Modern Programming LanguagesACM Transactions on Programming Languages and Systems10.1145/346220643:3(1-50)Online publication date: 3-Sep-2021
https://dl.acm.org/doi/10.1145/3462206
Jagadeesan RJeffrey ARiely J(2020)Pomsets with preconditions: a simple model of relaxed memoryProceedings of the ACM on Programming Languages10.1145/34282624:OOPSLA(1-30)Online publication date: 13-Nov-2020
https://dl.acm.org/doi/10.1145/3428262
Show More Cited By

Index Terms

Plan B: a buffered memory model for Java
1. Software and its engineering
  1. Software notations and tools
    1. Formal language definitions
      1. Semantics
2. Theory of computation
  1. Semantics and reasoning
    1. Program semantics

Recommendations

Plan B: a buffered memory model for Java
POPL '13

Recent advances in verification have made it possible to envision trusted implementations of real-world languages. Java with its type-safety and fully specified semantics would appear to be an ideal candidate; yet, the complexity of the translation ...
JDMM: a java memory model for non-cache-coherent memory architectures
ISMM '14: Proceedings of the 2014 international symposium on Memory management

As the number of cores continuously grows, processor designers are considering non coherent memories as more scalable and energy efficient alternatives to the current coherent ones. The Java Memory Model (JMM) requires that all cores can access the Java ...
JDMM: a java memory model for non-cache-coherent memory architectures
ISMM '14

As the number of cores continuously grows, processor designers are considering non coherent memories as more scalable and energy efficient alternatives to the current coherent ones. The Java Memory Model (JMM) requires that all cores can access the Java ...

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences

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

January 2013

586 pages

ISBN:9781450318327

DOI:10.1145/2429069

General Chair:
Roberto Giacobazzi
Università di Verona, Italy
,
Program Chair:
Radhia Cousot
École normale supérieure CNRS & INRIA, France

ACM SIGPLAN Notices Volume 48, Issue 1
POPL '13
January 2013
561 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/2480359
Issue’s Table of Contents

Copyright © 2013 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

SIGPLAN: ACM Special Interest Group on Programming Languages

In-Cooperation

SIGACT: ACM Special Interest Group on Algorithms and Computation Theory

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 23 January 2013

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

POPL '13

Sponsor:

SIGPLAN

POPL '13: The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

January 23 - 25, 2013

Rome, Italy

Acceptance Rates

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

Upcoming Conference

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

32
Total Citations
View Citations
488
Total Downloads

Downloads (Last 12 months)8
Downloads (Last 6 weeks)0

Reflects downloads up to 18 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Xiao LZhu H(2022)UTP semantics for the MCA ARMv8 architectureJournal of Systems Architecture: the EUROMICRO Journal10.1016/j.sysarc.2022.102438125:COnline publication date: 18-May-2022
https://dl.acm.org/doi/10.1016/j.sysarc.2022.102438
Liu LMillstein TMusuvathi M(2021)Safe-by-default Concurrency for Modern Programming LanguagesACM Transactions on Programming Languages and Systems10.1145/346220643:3(1-50)Online publication date: 3-Sep-2021
https://dl.acm.org/doi/10.1145/3462206
Jagadeesan RJeffrey ARiely J(2020)Pomsets with preconditions: a simple model of relaxed memoryProceedings of the ACM on Programming Languages10.1145/34282624:OOPSLA(1-30)Online publication date: 13-Nov-2020
https://dl.acm.org/doi/10.1145/3428262
Liu LMillstein TMusuvathi MMcKinley KFisher K(2019)Accelerating sequential consistency for Java with speculative compilationProceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/3314221.3314611(16-30)Online publication date: 8-Jun-2019
https://dl.acm.org/doi/10.1145/3314221.3314611
Zakowski YCachera DDemange DPetri GPichardie DJagannathan SVitek J(2019)Verifying a Concurrent Garbage Collector with a Rely-Guarantee MethodologyJournal of Automated Reasoning10.1007/s10817-018-9489-x63:2(489-515)Online publication date: 1-Aug-2019
https://dl.acm.org/doi/10.1007/s10817-018-9489-x
Jeon MJeong SOh H(2018)Precise and scalable points-to analysis via data-driven context tunnelingProceedings of the ACM on Programming Languages10.1145/32765102:OOPSLA(1-29)Online publication date: 24-Oct-2018
https://dl.acm.org/doi/10.1145/3276510
Szabó TBergmann GErdweg SVoelter M(2018)Incrementalizing lattice-based program analyses in DatalogProceedings of the ACM on Programming Languages10.1145/32765092:OOPSLA(1-29)Online publication date: 24-Oct-2018
https://dl.acm.org/doi/10.1145/3276509
Vedurada JNandivada V(2018)Identifying refactoring opportunities for replacing type code with subclass and stateProceedings of the ACM on Programming Languages10.1145/32765082:OOPSLA(1-28)Online publication date: 24-Oct-2018
https://dl.acm.org/doi/10.1145/3276508
Raad AVafeiadis V(2018)Persistence semantics for weak memory: integrating epoch persistency with the TSO memory modelProceedings of the ACM on Programming Languages10.1145/32765072:OOPSLA(1-27)Online publication date: 24-Oct-2018
https://dl.acm.org/doi/10.1145/3276507
Ou PDemsky B(2018)Towards understanding the costs of avoiding out-of-thin-air resultsProceedings of the ACM on Programming Languages10.1145/32765062:OOPSLA(1-29)Online publication date: 24-Oct-2018
https://dl.acm.org/doi/10.1145/3276506
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