Process Analysis Toolkit  (PAT) 3.5 Help  
3.6.2.1 Fischer's Protocol

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
      ////////////////The Model//////////////////

      #define k 2;
      #define Idle -1;
      #define N 4;

var id = Idle;
      var count = 0;

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
      #define MutualExclusionFail count > 1;
      #assert System reaches MutualExclusionFail;

//deadlock checking
      #assert System deadlockfree;

//verifying responsiveness by LTL model checking 
      #define request id != Idle;
      #define accessCS count > 0;
      #assert System |= [](request -> <>accessCS);


 
Copyright © 2007-2012 Semantic Engineering Pte. Ltd.