Thread Contracts for Race-Freedom

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