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:
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 + 6In 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 + 6In 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)