CIS 301. Logical Foundations of Programming, Spring 2000

Mutual Exclusion Revisited.


The main module for modeling the mutual exclusion protocol for two processes

MODULE main
  VAR
          pr1 : process prc(pr2.st, turn, 0);
          pr2 : process prc(pr1.st, turn, 1);
          turn : boolean;
  ASSIGN
          init(turn) := 0;
  --safety
  SPEC AG!((pr1.st = c) & (pr2.st = c))
  --liveness
  SPEC AG((pr1.st = t) -> AF (pr1.st = c))
  --non-blocking
  SPEC AG((pr1.st = n) -> EF (pr1.st = t))
  --no strict sequencing
  SPEC EF(pr1.st = c & E[pr1.st = c U (!pr1.st = c & E[! pr2.st = c U pr1.st = c ])])


The module for a process is

MODULE prc(other-st, turn, myturn)
  VAR
          st : {n, t, c};
  ASSIGN
          init(st) := n;
          next(st) :=
                  case
                          (st = n)                                     :{t, n};
                          (st = t) & (other-st = n)                    : c;
                          (st = t) & (other-st = t) & (turn = myturn)  : c;
                          (st = c)                                     : {c, n};
                          1                                            : st;
                  esac;
          next(turn) :=
                  case
                          turn = myturn & st = c  : !turn;
                          1                       : turn;
                  esac;
  FAIRNESS running
  FAIRNESS !(st = c)


Notice the fairness conditions:

We run this program and obtain:
nunk% pwd
/home/faculty/huth/.html/lics/ancillary/smv
nunk% smv p198.smv
-- specification AG (!(pr1.st = c & pr2.st = c)) is true
-- specification AG (pr1.st = t -> AF pr1.st = c) is true
-- specification AG (pr1.st = n -> EF pr1.st = t) is true
-- specification EF (pr1.st = c & E(pr1.st = c U (!pr1.st... is true

resources used:
user time: 0.03 s, system time: 0.04 s
BDD nodes allocated: 985
Bytes allocated: 1245184
BDD nodes representing transition relation: 56 + 6


Next, let us consider what happens if we remove the "FAIRNESS running" option from the program:

nunk% smv mutex2.smv
-- specification AG (!(pr1.st = c & pr2.st = c)) is true
-- specification AG (pr1.st = t -> AF pr1.st = c) is false
-- as demonstrated by the following execution sequence
state 1.1:
pr1.st = n
pr2.st = n
turn = 0
[stuttering]

state 1.2:
[executing process pr1]

-- loop starts here --
state 1.3:
pr1.st = t
[stuttering]

state 1.4:
[stuttering]

-- specification AG (pr1.st = n -> EF pr1.st = t) is true
-- specification EF (pr1.st = c & E(pr1.st = c U (!pr1.st... is true

resources used:
user time: 0.06 s, system time: 0.03 s
BDD nodes allocated: 1067
Bytes allocated: 1245184
BDD nodes representing transition relation: 56 + 6
In the generated counter example, notice how process 1 enters its trying state. Then process 1 can execute forever (as "FAIRNESS running" is off) and stay in its trying state.


Now, we retain "FAIRNESS running", but remove "FAIRNESS !(st = c)":

nunk% smv mutex3.smv
-- specification AG (!(pr1.st = c & pr2.st = c)) is true
-- specification AG (pr1.st = t -> AF pr1.st = c) is false
-- as demonstrated by the following execution sequence
state 1.1:
pr1.st = n
pr2.st = n
turn = 0
[stuttering]

state 1.2:
[executing process pr2]

state 1.3:
pr2.st = t
[executing process pr2]

state 1.4:
pr2.st = c
[executing process pr1]

-- loop starts here --
state 1.5:
pr1.st = t
[stuttering]

state 1.6:
[executing process pr1]

state 1.7:
[executing process pr2]

state 1.8:
[stuttering]

-- specification AG (pr1.st = n -> EF pr1.st = t) is true
-- specification EF (pr1.st = c & E(pr1.st = c U (!pr1.st... is true

resources used:
user time: 0.02 s, system time: 0.06 s
BDD nodes allocated: 1520
Bytes allocated: 1245184
BDD nodes representing transition relation: 56 + 6
In this run,


By removing all FAIRNESS conditions, we find the violations as before, but the counter example produced is the one obtained from removing "FAIRNESS running":

nunk% smv mutex4.smv
-- specification AG (!(pr1.st = c & pr2.st = c)) is true
-- specification AG (pr1.st = t -> AF pr1.st = c) is false
-- as demonstrated by the following execution sequence
state 1.1:
pr1.st = n
pr2.st = n
turn = 0
[stuttering]

state 1.2:
[executing process pr1]

-- loop starts here --
state 1.3:
pr1.st = t
[stuttering]

state 1.4:
[stuttering]

-- specification AG (pr1.st = n -> EF pr1.st = t) is true
-- specification EF (pr1.st = c & E(pr1.st = c U (!pr1.st... is true

resources used:
user time: 0.04 s, system time: 0.03 s
BDD nodes allocated: 1022
Bytes allocated: 1245184
BDD nodes representing transition relation: 56 + 6


Copyright 2001 Michael Huth (huth@cis.ksu.edu)