University of Cambridge > Talks.cam > Logic and Semantics Seminar (Computer Laboratory) > The Semantics of Shared Memory in Intel CPU/FPGA Systems

The Semantics of Shared Memory in Intel CPU/FPGA Systems

Add to your list(s) Download to your calendar using vCal

  • UserDan Iorga, Imperial College London
  • ClockFriday 29 October 2021, 14:00-15:00
  • HouseFW26.

If you have a question about this talk, please contact Jamie Vicary.

Heterogeneous CPU /FPGA devices, in which a CPU and an FPGA can 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 programs that run on them. We describe the weak-memory behaviours that are allowed (and observable) on these devices when CPU threads and an FPGA thread access common memory locations in a fine-grained manner through multiple channels. Some of these behaviours are familiar from well-studied CPU and GPU concurrency; others are weaker still. We encode these behaviours in two formal memory models: one operational, one axiomatic. We develop executable implementations of both models, using the CBMC bounded model-checking tool for our operational model and the Alloy modelling language for our axiomatic model. Using these, we cross-check our models against each other via a translator that converts Alloy-generated executions into queries for the CBMC model. We also validate our models against actual hardware by translating 583 Alloy-generated executions into litmus tests that we run on CPU /FPGA devices; when doing this, we avoid the prohibitive cost of synthesising a hardware design per litmus test by creating our own `litmus-test processor’ in hardware. We expect that our models will be useful for low-level programmers, compiler writers, and designers of analysis tools. Indeed, as a demonstration of the utility of our work, we use our operational model to reason about a producer/consumer buffer implemented across the CPU and the FPGA .

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2021 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity