BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:A promising semantics for relaxed-memory concurrency - Chung-Kil H
 ur\, Seoul National University
DTSTART:20170908T130000Z
DTEND:20170908T140000Z
UID:TALK75421@talks.cam.ac.uk
CONTACT:Dominic Mulligan
DESCRIPTION:Despite many years of research\, it has proven very difficult 
 to\ndevelop a model for relaxed-memory concurency that satisfies all the\n
 requirements of programmers\, compilers\, and hardware.\n\nIn this talk\, 
 I will introduce the first relaxed-memory model\, called\n"promising seman
 tics"\, that fulfills (most of) the requirements.\nIt (1) accounts for a b
 road spectrum of features from the C++11\nconcurrency model\, (2) is imple
 mentable\, in the sense that it provably\nvalidates many standard compiler
  optimizations and reorderings\, as\nwell as standard compilation schemes 
 to x86-TSO and Power\, (3)\njustifies simple invariant-based reasoning\, t
 hus demonstrating the\nabsence of bad "out-of-thin-air" behaviors\, (4) su
 pports "DRF"\nguarantees\, ensuring that programmers who use sufficient\ns
 ynchronization need not understand the full complexities of\nrelaxed-memor
 y semantics\, and (5) defines the semantics of racy\nprograms without rely
 ing on undefined behaviors\, which is a\nprerequisite for applicability to
  type-safe languages like Java.  To\nestablish confidence in our model\, w
 e have formalized most of our key\nresults in Coq.\n\nAlso\, in this talk\
 , no prior knowledge of relaxed memory concurrency\n(in particular\, exist
 ing axiomatic semantics) is assumed. This is\nparticularly because the pro
 mising semantics is a standard\ninterleaving operational semantics with ju
 st two new notions: "view"\nand "promise".
LOCATION:FW26
END:VEVENT
END:VCALENDAR