Files in this item



application/pdf2015-ASE-Inference-TR.pdf (198kB)
Technical ReportPDF


Title:Technical Report: Region and Effect Inference for Safe Parallelism
Author(s):Tzannes, Alexandros; Han, Michael; Adve, Vikram S.; Vakilian, Mohsen; Eloussi, Lamyaa; Heumann, Stephen T.
Subject(s):Annotation Inference, Safe Parallelism, Static Analysis
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 \emph{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.
Issue Date:2015-08-17
Citation Info:Alexandros Tzannes, Stephen T. Heumann, Lamyaa Eloussi, Mohsen Vakilian, Vikram S. Adve, and Michael Han, "Region and Effect Inference for Safe Parallelism", in Proceedings of the 30th International Conference on Automated Software Engineering (ASE), 2015.
Genre:Technical Report
Rights Information:IEEE
Date Available in IDEALS:2015-08-18

This item appears in the following Collection(s)

Item Statistics