BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Verifying Concurrent Programs with Relaxed Conflict Detection - Se
 rdar Tasiran\, Koç University
DTSTART:20120817T090000Z
DTEND:20120817T100000Z
UID:TALK39318@talks.cam.ac.uk
CONTACT:Microsoft Research Cambridge Talks Admins
DESCRIPTION:In a frequently-encountered pattern in concurrent programs\, a
 n operation first reads a large portion of shared data\, then performs loc
 al computation\, and finally writes to a small portion of shared data. Thi
 s pattern leads to frequent conflicts between operations intended to appea
 r atomic. To provide good performance alongside atomicity\, implementation
 s ranging from fine-grain locking to variations on transactional memory (T
 M) have been investigated.  \n\nWe present an approach for statically veri
 fying TM-based solutions with programmer-directed conflict detection. We s
 how how static correctness proofs of such programs can be streamlined. The
  key challenge is that one can no longer reason sequentially within transa
 ctions. To address this challenge\, we provide an abstraction recipe that 
 restores the ability to reason sequentially. We demonstrate our approach b
 y mechanically verifying examples from the STAMP benchmark suite.\n
LOCATION:Small lecture theatre\, Microsoft Research Ltd\, 7 J J Thomson Av
 enue (Off Madingley Road)\, Cambridge
END:VEVENT
END:VCALENDAR