A Verified Thread-Safe Array in Rust
summary
A verified thread-safe array API in Rust uses the Verus verifier and permission-based interior mutability to let shared references enable arbitrary parallel access without runtime checks. The implementation produces a usable array + ghost permission set, requires uses Arc for thread spawn support, and runs a parallel merge sort that is 0.8% slower than the runtime-checked slice-splitting baseline. The prototype is workable but verbose — 264 LOC with about half annotations — and cannot yet express general mutable-reference lifetimes.
AI-written summary · about
chapters (10)
- 0:00Verified thread-safe arrays in Rust
- 1:06Borrow checker limits and thread safety
- 3:36Introducing Verus for verification
- 5:00Verified array API with permissions
- 7:09Parallel merge sort implementation
- 11:55Benefits of formal verification
- 13:21Code complexity and annotations
- 14:44Verus limitations and thread spawning
- 16:08Future work and sharing patterns
- 19:23Q&A
related talks
18mVerus: Verifying Rust Programs using Linear Ghost Types
45mRust: safe and concurrent. But how does it do it?
19mA Hybrid Approach to Semi-automated Rust Verification
19mExternal locking for internally synchronized data structures
15mNon-binary Rust: Between Safe and Unsafe
42mThe Edge of Safe Rust
21mUsing Ghost Ownership to Verify Union-Find and Persistent Arrays in Rust
19mProduction Unsafe Rust