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
|10:30 - 10:55|
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 RosuUniversity of Illinois at Urbana-ChampaignDOI Media Attached
|10:55 - 11:20|
Ilya SergeyUniversity College London, Aleksandar NanevskiIMDEA Software Institute, Anindya BanerjeeIMDEA Software Institute, Germán Andrés DelbiancoIMDEA Software InstituteDOI Pre-print Media Attached File Attached
|11:20 - 11:45|
Kyndylan NienhuisUniversity of Cambridge, Kayvan MemarianUniversity of Cambridge, Peter SewellUniversity of CambridgeDOI
|11:45 - 12:10|
Andrei Marian DanETH Zurich, Patrick LamUniversity of Waterloo, Canada, Torsten HoeflerETH Zurich, Martin VechevETH ZurichDOI Pre-print Media Attached