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 journalArticlepeer-review

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

Keywords

  • Annotation inference
  • Fork-join parallelism
  • Safe parallelism

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