Restructuring a concurrent refinement algebra
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , |
|---|---|
| Format: | Preprint |
| Publié: |
2024
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866917662135681024 |
|---|---|
| author | Hayes, Ian J. Meinicke, Larissa A. Evangelou-Oost, Naso |
| author_facet | Hayes, Ian J. Meinicke, Larissa A. Evangelou-Oost, Naso |
| contents | The concurrent refinement algebra has been developed to support rely/guarantee reasoning about concurrent programs. The algebra supports atomic commands and defines parallel composition as a synchronous operation, as in Milner's SCCS. In order to allow specifications to be combined, the algebra also provides a weak conjunction operation, which is also a synchronous operation that shares many properties with parallel composition. The three main operations, sequential composition, parallel composition and weak conjunction, all respect a (weak) quantale structure over a lattice of commands. Further structure involves combinations of pairs of these operations: sequential/parallel, sequential/weak conjunction and parallel/weak conjunction, each pair satisfying a weak interchange law similar to Concurrent Kleene Algebra. Each of these pairs satisfies a common biquantale structure. Additional structure is added via compatible sets of commands, including tests, atomic commands and pseudo-atomic commands. These allow stronger (equality) interchange and distributive laws. This paper describes the result of restructuring the algebra to better exploit these commonalities. The algebra is implemented in Isabelle/HOL. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2405_05690 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Restructuring a concurrent refinement algebra Hayes, Ian J. Meinicke, Larissa A. Evangelou-Oost, Naso Logic in Computer Science F.3.1; D.1.3 The concurrent refinement algebra has been developed to support rely/guarantee reasoning about concurrent programs. The algebra supports atomic commands and defines parallel composition as a synchronous operation, as in Milner's SCCS. In order to allow specifications to be combined, the algebra also provides a weak conjunction operation, which is also a synchronous operation that shares many properties with parallel composition. The three main operations, sequential composition, parallel composition and weak conjunction, all respect a (weak) quantale structure over a lattice of commands. Further structure involves combinations of pairs of these operations: sequential/parallel, sequential/weak conjunction and parallel/weak conjunction, each pair satisfying a weak interchange law similar to Concurrent Kleene Algebra. Each of these pairs satisfies a common biquantale structure. Additional structure is added via compatible sets of commands, including tests, atomic commands and pseudo-atomic commands. These allow stronger (equality) interchange and distributive laws. This paper describes the result of restructuring the algebra to better exploit these commonalities. The algebra is implemented in Isabelle/HOL. |
| title | Restructuring a concurrent refinement algebra |
| topic | Logic in Computer Science F.3.1; D.1.3 |
| url | https://arxiv.org/abs/2405.05690 |