Tree-Regular Analysis of Parallel Programs with Dynamic Thread Creation and Locks

Nordhoff Benedikt

Abstract

We utilize Monitor-DPN to precisely model concurrent programs with unbounded recursion, dynamic thread creation and synchronization via well-nested locks based on finite abstractions of procedure- and thread-local state. One obtains a tree-regular characterization of reachable configurations by using acquisition structures to check for lock-sensitive schedulability. This technique can then be iterated using additional release structures. This then allows to solve for instance bit-vector problems. The techniques have been implemented for the analysis of Java programs and applied for data race detection and improvement of an information flow control analysis.