english only
EPFL > I&C > Tresor > Seminars
Research Topics
Useful Links


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

Link to this comparison view

Both sides previous revision Previous revision
Next revision Both sides next revision
seminars:2009 [2009/11/16 14:48]
seminars:2009 [2009/11/26 13:56]
Line 834: Line 834:
 (Joint work with Jürgen Giesl, René Thiemann, Alexander Serebrenik, (Joint work with Jürgen Giesl, René Thiemann, Alexander Serebrenik,
 Stephan Swiderski, and Thomas Ströder) Stephan Swiderski, and Thomas Ströder)
 +===== Sequential Verification of Serializability =====
 +  * 2009-11-25 - 14:00 [[http://​www.cs.technion.ac.il/​~hagit/​|Hagit Attiya]]
 +Serializability is a commonly used correctness condition in concurrent
 +programming. When a concurrent module is serializable,​ certain
 +other properties of the module can be verified by considering
 +only its sequential executions. In many cases, concurrent modules
 +guarantee serializability by using standard locking protocols, such
 +as tree locking or two-phase locking. Unfortunately,​ according to
 +the existing literature, verifying that a concurrent module adheres
 +to these protocols requires considering concurrent interleavings.
 +In this paper, we show that adherence to a large class of locking
 +protocols (including tree locking and two-phase locking) can
 +be verified by considering only sequential executions. The main
 +consequence of our results is that in many cases, the (manual or
 +automatic) verification of serializability can itself be done using
 +sequential reasoning.
 +Joint work with G. Ramalingam and Noam Rinetzky, to appear in POPL 2010