Write a Blog >>
SPLASH 2019
Sun 20 - Fri 25 October 2019 Athens, Greece
Wed 23 Oct 2019 16:22 - 16:45 at Attica - Formalization Chair(s): Eric Koskinen

Java’s memory model was recently updated and expanded with new access modes. The accompanying documentation for these access modes is intended to make strong guarantees about program behavior that the Java compiler must enforce, yet the documentation is frequently unclear. This makes the intended program behavior ambiguous, impedes discussion of key design decisions, and makes it impossible to prove general properties about the semantics of the access modes.

In this paper we present the first formalization of Java’s access modes. We have constructed an axiomatic model for all of the modes using the Herd modeling tool. This allows us to give precise answers to questions about the behavior of example programs, called litmus tests. We have validated our model using a large suite of litmus tests from existing research which helps to shed light on the relationship with other memory models. We have also modeled the semantics in Coq and proven several general theorems including a DRF guarantee, which says that if a program is properly synchronized then it will exhibit sequentially consistent behavior. Finally, we use our model to prove that the unusual design choice of a partial order among writes to the same location is unobservable in any program.

This program is tentative and subject to change.

Wed 23 Oct

splash-2019-oopsla
16:00 - 17:30: OOPSLA - Formalization at Attica
Chair(s): Eric KoskinenStevens Institute of Technology
splash-2019-oopsla16:00 - 16:22
Talk
Abhinav JangdaUniversity of Massachusetts Amherst, Donald PinckneyUniversity of Massachusetts Amherst, Yuriy BrunUniversity of Massachusetts Amherst, Arjun GuhaUniversity of Massachusetts, Amherst
Link to publication DOI Pre-print
splash-2019-oopsla16:22 - 16:45
Talk
John BenderUniversity of California, Los Angeles, Jens PalsbergUniversity of California, Los Angeles
splash-2019-oopsla16:45 - 17:07
Talk
Marianna RapoportUniversity of Waterloo, Ondřej LhotákUniversity of Waterloo
Pre-print
splash-2019-oopsla17:07 - 17:30
Talk
Pre-print