Files in this item



application/pdfaccord.pdf (248kB)
(no description provided)PDF


Title:Thread Contracts for Race-Freedom
Author(s):Karmani, Rajesh Kumar; Madhusudan, P.; Moore, Brandon
Abstract:The goal of this paper is to build an annotation framework of thread contracts, called Accord to argue that a parallel program has no data-races, and build accompanying verification and testing tools. Accord annotations allow programmers to declaratively specify the fine-grained parts of memory that a thread may read or write into, and the locks that protect them, and hence can be used to establish race-freedom. We show that this can be achieved using automatic constraint-solvers based on SMT-solvers. We also show how to compile Accord thread contracts to runtime assertions that check the contracts dynamically during testing. Furthermore, we explore static verification of annotation correctness for parallel programs, using a new and surprising reduction to verifying assertions in sequential programs; the latter can be tackled using sequential contract-verification tools. Using a large class of data-parallel programs that share memory in intricate ways, we show that natural and simple contracts suffice to argue race-freedom, and that the task of showing that the annotations imply race-freedom and the task of showing the annotations are respected by the program, can be handled by existing SMT solvers (Z3) and sequential verification tools (Boogie, with specifications in Spec#).
Issue Date:2010-04-19
Genre:Technical Report
Publication Status:published or submitted for publication
Peer Reviewed:not peer reviewed
Date Available in IDEALS:2010-04-19

This item appears in the following Collection(s)

Item Statistics