CIS 301. Logical Foundations of Programming, Spring 2000

Mutual Exclusion Revisited.

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

sets an initial value for the "semaphore" turn;
instantiates two asynchronous process modules; and
checks the specifications discussed in the textbook.

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:

"FAIRNESS running" guarantees that no participating process will be subject to starvation;
"FAIRNESS !(st = c)" instructs SMV to check the specifications in the main module only on those paths where !(st = c) is true infinitely often; this ensures that no process can remain in their critical section forever.

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,

process 2 progresses from n to t to c;
then process 1 evolves from n to t;
finally, process 2 may stay in its critical section forever, as !(st = c) no longer needs to be true infinitely often; this forces process 1 to remain in its trying state forever;
Here we used the instance "Fairness !(pr2.st = c)", but the clause "FAIRNESS !(st = c)" also enforces "FAIRNESS !(pr1.st = c)".

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