The semantics of shared memory in Intel CPU/FPGA systems
File(s)
Published version
Author(s)
Iorga, Dan
Donaldson, Alastair
Sorensen, Tyler
Wickerson, John
Wickerson, John
Type
Journal Article
Abstract
Heterogeneous CPU/FPGA devices, in which a CPU and an FPGA can execute together while sharing memory,are becoming popular in several computing sectors. In this paper, we study the shared-memory semanticsof these devices, with a view to providing a firm foundation for reasoning about the programs that run onthem. Our focus is on Intel platforms that combine an Intel FPGA with a multicore Xeon CPU. We describe theweak-memory behaviours that are allowed (and observable) on these devices when CPU threads and an FPGAthread access common memory locations in a fine-grained manner through multiple channels. Some of thesebehaviours are familiar from well-studied CPU and GPU concurrency; others are weaker still. We encodethese behaviours in two formal memory models: one operational, one axiomatic. We develop executableimplementations of both models, using the CBMC bounded model-checking tool for our operational modeland the Alloy modelling language for our axiomatic model. Using these, we cross-check our models againsteach other via a translator that converts Alloy-generated executions into queries for the CBMC model. Wealso validate our models against actual hardware by translating 583 Alloy-generated executions into litmustests that we run on CPU/FPGA devices; when doing this, we avoid the prohibitive cost of synthesising ahardware design per litmus test by creating our own ‘litmus-test processor’ in hardware. We expect that ourmodels will be useful for low-level programmers, compiler writers, and designers of analysis tools. Indeed, as ademonstration of the utility of our work, we use our operational model to reason about a producer/consumerbuffer implemented across the CPU and the FPGA. When the buffer uses insufficient synchronisation – asituation that our model is able to detect – we observe that its performance improves at the cost of occasionaldata corruption.
Date Issued
2021-10-01
Date Acceptance
2021-08-31
Citation
Proceedings of the ACM on Programming Languages, 2021, 5 (OOPSLA), pp.1-28
ISSN
2475-1421
Publisher
Association for Computing Machinery (ACM)
Start Page
1
End Page
28
Journal / Book Title
Proceedings of the ACM on Programming Languages
Volume
5
Issue
OOPSLA
Copyright Statement
© 2021 Copyright held by the owner/author(s). This work is licensed under a Creative Commmons Attribution International License 4.0 (https://creativecommons.org/licenses/by/4.0/)
License URL
Sponsor
Engineering & Physical Science Research Council (E
Imperial Institute for Security Science and Technology
Engineering and Physical Sciences Research Council
Grant Number
Ref: 542716
ISST Champions Fund
EP/L016796/1
Subjects
Science & Technology
Technology
Computer Science, Software Engineering
Computer Science
CPU/FPGA
Core Cache Interface (CCI-P)
memory model
COMPUTER
Publication Status
Published
Article Number
ARTN 120