DROPS

Document

Invited Paper

DOI: 10.4230/LIPIcs.CONCUR.2016.3

Consistency in 3D (Invited Paper)

Authors: Marc Shapiro, Masoud Saeida Ardekani, and Gustavo Petri

Published in: LIPIcs, Volume 59, 27th International Conference on Concurrency Theory (CONCUR 2016)

Abstract

Comparisons of different consistency models often try to place them in a linear strong-to-weak order. However this view is clearly inadequate, since it is well known, for instance, that Snapshot Isolation and Serialisability are incomparable. In the interest of a better understanding, we propose a new classification, along three dimensions, related to: a total order of writes, a causal order of reads, and transactional composition of multiple operations. A model may be stronger than another on one dimension and weaker on another. We believe that this new classification scheme is both scientifically sound and has good explicative value. The current paper presents the three-dimensional design space intuitively.

Cite as

Marc Shapiro, Masoud Saeida Ardekani, and Gustavo Petri. Consistency in 3D (Invited Paper). In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 3:1-3:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{shapiro_et_al:LIPIcs.CONCUR.2016.3,
  author =	{Shapiro, Marc and Ardekani, Masoud Saeida and Petri, Gustavo},
  title =	{{Consistency in 3D}},
  booktitle =	{27th International Conference on Concurrency Theory (CONCUR 2016)},
  pages =	{3:1--3:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-017-0},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{59},
  editor =	{Desharnais, Jos\'{e}e and Jagadeesan, Radha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.3},
  URN =		{urn:nbn:de:0030-drops-61889},
  doi =		{10.4230/LIPIcs.CONCUR.2016.3},
  annote =	{Keywords: Consistency models, replicated data, structural invariants, correctness of distributed systems}
}

Document

DOI: 10.4230/LIPIcs.ECOOP.2015.445

Cooking the Books: Formalizing JMM Implementation Recipes

Authors: Gustavo Petri, Jan Vitek, and Suresh Jagannathan

Published in: LIPIcs, Volume 37, 29th European Conference on Object-Oriented Programming (ECOOP 2015)

Abstract

The Java Memory Model (JMM) is intended to characterize the meaning of concurrent Java programs. Because of the model's complexity, however, its definition cannot be easily transplanted within an optimizing Java compiler, even though an important rationale for its design was to ensure Java compiler optimizations are not unduly hampered because of the language's concurrency features. In response, Lea's JSR-133 Cookbook for Compiler Writers, an informal guide to realizing the principles underlying the JMM on different (relaxed-memory) platforms was developed. The goal of the cookbook is to give compiler writers a relatively simple, yet reasonably efficient, set of reordering-based recipes that satisfy JMM constraints. In this paper, we present the first formalization of the cookbook, providing a semantic basis upon which the relationship between the recipes defined by the cookbook and the guarantees enforced by the JMM can be rigorously established. Notably, one artifact of our investigation is that the rules defined by the cookbook for compiling Java onto Power are inconsistent with the requirements of the JMM, a surprising result, and one which justifies our belief in the need for formally provable definitions to reason about sophisticated (and racy) concurrency patterns in Java, and their implementation on modern-day relaxed-memory hardware. Our formalization enables simulation arguments between an architecture-independent intermediate representation of the kind suggested by Lea with machine abstractions for Power and x86. Moreover, we provide fixes for cookbook recipes that are inconsistent with the behaviors admitted by the target platform, and prove the correctness of these repairs.

Cite as

Gustavo Petri, Jan Vitek, and Suresh Jagannathan. Cooking the Books: Formalizing JMM Implementation Recipes. In 29th European Conference on Object-Oriented Programming (ECOOP 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 37, pp. 445-469, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{petri_et_al:LIPIcs.ECOOP.2015.445,
  author =	{Petri, Gustavo and Vitek, Jan and Jagannathan, Suresh},
  title =	{{Cooking the Books: Formalizing JMM Implementation Recipes}},
  booktitle =	{29th European Conference on Object-Oriented Programming (ECOOP 2015)},
  pages =	{445--469},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-86-6},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{37},
  editor =	{Boyland, John Tang},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2015.445},
  URN =		{urn:nbn:de:0030-drops-52334},
  doi =		{10.4230/LIPIcs.ECOOP.2015.445},
  annote =	{Keywords: Concurrency, Java, Memory Model, Relaxed-Memory}
}

Search Results

Documents authored by Petri, Gustavo

Consistency in 3D (Invited Paper)

Abstract

Cite as

Cooking the Books: Formalizing JMM Implementation Recipes

Abstract

Cite as

Thanks for your feedback!

Could not send message