english only
EPFL > I&C > Tresor > Seminars
RESOURCES
Home
People
Seminars
Courses
Research Topics
Events
Useful Links

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
Last revision Both sides next revision
seminars:2009 [2009/11/26 13:56]
losa
seminars:2009 [2010/01/04 17:09]
psuter
Line 857: Line 857:
  
 Joint work with G. Ramalingam and Noam Rinetzky, to appear in POPL 2010 Joint work with G. Ramalingam and Noam Rinetzky, to appear in POPL 2010
 +
 +
 +===== Automatic Inference of Synchronization =====
 +
 +  * 2009-12-15 - 14:30, BC 410 [[http://​domino.research.ibm.com/​comm/​research_people.nsf/​pages/​mtvechev.index.html|Martin Vechev]]
 +([[http://​ditwww.epfl.ch/​cgi-bin/​EPFLTV/​home.pl?​page=video&​lang=2&​connected=0&​id=664&​plugin=9&​plugin=1&​checkplugin=1|Watch the video ]])
 +
 +Abstract:
 +
 +Current practices for developing correct and efficient concurrent
 +programs are rather limited and error-prone.
 +In practice, manual ad-hoc use of low-level synchronization often leads
 +to programs that are inefficient
 +or incorrect (or both). High-level constructs (e.g. transactional
 +memory) are not clearly easier to use.
 +
 +In this talk I will briefly discuss techniques for automatically
 +inferring correct and efficient synchronization:​
 +atomic sections, scheduler control, guards in Hoare'​s CCRs, and memory
 +fences in weak memory models.
 +We have implemented these techniques and used them to: create new
 +practical linearizable concurrent data structures,
 +new memory management algorithms, find and automatically correct errors
 +in concurrent programs due to weak memory models.
 +
 +I will then discuss abstraction-guided synthesis of synchronization (an
 +upcoming POPL'​10 paper).
 +In this work we combine abstraction interpretation with synchronization
 +inference. We add the symmetrical choice
 +to traditional abstraction refinement: at any step during abstract
 +interpretation,​ we can refine the abstraction or
 +change the program by adding more synchronization. This means for
 +example that even if the original
 +program is incorrect or unprovable under the abstraction,​ we may be able
 +to add synchronization to make it provable.
 +
 +Throughout the talk, I will also mention various insights obtained in
 +this work that pertain to concurrency verification,​ synthesis
 +and program representation in general.
 +
 +(Joint work with Eran Yahav and Greta Yorsh)
 +
 +**Short biography:​** [[http://​domino.research.ibm.com/​comm/​research_people.nsf/​pages/​mtvechev.index.html|Dr. Martin Vechev]] is a researcher at the IBM Watson Center in New York.
 +He obtained his PhD in 2007 from Cambridge University. His interests are in
 +concurrency,​ synthesis, verification and dynamic program analysis.