摘要: 1、研究背景（context）。
内存模型可以被用来确定并发程序的行为，最广为人知和符合大家直观理解的内存模型是顺序一致性模型（Sequential Consistency Model）。这个模型规定了不同线程的操作以穿插的方式进行，而每个线程的操作是严格按照程序执行顺序（Program Order）出现的。为了提高硬件和编译器的执行效率，现代处理器大多选择使用弱内存模型（Weak Memory Model）。弱内存模型是指允许经过优化而产生的不符合顺序一致性的行为的模型。Total Store Order（TSO）内存模型是在顺序一致性模型的基础上放松了对写读（write-read）操作顺序约束的一种模型，并且它已经在x86架构和SPARC（Scalable Processor Architecture）平台中得到了广泛的应用。源于弱内存模型的复杂性，非形式化的研究作用有限，散文化的、冗长的C11工业标准先后被形式化工作者发现多个漏洞，因此，对弱内存模型形式化语义的研究是很有价值的。然而，在形式化方面，大部分现有的工作都是单独研究TSO模型的操作语义、指称语义和证明系统，很少有文章在TSO模型上综合考虑多种语义。
2、目的（Objective）：准确描述该研究的目的,说明提出问题的缘由，表明研究的范围和重要性。
我们的研究目的是展示Total Store Order（TSO）内存模型的轨迹语义和代数规则，以及如何从代数语义生成轨迹语义，即确保代数语义和轨迹语义的一致性。
3、方法（Method）：简要说明研究课题的基本设计，结论是如何得到的。
我们首先以程序统一理论（Unifying Theories of Programming,UTP）为基础理论，研究TSO内存模型的轨迹语义，该语义用来描述TSO模型下的任意程序的执行效果，即关注的是程序做了什么。轨迹是由一系列的快照组成。这些快照记录了程序语句在存储缓冲区、寄存器和共享内存上所引起的变化。在上述语义模型的基础上，我们研究了基本语句的轨迹语义、顺序组合的轨迹语义和并发组合的轨迹语义。TSO内存模型的“reordering”特性主要是通过顺序组合得以体现。对于顺序组合，我们通过穿插执行的方式得到初始的执行轨迹，再定义程序顺序函数和内存修改顺序函数来剔除掉不合法的程序执行。
程序的属性通常使用代数等式进行表达。我们其次研究了TSO内存模型的代数规则，包括顺序组合的代数规则和并发组合的代数规则。为了方便代数规则和统一理论的研究，这里引入了首规范型（head normal form）和卫兵选择（guarded choice）的概念。从这些代数规则中，我们可以发现每一个程序都可以转换为卫兵选择的形式。同时，TSO内存模型的线性化也得以体现。
此外，我们还通过定义了转换策略（derivation strategy）研究了从代数语义生成轨迹语义，其目的是确保代数语义和轨迹语义的一致性。
4、结果（Result&Findings）：简要列出该研究的主要结果，有什么新发现，说明其价值和局限。叙述要具体、准确，尽量给出量化数据而不只是定性描述，并给出结果的置信值（如果有）。
本文的研究重点是展示TSO内存模型的轨迹语义、代数规则以及如何从代数语义生成轨迹语义。相关的语义模型都能支持TSO的线性化（linearizability）。对于某一程序，通过比较由原始轨迹语义得到的轨迹，和使用转换策略从代数语义生成的轨迹，我们发现TSO内存模型下的代数语义和轨迹语义的一致性得到了体现。
5、结论（Conclusions）：简要地说明经验，论证取得的正确观点及理论价值或应用价值，是否还有与此有关的其它问题有待进一步研究，是否可推广应用，其应用价值如何？
本文在形式语义学和程序统一理论的指导下，研究了TSO内存模型的轨迹语义和代数规则，相关的语义模型都能支持TSO的线性化（linearizability）。此外，通过定义从代数语义到轨迹语义的转换策略，研究了TSO内存模型下轨迹语义和代数语义的一致性。我们可以通过对本文的研究方法进行扩展，从而支持其他更加复杂的弱内存模型。
近来，Hoare教授提出了四种语义（即操作语义、指称语义、代数语义和证明系统）之间的一致性的研究。本文我们已经研究了从代数语义生成轨迹语义，未来我们将对其他语义之间的一致性进行研究。同时，在理论研究的基础上，我们将尝试使用定理证明器（比如Coq）对TSO内存模型的形式化语义及其语义连接进行辅助研究。