Reasoning about expression evaluation under interference
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2024
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866912731303510016 |
|---|---|
| author | Hayes, Ian J. Jones, Cliff B. Meinicke, Larissa A. |
| author_facet | Hayes, Ian J. Jones, Cliff B. Meinicke, Larissa A. |
| contents | Hoare-style inference rules for program constructs permit the copying of expressions and tests from program text into logical contexts. It is known that this requires care even for sequential programs but much more serious issues arise with concurrent programs because of potential interference to the values of variables. The "rely-guarantee" approach tackles the challenge of recording acceptable interference and offers a way to provide safe inference rules for concurrent constructs. This paper shows how the algebraic presentation of rely-guarantee ideas can clarify and formalise the conditions for safely re-using expressions and tests from program text in logical contexts for reasoning about concurrent programs; crucially this extends to handling expressions that reference more than one shared variable. A non-trivial example related to the Fischer-Galler forest representation of equivalence relations is treated. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2409_07741 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Reasoning about expression evaluation under interference Hayes, Ian J. Jones, Cliff B. Meinicke, Larissa A. Logic in Computer Science Software Engineering F.3.1; D.1.3 Hoare-style inference rules for program constructs permit the copying of expressions and tests from program text into logical contexts. It is known that this requires care even for sequential programs but much more serious issues arise with concurrent programs because of potential interference to the values of variables. The "rely-guarantee" approach tackles the challenge of recording acceptable interference and offers a way to provide safe inference rules for concurrent constructs. This paper shows how the algebraic presentation of rely-guarantee ideas can clarify and formalise the conditions for safely re-using expressions and tests from program text in logical contexts for reasoning about concurrent programs; crucially this extends to handling expressions that reference more than one shared variable. A non-trivial example related to the Fischer-Galler forest representation of equivalence relations is treated. |
| title | Reasoning about expression evaluation under interference |
| topic | Logic in Computer Science Software Engineering F.3.1; D.1.3 |
| url | https://arxiv.org/abs/2409.07741 |