trunk/verif/Spin/Test/peterson

   1 /* Peterson's solution to the mutual exclusion problem - 1981 */
   2
   3 bool turn, flag[2];
   4 byte ncrit;
   5
   6 active [2] proctype user()
   7 {
   8         assert(_pid == 0 || _pid == 1);
   9 again:
  10         flag[_pid] = 1;
  11         turn = _pid;
  12         (flag[1 - _pid] == 0 || turn == 1 - _pid);
  13
  14         ncrit++;
  15         assert(ncrit == 1);     /* critical section */
  16         ncrit--;
  17
  18         flag[_pid] = 0;
  19         goto again
  20 }