BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Types and Safety of Lock-free Data Structures - Elias Castegren\, 
 MSR
DTSTART:20180629T130000Z
DTEND:20180629T140000Z
UID:TALK106363@talks.cam.ac.uk
CONTACT:Victor Gomes
DESCRIPTION:The increasing importance of parallel and concurrent programmi
 ng has rejuvenated interest in systems that statically control the use of 
 shared mutable state in order to guarantee properties such as data-race fr
 eedom. This control is commonly achieved by banning concurrent access to m
 utable state altogether\, either through isolation (e.g.\, ownership types
 )\, synchronisation (e.g.\, by enforcing correct usage of locks)\, immutab
 ility (e.g.\, read-only references)\, or uniqueness (e.g.\, linear referen
 ces).\n \nBanning shared mutable state simplifies reasoning about concurre
 nt programs -- for programmers as well as for optimizing compilers – but
  it is too strong a restriction for many applications. Notably\, lock-free
  algorithms\, which implement protocols that ensure safe\, non-blocking co
 ncurrent access to data structures\, generally rely on shared mutable stat
 e to achieve lock-freedom.\n \nThis presentation details the work on LOLCA
 T\, a type system that allows an unbounded number of aliases to a shared m
 utable resource\, as long as at most one alias at a time owns the right to
  access the contents of the resource. This ownership can be transferred be
 tween aliases\, but can never be duplicated. LOLCAT types are flexible eno
 ugh to type several lock-free data structures\, but also powerful enough t
 o give a compile-time guarantee of absence of data-races when accessing ow
 ned data. In particular\, LOLCAT is able to assign meaningful types to the
  CAS (compare and swap) primitive that precisely describe how ownership is
  transferred across aliases\, possibly across different threads.
LOCATION:FW26
END:VEVENT
END:VCALENDAR