作者：罗胜金
版权声明：欢迎转载，请注明原作者
1. 前言
下文将总结我的TLA+技术学习心得，分为道（理论）、法（方法）、术（技术）、器（工具）、用（案例）五个主要部分。
2. TLA+之“道”——时态逻辑
如何保证和证明软件系统的正确性？
正确性，是系统最重要的特性。
CORRECTNESS driven Design。
一般认为，正确性是很难证明的，尤其是并发系统的正确性，因为其行为变化的可能性太多。但是，如果能够把系统的状态/行为抽象为时态逻辑，再结合数学分析方法，就可以判断系统是否正确。
TLA+与Debug的类比
Debug的原理是通过观测软件的属性和状态，判断软件执行过程的正确性。
属性和状态随时间的变化过程，就是TLA+中的“时态”。
通过分析系统的状态序列变化，可以找到系统特性（规律）
1） 黑子白子问题的例子
壶中有黑子、白子各若干，每次取出2子。若2子同色，则放回1个黑子；若2子不同色，则放回1个白子。问最后壶中为黑子还是白子？
举例分析系统状态序列变化。下图中：B为黑子，W为白子，S为状态：
说明：公式(N - Wi) % 2 == 0，N、Wi分别为壶中白子最初、最后数量，公式说明壶中“白子奇偶性不变”，这就是系统的特性（规律）。
2）一个简单的多进程并发例子
Lamport论文中给出的多进程并发简单例子——
有N个并发的进程，进程号i为0～N-1，
每个进程的初始化，X[i]:=0，
每个进程执行后，
X[i]:=1
Y[i]:=X[(i-1) mod N] // 当i = 0，((i-1) mod N) = N-1
如何证明：这个系统满足——当所有进程停止后，至少有一个进程的Y[i]:=1？
举例分析如下——
假设系统中只有2个进程，进程号为0、1，每个进程执行A、B两步（说明：A——X[i]:=1，B——Y[i]:=X[(i-1) mod N]），那么：
【进程0执行后】
P0A: X[0]:=1
P0B: Y[0]=x[1]
【进程1执行后】
P1A:X[1]:=1
P1B:Y[1]=X[0]
系统所有的可能执行序列如下（6种）：
P0A P0B P1A P1B ——Y[1]=1
P0A P1A P0B P1B ——Y[0]=1 Y[1]=1
P0A P1A P1B P0B ——Y[0]=1 Y[1]=1
P1A P1B P0A P0B ——Y[0]=1
P1A P0A P1B P0B ——Y[0]=1 Y[1]=1
P1A P0A P0B P1B ——Y[0]=1 Y[1]=1
由分析结果看出，每种可能序列，都至少有一个进程的Y[i]:=1。
当然，这是用小样本例子分析的结果。如果要证明正确性，则需要把问题抽象为时态逻辑，用数学分析证明。
3）电影《Die Hard》问题
一个3加仑桶，一个5加仑桶，倒腾出4加仑水：
｛3加仑桶水量，5加仑桶水量｝变化序列——
{0,0} {3,0} {0,3} {3,3} {1,5} {1,0} {0,1} {3,1} {0,4}
这个问题的时态逻辑，又应该如何描述，让数学自动推理得到结果呢？
无疑，对很多问题进行分析，最终我们会发现，问题核心在于其时态逻辑。
那么，如何让计算机高效地帮助我们把问题的时态逻辑分析清楚，证明系统的正确性，给出软件设计人员想要的结果呢？
微软研究院首席研究员、2013年图灵奖获得者，Leslie Lamport大神历时数十年，研究出了一种方法（数理逻辑分析）和一套实用的工具集（TLA+/TLC）。
3. TLA+之“法”——数理逻辑
要清晰的思考，深入的思考
清晰、深入的思考，是个人进步的来源。
清晰的思考，使得TLA+成为一个不容易过时的技术（Leslie Lamport）。
数学，是帮助我们清晰、深入思考的一个工具、一种语言。
软件设计及其语言的复杂性，会干扰我们对业务问题本身的思考。
用数理逻辑表达时态公式（1）
说明：
上图中的符号，大多数来自数学中集合论和逻辑论的基础部分。
其中，相对不易理解的是“X=>Y”，意思是X“蕴含”（imply）Y，意味着如果X为TRUE则Y一定为TRUE，X为FALSE则Y可能为FALSE也可能为TRUE，即X是一个比Y更强的条件。那么，[X]（满足X的集合元素）是[Y]（满足Y的集合元素）的子集。
举例说明，X为n>5，Y为n>1，n为整数，那么显然X是比Y更强的条件,满足n>5的集合[X]是满足n>1的集合[Y]的子集。
用数理逻辑表达时态公式（2）
说明：个人理解，上图中，“方块”符号表示Always（总是），和“任给”符号都是强条件。“菱形”符号表示“Eventually”（最终，总会），和“存在”符号都是弱条件。
用数理逻辑表达时态公式（3）
说明：上图中的数理逻辑公式，参考（1）和（2）不难理解。
用数理逻辑表达时态公式（4）
用数理逻辑表达时态公式（5）
说明：
上图中，[A]_e定义为，系统要么执行A行为（通常A = Next，执行下一步）、要么保持目前状态/属性不变（e’ = e，e通常为系统中的所有变量）。
<A>_e定义为，系统执行A行为（通常A = Next）、并且状态/属性发生变化（e’ /= e）。stutter字面意思是“口吃”，表示重复、状态不变。
[][Next]_v表示“系统总是执行下一步或者保持状态/属性不变”，这正是系统设计者期望的结果，因此是safety（安全）的，意味着坏事不会发生。
[]<><Next>_v表示“系统总是最终会执行下一步并且改变状态/属性”，这是系统保持liveness（活性）的表现，意味着好事早晚总是会发生。
Safety和liveness是软件系统正确性的两个重要因素，Lamport和别的计算机科学家在多篇论文中论述了Safety和liveness的含义和作用，包括：
- Recognizing safety and liveness
- Preserving Liveness: Comments on `Safety and Liveness from a Methodological Point of View'
- Verifying Safety Properties With the TLA+ Proof System
- Proving the Correctness of Multiprocess Programs
- Mechanical Verification of Concurrent Systems with TLA
- Reduction in TLA
- Proving Possibility Properties
用数学（数理逻辑）描述一个系统（包括硬件和软件系统，包括并发系统）的时态逻辑，进而分析、论证这个系统的正确性，这是理论上可行的一种方法。但是，这种方法，如何工程化为一种“技术”呢？这就是Lamport发明的TLA+。
4. TLA+之“术”——TLA+语言
TLA+不是一种传统意义上的编程语言，它的语法大部分来自于实际的数学（数理逻辑），因此可以把TLA+视为一种程序员容易理解的数学语言。
TLA+编码模板
----- MODULE M ----
EXTENDS M1, ..., Mn \\* 引入其他模块，类似#include
CONSTANTS C1, ..., Cn \\* 定义常量
VARUABLE x1, ..., xn \\* 定义变量
ASSUME P1 \\* 假设、假定
\\* Definitions() 类似宏
OP(x1, ..., xn) == exp
\\* Functions 函数
f(x \in S) == exp
TLA+保留字
以下为TLA+语法的保留字，部分保留字的含义和其他编程语言类似。保留字的用法请参考：http://lamport.azurewebsites.net/tla/book.html。
常用操作符
以下为TLA+的操作符，可以看出，其中绝大部分来自数学领域，其含义也和数学公式中的对应符号相同，只是为了方便编写，可以采用ASCII码来代表。保留字的用法请参考：http://lamport.azurewebsites.net/tla/book.html。
个别容易用错的TLA+语法说明
1）Records（记录）类型用法
x == [a |-> 1, b |-> {2,3}] \* “==”表示“定义为”
x.a = 1
x["b"]={2, 3}
DOMAIN x = {"a", "b"}
[a : {1}] = {[a |-> 1]}
[b : {{2,3}}] = {[b |-> {2, 3}]}
2） DOMAIN关键字的用法
DOMAIN(<<"a","b","c">>)=1..3
DOMAIN([a |-> 1, b |-> {2,3}])={"a","b"}
DOMAIN({"a","b","c"}) \\* failed. DOMAIN不能应用于1个non-function(a set of the form {e1, ... ,eN})
用TLA+语法描述好系统的时态逻辑之后，如何验证系统的正确性呢？（实际上，TLA+还可以验证软件系统的性能、时序等其他重要的特性）答案是使用TLA+提供的工具集TLAToolbox/TLC，还可以使用TLA+的语法糖PlusCal。
5. TLA+之“器”——TLAToolbox/TLC、PlusCal
Toolbox/TLC
执行TLA+语句，进行TLC Model Check的工具。
下载地址：http://lamport.azurewebsites.net/tla/toolbox.html
PlusCal
TLA+的语法糖。有C和Pascal两种风格。
建议：先熟悉TLA+语法，具备用TLA+编写时态逻辑的能力，再使用PlusCal。PlusCal用“TLA+注释”的方式编写，写完后，按“Ctrl + t”·，Toolbox可自动将PlusCal翻译成TLA+语法。出问题了，可以从翻译生成的TLA+语句开始分析。
6. TLA+之“用”——验证并发系统的正确性
TLA+的设计，最初用于验证硬件系统设计的正确性，后来延伸到软件系统。
目前，TLA+最有价值的应用之一，是验证并发系统的正确性。
例子一：分析生产者-消费者模型的并发死锁问题
互联网广泛使用经典的生产者（Producer）-消费者（Consumer）模型的消息队列（MQ）组件，例如RabbitMQ、NSQ等，在一些数据库缓存模块中也实现了类似的生产者-消费者模型组件，例如Memcached、Redis等。
在这种模型下，当多个Producer和Consumer进程并发访问消息队列时，如果处理不当，会产生死锁问题。而且，并发引起的死锁一旦发生，很难分析出原因。
例如，我们不妨以Buffer替代消息队列，来分析下面这段Java代码的潜在错误：
public class Buffer<E> {
public final int capacity;
private final E[] store;
private int head, tail, size;
@SuppressWarnings("unchecked")
public Buffer (int capacity){
this.capacity = capacity;
this.store = (E[])new Object[capacity];
}
private int next (int x){
return (x + 1) % store.length;
}
public synchronized void put(E e)throws InterruptedException {
while(isFull())
wait();
notify();
store[tail] = e;
tail = next(tail);
size++;
}
public synchronized E get() throws InterruptedException {
while(isEmpty())
wait();
notify();
E e = store[head];
store[head] = null; // 由GC自动回收
head = next(head);
size--;
return e;
}
public synchronized boolean isFull(){
return size == capacity;
}
public synchronized boolean isEmpty(){
return size == 0;
}
}
上面代码中，wait()和notify()是Object类提供的方法，wait()阻塞当前线程，notify()唤醒等待当前对象的线程池中的任意一个。
这段代码存在着一个死锁隐患。如果想通过Log来Debug出这个死锁问题，代价巨大。有一篇英文文章介绍，国外某位程序员做了多种尝试，最后在一台8核高配机上，跑了18天、产生40亿条消息后，复现了这个死锁。
实际上，要找出这个代码中的Bug，可以用TLA+来对系统建模，分析其时态逻辑的变化过程，找到死锁原因，进而解决它。
TLA+对这个问题的建模：
EXTENDS Naturals, Sequences
CONSTANTS Producers, (* set of producers *)
Consumers, (* set of consumers *)
BufCapacity (* the max numer of messages in the bounded buffer *)
VARIABLES buffer, (* the buffer, as a sequence of objects *)
waitSet (* the wait set, as a set of threads *)
Participants == Producers \union Consumers
RunningThreads == Participants \ waitSet
Notify == IF waitSet # {}
THEN \E x \in waitSet : waitSet' = waitSet \ {x}
ELSE UNCHANGED waitSet
NotifyAll == waitSet' = {}
Wait(t) == waitSet' = waitSet \union {t}
Init == buffer = <<>> /\ waitSet = {}
Put(t) == IF Len(buffer) < BufCapacity
THEN /\ buffer' = Append(buffer, 1)
/\ Notify
ELSE /\ Wait(t)
/\ UNCHANGED buffer
Get(t) == IF Len(buffer) > 0
THEN /\ buffer' = Tail(buffer)
/\ Notify
ELSE /\ Wait(t)
/\ UNCHANGED buffer
Next == \E t \in RunningThreads :
IF t \in Producers THEN Put(t)
ELSE Get(t)
Spec == Init /\ [][Next]_<<buffer, waitSet>>
NoDeadLock == [](RunningThreads # {})
在TLAToolbox中，用TLC运行、检查以上模型，很快（24步，不到2分钟）就复现了并发死锁过程：
上图中，p1、p2、p3为3个生产者线程，c1、c2为2个消费者线程，Buffer（仓库）容量为2。
上图中，死锁发生的过程是这样的：
- 某个时刻，所有“消费者”（c1、c2）和1个“生产者”（p3）站在等待队伍（waitSet）中，仓库中有1个商品；
- 接下来，正在工作的“生产者”（可能为p1或p2，假设为p1）把仓库塞满（放入另1个商品），然后p1要notify()等待队伍中的一个人；
- 这时候，悲剧发生了，p1它notify()的竟然是p3！p3离开等待队伍后，留下所有“消费者”（c1、c2）在队伍中，并且仓库是满的；
- 这时候系统已经回天乏力，因为正开心工作的p1、p2、p3都发现，仓库已经没有地方让它们放入商品，它们只好一一重新进入等待队伍。而可怜的“消费者”们（c1、c2），已经没有任何人有机会notify它们从仓库取出商品（注意：只有完成1次Put或Get后，才有1次notify的机会）；
- 这样，所有人都进入等待队伍，发生死锁。
如此清晰地复现死锁过程后，解决起来也很简单：把Notify()改为NotifyAll()，每完成1次Put()或Get()后，都把所有线程赶出等待队列，就不会发生这个死锁。
例子二：多线程通过缓存访问数据库的数据一致性问题
系统示意图如下——
图中，多个客户线程通过cache操作数据库，每次操作过程是“先读取、再加1、后写入”。
每个线程的执行代码如下——
cache = {}
def increment(id):
x = cache.get(id, None)
if x is None:
x = DB_Read(id)
cache[id] = x
x = x + 1
DB_Write(id, x)
cache[id] = x
软件设计者期望，假设数据库中（key：id）的value初值为0，当N个线程分别操作1次数据库后，数据库中（key：id）的value为N。这段代码能实现吗？
用TLA+的语法糖（PlusCal）建模如下：
EXTENDS Integers
CONSTANTS N, not_set
(********************************************************
--algorithm Cache{
variables cache= not_set, database = 0;
process(Thread \in 1..N)
variable x;
{
t1: if(cache /= not_set){
x := cache;
}else{
t2: x := database;
cache := x;
};
t3: x := x + 1;
t4: database := x;
t5: cache := x;
}
} ********************************************************)
样本数据把N设为2（2个客户线程），在TLC中运行以上模型，分析结果如下：
上图中，在第10步（num=10），当线程0、线程1都执行结束（Done）后，database为“1”，而不是软件设计者期望的“2”。为什么呢？
分析可知，原因是在线程0更新cache值为1（t5）之前，线程1已经取出cache中原来的0值，作为当前操作对象，导致了最终的错误。
分析发现，这是数据库访问的一个常见问题：在数据库数据（本例中为1）和Cache数据（本例中为0）不一致时写入导致。解决方案，是业界成熟的CAS（Compare and Swap，“乐观锁”的一种实现方式）协议——
修改PlusCal建模的“写数据库”部分如下，用TLC分析验证正确：
t2: y := x + 1;
t3: if(database = x){ \* cas语义，目前比较流行的做法
database := y;
} else {
goto t0; \* retry
};
t4: cache := y;
使用TLA+把问题分析清楚后，“写数据库”部分的软件代码修改如下：
y = x + 1
if DB_CASWrite(id, x, y): # if db[id] == x then db[id] = y
cache[id] = y
else:
increment(id) # retry
7. 后记
现场记录的思维导图
周六聚餐时邓辉老师表达的一些观点
- 这次是历次软件高级设计技术培训中最有价值的。
- 几年之内，掌握TLA+，将成为高端软件设计人才的一个核心竞争力。
- 以前一直认为软件设计是一门艺术/匠艺，TLA+将把软件设计变为一门科学技术。很多行业在被科学攻克之前，都被认为是艺术，例如围棋。
- 准备这次培训，邓辉老师看了Lamport的180篇论文中的大部分，3本专著，还有很多Lamport的技术视频。
- 国内BAT今后可能会先引入TLA+来解决一些并发系统难题（这次培训有阿里人员过来参加）。国外亚马逊应用TLA+估计超过10年（罗胜金注：原文称从2011年开始），2014年亚马逊10个核心项目使用了TLA+；目前谷歌、微软、甲骨文等公司都在应用TLA+。参考：
Since 2011, engineers at Amazon have been using TLA + to help solve difficult design problems in critical systems. This paper describes the reasons why we chose TLA + instead of other methods, and areas in which we would welcome further progress.
来源：https://link.springer.com/chapter/10.1007%2F978-3-662-43652-3_3
Since 2011, engineers at Amazon Web Services (AWS) have used formal specification and model checking to help solve difficult design problems in critical systems. Here, we describe our motivation and experience, what has worked well in our problem domain, and what has not.
来源：https://cacm.acm.org/magazines/2015/4/184701-how-amazon-web-services-uses-formal-methods/abstract
- TLA+最有价值的地方，是它致力于解决工程实际问题，而不是做理论研究。
- TLA+能够改变软件设计的思维，提高软件设计人员的思考能力，清晰化思考，这是最有价值的。
我的个人感觉
这次培训学习确实很不一样，之前几次主要讲具体技术，例如高可用并发，机器学习等等。这次主要讲一种思考问题、解决问题的全新视觉——使用数理逻辑，分析系统的时态逻辑，从而验证系统（尤其是并发系统）的正确性。
当然，邓辉老师对软件开发的很多观点是一以贯之的。例如，以前在解释“语义+计算”时讲过，DDD/DSL是用清晰明确的Spec描述系统行为（再通过解析器把Spec运行起来，成为一个特定功能的机器），Spec是可执行、“明显无错误”的；TLA+，也是用可执行、“明显无错误”的Spec来描述系统行为。
所不同的是，DDD/DSL还是用编程语言来描述，而TLA+可以等同于数学语言，更为精确、直截了当。
作为软件设计人员，核心的能力是思考能力，如果能把软件需要解决的问题、系统的逻辑关系思考清楚了，问题就解决大半了。用何种编程语言和技巧把软件写出来，并非核心能力。TLA+给我们提供了一个清晰化思考的工具。
诗以记之
不辞炎暑金陵行，会友寻师意难平。
软件匠工成往事，编程科技蕴光明。
数学设计同思考，技巧语言费钻营。
江上流波长渺渺，不及传道良师情。
