形式化验证工具（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.{pos[] = ; turn=} -> Wait0(); cs. -> reset.{pos[] = } -> P0();

Wait0() = if (pos[]== && turn == ) { Wait0() };

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

Wait1() = if (pos[]== && turn == ) { Wait1() };

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

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