Thread contracts for safe parallelism

Rajesh K. Karmani, P. Madhusudan, Brandon M. Moore

Research output: Contribution to journalArticle

Abstract

We build a framework of thread contracts, called ACCORD, that allows programmers to annotate their concurrency co-ordination strategies. ACCORD annotations allow programmers to declaratively specify the parts of memory that a thread may read or write into, and the locks that protect them, reflecting the concurrency co-ordination among threads and the reason why the program is free of data-races. We provide automatic tools to check if the concurrency co-ordination strategy ensures race-freedom, using constraint-solvers (SMT solvers). Hence programmers using ACCORD can both formally state and prove their co-ordination strategies ensure race freedom. The programmer's implementation of the co-ordination strategy may however be correct or incorrect. We show how the formal ACCORD contracts allow us to automatically insert runtime assertions that serve to check, during testing, whether the implementation conforms to the contract. Using a large class of data-parallel programs that share memory in intricate ways, we show that natural and simple contracts suffice to document the co-ordination strategy amongst threads, and that the task of showing that the strategy ensures race-freedom can be handled efficiently and automatically by an existing SMT solver (Z3). While co-ordination strategies can be proved race-free in our framework, failure to prove the co-ordination strategy racefree, accompanied by counter-examples produced by the solver, indicates the presence of races. Using such counterexamples, we report hitherto undiscovered data-races that we found in the longtested applu l benchmark in the Spec OMP2001 suite.

Original languageEnglish (US)
Pages (from-to)125-134
Number of pages10
JournalACM SIGPLAN Notices
Volume46
Issue number8
DOIs
StatePublished - Aug 1 2011

Keywords

  • Concurrent contracts
  • Constraint solvers
  • Data-races
  • Testing

ASJC Scopus subject areas

  • Computer Science(all)

Fingerprint Dive into the research topics of 'Thread contracts for safe parallelism'. Together they form a unique fingerprint.

  • Cite this