Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Wed 16 Jan 2019 11:41 - 12:03 at Sala II - Concurrency Chair(s): Ori Lahav

Effective software specifications enable modular reasoning, allowing clients to establish program properties without knowing the details of module implementations. While some modules’ operations behave atomically, others admit weaker consistencies to increase performance. Consequently, since current methodologies do not capture the guarantees provided by operations of varying non-atomic consistencies, specifications are ineffective, forfeiting the ability to establish properties of programs that invoke non-atomic operations.

In this work we develop a methodology for specifying software modules whose operations satisfy multiple distinct consistency levels. In particular, we develop a simple annotation language for specifying weakly-consistent operations via visibility relaxation, wherein annotations impose varying constraints on the visibility among operations. To integrate with modern software platforms, we identify a novel characterization of consistency called sequential happens-before consistency, which admits effective validation. Empirically, we demonstrate the efficacy of our approach by deriving and validating relaxed-visibility specifications for Java concurrent objects. Furthermore, we demonstrate an optimality of our annotation language, empirically, by establishing that even finer-grained languages do not capture stronger specifications for Java objects.

Wed 16 Jan

10:35 - 12:03: Research Papers - Concurrency at Sala II
Chair(s): Ori LahavTel Aviv University
POPL-2019-Research-Papers10:35 - 10:57
Nikos Gorogiannis, Peter W. O'HearnFacebook and University College London, Ilya SergeyYale-NUS College and National University of Singapore
Link to publication DOI Pre-print File Attached
POPL-2019-Research-Papers10:57 - 11:19
Link to publication DOI Pre-print File Attached
POPL-2019-Research-Papers11:19 - 11:41
Klaus v. GleissenthallUniversity of California at San Diego, USA, Rami Gökhan KıcıUniversity of California at San Diego, USA, Alexander Bakst, Deian StefanUniversity of California San Diego, Ranjit JhalaUniversity of California, San Diego
Link to publication DOI
POPL-2019-Research-Papers11:41 - 12:03
Michael EmmiSRI International, Constantin EneaUniversité Paris Diderot
Link to publication DOI File Attached