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: 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 - 10:55
Semantics-Based Program Verifiers for All LanguagesAECDistinguished Paper Award
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 - 11:20
Hoare-Style Specifications as Correctness Conditions for Non-linearizable Concurrent ObjectsAEC
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 - 11:45
An Operational Semantics for C/C++11 ConcurrencyAEC
Kyndylan NienhuisUniversity of Cambridge, Kayvan MemarianUniversity of Cambridge, Peter SewellUniversity of Cambridge
11:45 - 12:10
Modeling and Analysis of Remote Memory Access ProgrammingAECDistinguished Paper Award
Andrei Marian DanETH Zurich, Patrick LamUniversity of Waterloo, Canada, Torsten HoeflerETH Zurich, Martin VechevETH Zurich
DOI Pre-print Media Attached