2016 24th Euromicro International Conference on Parallel, Distributed, and Network-Based Processing (PDP) (2016)
Heraklion, Crete, Greece
Feb. 17, 2016 to Feb. 19, 2016
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/PDP.2016.107
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.
Message systems, Synchronization, Silicon, Software, History, Concurrent computing, Java
A. Amighi, S. Blom and M. Huisman, "VerCors: A Layered Approach to Practical Verification of Concurrent Software," 2016 24th Euromicro International Conference on Parallel, Distributed, and Network-Based Processing (PDP), Heraklion, Crete, Greece, 2016, pp. 495-503.