BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Promising ARMv8/RISC-V relaxed memory - Christopher Pulte\, Univer
 sity of Cambridge
DTSTART:20210129T140000Z
DTEND:20210129T150000Z
UID:TALK153283@talks.cam.ac.uk
CONTACT:Jamie Vicary
DESCRIPTION:https://us02web.zoom.us/j/177472153?pwd=MFgwd0EzY05QSGtpSDc2dU
 16aG9wdz09\n\nFor ARMv8 and RISC-V\, there are concurrency models in two s
 tyles:\naxiomatic models\, expressing the concurrency semantics in terms o
 f\nglobal properties of complete executions\; and operational models\, tha
 t\ncompute incrementally. The latter are in an abstract\nmicroarchitectura
 l style: they execute each instruction in multiple\nsteps\, out-of-order a
 nd with explicit branch speculation.  This\nsimilarity to hardware impleme
 ntations has been important in\ndeveloping the models and in establishing 
 confidence\, but involves\ncomplexity that\, for programming and model-che
 cking\, one would prefer\nto avoid.\n\nWe present new equivalent\, more ab
 stract operational models for ARMv8\nand RISC-V\, and an exploration tool 
 based on them. The models compute\nthe allowed concurrency behaviours incr
 ementally based on thread-local\nconditions and are significantly simpler 
 than the existing operational\nmodels: executing instructions in a single 
 step and (with the\nexception of early writes) in program order\, and with
 out branch\nspeculation. The exploration tool is fast enough for exhaustiv
 ely\nchecking the concurrency behaviour of a number of interesting\nexampl
 es. We use the tool for checking several standard concurrent\ndatastructur
 e and lock implementations\, and for interactively stepping\nthrough model
 -allowed executions for debugging.
LOCATION:Online
END:VEVENT
END:VCALENDAR