About the Event
Computer and software engineering is a rich application area for
control systems technology.
Many important problems in computer and software engineering are
discrete in nature and naturally
fall into the realm of discrete-variable and event-driven systems,
i.e., Discrete Event Systems (DES).
In the last few years, several applications of DES to computer systems
problems have emerged.
In particular, the paradigm of controlling software execution to avoid
software defects at runtime
has received significant attention.
In this talk, we present a control engineering approach to the
elimination of certain
classes of concurrency bugs in concurrent software. A model
of the source code is extracted at compile time and represented in the
form of a Petri net, a widely-used discrete-event modeling formalism.
DES techniques are then employed to analyze the behavior of the concurrent
program. The property of deadlock-freedom of the program is mapped to
that of liveness of its Petri net model, called a Gadara net. A new
methodology for Iterative Control of Gadara nets is
developed for synthesizing control logic that is liveness-enforcing
and maximally-permissive. The synthesized control logic is then
implemented by program instrumentation. At run-time, the control logic
will provably enforce deadlock-freedom of the program without altering
its control flow.
The results presented pertain to the case of circular-wait deadlocks in
multithreaded programs employing mutual exclusion locks for shared
data. However, the methodology can be applied to tackle other classes
of concurrency bugs.
This is collaborative work with the members of the Gadara team: