Safety Verification of Phaser Programs

TL;DR

This paper presents a static analysis method for verifying control state reachability in phaser programs, addressing the challenges posed by their dynamic synchronization features and infinite state spaces.

Contribution

We introduce an exact gap-order based procedure for control reachability and demonstrate how to adapt it for sound plain reachability analysis in phaser programs.

Findings

The procedure terminates for programs with bounded tasks and phasers.

Verifying plain reachability is undecidable even with few tasks and phasers.

Preliminary experiments show promise of the approach.

Abstract

We address the problem of statically checking control state reachability (as in possibility of assertion violations, race conditions or runtime errors) and plain reachability (as in deadlock-freedom) of phaser programs. Phasers are a modern non-trivial synchronization construct that supports dynamic parallelism with runtime registration and deregistration of spawned tasks. They allow for collective and point-to-point synchronizations. For instance, phasers can enforce barriers or producer-consumer synchronization schemes among all or subsets of the running tasks. Implementations %of these recent and dynamic synchronization are found in modern languages such as X10 or Habanero Java. Phasers essentially associate phases to individual tasks and use their runtime values to restrict possible concurrent executions. Unbounded phases may result in infinite transition systems even in the case of programs only creating finite numbers of tasks and phasers. We introduce an exact gap-order based procedure that always terminates when checking control reachability for programs generating bounded numbers of coexisting tasks and phasers. We also show verifying plain reachability is undecidable even for programs generating few tasks and phasers. We then explain how to turn our procedure into a sound analysis for checking plain reachability (including deadlock freedom). We report on preliminary experiments with our open source tool.