Plan B: A Buffered Memory Model for Java

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.
Type de document :
Communication dans un congrès
Proc. of the 40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2013, Jan 2013, Rome, Italy. ACM, 2013
Liste complète des métadonnées

https://hal.inria.fr/hal-00924716
Contributeur : Delphine Demange <>
Soumis le : mardi 7 janvier 2014 - 10:22:08
Dernière modification le : mercredi 16 mai 2018 - 11:23:28

Identifiants

  • HAL Id : hal-00924716, version 1

Citation

Delphine Demange, Vincent Laporte, Lei Zhao, David Pichardie, Suresh Jagannathan, et al.. Plan B: A Buffered Memory Model for Java. Proc. of the 40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2013, Jan 2013, Rome, Italy. ACM, 2013. 〈hal-00924716〉

Partager

Métriques

Consultations de la notice

910