The Taub Faculty of Computer Science Events and Talks

In this talk I will present a framework for synthesizing efficient synchronization in concurrent programs, a task known to be difficult and error-prone when done manually. The framework is based on abstract interpretation and can infer synchronization for infinite state programs. Given a program, a specification, and an abstraction, we infer synchronization that avoids all (abstract) interleavings that may violate the specification, but permits as many valid interleavings as possible. I will show application of this general idea for automatic inference of atomic sections and memory fences in programs running over relaxed memory models.

Joint work with Michael Kuperstein, Martin Vechev, and Greta Yorsh.