Modeling, Analysis, and Control of a Class of Resource Allocation Systems Arising in Concurrent Software

In the past decade, computer hardware has undergone a true revolution, moving from uniprocessor architectures to multiprocessor architectures, or multicore. In order to exploit the full potential of multicore hardware, there is an unprecedented interest in parallelizing the applications that were previously conducted in series. This trend forces parallel programming upon the average programmer. However, reasoning about concurrency is challenging for human programmers. Significant effort has been spent to eliminate several types of concurrency bugs.
In this dissertation, we study the modeling, analysis, control, and evaluation of a class of resource allocation systems arising in concurrent software using Petri nets, a commonly used modeling formalism in Discrete Event Systems. We formally define a new class of Petri nets, called Gadara nets, to systematically model multithreaded programs with lock allocation and release operations, a widely used programming paradigm for concurrent software with shared data. We focus on an important class of concurrency bugs, known as circular-mutex-wait deadlocks, or simply deadlocks. Deadlock-freeness of a program corresponds to liveness of its Gadara net model. We establish necessary and sufficient conditions for liveness and reversibility properties of Gadara nets, which lay the foundations for their control synthesis. We propose a new liveness-enforcing control synthesis methodology for general Gadara nets that need not be ordinary. The method is based on structural analysis and converges in finite iterations. It is shown to be correct and maximally permissive with respect to the goal of liveness enforcement. We further customize this control synthesis methodology for ordinary Gadara nets, and establish a set of important properties. Performance evaluations are conducted for comparing the original and controlled program models, using Discrete Event Simulation. Our results are applied to the analysis of large-scale, randomly generated programs, showing that our approach is scalable to real-world software. Finally, we discuss potential directions for future work.