Thread contracts for safe parallelism

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

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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 race-free, 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 long-tested applu-l benchmark in the Spec OMP2001 suite.

Original languageEnglish (US)
Title of host publicationPPoPP'11 - Proceedings of the 2011 ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming
Pages125-134
Number of pages10
DOIs
StatePublished - Mar 25 2011
Event16th ACM Symposium on Principles and Practice of Parallel Programming, PPoPP'11 - San Antonio, TX, United States
Duration: Feb 12 2011Feb 16 2011

Publication series

NameProceedings of the ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPOPP

Other

Other16th ACM Symposium on Principles and Practice of Parallel Programming, PPoPP'11
Country/TerritoryUnited States
CitySan Antonio, TX
Period2/12/112/16/11

Keywords

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

ASJC Scopus subject areas

  • Software

Fingerprint

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

Cite this