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

Nordhoff Benedikt

Zusammenfassung

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.

Projekte, aus denen die Publikation entstanden ist