BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Atomicity Abstractions in Relaxed Memory Architectures - Brijesh D
 ongol\, Brunel University London
DTSTART:20180126T140000Z
DTEND:20180126T150000Z
UID:TALK95164@talks.cam.ac.uk
CONTACT:Victor Gomes
DESCRIPTION:Atomicity abstractions\, which include concurrent objects and 
 transactional memory\, are well studied for sequentially consistent archit
 ectures. Here\, correctness of an implementation is defined by conditions 
 such as linearizability (concurrent objects)\, opacity (transactional memo
 ry) etc. These notions of correctness however\, assume a single global clo
 ck (i.e.\, a total order over memory events)\, which is not available in a
  relaxed memory architecture. This talk presents two recent efforts to red
 efine linearizability\, opacity and their variations in a relaxed memory s
 etting. We build on the "herding cats" framework of Alglave et al\, and he
 nce\, our methods apply to several memory models including SC\, TSO\, ARMv
 8 and PPC. For concurrent objects\, we show that abstract specifications m
 ust be strengthened with additional happens-before information. For transa
 ctional memory\, we provide flexible and expressive forms of transaction a
 borts and execution that have hitherto been in the realm of software trans
 actional memory. We also prove abstraction theorems to demonstrate that th
 e programmer API matches the intuitions and expectations about the objects
  in question.
LOCATION:FW26
END:VEVENT
END:VCALENDAR