Friday, January 10, 2014, 11:00am - 12:00pm
Professor, EECS, University of Michigan
"Eliminating Concurrency Bugs in Multithreaded Software: A New Approach Based on Discrete-Event Control"
Abstract: We describe the Gadara project, a research effort involving the University of Michigan, the Georgia Institute of Technology, and HP Laboratories, whose goal is to eliminate certain classes of concurrency bugs in concurrent software by controlling the execution of programs at runtime. The Gadara process involves four stages: modeling of the source code at compile time, offline analysis of its properties, feedback control synthesis, and control logic implementation into the source code. Concurrent programs are modeled as a special class of resource allocation Petri nets, called Gadara nets, that capture control flow and lock allocation and release operations. Deadlock-freeness of a concurrent program is captured in terms of liveness of its Gadara net model. We describe two optimal control synthesis methodologies for Gadara nets that have been developed in our project. Optimality in this context refers to the elimination of deadlocks in the program with minimally restrictive control logic. These methodologies exploit the structural properties of the nets via siphon analysis or via classification theory. We describe important properties of the proposed control synthesis methodologies and present experimental results that illustrate their scalability. Finally, we discuss the application of our results to real-world concurrent software. The presentation considers the case of circular-wait deadlocks in multithreaded programs employing mutual exclusion locks for shared data; the application of the Gadara methodology to other classes of concurrency bugs is briefly discussed.
This is collaborative work with the members of the Gadara team.
Bio: Prof. Stephane Lafortune received the B. Eng. degree from the École Polytechnique de Montréal in 1980, the M. Eng. degree from McGill University in 1982, and his Ph.D. degree from the University of California at Berkeley in 1986, all in electrical engineering. Since 1986, he has been with the Department of Electrical Engineering and Computer Science at the University of Michigan, Ann Arbor, where he is a Professor. He was elected Fellow of the IEEE in 1999 for "Contributions to the Theory of Discrete Event Systems". He serves on the editorial boards of the 'Journal of Discrete Event Dynamic Systems:Theory and Applications' and of the 'International Journal of Control.' He was twice the recipient of the Axelby Outstanding Paper Award from the IEEE Control Systems Society: in 1994 (for a paper co-authored with S.L. Chung and F. Lin) and in 2001 (for a paper co-authored with G. Barrett). He co-authored a book (with Christos G. Cassandras), titled "Introduction to Discrete Event Systems," the 2nd edition of which was published by Springer in 2008.
Hosted by: Prof. Dongning Guo
Friday, Jan 10, 2014 at 11:00am in Tech Room L324