Trace Semantics and Algebraic Laws for Total Store Order Memory Model |
| |
| Authors: | Li-Li Xiao Hui-Biao Zhu Qi-Wen Xu |
| |
| Affiliation: | 1.Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai 200062, China;2.Department of Computer and Information Science, Faculty of Science and Technology, University of Macau Macau, China |
| |
| Abstract: | Modern multiprocessors deploy a variety of weak memory models(WMMs).Total Store Order(TSO) is a widely-used weak memory model in SPARC implementations and x86 architecture.It omits the store-load constraint by allowing each core to employ a write buffer.In this paper,we apply Unifying Theories of Programming(abbreviated as UTP) in investigating the trace semantics for TSO,acting in the denotational semantics style.A trace is expressed as a sequence of snapshots,which records the changes in registers,write buffers and the shared memory.All the valid execution results containing reorderings can be described after kicking out those that do not satisfy program order and modification order.This paper also presents a set of algebraic laws for TSO.We study the concept of head normal form,and every program can be expressed in the head normal form of the guarded choice which is able to model the execution of a program with reorderings.Then the linearizability of the TSO model is supported.Furthermore,we consider the linking between trace semantics and algebraic semantics.The linking is achieved through deriving trace semantics from algebraic semantics,and the derivation strategy under the TSO model is provided. |
| |
| Keywords: | weak memory model Total Store Order(TSO) trace semantics algebraic law Unifying Theories of Programming(UTP) |
| 本文献已被 万方数据 等数据库收录！ |
| 点击此处可从《计算机科学技术学报》浏览原始摘要信息 |
|
点击此处可从《计算机科学技术学报》下载全文 |
|
