Region and effect inference for safe parallelism

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

Research output: Contribution to journalArticle

Abstract

In this paper, we present the first full regions-and-effects inference algorithm for explicitly parallel fork-join programs. We infer annotations equivalent to those in Deterministic Parallel Java (DPJ) for type-safe C++ programs. 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)
Pages (from-to)463-509
Number of pages47
JournalAutomated Software Engineering
Volume26
Issue number2
DOIs
StatePublished - Jun 15 2019

    Fingerprint

Keywords

  • Annotation inference
  • Fork-join parallelism
  • Safe parallelism

ASJC Scopus subject areas

  • Software

Cite this

Tzannes, A., Heumann, S. T., Eloussi, L., Vakilian, M., Adve, V. S., & Han, M. (2019). Region and effect inference for safe parallelism. Automated Software Engineering, 26(2), 463-509. https://doi.org/10.1007/s10515-019-00257-3