Saved in:
| Main Author: | |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2505.15053 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866914330190020608 |
|---|---|
| author | Abe, Tatsuya |
| author_facet | Abe, Tatsuya |
| contents | Whereas an extension with non-interference of Hoare logic for sequential programs Owicki--Gries logic ensures the correctness of concurrent programs on strict consistency, it is unsound to weak memory models adopted by modern computer architectures and specifications of programming languages. This paper proposes a novel non-interference notion and provides concurrent program logic sound to timestamp semantics corresponding to a weak memory model that allows delays in the effects of store instructions. This paper reports three theoretically interesting techniques for modifying non-interference to support delays in the effects of store instructions. The techniques contribute to a better understanding of constructing concurrent program logic. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2505_15053 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Owicki--Gries Logic for Timestamp Semantics Abe, Tatsuya Logic in Computer Science Whereas an extension with non-interference of Hoare logic for sequential programs Owicki--Gries logic ensures the correctness of concurrent programs on strict consistency, it is unsound to weak memory models adopted by modern computer architectures and specifications of programming languages. This paper proposes a novel non-interference notion and provides concurrent program logic sound to timestamp semantics corresponding to a weak memory model that allows delays in the effects of store instructions. This paper reports three theoretically interesting techniques for modifying non-interference to support delays in the effects of store instructions. The techniques contribute to a better understanding of constructing concurrent program logic. |
| title | Owicki--Gries Logic for Timestamp Semantics |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2505.15053 |