形式化验证工具（PAT）Perterson Algorithm学习

今天学习一下Perterson Algorithm.

这个算法是使用三个变量来实现并发程序的互斥性算法。

具体看一下代码：

Peterson算法是一个实现互斥锁的并发程序设计算法，核心就是三个标志位是怎样控制两个方法对临界区的访问，这个算法设计的想当精妙，我刚开始看的时候就被绕了一下。

算法使用两个控制变量flag与turn. 其中flag[n]的值为真，表示ID号为n的进程希望进入该临界区. 标量turn保存有权访问共享资源的进程的ID号。

注意到如果进程P0和P1并发，那么两者中必然会有一个会被while堵塞住（因为flag[0和1]均等于true），而另一个会完成自己的任务并置对方的flag位为false，这时while的条件不再满足，即可执行自己的程序，实现了互斥。

下面看一下PAT里面是如何实现的：

#define N 2;
var turn;
var pos[N];

P0() = req.0{pos[0] = 1; turn=1} -> Wait0(); cs.0 -> reset.0{pos[0] = 0} -> P0();
Wait0() = if (pos[1]==1 && turn == 1) { Wait0() };

P1() = req.1{pos[1] = 1; turn=0} -> Wait1(); cs.1 -> reset.1{pos[1] = 0} -> P1();
Wait1() = if (pos[0]==1 && turn == 0) { Wait1() };

Peterson() = P0() ||| P1();

这里我不是太懂，就是Wait0和Wait1两个进程，我觉得可能就是源代码里面的while进程，就Wait0进程而言，如果满足(pos[1]==1&&turn==1)这些条件，就一直卡在这里。如果不满足这个条件，就相当于Skip动作，什么都不做。不知道我的理解是不是有问题。