Orchestrating the execution of parallel programs using Discrete Control Theory

Research Focus

The Gadara project is the first attempt at developing a formal Petri net model for failure avoidance in general-purpose concurrent software. The architecture adopted in the Gadara project comprises four stages. (1) Extract per-function Control Flow Graphs (CFGs) from program source code. We enhance the CFGs to facilitate deadlock analysis by including lock information of the program. (2) Translate the enhanced CFGs into a Petri net model of the program. The model is constructed in such a way that deadlocks in the original program correspond to structural features in the Petri net. (3) Synthesize control logic for deadlock avoidance. The output of this step is the original Petri net model augmented with additional features that guarantee deadlock avoidance in the original program. (4) Instrument the program to incorporate the control logic. This instrumentation ensures that the real program's runtime behavior conforms to that of the augmented model that was generated in the previous step, thus ensuring that the program cannot deadlock.

Some research problems that arise from the above process are discussed as follows.

One of the problems that the Gadara team is solving is the Lock/Unlock pairing problem. Many of the concurrency bug detection/avoidance tools rely on the static knowledge of critical sections. For accurate modeling of concurrent programs, Gadara also needs to know where locks are acquired and released. It is not a trivial task, however, to statically figure out critical sections for languages such as C or C++. Unlike Java in which critical sections are expressed as blocks syntactically, for C/C++, they are embraced by a pair of library calls, i.e., lock and unlock. Due to the potential exponential number of control path instantiations, it is difficult for static analysis to decide which "locks" would pair up with which "unlocks." Moreover, these pairs often span across function boundaries. The Gadara team is seeking an inter-procedural analysis algorithm to pair up Locks/Unlocks for all feasible paths.

Another research focus of the Gadara team is on the use of Petri nets to formally model, analyze, and control multithreaded programs. (1) Modeling. We define a new class of Petri nets, called Gadara nets, that systematically models multithreaded programs with lock allocation and release operations. Gadara nets provide the foundation of model-based analysis and control of multithreaded programs. (2) Analysis. We establish several crucial properties of Gadara nets that bridge a behavioral property of a program (deadlock) and a structural property of its Gadara net model (a feature technically known as a siphon). This correspondence enables our overall approach to work efficiently and handle large, real-world programs. (3) Control. We develop a novel methodology to synthesize control logic for Gadara nets to provably eliminate deadlocks while otherwise minimally constraining program behavior. The control logic is both correct and maximally permissive.

Please refer to our publications for our published results.