硬件内存模型论文阅读

引言

内存模型定义了内存操作的语义,提出内存模型的目的在于指明内存操作之间的次序有何限制.

内存模型并不直接指定内存操作的次序,它只提供一种行为描述,只要你的执行结果 与 按内存模型规定的次序执行结果 一致就行,并不要求具体实现一定按这个顺序.

Java 内存模型论文阅读

引言

Java 的内存模型最早出现在1995年，但是自1997年起，这一内存模型被发现了许多严重的错误和缺陷，它阻碍了很多优化措施，对程序的安全性也没有足够的保证。2001年JSR 133被确立下来，由William Pugh领导，专家组的成员包括了Adve，Doug Lea， William Pugh等。2004年，JSR 133最终版本发布。2005年，Manson Jeremy, William Pugh, 和 Sarita V. Adve 一同发表了论文 The Java memory model，描述了最新的Java内存模型，这一内存模型在Java 5.0中引入，一直沿用至今。此后，科学家们对Java内存模型进行了进一步的研究的探索，但大的改动并没有出现。

论文介绍

Pugh2000

• 论文名 Pugh W. The Java memory model is fatally flawed[J]. Concurrency - Practice and Experience, 2000, 12(6): 445-455.

• 主要内容 介绍了现有Java内存模型的不足之处： * 难以理解，不同的人有不同解读 * 禁止了很多编译器优化，大多数JVM实现都违反Java内存模型 * 一些常用编程范式违反Java内存模型 * 没有考虑到在共享内存，弱一致性内存模型下实现Java所带来的一些问题

• 参考文献

  • Gontmakher 1997: 证明了Java内存模型需要Coherence

Manson 2005

• 论文名 Manson J, Pugh W, Adve S V. The Java memory model[M]. ACM, 2005.

• 主要内容 JSR 133的成果，介绍了新的Java内存模型，由Java 5.0引入，沿用至今。 基本思想包括： * 对满足 Data Race Free 的程序保证顺序一致性(sequential consistency) * 对没有正确同步的程序，使用causality的概念加以限制，以保证程序的安全性 * 新的内存模型足够强，以保证安全性，又足够弱，以保证编译器可以使用足够的优化

• 参考文献

  • Lamport 1979: 提出 Sequential Consistency 概念
  • Relaxed models in academia and commercial hardware - Adve 1990 - Adve 1993 - Dubois 1986 - Gharachorloo 1990 - IBM 1983(System/370 Principles of Operation) - May 1994(The PowerPC Architecture) - Sites 1995(Alpha AXP Architecture Reference Manual) - Weaver 1994(The SPARC Architecture Manual)
  • SC for DRF - Adve 1990 - Adve 1993 - Gharachorloo 1990
  • Flaws in original Java Memory Model - Pugh 1999
  • Original Java Memory Model Research - Gosling 1996 - Kotrajaras 2001 - Saraswat 2004

Polyakov 2006

• 论文名 Polyakov S, Schuster A. Verification of the Java causality requirements [M]//Hardware and Software, Verification and Testing. Springer Berlin Heidelberg, 2006: 224-246.

• 主要内容 * 证明验证causality是NP-complete的 * 跟踪每个线程实际运行时 read 操作的顺序可以简化验证 * 对可简化的验证提出了多项式算法 * 不能简化的提出非多项式算法（仅用于短的测试序列） * 使用了Post-mortem的方法，实际运行一个多线程程序，在JVM或者定制过的JVM或者模拟器上运行程序，拿到trace，分析trace，以验证内存是否有问题 * 使用frontier graph验证

• 参考文献

  • Boehm 2005: 通过库实现多线程不能保证程序正确性
  • causal acyclicity 形式化定义(reach condition)： - Sufficient System Requirements for Supporting the PLpc Memory Model. 1993 - Specifying System Requirements for Memory Consistency Models. 1993
  • Gibbons 1993：使用frontier graph验证SC

学习英语第三周

阅读英文原著

这周按照预定计划，把每天的阅读量降低了一半，每天20页左右。下面是时间表。

这周把 The Three Musketeers 阅读完了，第一本英文小说，从一开始看40页需要六个小时，到最后基本可以流畅地看下来，感觉还是不错的。

下面是关键数据：

• 20天（2月16日至3月7日）
• 625页
• 228402单词
• 320个新单词

Data Race Free 的前世今生

Data Race Free 是多线程程序是非常重要的概念，因为Java 和 C++的内存模型都是基于 Data Race Free 的，这篇文章将介绍这个概念的由来，另一篇文章《Data Race Free的理解》介绍它的主要思想。

事情要追溯到遥远的1979年， Lamport 在他的著名论文 How to make a multiprocessor computer that correctly executes multiprocess programs 中提出了今后在内存模型领域被广泛使用的概念 ：sequential consistency，即顺序一致性。这篇文章告诉我们，你要做一台多处理器的计算机，需要满足什么条件，才能保证程序的正确性。当然，这里的程序跑在不同处理器上，共享同一块内存。虽然现在不说多处理器了，都说多核，多线程，但是问题的本质是没有变的。就是多个执行单元一起完成一个任务，并且通过共享存储单元的方式通信，在这种情况下，底层的系统需要提供什么样的支持，才能保证计算的结果和程序员的预期是一样的。

对Data Race Free 的理解

Data Race Free 的动机

Data Race Free 是对多线程程序 同步程度 的一种描述，假如你的多线程程序的同步程度满足 DRF 的要求，那么，你的程序会有这样一个好处：

程序在弱一致性模型下执行，执行的结果与在SC模型下执行一样

这意味着，程序员在写程序时，可以按SC模型来推断程序的执行。而程序在底层运行时，可以享受弱一致性模型带来的种种优化措施。

Data Race Free 具体内容

DRF 要求多线程程序中不能有冲突的操作。

什么是冲突的操作呢？

冲突的操作是指：两个操作来自不同线程，操作同一地址，至少有一个是写操作。

如何让冲突的操作不冲突呢？

需要使用同步操作将冲突的操作隔离开。

为什么要用同步操作将冲突的操作隔离开呢?