Abstract Interpretation Against Races

Issue title: Concurrency Specification and Programming (CS&P 2003)

Article type: Research Article

Authors: Barbuti, Roberto | Cataudella, Stefano | Tesei, Luca

Affiliations: Dipartimento di Informatica, Universitá di Pisa, Via F.Buonarroti, 2, 56127 Pisa, Italy

Abstract: In this paper we investigate the use of abstract interpretation techniques for statically preventing race conditions. To this purpose we enrich the concurrent object calculus concζ by annotating terms with the set of "locks" owned at any time. We use an abstract form of the object calculus to check the absence of race conditions. We show that abstract interpretation is more flexible than type analyses, and it allows to certify as "race free" a larger class of programs.

Keywords:

Journal: Fundamenta Informaticae, vol. 60, no. 1-4, pp. 67-79, 2004