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 - 10:57|
Nikos Gorogiannis, Peter W. O'HearnFacebook and University College London, Ilya SergeyYale-NUS College and National University of SingaporeLink to publication DOI Pre-print File Attached
|10:57 - 11:19|
|Link to publication DOI Pre-print File Attached|
|11: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 DiegoLink to publication DOI
|11:41 - 12:03|
|Link to publication DOI File Attached|