Technical Report: Region and Effect Inference for Safe Parallelism

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

Permalink

https://hdl.handle.net/2142/79048 Copy

Description

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.

Issue Date

2015-08-17

Keyword(s)

Annotation Inference, Safe Parallelism, Static Analysis

Date of Ingest

2015-08-18T05:48:18Z

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.

Publisher

IEEE

Series/Report Name or Number

ASE

Type of Resource

text

Genre of Resource

Technical Report

Language

en

Permalink

http://hdl.handle.net/2142/79048

Copyright and License Information

IEEE

Owning Collections