PhD Seminar Course on

Modeling, Analysis, and Control of Software Execution for Failure Avoidance Using Discrete-Event Control

Cagliari, May 11, 2011

This activity was made possible by the "Visiting Professors 2010" program of the University of Cagliari, sponsored by the Autonomous Region of Sardinia

Instructor: Stephane Lafortune
Dept. of Electrical Engineering and Computer Science,
University of Michigan, Ann Arbor (MI), US
Duration: 1.5 hours
Schedule: Wednesday May 11, 2011 - h: 11:00 am
Venue: Room B1 (DIEE, Stand B)
Topics: We present recent accomplishments in the Gadara project, a collaborative effort involving the University of Michigan, the Georgia Institute of Technology, and HP Laboratories (Palo Alto, USA). The overarching objective of this project is to control the execution of software to avoid potential failures using control techniques from the field of discrete-event systems. We have focused our efforts so far on the problem of deadlock avoidance in multithreaded C programs that use locking primitives to control access to shared data. We describe how we construct Petri net models of the locking behavior of concurrent programs, resulting in a special class of nets that we have termed Gadara nets. We establish a correspondence between deadlock-freeness of a program and liveness of its Gadara net model. Gadara nets enjoy structural properties that facilitate the synthesis of liveness-enforcing control policies that are maximally permissive. We describe these properties and our control synthesis methodology, which extends previous work on liveness-enforcing control of other classes of Petri nets. This methodology is applicable to other resource allocation systems that can be modeled as Gadara nets. We will conclude with general remarks about the theory and application of discrete-event control.
Organizer: Carla Seatzu
Dep. of Electrical and Electronic Engineering
University of Cagliari, Italy