Reasoning about concurrent loops and recursion with rely-guarantee rules
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866911305342910464 |
|---|---|
| author | Hayes, Ian J. Meinicke, Larissa A. Jones, Cliff B. |
| author_facet | Hayes, Ian J. Meinicke, Larissa A. Jones, Cliff B. |
| contents | The objective of this paper is to present general, mechanically verified, refinement rules for reasoning about recursive programs and while loops in the context of concurrency. Unlike many approaches to concurrency, we do not assume that expression evaluation is atomic. We make use of the rely-guarantee approach to concurrency that facilitates reasoning about interference from concurrent threads in a compositional manner. Recursive programs can be defined as fixed points over a lattice of commands and hence we develop laws for reasoning about fixed points. Loops can be defined in terms of fixed points and hence the laws for recursion can be applied to develop laws for loops. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2512_06242 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Reasoning about concurrent loops and recursion with rely-guarantee rules Hayes, Ian J. Meinicke, Larissa A. Jones, Cliff B. Logic in Computer Science Programming Languages Software Engineering F.3.1; D.1.3 The objective of this paper is to present general, mechanically verified, refinement rules for reasoning about recursive programs and while loops in the context of concurrency. Unlike many approaches to concurrency, we do not assume that expression evaluation is atomic. We make use of the rely-guarantee approach to concurrency that facilitates reasoning about interference from concurrent threads in a compositional manner. Recursive programs can be defined as fixed points over a lattice of commands and hence we develop laws for reasoning about fixed points. Loops can be defined in terms of fixed points and hence the laws for recursion can be applied to develop laws for loops. |
| title | Reasoning about concurrent loops and recursion with rely-guarantee rules |
| topic | Logic in Computer Science Programming Languages Software Engineering F.3.1; D.1.3 |
| url | https://arxiv.org/abs/2512.06242 |