Speaker: Arjun Radhakrishna, University of Pennsylvania
Title: Performance-aware Repair for Concurrent Programs
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. These 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 the talk with a brief note on the general theme of soft specifications, such as performance and energy consumption, in program synthesis.
I am a post-doctoral researcher at the University of Pennsylvania working in the group of Prof. Rajeev Alur. Previously, I completed my PhD at IST Austria under the guidance of Prof. Thomas A. Henzinger. My research area relates to using programming languages and formal methods to help programmers and designers develop reliable, safe, and correct systems. In particular, I have been working heavily on program synthesis. However, I'm interested in all domains of formal methods and rigorous system engineering. My specific interests are in developing tools to handle soft and quantitative specifications in various domains such as concurrency and embedded systems. Soft specifications are program properties which are desirable but are not necessary for correctness (e.g., program performance and energy consumption).