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.
Conference DayWed 16 JanDisplayed time zone: Belfast change
10:35 - 12:03
|A True Positives Theorem for a Static Race Detector|
Nikos Gorogiannis, Peter W. O'HearnFacebook and University College London, Ilya SergeyYale-NUS College and National University of SingaporeLink to publication DOI Pre-print Media Attached File Attached
|Decoupling Lock-Free Data Structures from Memory Reclamation for Static Analysis|
Research PapersLink to publication DOI Pre-print Media Attached File Attached
|Pretend Synchrony: Synchronous Verification of Asynchronous Distributed Programs|
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 DiegoLink to publication DOI Media Attached
|Weak-Consistency Specification via Visibility Relaxation|
Research PapersLink to publication DOI Media Attached File Attached