BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Axiomatic Concurrency Semantics for Full-Scale ARMv8-A using Symbo
 lic Execution - Alasdair Armstrong\, University of Cambridge
DTSTART:20201023T130000Z
DTEND:20201023T140000Z
UID:TALK152584@talks.cam.ac.uk
CONTACT:Jamie Vicary
DESCRIPTION:https://us02web.zoom.us/j/177472153?pwd=MFgwd0EzY05QSGtpSDc2dU
 16aG9wdz09\n\nIn this talk I will present work on an in-progress tool for\
 nsimulating relaxed memory models over the full ARMv8-A\narchitecture. Usi
 ng symbolic execution of Sail instruction set\narchitecture specifications
 \, and in particular a translation of\nARM's ASL specification\, this tool
  allows us to simulate the\nconcurrent behavior of litmus tests spanning t
 he entire\narchitecture. As an illustrative example\, we can consider how 
 the\ninstruction cache maintenance instructions interact with\nself-modify
 ing code in an axiomatic setting\, or the weak-memory\nbehavior of page ta
 ble updates. Such behavior is relevant for the\nsemantics of systems softw
 are like operating systems and\nhypervisors which routinely interact with 
 such architectural\nfeatures in a concurrent way.
LOCATION:Online
END:VEVENT
END:VCALENDAR