Process Analysis Toolkit (PAT) 3.5 Help |
Fischer’s protocol we examined here is a
mutual exclusion protocol designed for n processes. It only assumes
atomic reads and writes to a shared variable (when the first mutual exclusion
protocols were developed in the late 1960s all exclusion protocols were of the
"shared variable kind", later on researchers have more concentrated on
the "semaphore kind" of protocol). Mutual exclusion in Fischer's Protocol is
guaranteed by carefully placing bounds on the execution times of the
instructions, leading to a protocol which is very simple, and relies heavily on
time aspects. The global declaration
part var id =
Idle; clock x[N]; In this example, we define N as a constant tha
represents four processes competing for the shared variable. Clock x[N] is an
array which record the clock value of each process during the execution.
Constant k constranis every process must finish their request within k time
slots. Idle denotes the shared variable is not been used. Variable id records
the shared variable state, initial, it's idele. Variable count records the
nunber of processes that has got the shared variable and it has to be no more
than one all the time. The process definition
part Process P with parameter i: The whole system is defined as
follows: System = ||| y:{0..N-1} @P(y); The asserstion
part //verifying mutual exclusion by reachability
analysis //deadlock
checking //verifying responsiveness by LTL model
checking
////////////////The
Model//////////////////
#define k
2;
#define Idle
-1;
#define N 4;
var count = 0;
////////////////////////////////////////////////////////////////////////////////////
#define MutualExclusionFail count
> 1;
#assert System reaches
MutualExclusionFail;
#assert System
deadlockfree;
#define request id
!= Idle;
#define accessCS count >
0;
#assert System |= [](request ->
<>accessCS);