BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:ArchSem: Reusable Rigorous Semantics of Relaxed Architectures - Th
 ibaut Pérami
DTSTART:20260126T130000Z
DTEND:20260126T140000Z
UID:TALK243319@talks.cam.ac.uk
CONTACT:Rini Banerjee
DESCRIPTION:The specifications of mainstream processor architectures\, suc
 h as Arm\, x86\, and RISC-V\, underlie modern computing\, as the targets o
 f compilers\, operating systems\, and hypervisors. However\, despite exten
 sive research and tooling for instruction-set architecture (ISA) and relax
 ed-memory semantics\, recently including systems features\, there still do
  not exist integrated mathematical models that suffice for foundational fo
 rmal verification\, of concurrent architecture properties or of systems so
 ftware. Previous proof-assistant work has had to substantially simplify th
 e ISA semantics\, the concurrency model\, or both.\n\nIn this talk\, we pr
 esent ArchSem\, an architecture-generic framework for architecture semanti
 cs\, modularly combining ISA and concurrency models along a tractable inte
 rface of instruction-semantics effects\, that covers a range of systems as
 pects. To do so\, one has to handle many issues that were previously uncle
 ar\, about the architectures themselves\, the interface\, the proper defin
 ition of reusable models\, and the Rocq and Isabelle idioms required to ma
 ke it usable. We instantiate it to the Arm-A and RISC-V instruction-set ar
 chitectures and multiple concurrency models.\n\nWe demonstrate usability f
 or proof\, despite the scale\, by establishing that the Arm architecture (
 in a particular configuration) provides a provable virtual memory abstract
 ion\, with a combination of Rocq\, Isabelle\, and paper proof. Previous wo
 rk provides further confirmation of usability: the AxSL program logic for 
 Arm relaxed concurrency was proved sound above an earlier version of ArchS
 em.\n\nThis establishes a basis for future proofs of architecture properti
 es and systems software\, above production architecture specifications.
LOCATION:FS07\, Computer Laboratory
END:VEVENT
END:VCALENDAR