Files in this item
Files | Description | Format |
---|---|---|
application/pdf ![]() | (no description provided) |
Description
Title: | Thread Contracts for Race-Freedom |
Author(s): | Karmani, Rajesh Kumar; Madhusudan, P.; Moore, Brandon |
Subject(s): | data-race
annotations thread contracts prove |
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 |
Type: | Text image |
Language: | English |
URI: | http://hdl.handle.net/2142/15412 |
Publication Status: | published or submitted for publication |
Peer Reviewed: | not peer reviewed |
Date Available in IDEALS: | 2010-04-19 |