Region and effect inference for safe parallelism

Alexandros Tzannes, Stephen T. Heumann, Lamyaa Eloussi, Mohsen Vakilian, Vikram Sadanand Adve, Michael Han

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

Abstract

In this paper, we present the first full regions-and-effects inference algorithm for explicitly parallel fork-join programs. We infer annotations inspired by Deterministic Parallel Java (DPJ) for a type-safe subset of C++. We chose the DPJ annotations because they give the strongest safety guarantees of any existing concurrency-checking approach we know of, static or dynamic, and it is also the most expressive static checking system we know of that gives strong safety guarantees. This expressiveness, however, makes manual annotation difficult and tedious, which motivates the need for automatic inference, but it also makes the inference problem very challenging: the code may use region polymorphism, imperative updates with complex aliasing, arbitrary recursion, hierarchical region specifications, and wildcard elements to describe potentially infinite sets of regions. We express the inference as a constraint satisfaction problem and develop, implement, and evaluate an algorithm for solving it. The region and effect annotations inferred by the algorithm constitute a checkable proof of safe parallelism, and it can be recorded both for documentation and for fast and modular safety checking.

Original languageEnglish (US)
Title of host publicationProceedings - 2015 30th IEEE/ACM International Conference on Automated Software Engineering, ASE 2015
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages512-523
Number of pages12
ISBN (Electronic)9781509000241
DOIs
StatePublished - Jan 4 2016
Event30th IEEE/ACM International Conference on Automated Software Engineering, ASE 2015 - Lincoln, United States
Duration: Nov 9 2015Nov 13 2015

Publication series

NameProceedings - 2015 30th IEEE/ACM International Conference on Automated Software Engineering, ASE 2015

Other

Other30th IEEE/ACM International Conference on Automated Software Engineering, ASE 2015
CountryUnited States
CityLincoln
Period11/9/1511/13/15

Keywords

  • Annotation Inference
  • Checkable Proof
  • Safe Parallelism
  • Static Analysis

ASJC Scopus subject areas

  • Software

Fingerprint Dive into the research topics of 'Region and effect inference for safe parallelism'. Together they form a unique fingerprint.

  • Cite this

    Tzannes, A., Heumann, S. T., Eloussi, L., Vakilian, M., Adve, V. S., & Han, M. (2016). Region and effect inference for safe parallelism. In Proceedings - 2015 30th IEEE/ACM International Conference on Automated Software Engineering, ASE 2015 (pp. 512-523). [7372039] (Proceedings - 2015 30th IEEE/ACM International Conference on Automated Software Engineering, ASE 2015). Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1109/ASE.2015.59