Abstract
We design an invariance proof method for concurrent programs parameterised by a weak consistency model. The calculational design of the invariance proof method is by abstract interpretation of a truly parallel analytic semantics. This generalises the methods by Lamport and Owicki-Gries for sequential consistency. We use cat as an example of language to write consistency specifications of both concurrent programs and machine architectures.
Original language | English (US) |
---|---|
Pages (from-to) | 3-18 |
Number of pages | 16 |
Journal | ACM SIGPLAN Notices |
Volume | 52 |
Issue number | 1 |
DOIs | |
State | Published - Jan 2017 |
Keywords
- concurrency
- distributed and parallel programming
- in- variance
- verification
- weak consistency models
ASJC Scopus subject areas
- General Computer Science