The Semantics of Shared Memory in Intel CPU/FPGA Systems
summary
Defines precise weak‑memory behaviors for Intel Xeon + Arria FPGA systems, encoding them as an operational model in CBMC and an axiomatic model in Alloy and cross‑checking via a translator; generates 477 Alloy executions, converts them to litmus tests and validates on hardware using a reusable litmus‑test processor on the FPGA. Shows multiple channels + fences yield better throughput, while removing synchronization gives about 10% data loss in producer/consumer queues under stress.
AI-written summary · about
chapters (20)
- 0:00FPGA vs CPU - What is the difference?
- 0:40The best of both worlds: CPU and FPGA
- 1:26X86-TSO Memory model
- 1:48CPU/FPGA system
- 1:59CPU/FPGA Architecture
- 2:23FPGA coherency examples
- 3:16CPU/FPGA synchronization examples
- 4:44FPGA and CPU operations CPU operations
- 6:06Justifications for modelling decisions
- 6:25Axiomatic model
- 6:49Empirical validation
- 7:18Litmus test generator
- 7:40Litmus test alternative
- 8:34Soft-core processor
- 9:33Stress generator
- 10:02Producer/Consumer queue
- 10:20Synchronization and validation
- 10:43Properly synchronized queues
- 11:18Does synchronization matter?
- 12:03Conclusions
related talks
30mA Tale of Shared Memory Concurrency in Programming Languages
18mThe Semantics of Transactions and Weak Memory in x86, Power, ARM, and C++
16mCompound Memory Models
01h 02mThe Two Memory Models
01h 11mProgramming language memory models: Problems, solutions, and directions
22mExtending Intel-x86 Consistency and Persistency: Formalising the Semantics of In
21mWeak Memory Demands Model-based Compiler Testing
51mMemory Model: Get your shared data under control