学习英语第二周

阅读英文原著

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

这周阅读起来没什么压力了，下周还按这个节奏，努力一下没准就能读完了。

学习音标

这周的任务是学习辅音，到这周结束，已经完成了任务。下面是时间表。

C语言中的int类型的范围是由什么决定的

在 K&R 经典教材 The C Programming Language 的2.2节中，对 int 类型是这样描述的

an integer, typically reflecting the natural size of integers on the host machine

意思是反映了机器整数类型的 natural size，可是，

这个 natural size 又是什么意思呢？

书中后来在谈到 short, int, long 的关系时，又说，这些类型由编译器根据机器自由选择合适的大小，但是 short 和 int 至少 16 位，long 至少 32 位。

这里的问题是

编译器是根据什么决定类型大小呢？

后面书中又提到，这些类型啊，在<limits.h>中都有，我就在ubuntu下查看了 /usr/include/limits.h，里面确实提到

/* Minimum and maximum values a `signed int' can hold.  */
#  define INT_MIN   (-INT_MAX - 1)
#  define INT_MAX   2147483647

但是，这也是一种定义，还是没有说出为什么，我现在想知道的是

为什么

对Data Race Free 的理解

Data Race Free 的动机

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

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

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

Data Race Free 具体内容

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

什么是冲突的操作呢？

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

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

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

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

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，即顺序一致性。这篇文章告诉我们，你要做一台多处理器的计算机，需要满足什么条件，才能保证程序的正确性。当然，这里的程序跑在不同处理器上，共享同一块内存。虽然现在不说多处理器了，都说多核，多线程，但是问题的本质是没有变的。就是多个执行单元一起完成一个任务，并且通过共享存储单元的方式通信，在这种情况下，底层的系统需要提供什么样的支持，才能保证计算的结果和程序员的预期是一样的。

学习英语第三周

阅读英文原著

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

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

下面是关键数据：

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

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

硬件内存模型论文阅读

引言

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

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

内存模型的验证论文阅读

动态验证

Hangal2004

• 论文名 Hangal S, Vahia D, Manovit C, et al. TSOtool: A program for verifying memory systems using the memory consistency model[C]//ACM SIGARCH Computer Architecture News. IEEE Computer Society, 2004, 32(2): 114.

• 主要内容

  • 实现工具TSOtool，用于检测多处理器的共享内存系统
  • 内存模型TSO
  • 随机生成包含data race的程序
  • 提出多项式时间算法，incomplete
  • 检测出商业系统中的设计错误
  • 根据内存模型定义一种次序关系，通过程序及结果构造有向图， 在图中找环
  • 时间复杂度：最坏O(n^5)

• 参考文献

  • 验证SC的复杂度, 将问题定义为VSC, VSC-read(map read to write), VSC-conflict(VSC-read + total order of write): Gibbons P B, Korach E. Testing shared memories[J]. SIAM Journal on Computing, 1997, 26(4): 1208-1244.

Manovit 2005

• 论文名 Manovit C, Hangal S. Efficient algorithms for verifying memory consistency[C]//Proceedings of the seventeenth annual ACM symposium on Parallelism in algorithms and architectures. ACM, 2005: 245-252.

• 主要内容　

  • 将vector clock引入TSOtool工具
  • 为VSC-conflict问题提出一个多项式算法
  • 为VSC-read提出多项式算法，快速，有效，但不完备
  • 时间复杂度：O(k*n^3)

• 参考文献

Manovit 2006

• 论文名 Manovit C, Hangal S. Completely verifying memory consistency of test program executions[C]//High-Performance Computer Architecture, 2006. The Twelfth International Symposium on. IEEE, 2006: 166-175.

• 主要内容

  • 在TSOtool中引入回溯，使验证TSO内存模型的算法完备
  • 时间复杂度: O(p*n^3)

• 参考文献

学习英语第四周

阅读英文原著

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

学习英语第五周

阅读英文原著

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

学习英语第六周

阅读英文原著