Realistic Realizability: Specifying ABIs You Can Count On
summary
Proposes using realistic realizability models to specify ABIs by connecting high-level types to concrete target code and builds a graph-based separation logic with two modalities to model reference counts and ownership. Formalizes a reference-counting implementation for a C-like target, encodes Swift-style library evolution via a resilient offset table, proves safety and memory reclamation for the case study, and shows compliance with an ARC compiler model so the approach actually verifies ABI properties rather than only describing them.
AI-written summary · about
chapters (11)
- 0:00ABI specification intro
- 1:26ABI interoperability motivation
- 3:12Realistic realizability formalization
- 4:35Case study: reference counting ABI
- 7:02Function calling conventions ABI
- 8:05Struct layout and memory management
- 10:11Separation logic for graphs
- 12:38ABI compatibility and type updates
- 14:03Swift’s resilient layout
- 15:09Future work and Rust integration
- 15:59Q&A
related talks
19mSpecifying ABIs with Realizability and Type-Preserving Compilation
35mAll the Binaries Together: A Semantic Approach to Application Binary Interfaces
27mTaming Unsoundness with Gradual Abstract Interpretation
26mSemantic Encapsulation using Linking Types
18mBlame-aware Recomposition for Formally Secure Low-level Compiler Backends
26mArchSem: Reusable Rigorous Semantics of Relaxed Architectures
01h 03mCRIS: The power of imagination in specification and verification
58mC++, Abstract Algebra and Practical Applications