Residential College | false |
Status | 已發表Published |
A simple proof of data-race freedom and coherence for simpson's 4-slot algorithm | |
Wang, Xu1; Xu, Qiwen2 | |
2022-05-06 | |
Conference Name | The 37th ACM/SIGAPP Symposium on Applied Computing (SAC ’22) |
Source Publication | Proceedings of the ACM Symposium on Applied Computing |
Pages | 1853-1856 |
Conference Date | 2022/04/25-2022/04/29 |
Conference Place | New York, NY, USA |
Publisher | Association for Computing Machinery |
Abstract | In this paper we present an invariance proof of two properties on Simpson's 4-slot algorithm, i.e. data-race freedom and data coherence, which, together with data freshness, implies linearisability of the algorithm. It is an extension of previous works which focus mostly on the proof of data-race freedom. In addition, our proof uses simply inductive invariants and transition invariants [7], whereas previous work uses more sophisticated machinery like separation logics, rely-guarantee or ownership transfer. |
DOI | 10.1145/3477314.3507231 |
URL | View the original |
Language | 英語English |
Scopus ID | 2-s2.0-85130339649 |
Fulltext Access | |
Citation statistics | |
Document Type | Conference paper |
Collection | DEPARTMENT OF COMPUTER AND INFORMATION SCIENCE |
Affiliation | 1.East China Normal University, Shanghai, China 2.University of Macau, Macao |
Recommended Citation GB/T 7714 | Wang, Xu,Xu, Qiwen. A simple proof of data-race freedom and coherence for simpson's 4-slot algorithm[C]:Association for Computing Machinery, 2022, 1853-1856. |
APA | Wang, Xu., & Xu, Qiwen (2022). A simple proof of data-race freedom and coherence for simpson's 4-slot algorithm. Proceedings of the ACM Symposium on Applied Computing, 1853-1856. |
Files in This Item: | There are no files associated with this item. |
Items in the repository are protected by copyright, with all rights reserved, unless otherwise indicated.
Edit Comment