Sergey, I;
Nanevski, A;
Banerjee, A;
Andres Delbianco, G;
(2016)
Hoare-Style Specifications as Correctness Conditions for Non-linearizable Concurrent Objects.
In:
Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications.
(pp. pp. 92-110).
ACM
Preview |
Text
Sergey_non-linearizable-oopsla16.pdf - Accepted Version Download (622kB) | Preview |
Abstract
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.
| Type: | Proceedings paper |
|---|---|
| Title: | Hoare-Style Specifications as Correctness Conditions for Non-linearizable Concurrent Objects |
| Event: | ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA) |
| Location: | Amsterdam, NETHERLANDS |
| Dates: | 02 November 2016 - 04 November 2016 |
| ISBN-13: | 978-1-4503-4444-9 |
| Open access status: | An open access version is available from UCL Discovery |
| DOI: | 10.1145/2983990.2983999 |
| Publisher version: | https://doi.org/10.1145/3022671.2983999 |
| Language: | English |
| Additional information: | This version is the author accepted manuscript. For information on re-use, please refer to the publisher’s terms and conditions. |
| Keywords: | Science & Technology, Technology, Computer Science, Software Engineering, Computer Science, Concurrency, Hoare logic, linearizability, quiescent consistency, counting networks, mechanized proofs, Theory, Verification |
| UCL classification: | UCL UCL > Provost and Vice Provost Offices > UCL BEAMS UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science |
| URI: | https://discovery.ucl.ac.uk/id/eprint/1531761 |
Loading...
Loading...Loading...Loading...Archive Staff Only
 |
View Item |
