Safe nondeterminism in a deterministic-by-default parallel language

Robert L. Bocchino, Stephen Heumann, Nima Honarmand, Sarita V. Adve, Vikram S. Adve, Adam Welc, Tatiana Shpeisman

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

Abstract

A number of deterministic parallel programming models with strong safety guarantees are emerging, but similar support for nondeterministic algorithms, such as branch and bound search, remains an open question. We present a language together with a type and effect system that supports nondeterministic computations with a deterministic-by-default guarantee: nondeterminism must be explicitly requested via special parallel constructs (marked nd), and any deterministic construct that does not execute any nd construct has deterministic input-output behavior. Moreover, deterministic parallel constructs are always equivalent to a sequential composition of their constituent tasks, even if they enclose, or are enclosed by, nd constructs. Finally, in the execution of nd constructs, interference may occur only between pairs of accesses guarded by atomic statements, so there are no data races, either between atomic statements and unguarded accesses (strong isolation) or between pairs of unguarded accesses (stronger than strong isolation alone). We enforce the guarantees at compile time with modular checking using novel extensions to a previously described effect system. Our effect system extensions also enable the compiler to remove unnecessary transactional synchronization. We provide a static semantics, dynamic semantics, and a complete proof of soundness for the language, both with and without the barrier removal feature. An experimental evaluation shows that our language can achieve good scalability for realistic parallel algorithms, and that the barrier removal techniques provide significant performance gains.

Original languageEnglish (US)
Title of host publicationPOPL'11 - Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
Pages535-548
Number of pages14
DOIs
StatePublished - 2010
Event38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'11 - Austin, TX, United States
Duration: Jan 26 2011Jan 28 2011

Publication series

NameConference Record of the Annual ACM Symposium on Principles of Programming Languages
ISSN (Print)0730-8566

Conference

Conference38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'11
Country/TerritoryUnited States
CityAustin, TX
Period1/26/111/28/11

Keywords

  • Languages
  • Performance
  • Verification

ASJC Scopus subject areas

  • Software

Fingerprint

Dive into the research topics of 'Safe nondeterminism in a deterministic-by-default parallel language'. Together they form a unique fingerprint.

Cite this