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.

Wed 23 Oct

Displayed time zone: Beirut change

16:00 - 17:30
FormalizationOOPSLA at Attica
Chair(s): Eric Koskinen Stevens Institute of Technology
16:00
22m
Talk
Formal Foundations of Serverless ComputingACM SIGPLAN Distinguished Paper Award
OOPSLA
Abhinav Jangda University of Massachusetts Amherst, Donald Pinckney University of Massachusetts Amherst, Yuriy Brun University of Massachusetts Amherst, Arjun Guha University of Massachusetts, Amherst
Link to publication DOI Pre-print
16:22
22m
Talk
A Formalization of Java’s Concurrent Access Modes
OOPSLA
John Bender University of California, Los Angeles, Jens Palsberg University of California, Los Angeles
DOI
16:45
22m
Talk
A Path to DOT: Formalizing Fully Path-Dependent Types
OOPSLA
Marianna Rapoport University of Waterloo, Ondřej Lhoták University of Waterloo
DOI Pre-print Media Attached
17:07
22m
Talk
Qubit Allocation as a Combination of Subgraph Isomorphism and Token Swapping
OOPSLA
DOI Pre-print