Name
Abstract | ||
|---|---|---|
Software Transactional Memory (STM) algorithms provide programmers with a high-level synchronization technique for concurrent programming. STMs guarantee "seemingly atomic" access to shared state via transactions. This seeming atomicity is the standard requirement on STM implementations and formalized in the concept of opacity. The standard proof technique for opacity is via refinement: the STM implementation is shown to refine an IO automaton called TMS2 which itself is known to be opaque. This paper presents a case study of proving opacity via TMS2 refinement. Our case study concerns the FASTLANE implementation of STM which is specifically designed to achieve good performance on varying contention: it supports different modes for low and high thread counts plus provides a switching scheme between modes. This basic concept provides new challenges for verification: besides having to prove opacity of every mode itself, we also need to show that switching does not invalidate opacity. For both parts, we present fully mechanized proofs of opacity carried out in the interactive theorem prover KIV. |
Year | DOI | Venue |
|---|---|---|
2018 | 10.1007/978-3-319-92970-5_7 | Lecture Notes in Computer Science |
Field | DocType | Volume |
Atomicity,Software transactional memory,Synchronization,Programming language,Computer science,Automaton,Implementation,Real-time computing,Opacity,Mathematical proof,Concurrent computing | Conference | 10886 |
ISSN | Citations | PageRank |
0302-9743 | 0 | 0.34 |
References | Authors | |
14 | 5 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Gerhard Schellhorn | 1 | 769 | 56.43 |
| Monika Wedel | 2 | 0 | 0.34 |
| Oleg Travkin | 3 | 52 | 5.66 |
| Jürgen König | 4 | 0 | 0.68 |
| Heike Wehrheim | 5 | 1013 | 104.85 |