201707 The Science of System Design 培训笔记 - xiaoxianfaye/Learning GitHub Wiki
The Science of System Design
using TLA+, PlusCal and TLC
1 Preface
1.1 Introduction
老师在课程简介中写到：
我们都知道，随着系统复杂性的升高，人在设计、编码和运维方面发生错误的概率也会随之升高。这些隐藏在系统核心中的错误会伤害系统的可用性，造成极大的经济损失，并增加系统的开发、维护成本。尽管我们花费大量努力避免那些不必要的复杂性，但是系统的固有复杂性可能依然很高。并且，我们还必须要在交付新特性、发布新服务时，对系统核心的正确性抱有极大的信心。
这些信心从哪里来呢？一般来讲，我们会采用很多方法，包括：编写设计文档、进行设计评审、静态代码检查、代码评审、压力测试、故障注入测试等等。这些技术都是必要的，但是对于高度复杂的系统(比如：并发和分布式系统)来讲，还远远不够。由于这类系统的固有复杂性很高，一些隐藏在系统设计核心中的微妙错误是很难通过这些方法发现的。
软件系统设计文档往往不能做到精确，一般都用自然语言和一些图示进行表达，因此无法通过工具自动检查设计的正确性。从精确性方面来讲，只有代码才是精确的(这也是有人说“源代码就是设计”的原因)。但是，编程语言编写的代码中混杂了很多实现层面的决策和细节，无法清晰的呈现出设计层面的规范，因此会造成设计难以理解，难以保证实现的正确性，并且对于一些微妙的错误也难以调试。在这种情况下，为了提升对正确性信心，只能采用强化条件、加强测试等方法，而这则会增加不必要的设计复杂性和成本。因此，越来越多的软件领导企业开始寻找新的设计表达方法。
我们希望可以清晰、准确地描述系统的行为而又不陷入繁杂的细节，可以用几百行代码就可以表达极其复杂的设计。我们希望有工具可以在设计层面快速地检查出各种失败条件，并自动给出导致失败的用例。我们希望表达方法和工具能解决真实世界的问题，并对一线设计师、程序员友好。这样的表达方法和工具存在吗？答案是：存在！表达方法是TLA+和PlusCal，工具是TLC。
TLA+是Leslie Lamport (2013年图灵奖得主) 近半个世纪的研究成果，和其他类似技术(dependent type，Coq等)相比，TLA+更加简单和注重实效，它一开始就把目标人群定位成解决现实复杂问题的工程师，而不是做学术研究的数学家和逻辑学家。这和Lamport一直投身工业，以解决工业界实际问题为目标密不可分。目前的整个互联网、云计算系统的核心基础都建立在Lamport的两篇论文(一篇是关于分布式系统中的时间问题的，一篇是关于分布式系统中数据一致性问题的)之上就是最好的证明。
TLA+的核心是时态逻辑加上集合论和一阶逻辑(都是一些初等数学)，是Lamport在时态逻辑基础上的天才发明。那些让绝大多数软件从业人员带着敬畏避而远之的复杂系统(比如：分布式系统、并发并行系统、拜占庭系统等等)，都可以用很少的几个布尔逻辑原语进行表达、验证和证明，而这类系统仅靠测试是无法发现设计层面的一些微妙错误的。有了TLA+来保证和维持设计的正确性，就可以大胆弱化条件、简化设计，可以采取创新性的优化手段来消除瓶颈、提升性能，可以省去很多不必要的测试工作，可以极大地提升DevOPS的可靠性。总之，这个正确性的保证为软件生产、交付环节的各种创新提供了坚实的基础。目前业界很多知名公司(微软、Intel、Oracle、Amazon等)使用TLA+的案例都很好地证明了这一点。
在本次培训中，我们将教授大家如何在更高的维度做思考、如何从数学的视角理解定义计算、如何用数学语言清晰地表达思考并写出高层次的系统规格说明、如何自动生成模型去验证规格说明的正确性、如何去证明规格说明的正确性等。所采用的工具正是是TLA+、 PlusCal(可以看作是TLA+的语法糖，供患有数学恐惧症的程序员使用)和TLC(模型检查器，可以根据specification自动生成模型验证specification的正确性)。
很多人一听到数学就觉得恐惧，造成这个结果的主要原因是教育。在本课程中，希望能消除大家对数学的误解，我们会通过深入浅出的讲解和大量实战，让大家领略到数学之美，喜欢上数学，我们对此抱有信心。通过本课程的训练，你的抽象能力、思考的深度和清晰性、表达能力都会得到大幅的提升。即使你在工作中不使用TLA+，通过本课程的训练，也会让你写出更加简单、高效、正确而富有逻辑美的代码，而这是你之前学习的那些设计技巧远不能做到的。一旦你学会了TLA+，你的工作就更加接近科学家，因为用数学公式表达对问题的理解和认识，用数学工具解决问题是所有科学工作的共性。
当然，这不是一件容易的事情，本次培训充满挑战，同时充满乐趣 ... ...
Happy Learning!
1.2 Requirement
1.2.1 Software
学员自带笔记本电脑，培训前在电脑上安装JDK1.8.0以上版本和TLA Toolbox1.5.3版本，Toolbox的安装方法见如下链接：
http://lamport.azurewebsites.net/tla/toolbox.html
安装完毕后，确认安装目录中有toolbox.exe文件(Windows系统)，点击确认能正常运行。
1.2.2 Preparation
下面两个链接是对Leslie Lamport的两个简短采访，有兴趣的同学可以先看看：
http://video.tudou.com/v/XMjI5MjI5NzY4NA==.html
其中谈到了他的工作对计算机科学的影响，他当前的兴趣所在(如何让人更好地思考)以及他对数学的热爱。
1.2.3 Schedule
- 7月20日上午 什么是计算：数学的视角
- 7月20日下午 TLC介绍、TLA+简介和训练
- 7月21日上午 时态逻辑：safty、liveness等
- 7月21日下午 时态逻辑实战和正确性的关键
- 7月22日上午 PlusCal介绍和实战练习
- 7月22日下午 编写TLA+ spec的要点和原则、实战练习
- 7月23日上午 答疑和探讨
2 Content
2.1 2017-07-20 Morning
什么是计算：数学的视角
2.1.1 computer "SCIENCE"
2.1.1.1 The heliocentric theory
日心说 布鲁诺
人类大脑的进化跟不上科学的发展。
动物大脑打断理性思考，元认知能力调动起来，可以长时间理性思考，会带来深远的成就感和愉悦感。
设计系统，有机械动作和清晰思考，清晰思考被压抑，通过训练把清晰思考调动起来，设计的系统就好理解了。
2.1.1.2 Leslie Lamport
不能给出最好的解决方案，而是识别出最好的问题，归结于长时间深入思考。
lamport.azurewesites.net/pubs/pubs.html
2.1.2 CORRECTNESS
我们的课程内容是关于“正确性”的。
2.1.2.1
编译器就是一个函数，即使再复杂，因为输入输出是固定的。
一些系统是可以用函数表达的，一般是小模块或类似编译器这种独立的系统。但大部分系统是无法用函数表达的。
正确性是基础，没有正确性，其他都是零。
Design Review、Code Review、Simple Design、Test、… …
固有复杂性、偶然复杂性
通过简单设计减少偶然复杂性。
测试。贝叶斯模型。点是独立分布的，测试点越多，正确率越高。
希望系统百分之百正确，而不是一个概率。
希望设计简单，怎么知道简单设计不会引入错误？首先应该有一个正确性的保证，才能做简单设计。
2.1.2.2 Foundation of Software Engineering
正确性是软件工程的基石。
如何用科学的方法表达你希望系统做什么东西。
2.1.2.3 Paper
软件工程有很多维度，正确性和好的设计方法等是正交的。
2.1.2.4 The Art of Debugging
系统运行起来，出问题了，最有效的方法就是调试。
对系统行为的一种期望——猜测。跟设计方法无关。
形式化证明方法的统一框架。
Note P1
并发系统，断点就不好用了，日志。日志也是断，但不影响race condition。
如何形式化？abstract如何违反了property的约束，如何保证Implementation一定有同样的问题呢？Implementation复杂很多。
把系统行为序列描述出来，如何表达状态、迁移、属性，而且Abstract的问题一定是Implementation的问题(保证隐含关系)，所有形式化的方法都是解决这个问题。
这样，并发、非并发就没区别了。
形式化Debug
2.1.2.5 Checking a Large Routine
Alan Turing
An Early Program Proof by Alan Turing
Manchester computers
Robert Floyd, Tony Hoare
Lamport 1977
语言派&计算派
- 语言层面的视角：如果语言不能描述，这个东西的形式化方法就不存在。如果做成，可以做end to end的验证，因此很有吸引力。
- 计算层面的视角：关注计算层面的概念。让Control state显式化。
不可能用一个复杂的东西去描述一个很简单的东西，肯定搞复杂了。
冰法跟顺序没有任何本质区别
2.1.2.6 Temporal logic
没有必要为了解决工具的纯粹性，而增加复杂度。
Temporal logic很复杂，做了很大简化，TLA。
2.1.2.7 TLA (Temporal logic of Action), 1994
TLA：行为的描述跟对行为属性的描述是一样的。而且高层、底层都可以用TLA描述。
TLA+：X、Y等是TLA的静态部分。TLA本身是描述行为的，是动态的。PLUS是如何描述静态状态。
这篇论文写得非常好。
数学最简单。集合论和 ？？逻辑
严格推理是避免微妙错误的手段。
形式化的手段是的推理变得很简单。
Paper：The Temporal Logic of Actions
2.1.2.8 Use of Formal Methods at Amazon Web Services
2.1.2.9 A real-time operating system designed using TLA+
TLA的抽象主要是基于正确性的。
2.1.2.10
2.1.2.11 Cosmos DB
2.1.2.10 Chris Newcombe, ...
2.1.2.11 CORRECTNESS driven Design
2.1.3 Informal Reasoning
非形式化推理，人能看懂，计算机不能
2.1.3.1 Insert Sort
性质：i之前是有序的，无序就错了。
Note P2
Inductive Invarient 归纳不变性
可以用一个公式描述。
2.1.3.2 Programming Pearls
COLUMN 4：WRITING CORRECT PROGRAMS
白豆是奇数，剩下白豆。白豆是偶数，剩下黑豆。 白豆的奇偶性保持不变。
Inductive Invarient：每一步，白豆的奇偶性保持不变。
两个都黑：b - 1，w 0 两个都百：b + 1, w -2 一黑一白：b - 1, w 0
Inductive invarience + 数学归纳法
Note P3
2.1.3.3 Teaching Concurrency
Thinking Clearly
建议阅读
并发性是理解并发系统的关键。
读x和写y是atomic操作，不会被打断。
Property：当每个进程stop的时候，肯定有一个y[i]等于1。
一个进程只跟该进程当前状态有关，跟前面的进程无关。
找到一个Inductive Invarience，而且可以证明。
Inductive Invarience
第一步：如何把问题变成状态序列 n=1时，状态序列是什么 n=2时，状态序列是什么
n=1时， n=2时，Note P4
所谓的并发、不确定性在本质上是一样的，只是看如何解释。
并发是一种幻觉。
对于不确定性的描述，可以用公式精确描述涵盖。
用一种逻辑涵盖了所有系统。
Debug时关心的是正确性问题。不关心实现语言、设计模式等。
2.1.4 What is a COMPUTATION
实用化、可伸缩性、不那么复杂。
什么是一个计算？如何描述一个计算？
2.1.4.1 Computation and State Machine
这篇论文一定要看
为什么提炼出来的抽象状态能够证明实现是正确的。
Preface
用数学表达，不要再发明语言表达了。
每一个可以计算的实体都可以表达为一个状态机。
正确性和代码的清晰组织是正交的。
2.1.4.2 Computation
沃尔夫综合症：混淆了语言和现实
State machine
bean
所有行为、状态都已经存在了。写出一个条件，把期望的状态过滤出来。
等号就是数学上的等号，不是赋值，是boolean过滤。
从整个宇宙行为里把我想要的行为过滤出来，而不是行为不存在、定义出来。 达到完美容纳不确定性的目的。
宇宙蕴含了一些可能，我们找出我们需要的。
2.1.4.3 Specifying a State Machine
常微分方程描述动态连续系统
TLA+：等同于解决动态离散系统的常微分方程
X' = X + 1 这是一个Relation
S X = 0 0 1 2 3 4 满足R 0 1 4 。。。不满足R
factorial
2.1.4.4 State Machine in Action
X： loop P; C endloop
Init P PC = 0 P PC = 1 C
PC：控制状态，隐含的
Note P5
两阶段握手协议
理解一个系统最好的方法是，举个简单例子把序列写出来。
Note P6
如果能够证明y是x的实现，就是说，x上满足的，y上一定满足。 x就是y的抽象。就可以通过证明x是对的，y是对的。 问题在于，如何证明y的行为都是x的行为。
y的所有行为的集合是x的子集。x的属性，y肯定满足。
refinement：精细化
抽象和实现，层次越高，确定性越多。越低，不确定性越多
通过一个公式描述一种或多种不确定的状态行为。
Y => X Imply Y的所有行为都是X的行为。
Note：P7
Abstraction/Implementation
State Machines Papers
上午的核心：debug的图如何形式化、如何理解State Machine。从无限行为里筛选出行为。
2.2 2017-07-20 Afternoon
TLC介绍、TLA+简介和训练
Introduction to TLA+
TLA：对Init和Next做一个提升，更加优雅，更简单地描述更复杂的东西 TLA：只关心序列，整体行为的描述 TLA+：关注具体的行为，Plus：一阶逻辑、集合论、函数。
首先要写、其次要用数学写、还要用formal形式化地写。
用数学解决问题跟用编程语言解决问题的区别。
2.2.1 Simple Math
Propositional Logic 命题逻辑 值、以及对值的操作符。
值：TRUE、FALSE 操作符：/\ 。。。
TRUE、FALSE也是表达式，原子表达式
F => G 如果整数X大于4，X一定大于2。 X = 5 TRUE X = 3 TRUE
Tautology：永真式
Sets
Predicate Logic
任给：对于集合中的所有元素 存在：集合中的存在一个元素 定义在一阶逻辑上，任给和存在只能修饰值。
对偶关系
用任给定义存在。
Set Constructor
空、字面量、filter、map
The Mathematical Definition of GCD
最大公约数
ASCII Representation
CHOOSE 集合里有一个或多个X，使得P为真，选一个出来。 可以认为CHOOSE是一个SUM，有一个拿出来就行。 CHOOSE得到一个值。 可能有多个值，CHOOSE永远选一个值，是确定性的。
ChooseOne：从S中选出唯一一个满足P的元素 (2, 3, 5)：ChooseOne 2 (2, 3, 4, 5)： ChooseOne Undefined
CONSTANTS：序列不能变化 VARIABLE ASSUME：定义一些Check
TLA里没有类型
Definitions：可以理解为简易写法 替换发生在脚本运行之前，大概理解为宏。OP支持递归
Functions：完全数学意义上的Function S是定义域。
Simple Operator
Higher-order Operators operator也可以作为参数
LET IN 用来定义局部的operator
<<>>其实是个函数 DOMAIN：返回函数的定义域的集合
<<"hello", "world", "!">> 在TLA中式一个Function f Function是从定义域Domain到值域Range的映射
f[1] = "hello"
f[2] = "world"
f[3] = "!"
DOMAIN是一个Operator，接受一个f，返回这个函数的定义域。
chess
\X 集合的笛卡尔积
Structures/Records 也是TLA中的Function
2.3 2017-07-21 Morning
时态逻辑：safty、liveness等
形式化表达
TLA+里复杂的逻辑都是用Functions表达的
把函数理解成编程语言的HashMap，key是domain，value是range
Function Set 所有函数定义域是A，值域是B的子集的函数都属于 A的元素个数是N，B的元素个数是M，[A -> B]的个数是M^N个。
Paper 如何编写二十一世纪证明 Calculus
The Standard Model
用TLA建模是，关心系统的变量和Step的大小。
什么是变量？ 变量的初始状态 Next
编程语言表达不出不确定性。没办法形式化地了解系统行为。 TLA+可以以统一的形式描述不确定性。一个精确的表达蕴含了所有的不确定性。
Model Check是对formula的解释。
Deadlock TLA+ 如果不指定，Next是无限的。 一个序列行为终止了，而且你没有告诉终止条件
什么是一个属性 X always equals 3 所有行为序列里，X=3，这些序列。。。
一切都是行为的集合，系统和属性都是，系统的行为是满足属性的集合的子集。
2.4 2017-07-21 Afternoon
时态逻辑实战和正确性的关键
x = x + 1 永远是FALSE x' = x + 1 当前状态和Next状态满足这个公式
spec是行为集合，Property也是行为集合，希望spec行为集合是property行为集合的子集。
** Invariant and Inductive Invariant **
Invariant 表明结果正确 Inductive Invariant 表明过程正确
Euclid's Algorithm
找到Inductive Invariant和Invariant，证明Inductive Invariant蕴含Invariant，就可以证明结果正确并且过程也是正确的。
一个程序的正确性一定是全局的。
** Temporal Logic of Action **
微积分是动态连续系统的无穷和极限 TLA是动态离散系统的无穷和极限
时态逻辑关注行为，是对行为的论断。
为什么程序会有Bug？ 我们一直通过赋值在创造行为。我们描述想要什么，别人才能给你什么。 两个完全不同的视角。
Init + Safty + Liveness
2.5 2017-07-22 Morning
PlusCal介绍和实战练习
随意地写Liveness是有危险的。一不小心会影响Safety。 Liveness一定不能影响Safty，Safty是保证正确性的。否则Safty合理的行为被抛弃掉，就出错了。
Fairness
坏的事情不发生：好的事情发生或者没事
为什么这种类型的公式能满足所有系统？ 为什么TLA适用所有系统？是否存在不适用的？
Stuttering的前提是一定要Enabled
** Essence of Concurrency ** 并发的本质
在并发系统里，一个step是atomic的
并发的本质是不确定性
行为之间有共享数据。
非并发问题
把非确定性问题确定化。
推演并发程序的时候，每一个进程的状态只跟自己的状态有关。
2.6 2017-07-22 Afternoon
编写TLA+ spec的要点和原则、实战练习
实现语言是为了产生高效的机器码
A Big Example
操作系统调度行为存在不确定性。
TLA帮我生成所有Producer和Consumer的序列
** PlusCal **
在PlusCal中，用Label指明Label中的是Step，Atomic的，不能被打断。
** TheProgram **
CAS原语、乐观锁
2.7 2017-07-23 Morning
答疑和探讨