Performance-aware Synthesis for Concurrency

Usable concurrency synthesis has been a long-standing goal, with over three decades of active research going into it. Here, a programmer is expected to write a program that is correct in a sequential context, and the synthesizer inserts sufficient synchronization (locks) to make the program behave correctly in a concurrent setting. However, the issue of performance of the synthesized program has not been fully addressed. In this project, we attempt to address this issue by both optimizing the synchronization inserted by the synthesizer, and by avoiding synchronization completely by using more “programmer-like” techniques.