Arjun Radhakrishna is a post-doctoral researcher at the University
of Pennsylvania. Previously, he completed his PhD at the Institute
of Science and Technology, Austria advised by Prof. Thomas
A. Henzinger. His research focuses primarily on using programming
language techniques, specifically, automated program synthesis, for
rigorous systems engineering.  His current research interests include
the use of alternative specification mechanisms to capture subtle soft
requirements on computing systems, such as program performance, energy
consumption, or a program's robustness to errors. He is also interested
in verification and synthesis of concurrent programs, in particular,
device drivers.

AG 1, AG 2, AG 3, AG 4, AG 5, SWS, RG1, MMCI   Info

AG Audience

English

60 Minutes

Kaiserslautern

We present a recent line of work on automated synthesis of
synchronization constructs for concurrent programs. Our techniques are
inspired by a study of the most common types of concurrency bugs and
bugs-fixes in Linux device-drivers.  As opposed to classical techniques
which tend to use expensive synchronization constructs, our technique
attempts to use inexpensive program transformations, such as reordering
independent statements, to improve the performance of generated fixes.

Our techniques are based on the observation that a large fraction of
concurrency bugs are data-independent. This observations allow us to
characterize and fix concurrency bugs based only on the order of
execution of the statements involved. We evaluated our techniques on
several real concurrency bugs that occurred in Linux device drivers, and
showed that our synthesis procedure is able to produce more efficient
and "programmer-like" bug-fixes.

We finish by talk with a brief note on the general theme of soft
specifications, such as performance and energy consumption, in program
synthesis. Specifically, we will discuss the use of quantitative
specifications and their applications to resource management in embedded
and cyber-physical systems.

Roslyn Stricker

--email hidden

Yes

Saarbrücken

E1 5

029

passcode not visible

logged in users only