Abstract
This paper discusses how several concurrent program verification techniques can be combined in a layered approach, where each layer is especially suited to verify one aspect of concurrent programs, thus making verification of concurrent programs practical. At the bottom layer, we use a combination of implicit dynamic frames and CSL-style resource invariants, to reason about data race freedom of programs. We illustrate this on the verification of a lock-free queue implementation. On top of this, layer 2 enables reasoning about resource invariants that express a relationship between thread-local and shared variables. This is illustrated by the verification of a reentrant lock implementation, where thread-locality is used to specify for a thread which locks it holds, while there is a global notion of ownership, expressing for a lock by which thread it is held. Finally, the top layer adds a notion of histories to reason about functional properties. We illustrate how this is used to prove that the lock-free queue preserves the order of elements, without having to reverify the aspects related to data race freedom.
Original language | Undefined |
---|---|
Title of host publication | Proceedings of the 24th Euromicro International Conference on Parallel, Distributed, and Network-Based Processing (PDP 2016) |
Place of Publication | USA |
Publisher | IEEE |
Pages | 495-503 |
Number of pages | 9 |
ISBN (Print) | 978-1-4673-8775-0 |
DOIs | |
Publication status | Published - Feb 2016 |
Event | 24th Euromicro International Conference on Parallel, Distributed, and Network-Based Processing, PDP 2016 - Heraklion, Crete, Greece Duration: 17 Feb 2016 → 19 Feb 2016 Conference number: 24 |
Publication series
Name | |
---|---|
Publisher | IEEE Computer Society |
ISSN (Print) | 2377-5750 |
Conference
Conference | 24th Euromicro International Conference on Parallel, Distributed, and Network-Based Processing, PDP 2016 |
---|---|
Abbreviated title | PDP |
Country/Territory | Greece |
City | Heraklion, Crete, |
Period | 17/02/16 → 19/02/16 |
Keywords
- EWI-27395
- Program Verification
- METIS-320885
- IR-102859
- Separation Logic