Abstract.
Verification of concurrent data structures is one of the most challenging tasks in software verification.
The topic has received considerable attention over the course of the last decade.
Nevertheless, human-driven techniques remain cumbersome and notoriously difficult while automated approaches suffer from limited applicability.
This is particularly true in the absence of garbage collection.
The intricacy of non-blocking manual memory management (manual memory reclamation) paired with the complexity of concurrent data structures has so far made automated verification prohibitive.
We tackle the challenge of automated verification of non-blocking data structures which manually manage their memory.
To that end, we contribute several insights that greatly simplify the verification task.
The guiding theme of those simplifications are semantic reductions.
We show that the verification of a data structure's complicated target semantics can be conducted in a simpler and smaller semantics which is more amenable to automatic techniques.
Some of our reductions rely on good conduct properties of the data structure.
The properties we use are derived from practice, for instance, by exploiting common programming patterns.
Furthermore, we also show how to automatically check for those properties under the smaller semantics.
The main contributions are:
(i)
A compositional verification approach that verifies the memory management and the data structure separately.
The approach crucially relies on a novel specification formalism for memory management implementations that over-approximates the reclamation behavior.
(ii)
A notion of weak ownership that applies when memory is reclaimed and reused.
Weak ownership bridges the gab between techniques for garbage collection, which can assume exclusive access to owned memory, and manual memory management, where dangling pointers break such exclusivity guarantees.
(iii)
A notion of pointer races and harmful ABAs the absence of which ensures that the memory management does not influence the operations of the data structure, i.e., it behaves as if executed under garbage collection.
Notably, we show that a check for pointer races and harmful ABAs only needs to consider executions where at most a single address is reused.
(iv)
A notion of strong pointer races the absence of which entails the absence of ordinary pointer races and harmful ABAs.
We devise a highly-efficient type check for strong pointer races.
This results in a light-weight analysis that first type checks a data structure and then performs the actual verification under garbage collection using an off-the-shelf verifier.
(v)
Experimental evaluations that substantiate the usefulness of the aforementioned contributions.
To the best of our knowledge, we are the first to fully automatically verify practical non-blocking data structures with manual memory management.
Examiners: Roland Meyer (TU Braunschweig), Rupak Majumdar (MPI-SWS Kaiserslautern), and Constantin Enea (IRIF Paris).
The thesis contains evaluations of the following tools: tmrexp and seal. There are two versions of tmrexp, one for free lists (FL) and one for epoch-based reclamation (EBR) Fraser04, McKenneyS98 and hazard pointers (HP) Michael02.
tmrexp for FL integrates the ownership reasoning technique from Chapter 6.
The tool appeared first in HazizaHMW16.
It is available here: branch1 and branch2.
The two branches differ in how version counter (age fields) are tracked in the memory abstraction.
tmrexp for EBR and HP integrates the reduction technique from Chapter 7.
The tool appeared first in MeyerW19.
It is available here: branchDS and branchSMR.
The two branches address verifying data structures and SMR implementations, respectively.
More details can be found here.
seal implements the technique from Chapter 8, that is, performs a type inference/check, discharges invariant annotations under GC, and verifies linearizability under GC. The tool first appeared in MeyerW20. As a GC back-end solver we use CAVE Vafeiadis09, Vafeiadis10a, Vafeiadis10b. Our tool is available here. More details can be found here.
Finally, there is a Python script that computes the simulation relation for the HP SMR automaton which supports the transfer of protections, cf. Figure A.5. The script is available here.