Imperial College London
Portrait Picture

ProfessorAlastairDonaldson

Faculty of Engineering, Department of Computing

Professor of Programming Languages
 
 
 
//

Contact

 

+44 (0)20 7594 8266alastair.donaldson Website

 
 
//

Location

 

422Huxley BuildingSouth Kensington Campus

//

Summary

 

Publications

Citation

BibTex format

@article{Iorga:2021:10.1145/3485497,
author = {Iorga, D and Donaldson, A and Sorensen, T and Wickerson, J and Wickerson, J},
doi = {10.1145/3485497},
journal = {Proceedings of the ACM on Programming Languages},
pages = {1--28},
title = {The semantics of shared memory in Intel CPU/FPGA systems},
url = {http://dx.doi.org/10.1145/3485497},
volume = {5},
year = {2021}
}
Download

RIS format (EndNote, RefMan)

TY  - JOUR
AB  - 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.
AU  - Iorga,D
AU  - Donaldson,A
AU  - Sorensen,T
AU  - Wickerson,J
AU  - Wickerson,J
DO  - 10.1145/3485497
EP  - 28
PY  - 2021///
SN  - 2475-1421
SP  - 1
TI  - The semantics of shared memory in Intel CPU/FPGA systems
T2  - Proceedings of the ACM on Programming Languages
UR  - http://dx.doi.org/10.1145/3485497
UR  - http://hdl.handle.net/10044/1/91779
VL  - 5
ER  -
Download