Partial-program synthesis is a technique that allows programmer to specify only part of the program imperatively and the rest of the requirements declaratively. In the domain of concurrency, the input usually consists of a non-deterministic partial program where the programmer omits synchronization constructs. The synthesizer fills in the appropriate synchronization to keep the program correct. However, a major hurdle to adoption of these techniques is the performance of the synthesized program. In this talk, I will present two different approaches we have explored for making synthesis for concurrent programs performance aware.
First, I will present an algorithmic method for the quantitative, performance-aware synthesis. In addition to the partial-program, the input consists of a non-deterministic partial program and of a parametric performance model. The performance model, specified as a weighted automaton, can capture system architectures by assigning different costs to actions such as locking, context switching, and memory and cache accesses. The quantitative synthesis problem is to automatically resolve the non-determinism of the partial program so that both correctness is guaranteed and performance is optimal. For worst-case (average-case) performance, we show that the problem can be reduced to 2-player graph games (with probabilistic transitions) with quantitative objectives.
Second, I will present an alternative approach which tries to avoid expensive synchronization constructs such as locks and atomic sections. The synthesis procedure explore a variety of (sequential) semantics-preserving program transformations for fixing concurrency bugs. Classically, only one such transformation has been considered, namely, the insertion of locks. Based on common manual bug-fixing techniques used by Linux device-driver developers, we explore additional, more efficient transformations, such as the reordering of independent instructions. We evaluated our techniques on several simplified examples of real concurrency bugs that occurred in Linux device drivers.
I completed my PhD at IST Austria under the guidance of Prof. Thomas A. Henzinger. Check out my dissertation here.
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 rigourous 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).