Just Verification of Mutual Exclusion Algorithms
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_ | 1866909693264265216 |
|---|---|
| author | van Glabbeek, Rob Luttik, Bas Spronck, Myrthe |
| author_facet | van Glabbeek, Rob Luttik, Bas Spronck, Myrthe |
| contents | We verify the correctness of a variety of mutual exclusion algorithms through model checking. We look at algorithms where communication is via shared read/write registers, where those registers can be atomic or non-atomic. For the verification of liveness properties, it is necessary to assume a completeness criterion to eliminate spurious counterexamples. We use justness as completeness criterion. Justness depends on a concurrency relation; we consider several such relations, modelling different assumptions on the working of the shared registers. We present executions demonstrating the violation of correctness properties by several algorithms, and in some cases suggest improvements. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2507_13198 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Just Verification of Mutual Exclusion Algorithms van Glabbeek, Rob Luttik, Bas Spronck, Myrthe Logic in Computer Science Distributed, Parallel, and Cluster Computing F.3.1 We verify the correctness of a variety of mutual exclusion algorithms through model checking. We look at algorithms where communication is via shared read/write registers, where those registers can be atomic or non-atomic. For the verification of liveness properties, it is necessary to assume a completeness criterion to eliminate spurious counterexamples. We use justness as completeness criterion. Justness depends on a concurrency relation; we consider several such relations, modelling different assumptions on the working of the shared registers. We present executions demonstrating the violation of correctness properties by several algorithms, and in some cases suggest improvements. |
| title | Just Verification of Mutual Exclusion Algorithms |
| topic | Logic in Computer Science Distributed, Parallel, and Cluster Computing F.3.1 |
| url | https://arxiv.org/abs/2507.13198 |