这些天我的工作是教授TLA+和正式方法：指定设计以查找其中的bug。但是，仅仅了解语法还不足以编写规范，还需要有示例可供参考。我最近读了Chris Siebenmann的“即使在Go，并发仍然不容易”一书，我想它会成为编写规范的一个很好的案例研究。在这篇文章中，他给出了一个死锁的GO代码的例子：
/*1*/func FindAll()[]P{//P=过程数据/*2*/pss，err：=ps。进程()/*3*/[...]/*4*/Found：=make(Chan P)/*5*/limitCh：=make(chan struct{}，concurrencyProcess)/*6*//*7*/for_，pr：=range pss{/*8*/limitCH<；-struct{}{}/*9*/pr：=pr/*10*/go func(){/*11*/defer func(){<；-limitCH}()/*12*/[...。获取带有一些错误检查的P...]/*13*/找到<；-P/*14*/}()/*15*/}/*16*/[...]/*17*//*18*/var Results[]P/*19*/for p：=找到的范围{/*20*/result=append(Results，p)/*21*/}/*22*/返回结果/*23*/}。
错误在于，Goroutines仅在将其结果发送到无缓冲的Found通道后才从limitCh接收以释放其令牌，而主代码仅在运行整个循环后才开始从Found接收，并且主代码在循环中获取令牌并在没有令牌可用时阻塞。
注意：此示例假设您了解TLA+和PlusCal的一些基本知识。如果您知道什么是流程标签，那么您就没有问题。我们看的不是比赛条件，所以你不需要知道标签和动作的细微之处，但这可能会让事情变得更直观。我在适当的地方包括了语法解释。它还假设了一些围棋的基本知识，这是我没有资格解释的。
最好从预先考虑一下我们将如何处理这个问题开始。形式化地指定一些东西有两个部分：描述系统和描述系统的属性。在这种情况下，我们可以忽略第二部分，因为我们只寻找死锁。添加健全性检查属性(如类型不变量)是很好的建模实践，但它们并不是严格必需的。
我们可以选择在TLA+中执行所有操作，也可以选择混合使用TLA+和PlusCal，PlusCal是编译为TLA+的顺序算法DSL。由于GO代码是高度连续的，而且PlusCal更容易被外人理解，所以我将使用PlusCal。对于无缓冲的通道，这将在以后导致阻抗不匹配，但总体来说，这是一个净收益。PlusCal规范的核心结构是一组同时具有本地和全局状态的已定义进程。至少，我们将有一个用于Main的进程和一个用于每个Goroutines的进程。
Chris的代码样本有三个“复杂部分”：GO、DEFER和GO频道的性质。当Goroutine运行完毕时，DEFER运行清理代码。目前，我们将通过将延迟代码移动到其自己的标签来表示这一点，但是为了更准确，我们也可以使用PlusCal过程。去产卵一只新的猩猩。由于PlusCal要求我们提前定义所有进程，因此我们不能“产生”一个新的Goroutine。相反，我们可以做的是定义每个进程，但阻止它们运行。然后，我们添加一个标志，表明是否在行为中初始化了goroutine。它看起来应该是这样的：
初始化的变量=[例程中的w\|->；false]；\*...。Process Goroutine\在例程中开始工作：等待初始化[SELF]；\*...
例程是我将在规范本身中定义的一组标识符。我们现在假设它是{1，2，3}。
Initialized是TLA+函数或映射。这是一个数学函数，而不是编程函数。Initialized[1]=False、Initialized[2]=False等。
通过在例程中编写goroutine，我为例程元素声明了一个独立的并发进程。在本例中，这将是3个进程。
因此，每个goroutine在执行任何操作之前都要等待主进程进行初始化。这就是我们可以模拟产生新流程的方式。
这就留下了通道，这是指定最复杂的部分。GO通道有两种：有缓冲的和无缓冲的。如果缓冲通道已满，则阻止发送到该通道。如果缓冲通道为空，则阻止来自该通道的接收。这两个都可以用PlusCal宏来表示：
宏SEND_BUFFERED(CHAN)BEGIN AWAIT CHANNELES[CHAN]<；BEGIN AWAIT CHANNELES[CHAN]；CHANNELES[CHAN]：=CHANNELES[CHAN]+1；END宏；宏RECEIVE_BUFFERED(CHAN)BEGIN AWAIT CHANNELES[CHAN]>；
出于教育学的目的，我并不是在模拟我们实际读到或写下的东西。在编写真实规范时，这也是一个很好的实践：编写最简单的规范，有效地捕获行为并迭代地添加细节。
这覆盖了缓冲通道。相比之下，除非同时有发送方和接收方，否则未缓冲的信道总是阻塞。在纯TLA+中，这不太难指定，但是PlusCal假设行为的每一步都是一个进程在做一件事。如果不添加一些烦人的记账功能，则无法在本地表示未缓冲的通道，因为我们需要“首先”有一个进程块。我们到了说明书后再谈这个问题。
现在，我们已经了解了一种粗略的方法和可能的痛点，让我们来编写规范。
常量是每次运行可配置的值，因此我可以使用2个goroutine和1个令牌运行一个模型检查，并使用6个goroutine和25个令牌运行另一个检查。这两个常量都被假定为正整数，我并不是出于纯粹的懒惰而强制执行这一点。
==定义一个新运算符，或用引号加“编程函数”。我们说例程是集合{1，2，...，NumRoutines}。
(*--算法通道变量Channels=[Tokens|->；0，Found|->；{}]；Buffered=[Tokens|->；NumTokens]；Initialized=[w\in routines|->；false]；
频道是每个频道的当前内容。对于缓冲通道，我们将其内容视为单个数字，并将最大容量存储在单独的缓冲变量中。对于未缓冲的信道，我们改为存储等待接收器的发送器集合。Initialized用于模拟Goroutines。
宏WRITE_BUFFERED(CHAN)BEGIN AWAIT CHANNEL[CHAN]<；BEGIN AWAIT CHANNEL[CHAN]；CHANCES[CHAN]：=CHANCES[CHAN]+1；END宏；宏RECEIVE_CHANNEL(CHAN)BEGIN如果域中的CHAN\缓冲了，则等待CHANNEL[CHAN]&>0；CHANCES[CHAN]：=CHANCES[CHAN]-1；否则等待CHANNECTS[CH。使用w\in channel[chan]do channel[chan]：=channels[chan]\{w}End With；End If；End宏；
这与我们原来的READ_BUFFERED有所不同，因为它同时处理缓冲通道和非缓冲通道。缓冲通道按预期工作。对于无缓冲通道，我们等待阻塞的写入器集为非空，并不确定地声明我们从其中之一读取。1个。
PROCEDURE WRITE_UNBUFFERED(CHAN)BEGIN DeclareSend：Channels[chan]：=Channels[chan]\Union{self
过程声明了一个多步骤编程函数。允许其他进程在运行DeclareSend和Send之间中断。
要对无缓冲通道建模，我们可以将状态设置为发送方，也可以将状态设置为接收方。我选择将其放在发送器上，因为GO允许同时从多个非缓冲通道读取。2在两个单独的时间步骤中，我们1)将进程添加到信道发送器集合，以及2)等待由接收器从该集合中移除。
我们的goroutine过程是GO代码的简单翻译。首先，我们等待Goroutine初始化，对应于第10行。然后我们写入找到的通道(第13行)。如果我想变得更忠实，我会写一些特殊的延迟语义，但是对于这个，我很乐意在这个过程的最后把它贴在标签上。
进程Main=0变量I=1；Begin Main：While I<；=NumRoutines do write_Buffered("；Tokens&34；)；GO(I)；I：=I+1；End While；Get：While I>；1 do I：=I-1；Receive_Channel("；Found"；)；End While；End Process；End Algorithm；*)。
TLA+没有本机for循环，所以我们必须用while来模拟它。与编程语言不同，我们计算的是1..N，而不是0..(N-1)。我们的仿真使用一个令牌来初始化每个Goroutine。因为WRITE_CHANNEL在其中有一个等待，所以如果Goroutines比内标识多，它就会阻塞。然后，它将一直被阻止，直到大猩猩释放令牌。3最终规格：
-模块通道-扩展整数、TLC、序列常量NumRoutines、NumTokens例程==1..。NumRoutines(*--算法通道变量Channels=[limitCH|->；0，Found|->；{}]；Buffered=[limitCH|->；NumTokens]；Initialized=[w\in routines|->；false]；宏SEND_BUFFERED(CHAN)BEGIN AWAIT CHANNELES[CHAN]<；BUFFERED[CHAN]；CHANNELES[CHAN]：=CHANNENS[CHAN]+1；END宏；宏RECEIVE_CHANNEL(CHAN)BEGIN IF CHAN\In域缓冲，然后等待CHANNELES[CHAN]>；0；CHANNELES[CHAN]：=CHANNEL[CHAN]-1；否则等待CHANNEL[CHAN]/={}；WITH CHANNEL[CHAN]DO CHANNELES[CHAN]：=CHANCES[CHAN]\{w}End With；End If；End宏；宏GO(例程)开始初始化[例程]：=true；END宏过程SEND_UNBUFFERED(CHAN)BEGIN DECLARESend：CHANNELES[CHAN]：=CHANNELES[CHAN]\Union{Self}；SEND：在CHANNEL[CHAN]；RETURN；END PROCEDURE PROCESS Goroutine\in例程中BEGIN A：等待初始化[Self]；调用SEND_UNBUBFEED("；Found"；)；B：Receive_Channel("；limitCH"；)；end process；process main=0 Variables I=1；BEGIN Main：While I<；=NumRoutines do send_Buffered("；limitCH"；)；GO(I)；I：=I+1；End While；Get：While I>；1 do I：=I-1；Receive_Channel("；Found"；)；End While；End Process；End Algorithm；*)=。
现在我们有了一个完整的规范，我们可以使用模型检查器TLC来查看它是否满足任何属性。我们没有指定任何值，但默认情况下TLC将检查死锁。我要用3个大猩猩和2个代币来做模型检查。4.。
状态1：<；初始谓词>；/\Buffered=[limitCH|->；2]/\channel=[limitCH|->；0，Found|->；{}]/\i=1/\pc=(0：>；"；main"；@@1：>；"；A"；@@2：>；"；A"；@@3：>；"；A"；)/\Initialized=<；<；FALSE，FALSE，FALSE；>；状态2：<；主行128，第9列至第137行，第48列模块库>；/\Buffered=[limitCH|->；2]/\channel=[limitCH|->；1，Found|->；{}]/\i=2/\pc=(0：>；"；main"；@@1：>；&34；A"；/\i=2/\pc=(0：>；"；main"；@@1：>；&34；A"；@@2：>；"；A"；@@3：>；"；A"；)/\Initialized=<；<；TRUE，FALSE，FALSE>；>；状态3：<；主行128，第9列至第137行，第48列模块库>；/\Buffered=[limitCH|-&>；2]/\channel=[limitCH|-&>；2，Found|->；2，Found|-&>；{}]/\i=3/\pc=(0：>；"；main"；@@1：>；"；A"；@@2：>；"；A"；@@3：>；&34；A"；)/\Initialized=<；<；<；true，true，false；>；状态4：<；A行106，列12至行114，列64；/\Buffered=[limitCH|->；2]/\channel=[limitCH|->；2，Found|->；{}]/\i=3/\pc=(0：>；"；main"；@@1：>；"；A"；@@2：>；"；DeclareSend"；@@3：>；"；A"；)/\Initialized=<；<；TRUE，TRUE，FALSE&>；状态5：<；A行106，第12列到第114行，第114行；/\Buffered=[limitCH|->；2]/\channel=[limitCH|->；2，Found|->；{}]/\i=3/\pc=(0：>；"；Main"；@@1：>；"；DeclareSend"；@@2：>；"；声明发送"；@@3：>；&34；A"；)/\Initialized=<；<；<；TRUE，TRUE，FALSE>；>；状态6：<；声明发送行92，列22至行95，列77，模块库>；/\Buffered=[limitCH|->；2]/\channel=[limitCH|->；2，Found|->；{1}]/\i=3/\pc=(0：>；"；main"；@@1：>；&34；发送"；@@2：>；&
这和克里斯的问题是一样的。只有在找到的通道上有接收器时，Goroutine才能返回它们的令牌，该通道的唯一接收器是Main，Main仅在初始化所有Goroutine之后读取，如果Goroutines多于令牌，则Main将阻塞。在初始化所有的goroutine之前，goroutine不能返回令牌，而main只有在一些goroutine返回它们的令牌之后才能初始化所有的goroutine。
克里斯建议了三种可能的方法来解决这个问题。我们可以通过修改我们的规范来测试这三个选项：
如果goroutines通过向limitCH而不是main for循环发送令牌来获取令牌，那么bug就不会存在；
Process Goroutine\in RoutinesBegin A：等待初始化[SELF]；+WRITE_BUFFERED("；limitCH"；)；\*...。While I<；=NumRoutines do-write_Buffered("；limitCH&34；)；初始化[i]：=true；i：=i+1；End While；
如果从limitCh接收的goroutines在发送到find之前释放它们的令牌，它就不会存在(但由于错误处理，在延迟中进行接收更简单、更可靠)。
RoutinesBegin A：等待初始化[Self]；+Receive_Channel("；limitCH"；)；-调用WRITE_UNBUFFERED("；Found"；)；B：-RECEIVE_CHANNEL("；limitCH"；)；+调用WRITE_UNBUFFEED("；Found"；)；结束进程；
这个有点复杂。我们为循环创建一个新进程，并将其标识符添加到Initialized。我将使用-1表示for循环。
Initialized=[w\in routines\Union{-1}|->；false]；\*在goroutines进程FOR_LOOP=-1变量-1\f25 i=1；Begin Loop：While I<；=NumRoutines do write_Buffered("；limitCH"；)；GO(I)；i：=i+1；End While；End Process；
进程Main=0变量I=NumRoutines；BEGIN Main：GO(-1)；GET：While I>；0 do I：=I-1；Receive_Channel("；Found"；)；End While；End Process；
最终，我们编写了大约75行规范来测试20行Go代码。超过一半的规范是通道逻辑，我们现在可以在其他规范中重用它们。不考虑这些会让我们更接近，尽管我承认真正的TLA+规范会更长，因为您会编写更健全的检查属性。当然，编写TLA+版本不会比编写原始版本的工作量大很多，如果在生产之前发现死锁，还可以节省您的净时间。
显然，我倾向于使用TLA+，因为这是我选择的专业语言。然而，我怀疑TLA+并不完全是建模Go频道的正确工具。这是因为还有另一种正式的方法，称为Spin，它更接近于Go的本机语义。它甚至将频道作为原生数据类型。我没有用过Spin，所以不能评论它到底有多有效，但我想它在这个领域会工作得很好。它以前也被用来对运行时调度器建模，不过当它最终失去同步时，该规范被删除了。您可以在这里看到相同问题的旋转规范。
如果您有兴趣了解更多关于正式方法的知识，我写了一本书，并在10月份举办了一个为期3天的TLA+研讨会。您也可以关注我的时事通讯，在那里我讨论了形式化的方法、技术和模式。
我在我的时事通讯上分享了这篇文章的初稿。如果你喜欢我的作品，为什么不订阅呢？
如果集合为空，则使用块，从而使其上方的AWAIT语句成为冗余。我添加它纯粹是为了清楚。 [返回]。
您也可以使用SELECT发送到多个频道，但我认为这不太常见？这就是能够编写原始TLA+操作可能真正有帮助的地方。 [返回]。
GET不准确地表示通道如何在范围内工作：它应该循环，直到通道关闭。我把它留在这里是因为规范的其余部分不依赖于关闭通道，我不想给这个示例增加额外的复杂性。[返回]
下面的人请注意：虽然我强烈建议初学者使用官方IDE，但我个人更喜欢在撰写文章时从命令行运行。我编写了一个简单的CLI包装器，它没有工具箱功能齐全，但可以完成我需要的工作。使用包装器，您可以使用tlacli check channel els.tla--Constant NumRoutines 3--Constant NumTokens 2--model-value defaultInitValue重现运行的模型。[返回]。
我从跟踪中删除了堆栈和chan变量，以使其更清楚一些。PlusCal使用STACK跟踪过程中的簿记信息，而Chan跟踪作为参数传入的输入。 [返回]