Formalization of Conflict Analysis of Programs with Procedures, Thread Creation, and Monitors.
Peter Lammich, Markus Müller-Olm · 2007
Abstract. We study conflict detection for programs with procedures, dynamic thread creation and a fixed finite set of (reentrant) monitors. We show that deciding the existence of a conflict is NP-complete for our model (that abstracts guarded branching by nondeterministic choice) and present a fixpoint-based complete conflict detection algorithm. Our algorithm needs worst-case exponential time in the number of monitors, but is linear in the program size. 1