BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:The Semantics of Shared Memory in Intel CPU/FPGA Systems - Dan Ior
 ga\, Imperial College London
DTSTART:20211029T130000Z
DTEND:20211029T140000Z
UID:TALK164428@talks.cam.ac.uk
CONTACT:Jamie Vicary
DESCRIPTION:Heterogeneous CPU/FPGA devices\, in which a CPU and an FPGA ca
 n execute together while sharing memory\, are becoming popular in several 
 computing sectors. We study the shared-memory semantics of these devices\,
  with a view to providing a firm foundation for reasoning about the progra
 ms that run on them.  We describe the weak-memory behaviours that are allo
 wed (and observable) on these devices when CPU threads and an FPGA thread 
 access common memory locations in a fine-grained manner through multiple c
 hannels. Some of these behaviours are familiar from well-studied CPU and G
 PU concurrency\; others are weaker still. We encode these behaviours in tw
 o formal memory models: one operational\, one axiomatic. We develop execut
 able implementations of both models\, using the CBMC bounded model-checkin
 g tool for our operational model and the Alloy modelling language for our 
 axiomatic model. Using these\, we cross-check our models against each othe
 r via a translator that converts Alloy-generated executions into queries f
 or the CBMC model. We also validate our models against actual hardware by 
 translating 583 Alloy-generated executions into litmus tests that we run o
 n CPU/FPGA devices\; when doing this\, we avoid the prohibitive cost of sy
 nthesising a hardware design per litmus test by creating our own `litmus-t
 est processor' in hardware. We expect that our models will be useful for l
 ow-level programmers\, compiler writers\, and designers of analysis tools.
  Indeed\, as a demonstration of the utility of our work\, we use our opera
 tional model to reason about a producer/consumer buffer implemented across
  the CPU and the FPGA.
LOCATION:FW26
END:VEVENT
END:VCALENDAR