Does Rust SPARK Joy? Safe Bindings from Rust to SPARK, Applied to the BBQueue Li...
summary
Implements safe Rust→SPARK bindings for a real BBQueue circular buffer, proving the approach works after iterative fixes and testing. Mirrors Rust types as explicit C structs, uses the C ABI layout, abandons Rust ownership across the boundary, and enforces correctness with a memory checker called valra. Reimplements the queue core in SPARK with atomic lock-free counters, documents the exact pointer layouts and compiler flags required, and reports all tests passing with no memory-safety violations.
AI-written summary · about
chapters (8)
- 0:00Rust and SPARK intro
- 1:46FFI challenges and risks
- 3:11Rust and SPARK ownership
- 8:13BBQueue case study
- 12:33Data types across boundaries
- 17:14FFI memory safety
- 20:25Feasibility and automation
- 22:57Q&A
related talks
45mRust: safe and concurrent. But how does it do it?
01h 05mKeynote - Rust: confident, productive systems programming
35mLet’s Talk About Rust
40mRust’s approach of getting things right
19mProduction Unsafe Rust
41mRust Meets Zephyr: Building Safer Embedded Applications
28mRust and Scala, Sitting in a Tree….
01h 14mRust: A Friendly Introduction