Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs
summary
Presents Coneris, the first higher-order concurrent separation logic that proves numeric error bounds for concurrent probabilistic programs and mechanizes all meta theory and examples in Rocq/Iris. It formalizes randomized logical atomicity using probabilistic update modality and presampling tapes, quantifies adequacy over all schedulers, and carries a worked example bounding a crash probability to 1/16. Case studies include a thread-safe random-oracle model and a concurrent Bloom filter with tight false positive bounds; all results are machine-checked and reusable.
AI-written summary · about