一句话：为 SPARC TSO 弱内存模型提出可组合的 pomsets 指称语义，并证明其相对公理语义可靠且完备。
SPARC TSO 是广泛使用的弱内存模型，其公理化定义是非组合式的，难以对程序行为进行模块化推理。本文提出一种基于 pomsets（偏序多重集）的指称语义：使用带缓冲的状态与归纳式的执行定义，为 pomsets 赋予输入-输出含义，从而精确刻画 SPARC TSO 所允许的行为。作者证明该指称语义相对于公理语义是可靠且完备的，即二者所允许的行为集合完全一致。该组合式语义便于研究 SPARC TSO，并支持程序行为的模块化分析。
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. It uses buffered states and an inductive definition of execution to assign an input-output meaning to pomsets. We show that our denotational account is sound and complete relative to the axiomatic account, that is, that it captures exactly the behaviours permitted by the axiomatic account. Our compositional approach facilitates the study of SPARC TSO and supports modular analysis of program behaviour.