Modular Safety Checking for Fine-Grained Concurrency

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 pointermanipulating 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.

• Type: Conference
• Year: 2007
• Where: SAS
• Authors: Cristiano Calcagno, Matthew J. Parkinson, Viktor Vafeiadis
• Keywords: Checker Uses Ownership, Concurrent Programs, Formal Methods, Heap Allocated Data, SAS 2007