TLA+是分布式领域大名鼎鼎的Turing 获得者 Leslie Lamport 发明的针对数字系统（算法，程序，计算机系统）的一种high-level 建模语言。TLA+专门为并行和分布式系统所设计，high-level意味着在代码之上的更高的设计抽象，在我们正式开始写下第一行代码之前，TLA+就可以帮助我们设计并验证一个复杂系统。
简单来讲，TLA+的任务用严格的数学语言去刻画（specify）一个系统中可能允许的所有行为，即，它在一次执行过程中所有可能达到的状态。TLA+没有办法直接帮我们产出任何一句有实际生产意义的代码，但它给我们提供了一个新的思考方式和设计工具，学习和理解 TLA+ ,无疑可以帮助你成为一个更好的编程者和工程师。
本系列博客可以看作TLA+的学习心笔记和心得，主要学习资料为The TLA+ Video Course和《Specifying Systems》。
本文为本系列的第一篇，作为系列的序篇主要谈一些TLA+学习过程中产生的主观体会，后面的章节会递进的介绍TLA+的语法和设计细节。
Why TLA+? : 可分析抽象的意义
相比于传统的串行计算，并行和分布式计算的开发，研究和验证难度都要高上好几个数量级。一方面，多个异步节点的并发系统中可能的行为数量相比单节点可能有指数级别的倍增，另一方面，人类的大脑并不擅长处理并行，我们很容易遗漏掉一些边界情况，给系统留下一些不易发现的bug。
与此同时，随着技术的进步，计算机的系统结构越来越多样越来越复杂，这导致系统研究成本进一步居高不下，在开发和研究某一个新型系统时，往往要经过原型系统实现和基准程序测试两个成本极高的阶段，才能对系统的性质进行实质的分析和调整。
因此，我们想要找到一种好的系统刻画方法，可以忽略掉一个并发系统繁杂的实现细节，抓住其本质特征，最好能在我们用代码实现之前，就可以分析系统的主要性质，换言之，我们想要一种好的针对系统的可分析抽象。
抽象到底是什么？lamport给出的解释是“Simplifying by removing details is called abstraction.”
抽象是所有的科学技术学科中都共有的一个重要方法，同样在计算机领域领域中也并不是一个陌生的概念。比如，算法就是一个经典且优秀的可分析计算抽象，学习、理解、研究一个算法，并不需要一定将其转化成可以在计算机上运行的代码，往往用简洁的伪代码形式，就可以分析它的重要性质，比如时间复杂度、空间复杂度，同样也可以通过严格的数学推导证明它的正确性。
有了类似算法这种可分析的抽象，我们就可以不再依赖具体的实现技术（比如如何存储数据和访存），来实现对本质特征地刻画和研究。如果系统领域也有类似算法这样优秀的可分析抽象，我们就可以超越原型系统实现和基准测试，改善现有系统研究效率低下的弊端。
我们之前说过，并行系统有特别的研究难度，这同样也导致了对复杂计算系统进行刻画的高难度。但其实，一个复杂并发系统中的行为，总可以找到一个顺序执行的程序来等价的模拟。TLA+巧妙地用一个单一的状态机的时序状态变化，利用数学中的一阶逻辑和集合知识，来模拟复杂的异步和并发系统。
TLA+的正确性和实用性已经在实际的工程中得到了验证，比如，Amazon在六年前（2014），就有7个团推和14个复杂的大型项目用TLA+进行了形式化刻画和验证，找到了许多在代码层面难以发现的bug。关于Amazon对于TLA+的实践工作，可以参考他们在2015年发表的论文：《How Amazon Web Services Uses Formal Methods》。
在后续的文章中，我们将详细的描述如何用TLA+刻画一个系统。值得注意的是，TLA+提供了一个优秀的抽象的工具和方法，但它没有教我们如何做抽象，想要正确且优雅地刻画一个系统的本质，还需要有系统领域丰富的知识和经验，同时有足够的抽象思维能力。TLA+提供的抽象方法也并不能完全替代原型设计和基准测试，但他能在我们进行具体的实现之前，就对我们的系统进行多次的迭代和更改，从而大幅减少研究成本。
学习TLA+最难的地方就是如何学会用抽象的思维去思考一个系统，学会抽象将对我们的系统设计大有裨益。
Why Mathematics? : 数学是抽象的语言
应该选取什么样的语言去刻画一个复杂的系统？
显然，自然语言（英文或者中文）不是一个好的答案，尽管某种程度上自然语言更适合人们特别是初学者理解，因此各种系统的基础教程中往往还是用自然语言配合图解的方式去阐述系统的性质和工作方式。但要作为抽象的语言，自然语言显然还不够简洁，更不够精确。
Lamport在TLA+中给出的答案是ordinary，simple math , 而没有选择某一门编程语言，或者类似编程语言的伪代码。对抽象的需求而言，编程语言仍然达不到最理想的简洁程度。在系统抽象中，我们想要说明的不是系统要干什么，而是可以干什么，而编程语言更擅长的是前者，后者则更适合用数学公式去刻画。
当然，类编程语言也并不是不能刻画抽象，考虑到很多程序员可能对数学的语法和概念比较陌生和抵触，Lamport还发明了一种接近C语言的语言PlusCal供他们使用，PlusCal可以在形式化验证之前被自动地翻译为TLA+。PlusCal只是对TLA+一种包装，牺牲了TLA+中简洁精确的数学抽象能力，我对其语法并不了解，本系列博客也并不会涉及，如有兴趣和需要可自己搜索学习。
作为中学搞数学竞赛、本科数学系出身的我而言，对数学自然一直保有一种特殊的情感，因此允许我再拿出一些篇幅讲述一些我对数学和抽象的理解。
数学学科的一项主要工作就是将客观世界中的数量（代数）、空间（几何）规律抽象提取出来，并用严格的数学语言对其进行刻画，让这些规律可以适用于其他所有的科学学科以及我们的日常生活中。
比如，最简单的计数以及加减乘除的运算，就是对客观规律的抽象，我们考虑计数和运算的规则时，不再去关心它针对的对象是谁，它可以是物理世界中任意可以被计数的东西，我们把它们共有的计算的规则提取出来抽象成数学的公式。
随着人类文明和数学科学的发展，我们逐渐从客观世界中抽象出更多的运算规律，比如指对数、微积分等等。同时，由于我们希望能更方便的定义更多复合的运算，于是有了映射和函数抽象，我们希望更好的指出函数的定义域和值域，于是有了集合的抽象。函数和集合的抽象，也是我们将在TLA+中使用的重要数学定义。(有关TLA+所需的数学基础，本系列文章中不会再花篇幅赘述，需要的可以参考《specifying system》的第一章和第六章)
当然抽象不并等于数学的全部，至少在我的认知里，推理演绎的证明工作也是数学中不同于抽象的一个重要部分。
虽然我学了很多年的数学，可是直到读研接触了一些学术性的工作，特别是最近半年接触TLA+后才体会到，原来在我之前十余年的数学学习中，我所学习到的只是理解抽象的能力，而从未上升到去刻画乃至提取抽象的高度，甚至我当时也许从未领悟到抽象一词究竟是何意义。
本科有一门课叫做近世代数，又名抽象代数，当时的主讲老师有一句名言，“一切小技巧都是垃圾”，一直当作段子去听，直到近来才感觉到稍稍理解到一些其中的含义。
Why Temporal Logic? : 计算思维和状态机
纯粹数学更关心如何分析客观的数学定理和规律，而不太care如何用它们解决实际问题。
当我们用数学的运算规律解决具体问题时，这个过程就称为计算。计算过程就是解决某个问题的有限个计算步骤的执行序列，而计算思维就是要精确地描述信息变换过程的执行序列，用来构造地解决某个问题。
一个计算过程可以通过人脑（可配合纸笔）来执行，也可以通过计算机来自动地执行。
计算机是一个庞杂的学科，但他最主要的工作就是研究如何自动执行一个计算过程，有的工作着眼于如何加速计算，比如各种硬件架构、应用框架以及算法的优化，以及用并行的方式加速运算，有的工作着眼于如何解决还未解决的计算问题，为它们发明新的算法（包括现在最热门的人工智能），h某种程度上来说，计算机可以看作一门应用数学。
此外，计算机领域还有一些看似与计算过程无关的工作，比如存储、通信和人机交互（包括web前端、移动端设计）等等，但其实这些工作要么是为了计算所服务，要么是为了让计算得到的结果产生更好的价值，这些工作也许可以看作应用计算机（本段有点扯远）。
前面我们讲过抽象是所有科学学科中共有的研究方法，当然计算机领域的前辈们也提出了多种通用的计算抽象，比如大名鼎鼎的图灵机，以及Post模型、Minsky机器等等；此外，使用编程语言，硬件描述语言（如verlog)，各种自动机，也可以描述相应的各种数字系统。但以上所有的抽象，我们都可以用状态机等价的描述，这也是TLA+选择状态机的理由。
刻画一个完整的状态机需要给出它的状态，以及当前状态与下一步状态的变化规则，这种状态迁移正是要用我们着重提到的时序逻辑来刻画，它很好地将计算思维中重要的时间维度抽象出来，并将连续的时间抽象成离散。
不管用人脑还是电脑完成一个计算过程，都需要消耗一定的时间。所以我们所有的计算步骤并不能同时完成，而是要指定它们的先后顺序，也就是状态机中的状态迁移。有的步骤需要其他步骤的输出作为输入，而在复杂的并发系统里，还要考虑进程间的通信等更复杂的因素。
数学和逻辑领域中并不会特别关心时间的概念，它允许我们量化我们关心的任何变量，并将其作为一个维度加入我们的量化空间中。时间在真实的物理世界中是个连续的量，在真实的计算机计算过程也是一个连续的执行，但是我们在考虑计算抽象的时候，我们只想关心计算的正确性，所以我们只要关心时间逻辑上的先后顺序，而不用关心具体的时间长短。因此，我们将时间抽象成一个离散的执行序列。
在经典的逻辑中增加一个特殊的离散时间维度，便有了时序逻辑。TLA+中状态机用状态的转移来刻画系统的行为，每种状态用变量的assignment来刻画。我们需要提前定义好我们描述状态所需要的变量，时序作为一个特殊的变量维度不需要我们再去专门维护，他隐藏在了每个状态转移公式之中。
时序逻辑是TLA+的一个核心思想，用单一状态机来刻画异步系统，看似不可思议，实则巧妙而自然。Lamport给出的TLA+的basic abstraction 就是：
An execution of a system is represented as a sequence of discrete steps.
小结
本文作为系列的序篇，主要为我的一些主观感悟和胡思乱想，试图阐述一下TLA+作为一个系统可分析抽象出现的必要意义，和TLA+选择数学语言和时序逻辑的必然原因。
接下来的文章中，我们将使用lamport在视频课程和《Specifying System》中的一些具体案例，具体阐述怎么用TLA+刻画和验证系统。
(完)
