TLA+ 笔记

很久以前学过一些 Prolog，当时主要是为了学习人工智能和数理逻辑。TLA+ 与之有一点点像，Prolog 可以用来处理各种规划问题、一阶逻辑推理，TLA+ 可以用来设计各种分布式、异步系统，搭配 TLC（model checker） 来做验证——他们的设计目标都不是解决通用的编程问题，而是通过数理逻辑解决一些特定领域问题。

在里面的链接指向的 github 地址里，有 Windows、 Linux 、Mac 的二进制版本，良心。

在看 TLA+ Community Meeting 2018 的时候还看到了一个形式验证语言（其实是 Python 的扩展）DistAlgo，整体思路和 Demo 看起来特别棒，就是目前各种材料和介绍还是相对少，所以我没有继续研究下去，有兴趣和时间的话，看看 DistAlgo 也挺好。

下面是笔记。

介绍

分布式系统的正确性特别难验证，所以做出了 TLA+，因为 2015 年 AWS 在 CACM 发了一篇 How Amazon Web Services Uses Formal Methods 引起了很多人注意，年底 TLA+ 作者之一的 Langworthy 和 Lamport 找微软高层推动 TLA+ 在微软落地，一定程度上得益于 AWS 的文章和 Lamport 2015 年拿到图灵奖带来的影响力，Satya 发邮件说 Go go go。

2016 年开始微软在内部办了一共三天的 TLA+ School，教学了很多微软工程师 TLA+，一共运行了三次，到第四次时，Lamport 终于受不了重复给别人讲 TLA+ 基础，于是做了教学视频，没错就是很火的这个视频： http://lamport.azurewebsites.net/video/videos.html

所以从 2018 年开始，School 变成了 Workshop，目的从基础教育提升到了继续教育，特别是生产实践带来的反馈。

现在 TLA+ 在微软内部应用在 Service Fabric（类似 kubernetes）、Azure Batch、Azure Storeage、Azure Networking、Azure IoT、Cosmos DB。

（本节主要来自 http://tla2018.loria.fr/contrib/langworthy-slides.pdf 和 https://www.youtube.com/watch?v=ifFfxRCX_jw ）

Learn TLA+ 笔记

主要是阅读 Learn TLA+ 的笔记，这个写了很多基础的练习和介绍，先是 PlusCal 的内容，在 TLA+ Tools 上用 ⌘+T 即可翻译成 TLA+，不过 PlusCal 并不能完全等价 TLA+。

Introduction & PlusCal

基本使用流程很简单，先在 modules 里建 module，写 PlusCal，转成 TLA+，再在 models 建 model，写条件，运行检查即可。

PlusCal 的基本语法：

---- MODULE module_name ----
\* TLA+ code

(* --algorithm algorithm_name
begin
\* PlusCal code
end algorithm; *)
====

每个文件里只能有一个 PlusCal 算法。

举个例子：

---- MODULE transfer ----
EXTENDS Naturals, TLC

(* --algorithm transfer
variables alice_account = 10, bob_account = 10, money = 5;

begin
A: alice_account := alice_account - money;
B: bob_account := bob_account + money;

end algorithm *)
====

里边 variable 即变量，声明变量使用 = ，算法实现中使用 := ，A、B 是标签，定义了算法步骤，一个标签里的内容被视作一个事务。{a..b} 表示整数 a 到 b 的整数集合，\in 即集合论里的 in。

基本的运算符：

可以通过 process 来设计一个多线程程序，比如这样：

---- MODULE Transfer ----
EXTENDS Naturals, TLC

(* --algorithm transfer
variables alice_account = 10, bob_account = 10,
          account_total = alice_account + bob_account;

process Transfer \in 1..2
  variable money \in 1..20;
begin
Transfer:
  if alice_account >= money then
    A: alice_account := alice_account - money;
       bob_account := bob_account + money;
end if;
C: assert alice_account >= 0;
end process

end algorithm *)

MoneyNotNegative == money >= 0
MoneyInvariant == alice_account + bob_account = account_total

====

其中通过类似 MoneyNotNegative 、 MoneyInvariant 这样的语句来帮助添加一个全局的一致性检查 ，invariant 可以在 TLC 里指定，来检查全局的一致性：

上面的代码在并发时显然是有问题，所以 TLC 可以检查出来它：

展开 Error Trace 可以看到状态转移记录：

可以看到并发执行时，money 同时有两个值，由于转账时没有对账户加全局锁，所以账户总大于零这个断言被 break 了。

这里都是 P-Syntax，PlusCal 还有 C-Syntax 的格式，具体参考 https://lamport.azurewebsites.net/tla/p-manual.pdf 和 https://lamport.azurewebsites.net/tla/c-manual.pdf 。

PlusCal 中是有 print 的，比如下面这个例子：

EXTENDS TLC

(* --algorithm hello_world
variable s \in {"Hello", "World!"};
begin
  A:
    print s;
end algorithm; *)

这里的 User Output 打出了内容：

PlusCal 的 if、while、goto 都和一般语言很想，就不赘述了。

Model Overview 里的 “no behavior spec” 一般很少用，运行后在 result 页可以使用 “evaluate constant expression”，然后可以写点东西来验证 TLA+ 是如何运行的。

最后是引入 divergent behavior，让系统在一个步骤里可以做不同的事情，对于单进程 PlusCal，可以通过 with 和 either 来引入。

either 简单地说就是没有条件的 if，可以让 TLC 知道这里有两种路径，都可以执行以下：

variables x = 3, i = 2;
begin
while i > 0 do
  either 
    x := x + 2;
  or 
    x := x * 2;
  end either;
  i := i - 1;
end while

结果是这样的：

另一种是 With：

with a \in {1, 2, 3} do
  x := x + a
end with;

结果是这样：