PL/SE Seminar - Simple and Efficient Concurrent Programming via Synchronization Synthesis
Abstract: Multithreaded concurrency is an extremely challenging programming setting, with bugs manifesting themselves in resource starvation and atomicity violations. While there have been efforts to simplify concurrent programming through higher-level programming abstractions, developers tend to choose low-level concurrent programming abstractions (with locks and condition variables as synchronization primitives) due to efficiency issues. This talk will present my recent work on bridging this efficiency vs. programmability trade-off in concurrent programming by employing lightweight formal methods in the compiler. Given a concurrent program implemented in a higher-level programming abstraction, our approach automatically synthesizes efficient and correct-by-construction code implemented in terms of standard synchronization primitives. Specifically, the first part of the talk will demonstrate how to synthesize all necessary signaling operations, and the second part will illustrate how to synthesize a fine-grained locking scheme that maximizes parallelism. As I will demonstrate through empirical results, this approach notably simplifies concurrent programming while achieving optimal performance.
Bio: Kostas Ferles is a postdoctoral fellow at the University of Texas at Austin where he is part of the UToPiA research group. His research areas are programming languages and formal methods, specializing in program analysis, verification, and synthesis. The goal of his research is to help developers produce correct, efficient, and secure software. Specifically, his research focuses on programming paradigms where proving correctness requires complex reasoning. He obtained his Ph.D. from the University of Texas at Austin and his B.Sc. and M.Sc. degrees from the University of Athens in Greece.
This seminar will be streaming via Zoom at the link above but requires a passcode. To obtain the passcode for this event, please see the announcements on the college email lists or contact us.