TLA+ 笔记

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

TLA+ Tools 包含很多工具,可以在这里下载,大部分人都是使用这个 Tools:
http://lamport.azurewebsites.net/tla/standalone-tools.html?back-link=tools.html

在里面的链接指向的 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

image.png-63.4kB

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

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

(本节主要来自 http://tla2018.loria.fr/contrib/langworthy-slides.pdfhttps://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。

基本的运算符:

image.png-24.7kB

可以通过 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

====

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

image.png-169.8kB

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

image.png-615.8kB

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

image.png-205kB

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

这里都是 P-Syntax,PlusCal 还有 C-Syntax 的格式,具体参考 https://lamport.azurewebsites.net/tla/p-manual.pdfhttps://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 打出了内容:

image.png-419.6kB

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

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

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

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

结果是这样的:

image.png-15.2kB

另一种是 With:

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

结果是这样:

image.png-18.9kB

1
Leave a Reply

avatar
1 Comment threads
0 Thread replies
1 Followers
 
Most reacted comment
Hottest comment thread
1 Comment authors
Xin Recent comment authors
  Subscribe  
Notify of
Xin
Guest
Xin

老王棒棒哒