In the multicore era, concurrency bugs threaten to reduce programmer productivity, impair software safety, and erode end-user value. Control engineering can eliminate concurrency bugs by constraining software behavior, preventing runtime failures, and offloading onerous burdens from human programmers onto automatically synthesized control logic.
This project found inspiration and useful technology to address the challenges of parallel programming in a seemingly unlikely quarter: control engineering. Classical control theory makes it possible to safely and efficiently control complex and potentially dangerous systems such as oil refineries and aircraft avionics. This theory has enjoyed remarkable successes in industrial applications for more than a century, and today it is pervasive in consumer applications that improve our everyday lives. Conventional control theory is best suited to physical systems with continuous state spaces and coupled-differential-equation dynamics systems with little obvious resemblance to concurrent software. A lesser-known and more recent branch of control theory, however, deals with discrete state spaces and event-driven dynamics.
The team consists of control engineers and systems/software and compiler specialists whose goal is to bring to concurrent software the benefits that classical control brought to physical systems. The Gadara project is the intersection of concurrent software and control engineering. Gadara uses discrete control theory (DCT) to analyze concurrent software and automatically repair an important class of concurrency bugs: deadlocks involving standard synchronization primitives, including circular-mutex-wait deadlocks. Because Gadara rests on a rigorous theoretical foundation, it can decompose the practical goal of deadlock elimination into well-studied formal problems, leverage a large body of proven methods, and deliver hard safety/correctness and performance guarantees.
Gadara was generously supported by an Open Innovation Award from Hewlett-Packard and by the National Science Foundation under grant CCF-0819882 in the period 2008-2012.
The Michigan effort on Gadara has been subsumed into the broader effort on ExCAPE: Expeditions in Computer Aided Programming, funded by an NSF Expeditions grant.