research-article

Plan B: a buffered memory model for Java

Authors:

Delphine Demange,

Vincent Laporte,

Suresh Jagannathan,

David Pichardie,

Jan VitekAuthors Info & Claims

ACM SIGPLAN Notices, Volume 48, Issue 1

Pages 329 - 342

https://doi.org/10.1145/2480359.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

Moiseenko EPodkopaev AKoznov D(2021)A Survey of Programming Language Memory ModelsProgramming and Computer Software10.1134/S036176882106005047:6(439-456)Online publication date: 3-Dec-2021
https://doi.org/10.1134/S0361768821060050
Fava DSteffen MStolz V(2018)Operational Semantics of a Weak Memory Model with Channel SynchronizationFormal Methods10.1007/978-3-319-95582-7_15(258-276)Online publication date: 12-Jul-2018
https://doi.org/10.1007/978-3-319-95582-7_15
Zakowski YCachera DDemange DPetri GPichardie DJagannathan SVitek J(2017)Verifying a Concurrent Garbage Collector Using a Rely-Guarantee MethodologyInteractive Theorem Proving10.1007/978-3-319-66107-0_31(496-513)Online publication date: 2017
https://doi.org/10.1007/978-3-319-66107-0_31
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: Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

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

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

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

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

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]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 23 January 2013

Published in SIGPLAN Volume 48, Issue 1

Check for updates

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

32
Total Citations
View Citations
485
Total Downloads

Downloads (Last 12 months)5
Downloads (Last 6 weeks)1

Reflects downloads up to 16 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Moiseenko EPodkopaev AKoznov D(2021)A Survey of Programming Language Memory ModelsProgramming and Computer Software10.1134/S036176882106005047:6(439-456)Online publication date: 3-Dec-2021
https://doi.org/10.1134/S0361768821060050
Fava DSteffen MStolz V(2018)Operational Semantics of a Weak Memory Model with Channel SynchronizationFormal Methods10.1007/978-3-319-95582-7_15(258-276)Online publication date: 12-Jul-2018
https://doi.org/10.1007/978-3-319-95582-7_15
Zakowski YCachera DDemange DPetri GPichardie DJagannathan SVitek J(2017)Verifying a Concurrent Garbage Collector Using a Rely-Guarantee MethodologyInteractive Theorem Proving10.1007/978-3-319-66107-0_31(496-513)Online publication date: 2017
https://doi.org/10.1007/978-3-319-66107-0_31
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
Sivaramakrishnan KZiarek LJagannathan S(2014)[InlineEquation not availableProceedings of the 16th International Symposium on Practical Aspects of Declarative Languages - Volume 832410.1007/978-3-319-04132-2_1(1-16)Online publication date: 20-Jan-2014
https://dl.acm.org/doi/10.1007/978-3-319-04132-2_1
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
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.

Media

Figures

Other

Tables

View Issue’s Table of Contents