论文部分内容阅读
摘 要：行为时序逻辑TLA是由Leslie Lamport提出的新的逻辑，它结合了行为逻辑和时序逻辑的特点，增强了表达能力。Dekker互斥算法最早是由荷兰数学家Dekker提出的一种解决并发进程互斥与同步的软件实现方法。本文以PlusCal语言和TLA+预言描述了Dekker算法，并利用ToolBox模型检测工具对DEKKER并发算法进行了验证。证明该算法满足互斥属性和非饥饿属性。
关键词：行为时序逻辑；PlusCal；ToolBox；DEKKER算法
中图分类号：TP311.52
行为时序逻辑是一种组合了时序逻辑（Temporal Logic）和行为逻辑（Logic of Action）来对并发系统进行描述与验证的逻辑。因此，断言一个系统是否满足它的规约和属性都可以通过逻辑蕴含来表示。TLA表达能力强，并且采用模块化、层次化的描述方法具有条理清晰，脉络分明的特点。
1 行为时序逻辑概述
1.1 TLA
一个系统是由变量集合Var、变量值集合Val、动作集合、作用在变量集合上的各种关系和状态函数组成。状态是在某一时刻对系统中所有变量赋值的函数，相应地决定了各种关系在某一时刻是否成立。一个行为时序逻辑模型实际上是一个迁移系统。
定义1.1 行为时序逻辑模型是一个六元组（S，Act，R，I，AP，L），其中：S是所有状态的集合；Act是一个包含哑步的原子动作集合；R是一个状态迁移关系， ；I是一个初态集合， ；AP是一个原子状态谓词集合；L：S→2AP是一个标签函数，对于任意的状态s∈S，L（s）是集合AP所有被状态s满足的原子状态谓词所组成的集合。
行为时序逻辑公式是由动作、状态谓词、各种命题逻辑操作符、时序操作符、函数表达式等组成的布尔表达式。行为时序逻辑用于描述系统模型的基本公式形式是由状态谓词Init和公式[Next]Vars组成的Init∧[Next]Vars形式，其中Init用于描述初始状态，Next通常是系统模型中所有非哑步的原子动作组成的析取公式用于表示任意原子动作的非确定性执行，下标Vars通常是一个包含系统模型中所有变量的元组，用于表示哑步的动作的执行，[Next]Vars用于描述状态间迁移的动作。
1.2 PlusCal和TLA+语言
PlusCal语言是一个具有强大功能的算法描述语言，其语义基于集合论和一阶逻辑，因此PlusCal可以使用普通数学来表达其意义。
PlusCal语言描述的算法可通过PlusCal转换器转换为TLA+语言的程序，在程序中添加系统应该具备的属性后再使用模型检测工具TLC检测，从而做到对系统的形式化验证。
TLA+是一种时序规约语言，它是以模块构造规约和系统，并通过扩展或实例化等方法可把多个模块组合成为复杂的规约，是一种用行为时序逻辑描述的语言。TLA+支持多种规约形式，本质上TLA+语言描述的是一个状态机。它基于ZF集合理论、一阶逻辑，适用于规约反应式、并发式和分布式系统等等。
1.3 TLC模型检测工具
TLA工具集包括PluaCal算法语言、TLA+语言、TLC模型检测器和PlusCal转换器，以及TLA+证明系统。
TLC模型检测器，其描述语言TLA+，基于行为时序逻辑TLA。没有一个模型检验器可以像TLC一样处理所有用像TLA一样表达性强的语言编写的描述规范。TLC采用多个工作线程并发检验得方法以加快验证速度，并利用磁盘技术来缓解状态爆炸问题。所以，和其它验证工具相比，TLA不用像Spin那样担心无法处理实时，不像UPPAAL那样担心表达能力有限和内存消耗过大，使用TLA进行描述并验证具有一定优势。TLA的一个特点是可以在一个程序中同时描述系统模型与系统属性，这是该逻辑最具有优势的特征。于是，我们选择TLC作为本文使用的模型检测工具。
2 DEKKER并发算法分析
DEKKER算法是第一个正确地通过软件方法解决两线程互斥问题的算法，算法中的status[1]和status[2]分别表示两个线程的状态，状态取值competing和out。若状态取值competing，表示当前线程处于竞争进入临界区的状态；若状态取值为out，则表示该线程放弃尝试进入临界区或已经退出临界区。每一个线程都有一个私有变量i，表示自己的id，由于有两个线程，所以i取值为1或2，因此other=3?i取值为2或者1，表示另一个线程的id。turn是一个共享变量，表示下一轮应该轮到谁进入临界区了。DEKKER算法如下表所示：
首先进行互斥性分析。若一个线程试图进入临界区，另一个线程没有竞争临界区，那么该线程简单直接进入临界区即可。如果两个线程同时在竞争进入临界区，那么根据第3行的条件判断，只有一个线程能够进入这个if语句，进入的线程将自己的状态设置为放弃，给另一个线程进入临界区的机会。另一个线程进入了临界区之后，会将turn设置为对方，所以放弃竞争临界区的线程又可以重新竞争临界区。从上述分析可以看出该算法可以保证两个线程的互斥。
饥饿性分析。若线程1和2同时进入临界区，并且假设turn=1，那么两个线程都进入while循环，其中线程2进入if语句。线程2将status[2]设置为out，然后等待turn变成2。此时线程1可以退出while循环。线程1退出while循环之后访问临界区，之后将turn设置为2。turn的下一次变化只能由线程2来完成，所以线程2最终turn总能变成2，因此可以将自己的状态设置为competing，然后继续在while循环中观察线程1的状态。线程1有两种可能，要么在退出临界区之后将状态设置为out，要么重新尝试进入临界区，此时也会阻塞在第5行等待，因为状态也设置为了out，所以线程2必然会退出while循环进入临界区。从以上分析得出，两个线程不会饿死，所以DEKKER算法也是不会死锁的互斥算法。 3 行为时序逻辑验证DEKKER并发算法
3.1 PlusCal描述DEKKER并发算法
使用PlusCal语言对DEKKER并发算法进行描述，如下所示：
在该算法中，变量will为一个值为布尔值的二元组，表示两个线程是否有访问临界区的愿望，为TRUE表示是，为FALSE为否。变量favor表示优先级，需指定初始值，在此描述中指定线程1在算法开始时具有优先级。
3.2 互斥性检测
并发算法的互斥性是指在某一时刻最多只有一个线程访问临界区。为了检测Dekker算法的互斥属性，在转换后的程序之后添加如下语句：
在属性配置环境中增加Mutex，使用ToolBox模型检测工具检测互斥性，检测未发现错误，说明该算法的是满足互斥性的，因此线程0及线程1不会同时访问临界区。
3.3 饥饿性检测
并发算法中的饥饿性是指一个或多个线程参与了竞争却始终访问不到临界区。在DEKKER该属性可用以下语句表示：
在属性配置环境中增加NoStarvation，使用ToolBox模型检测工具检测饥饿性，检测结果中没有错误发生，说明DEKKER算法不会出现饥饿现象。
4 结论
本文首先利用行为时序逻辑对算法进行规约，并详细对DEKKER算法进行分析，使用PlusCal语言对该算法描述，然后使用TLA+ToolBox工具转化成TLA+语言，最后使用模型检测工具TLC对该算法进行检测。结果表明DEKKER算法保证了并发算法的互斥性、无死锁性和无饥饿性。在此基础上，后续作者会继续在并发算法分析和验证上进行相关研究工作。
参考文献：
[1]Lamport L. The temporal logic of actions[J]. ACM Transactions on Programming Languages and Systems （TOPLAS）， 1994， 16（3）： 872-923.
[2]Eerz S. Modeling and developing systems using TLA+[J]. Escuela de Verano， 2005.
[3]Verhulst E， Boute R T， Faria J M S， et al. The Choice of TLA+/TLC： Comparing Formal Methods[M]. Formal Development of a Network-Centric RTOS. Springer US， 2011： 45-72.
[4]Merz S. On the Logic of TLA+[J]. Computing and Informatics， 2012， 22（3-4）： 351-379.
作者简介：赵梦龙（1981.12.21-），男，河南省驻马店人，讲师，硕士研究生，研究方向：密码学与信息安全。
作者单位：贵州广播电视大学，贵州贵阳 550004
关键词：行为时序逻辑；PlusCal；ToolBox；DEKKER算法
中图分类号：TP311.52
行为时序逻辑是一种组合了时序逻辑（Temporal Logic）和行为逻辑（Logic of Action）来对并发系统进行描述与验证的逻辑。因此，断言一个系统是否满足它的规约和属性都可以通过逻辑蕴含来表示。TLA表达能力强，并且采用模块化、层次化的描述方法具有条理清晰，脉络分明的特点。
1 行为时序逻辑概述
1.1 TLA
一个系统是由变量集合Var、变量值集合Val、动作集合、作用在变量集合上的各种关系和状态函数组成。状态是在某一时刻对系统中所有变量赋值的函数，相应地决定了各种关系在某一时刻是否成立。一个行为时序逻辑模型实际上是一个迁移系统。
定义1.1 行为时序逻辑模型是一个六元组（S，Act，R，I，AP，L），其中：S是所有状态的集合；Act是一个包含哑步的原子动作集合；R是一个状态迁移关系， ；I是一个初态集合， ；AP是一个原子状态谓词集合；L：S→2AP是一个标签函数，对于任意的状态s∈S，L（s）是集合AP所有被状态s满足的原子状态谓词所组成的集合。
行为时序逻辑公式是由动作、状态谓词、各种命题逻辑操作符、时序操作符、函数表达式等组成的布尔表达式。行为时序逻辑用于描述系统模型的基本公式形式是由状态谓词Init和公式[Next]Vars组成的Init∧[Next]Vars形式，其中Init用于描述初始状态，Next通常是系统模型中所有非哑步的原子动作组成的析取公式用于表示任意原子动作的非确定性执行，下标Vars通常是一个包含系统模型中所有变量的元组，用于表示哑步的动作的执行，[Next]Vars用于描述状态间迁移的动作。
1.2 PlusCal和TLA+语言
PlusCal语言是一个具有强大功能的算法描述语言，其语义基于集合论和一阶逻辑，因此PlusCal可以使用普通数学来表达其意义。
PlusCal语言描述的算法可通过PlusCal转换器转换为TLA+语言的程序，在程序中添加系统应该具备的属性后再使用模型检测工具TLC检测，从而做到对系统的形式化验证。
TLA+是一种时序规约语言，它是以模块构造规约和系统，并通过扩展或实例化等方法可把多个模块组合成为复杂的规约，是一种用行为时序逻辑描述的语言。TLA+支持多种规约形式，本质上TLA+语言描述的是一个状态机。它基于ZF集合理论、一阶逻辑，适用于规约反应式、并发式和分布式系统等等。
1.3 TLC模型检测工具
TLA工具集包括PluaCal算法语言、TLA+语言、TLC模型检测器和PlusCal转换器，以及TLA+证明系统。
TLC模型检测器，其描述语言TLA+，基于行为时序逻辑TLA。没有一个模型检验器可以像TLC一样处理所有用像TLA一样表达性强的语言编写的描述规范。TLC采用多个工作线程并发检验得方法以加快验证速度，并利用磁盘技术来缓解状态爆炸问题。所以，和其它验证工具相比，TLA不用像Spin那样担心无法处理实时，不像UPPAAL那样担心表达能力有限和内存消耗过大，使用TLA进行描述并验证具有一定优势。TLA的一个特点是可以在一个程序中同时描述系统模型与系统属性，这是该逻辑最具有优势的特征。于是，我们选择TLC作为本文使用的模型检测工具。
2 DEKKER并发算法分析
DEKKER算法是第一个正确地通过软件方法解决两线程互斥问题的算法，算法中的status[1]和status[2]分别表示两个线程的状态，状态取值competing和out。若状态取值competing，表示当前线程处于竞争进入临界区的状态；若状态取值为out，则表示该线程放弃尝试进入临界区或已经退出临界区。每一个线程都有一个私有变量i，表示自己的id，由于有两个线程，所以i取值为1或2，因此other=3?i取值为2或者1，表示另一个线程的id。turn是一个共享变量，表示下一轮应该轮到谁进入临界区了。DEKKER算法如下表所示：
首先进行互斥性分析。若一个线程试图进入临界区，另一个线程没有竞争临界区，那么该线程简单直接进入临界区即可。如果两个线程同时在竞争进入临界区，那么根据第3行的条件判断，只有一个线程能够进入这个if语句，进入的线程将自己的状态设置为放弃，给另一个线程进入临界区的机会。另一个线程进入了临界区之后，会将turn设置为对方，所以放弃竞争临界区的线程又可以重新竞争临界区。从上述分析可以看出该算法可以保证两个线程的互斥。
饥饿性分析。若线程1和2同时进入临界区，并且假设turn=1，那么两个线程都进入while循环，其中线程2进入if语句。线程2将status[2]设置为out，然后等待turn变成2。此时线程1可以退出while循环。线程1退出while循环之后访问临界区，之后将turn设置为2。turn的下一次变化只能由线程2来完成，所以线程2最终turn总能变成2，因此可以将自己的状态设置为competing，然后继续在while循环中观察线程1的状态。线程1有两种可能，要么在退出临界区之后将状态设置为out，要么重新尝试进入临界区，此时也会阻塞在第5行等待，因为状态也设置为了out，所以线程2必然会退出while循环进入临界区。从以上分析得出，两个线程不会饿死，所以DEKKER算法也是不会死锁的互斥算法。 3 行为时序逻辑验证DEKKER并发算法
3.1 PlusCal描述DEKKER并发算法
使用PlusCal语言对DEKKER并发算法进行描述，如下所示：
在该算法中，变量will为一个值为布尔值的二元组，表示两个线程是否有访问临界区的愿望，为TRUE表示是，为FALSE为否。变量favor表示优先级，需指定初始值，在此描述中指定线程1在算法开始时具有优先级。
3.2 互斥性检测
并发算法的互斥性是指在某一时刻最多只有一个线程访问临界区。为了检测Dekker算法的互斥属性，在转换后的程序之后添加如下语句：
在属性配置环境中增加Mutex，使用ToolBox模型检测工具检测互斥性，检测未发现错误，说明该算法的是满足互斥性的，因此线程0及线程1不会同时访问临界区。
3.3 饥饿性检测
并发算法中的饥饿性是指一个或多个线程参与了竞争却始终访问不到临界区。在DEKKER该属性可用以下语句表示：
在属性配置环境中增加NoStarvation，使用ToolBox模型检测工具检测饥饿性，检测结果中没有错误发生，说明DEKKER算法不会出现饥饿现象。
4 结论
本文首先利用行为时序逻辑对算法进行规约，并详细对DEKKER算法进行分析，使用PlusCal语言对该算法描述，然后使用TLA+ToolBox工具转化成TLA+语言，最后使用模型检测工具TLC对该算法进行检测。结果表明DEKKER算法保证了并发算法的互斥性、无死锁性和无饥饿性。在此基础上，后续作者会继续在并发算法分析和验证上进行相关研究工作。
参考文献：
[1]Lamport L. The temporal logic of actions[J]. ACM Transactions on Programming Languages and Systems （TOPLAS）， 1994， 16（3）： 872-923.
[2]Eerz S. Modeling and developing systems using TLA+[J]. Escuela de Verano， 2005.
[3]Verhulst E， Boute R T， Faria J M S， et al. The Choice of TLA+/TLC： Comparing Formal Methods[M]. Formal Development of a Network-Centric RTOS. Springer US， 2011： 45-72.
[4]Merz S. On the Logic of TLA+[J]. Computing and Informatics， 2012， 22（3-4）： 351-379.
作者简介：赵梦龙（1981.12.21-），男，河南省驻马店人，讲师，硕士研究生，研究方向：密码学与信息安全。
作者单位：贵州广播电视大学，贵州贵阳 550004