×

Modular safety checking for fine-grained concurrency. (English) Zbl 1211.68082

Nielson, Hanne Riis (ed.) et al., Static analysis. 14th international symposium, SAS 2007, Kongens Lyngby, Denmark, August 22–24, 2007. Proceedings. Berlin: Springer (ISBN 978-3-540-74060-5/pbk). Lecture Notes in Computer Science 4634, 233-248 (2007).
Summary: 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.
For the entire collection see [Zbl 1123.68008].

MSC:

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)

Software:

ESC/Java; Spec#; Zing
PDFBibTeX XMLCite
Full Text: DOI