Hoare-Style Specifications as Correctness Conditions for Non-linearizable Concurrent Objects
Designing efficient concurrent objects often requires abandoning the standard specification technique of linearizability in favor of more relaxed correctness conditions. However, the variety of alternatives makes it difficult to choose which condition to employ, and how to compose them when using objects specified by different conditions.
In this work, we propose a uniform alternative in the form of Hoare logic, which can explicitly capture–in the auxiliary state–the interference of environment threads. We demonstrate the expressiveness of our method by verifying a number of concurrent objects and their clients, which have so far been specified only by non-standard conditions of concurrency-aware linearizability, quiescent, and quantitative quiescent consistency. We report on the implementation of the ideas in an existing Coq-based tool, providing the first mechanized proofs for all the examples in the paper.
Slides in PDF (2016-OOPSLA-Sergey-al.pdf) | 909KiB |
Wed 2 Nov Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
10:30 - 12:10 | Semantics and VerificationOOPSLA at Matterhorn 2 Chair(s): Jonathan AldrichCarnegie Mellon University | ||
10:30 25mTalk | Semantics-Based Program Verifiers for All Languages OOPSLA Andrei StefanescuUniversity of Illinois at Urbana-Champaign, Daejun ParkUniversity of Illinois at Urbana-Champaign, Shijiao YuwenUniversity of Illinois at Urbana-Champaign, Yilong LiRuntime Verification, Inc., Grigore RoşuUniversity of Illinois at Urbana-Champaign DOI Media Attached | ||
10:55 25mTalk | Hoare-Style Specifications as Correctness Conditions for Non-linearizable Concurrent Objects OOPSLA Ilya SergeyUniversity College London, Aleksandar NanevskiIMDEA Software Institute, Anindya BanerjeeIMDEA Software Institute, Germán Andrés DelbiancoIMDEA Software Institute DOI Pre-print Media Attached File Attached | ||
11:20 25mTalk | An Operational Semantics for C/C++11 Concurrency OOPSLA Kyndylan NienhuisUniversity of Cambridge, Kayvan MemarianUniversity of Cambridge, Peter SewellUniversity of Cambridge DOI | ||
11:45 25mTalk | Modeling and Analysis of Remote Memory Access Programming OOPSLA Andrei Marian DanETH Zurich, Patrick LamUniversity of Waterloo, Canada, Torsten HoeflerETH Zurich, Martin VechevETH Zurich DOI Pre-print Media Attached |