Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs (Extended Version)
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , , , , |
|---|---|
| Format: | Preprint |
| Publié: |
2025
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866909725972496384 |
|---|---|
| author | Li, Kwing Hei Aguirre, Alejandro Gregersen, Simon Oddershede Haselwarter, Philipp G. Tassarotti, Joseph Birkedal, Lars |
| author_facet | Li, Kwing Hei Aguirre, Alejandro Gregersen, Simon Oddershede Haselwarter, Philipp G. Tassarotti, Joseph Birkedal, Lars |
| contents | We present Coneris, the first higher-order concurrent separation logic for reasoning about error probability bounds of higher-order concurrent probabilistic programs with higher-order state. To support modular reasoning about concurrent (non-probabilistic) program modules, state-of-the-art program logics internalize the classic notion of linearizability within the logic through the concept of logical atomicity.
Coneris extends this idea to probabilistic concurrent program modules. Thus Coneris supports modular reasoning about probabilistic concurrent modules by capturing a novel notion of randomized logical atomicity within the logic. To do so, Coneris utilizes presampling tapes and a novel probabilistic update modality to describe how state is changed probabilistically at linearization points. We demonstrate this approach by means of smaller synthetic examples and larger case studies.
All of the presented results, including the meta-theory, have been mechanized in the Rocq proof assistant and the Iris separation logic framework
This is the extended version of the same paper accepted at ICFP 2025, where more details of proofs and case studies are included in the Appendix. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2503_04512 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs (Extended Version) Li, Kwing Hei Aguirre, Alejandro Gregersen, Simon Oddershede Haselwarter, Philipp G. Tassarotti, Joseph Birkedal, Lars Logic in Computer Science Programming Languages We present Coneris, the first higher-order concurrent separation logic for reasoning about error probability bounds of higher-order concurrent probabilistic programs with higher-order state. To support modular reasoning about concurrent (non-probabilistic) program modules, state-of-the-art program logics internalize the classic notion of linearizability within the logic through the concept of logical atomicity. Coneris extends this idea to probabilistic concurrent program modules. Thus Coneris supports modular reasoning about probabilistic concurrent modules by capturing a novel notion of randomized logical atomicity within the logic. To do so, Coneris utilizes presampling tapes and a novel probabilistic update modality to describe how state is changed probabilistically at linearization points. We demonstrate this approach by means of smaller synthetic examples and larger case studies. All of the presented results, including the meta-theory, have been mechanized in the Rocq proof assistant and the Iris separation logic framework This is the extended version of the same paper accepted at ICFP 2025, where more details of proofs and case studies are included in the Appendix. |
| title | Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs (Extended Version) |
| topic | Logic in Computer Science Programming Languages |
| url | https://arxiv.org/abs/2503.04512 |