201707 The Science of System Design (TLA Plus) 学习笔记 (0) - xiaoxianfaye/Learning GitHub Wiki
- The Science of System Design
- 0 Preface
- 1 Introduction to Course
- 2 Introduction to TLA+
- 3 State Machines
- 4 Temporal Logic of Action
- 4 Essence of Concurrency
- 5 PlusCal
- 6 Summary
- 7 Readings
老师在课程简介中写到：
我们都知道，随着系统复杂性的升高，人在设计、编码和运维方面发生错误的概率也会随之升高。这些隐藏在系统核心中的错误会伤害系统的可用性，造成极大的经济损失，并增加系统的开发、维护成本。尽管我们花费大量努力避免那些不必要的复杂性，但是系统的固有复杂性可能依然很高。并且，我们还必须要在交付新特性、发布新服务时，对系统核心的正确性抱有极大的信心。
这些信心从哪里来呢？一般来讲，我们会采用很多方法，包括：编写设计文档、进行设计评审、静态代码检查、代码评审、压力测试、故障注入测试等等。这些技术都是必要的，但是对于高度复杂的系统(比如：并发和分布式系统)来讲，还远远不够。由于这类系统的固有复杂性很高，一些隐藏在系统设计核心中的微妙错误是很难通过这些方法发现的。
软件系统设计文档往往不能做到精确，一般都用自然语言和一些图示进行表达，因此无法通过工具自动检查设计的正确性。从精确性方面来讲，只有代码才是精确的(这也是有人说“源代码就是设计”的原因)。但是，编程语言编写的代码中混杂了很多实现层面的决策和细节，无法清晰的呈现出设计层面的规范，因此会造成设计难以理解，难以保证实现的正确性，并且对于一些微妙的错误也难以调试。在这种情况下，为了提升对正确性信心，只能采用强化条件、加强测试等方法，而这则会增加不必要的设计复杂性和成本。因此，越来越多的软件领导企业开始寻找新的设计表达方法。
我们希望可以清晰、准确地描述系统的行为而又不陷入繁杂的细节，可以用几百行代码就可以表达极其复杂的设计。我们希望有工具可以在设计层面快速地检查出各种失败条件，并自动给出导致失败的用例。我们希望表达方法和工具能解决真实世界的问题，并对一线设计师、程序员友好。这样的表达方法和工具存在吗？答案是：存在！表达方法是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!
安装JDK1.8.0以上版本和TLA Toolbox1.5.3版本，Toolbox的安装方法见如下链接：
http://lamport.azurewebsites.net/tla/toolbox.html
安装完毕后，确认安装目录中有toolbox.exe文件(Windows系统)，点击确认能正常运行。
下面两个链接是对Leslie Lamport的两个简短采访：
- http://video.tudou.com/v/XMjI5MjI5NzY4NA==.html 【Faye】链接貌似失效了，可以在优酷上搜索Leslie Lamport。
- https://channel9.msdn.com/Series/Microsoft-Research-Luminaries/Leslie-Lamport-ACM-2014-A-M-Turing-Award-Winner
其中谈到了他的工作对计算机科学的影响，他当前的兴趣所在(如何让人更好地思考)以及他对数学的热爱。
本次课程的授课时间从2017年7月20日到7月23日，共三天半。在这次课程中，
TODO 待整理补充
- 7月20日上午 什么是计算：数学的视角
- 7月20日下午 TLC介绍、TLA+简介和训练
- 7月21日上午 时态逻辑：safty、liveness等
- 7月21日下午 时态逻辑实战和正确性的关键
- 7月22日上午 PlusCal介绍和实战练习
- 7月22日下午 编写TLA+ spec的要点和原则、实战练习
- 7月23日上午 答疑和探讨
根据授课内容，整理出本次课程的学习笔记。
详见 201707 The Science of System Design (TLA Plus) 学习笔记 (1) Introduction to Course。
详见 201707 The Science of System Design (TLA Plus) 学习笔记 (2) Introduction to TLA+。
详见 201707 The Science of System Design (TLA Plus) 学习笔记 (3) State Machines。
详见 201707 The Science of System Design (TLA Plus) 学习笔记 (4) Temporal Logic Of Action