Thread Contracts for Race-Freedom

Karmani, Rajesh Kumar; Madhusudan, P.; Moore, Brandon

Permalink

https://hdl.handle.net/2142/15412 Copy

Description

Title

Thread Contracts for Race-Freedom

Author(s)

• Karmani, Rajesh Kumar
• Madhusudan, P.
• Moore, Brandon

Issue Date

2010-04-19

Keyword(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#).

Type of Resource

• text
• image

Language

en

Permalink

http://hdl.handle.net/2142/15412

Owning Collections