Ogre And Pythia: An Invariance Proof Method For Weak Consistency Models
POPL(2017)
摘要
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.
更多查看译文
关键词
concurrency,distributed and parallel programming,invariance,verification,weak consistency models
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要