Blogs (9) >>
Sun 30 October - Fri 4 November 2016 Amsterdam, Netherlands
Wed 2 Nov 2016 10:55 - 11:20 at Matterhorn 2 - Semantics and Verification Chair(s): Jonathan Aldrich

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: (GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

10:30 - 12:10: OOPSLA - Semantics and Verification at Matterhorn 2
Chair(s): Jonathan AldrichCarnegie Mellon University
splash-2016-oopsla10: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-Champaign
DOI Media Attached
splash-2016-oopsla10:55 - 11:20
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
splash-2016-oopsla11:20 - 11:45
Kyndylan NienhuisUniversity of Cambridge, Kayvan MemarianUniversity of Cambridge, Peter SewellUniversity of Cambridge
splash-2016-oopsla11:45 - 12:10
Andrei Marian DanETH Zurich, Patrick LamUniversity of Waterloo, Canada, Torsten HoeflerETH Zurich, Martin VechevETH Zurich
DOI Pre-print Media Attached