SPARC TSO的指称语义
摘要：SPARC TSO弱内存模型的符号定义以非组合式的形式进行，并且这种形式使得对程序进行模块化推理变得困难。我们的表示论方法使用pomsets来提供组合语义，准确捕捉SPARC TSO允许的行为。它使用缓冲状态和对执行的归纳定义，为pomsets赋予输入-输出的含义。我们证明了我们的表示论方法在相对于符号定义的账户上是完备和准确的，也就是说，它准确地捕捉了符号定义允许的行为。我们的组合式方法便于研究SPARC TSO，并支持对程序行为的模块化分析。
作者：Ryan Kavanagh, Stephen Brookes
论文ID：1711.00931
分类：Programming Languages
分类简称：cs.PL
提交时间：2023-06-22