A Denotational Semantics for SPARC TSO

被引：7
|
作者：
Kavanagh, Ryan [1 ]
Brookes, Stephen [1 ]
机构：
[1] Carnegie Mellon Univ, Dept Comp Sci, Pittsburgh, PA 15213 USA
来源：
ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE | 2018年 / 336卷 / 336期
基金：
加拿大自然科学与工程研究理事会;
关键词：
SPARC TSO; denotational semantics; pomsets; concurrency; weak memory models;
D O I：
10.1016/j.entcs.2018.03.025
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
The SPARC TSO weak memory model is defined axiomatically, with a non-compositional formulation that makes modular reasoning about programs difficult. Our denotational approach uses pomsets to provide a compositional semantics capturing exactly the behaviours permitted by SPARC TSO. Our approach facilitates the study of SPARC TSO and supports modular analysis of program behaviour.
引用
收藏
页码：223 / 239
页数：17
相关论文
共 50 条
12345