Lion: Modular Verification of Async Runtime Liveness
TL;DR
This work introduces an append-only logical event log that abstracts implementation details and enables a Kamp-style translation of Linear Temporal Logic into First-Order Logic, which enables deductive program verifiers to reason about progress via monotonic timestamps without needing native temporal logic support.
Abstract
Asynchronous programming (async) is the dominant paradigm for developing high-performance systems, where concurrent tasks voluntarily yield control to an async runtime when resources are unavailable. These programs expect a fundamental liveness promise from the runtime: every task that yields will eventually be resumed when its awaited event fires. A single scheduling bug can silently break this contract, leaving tasks permanently stalled with no observable symptoms, such as a crash or error trace, to signal the failure. We present a general parametric specification framework and methodology for discharging this promise in runtimes composed of multiple interacting modules. Our approach introduces an append-only logical event log that abstracts implementation details and enables a Kamp-style translation of Linear Temporal Logic (LTL) into First-Order Logic. This enables deductive program verifiers to reason about progress via monotonic timestamps without needing native temporal logic support. Our main liveness theorem abstracts over the sufficient conditions, such as environmental assumptions and calling conventions, allowing these proof obligations to be instantiated for different runtime implementations. We demonstrate this framework via Lion, a Tokio-compatible runtime in Rust verified using Verus. By establishing a bijective mapping between log events and concrete actions, we prove that Lion maintains the liveness contract and measure at least 95% of unverified-runtime throughput on nine real-world workloads.