Waterloo Programming Languages Seminars

Previous terms: S10 F08 S08 W08 F07 W07 F06 S06 W06

Current term:

Date	Speaker	Title (click for abstract)	Location
Thu. Nov. 25, 2010 at 1:00	Martin Vechev	Techniques for Building Correct and Efficient Concurrent Systems	DC 1331

All are welcome.

Talk announcements are also posted to a public mailing list.

To volunteer to give a talk, contact Ondřej Lhoták. Talks can range from informal to formal, and they can be about any of the following:

completed research
research that you plan to start ("half-baked ideas" to be critiqued by your peers)
interesting paper(s) you have read

The purpose is for us all to see what people are interested in, and motivate discussions.

Abstracts

Techniques for Building Correct and Efficient Concurrent Systems

Martin Vechev
Nov. 25, 2010
Virtually all chips today are built with an increasing number of processor cores. To effectively exploit these changes in technology, all future software will have to be concurrent. This poses a tremendous challenge as building correct and efficient concurrent software is known to be a very challenging problem. A fundamental reason for this difficulty is that programmers are forced to manually discover how to synchronize interfering threads correctly and efficiently, a task that has turned out to be quite elusive, even for expert programmers.

In this talk, I will survey some of the techniques we have developed for automatically synthesizing correct and efficient synchronization. I will then focus on a new approach that combines classic abstract interpretation and synchronization inference. The essence of this technique lays in its bidirectional nature: to produce a correct concurrent program, at any step, an automatic verifier can now manipulate both: i) the program by introducing synchronization, or ii) the abstraction by refining it or coarsening it.

Finally, I will present a new result which states that it is impossible to build correct concurrent implementations of virtually all known abstract data types such as stacks, sets, queues, hash tables, and others, without using certain very expensive synchronization. This result has implications on hardware architectures, concurrent algorithm design, and synchronization inference.

Martin Vechev is a researcher at the IBM T.J. Watson Center in New York. He obtained his PhD in 2007 from Cambridge University. His interests are in concurrency, analysis, and verification.