Blogs (9) >>
SPLASH 2016
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

Conference Day
Wed 2 Nov

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