Tree-Regular Analysis of Parallel Programs with Dynamic Thread Creation and Locks
Nordhoff Benedikt
Abstract in digital collection (conference) | Peer reviewedAbstract
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.
Details about the publication
Status: Published
Release year: 2012 (03/12/2012)
Language in which the publication is written: English
Conference: School for young researchers about Modelling and Verifying Parallel processes, Marseille, Frankreich
Authors from the University of Münster
| Nordhoff, Benedikt | Professorship for practical computer science (Prof. Müller-Olm) |
Projects the publication originates from
SPP 1496 – WP: Information Flow Control for Mobile Components Based on Precise Analysis for Parallel Programs (2nd funding period) (IFC for Mobile Components) Duration: 01/10/2012 - 30/09/2015 | 2nd Funding period Funded by: DFG - Priority Programme Type of project: Subproject in DFG-joint project hosted outside University of Münster |