Modular Safety Checking for Fine-Grained Concurrency

Cristiano Calcagno, Matthew J. Parkinson, and Viktor Vafeiadis


Concurrent programs are difficult to verify because the proof

must consider the interactions between the threads. Fine-grained concurrency

and heap allocated data structures exacerbate this problem,

because threads interfere more often and in richer ways. In this paper

we provide a thread-modular safety checker for a class of pointer-manipulating

fine-grained concurrent algorithms. Our checker uses ownership

to avoid interference whenever possible, and rely/guarantee (assume/

guarantee) to deal with interference when it genuinely exists.


Publication typeInproceedings
Published inSAS
PublisherSpringer Verlag
> Publications > Modular Safety Checking for Fine-Grained Concurrency