* ************************************************************ * Course: Verification * Kim G.Larsen, Spring 2000 * * Joost-Pieter Katoen: Concepts, Algorithms and Tools for Model Checking * Exercise 23 (page 184) * * ---------------------------- * Dekker's Mutex Algorithm * ---------------------------- * * M. Oliver Möller * ************************************************************ ** **************************************** ** Model of the 2 Processes ** **************************************** agent K_1 = readK_1.K_1 + 'setK_1.K_1 + 'setK_2.K_2 ; agent K_2 = readK_2.K_2 + 'setK_1.K_1 + 'setK_2.K_2 ; agent B1_false = readB1_false.B1_false + 'setB1_false.B1_false + 'setB1_true.B1_true ; agent B1_true = readB1_true.B1_true + 'setB1_false.B1_false + 'setB1_true.B1_true ; agent B2_false = readB2_false.B2_false + 'setB2_false.B2_false + 'setB2_true.B2_true ; agent B2_true = readB2_true.B2_true + 'setB2_false.B2_false + 'setB2_true.B2_true ; agent KickOff = tau.K_1 + tau.K_2 ; agent Memory = KickOff | B1_false | B2_false ; agent Empty = 'enter.Occupied ; agent Occupied = 'leave.Empty + 'enter.Fail ; agent Fail = fail.Fail ; agent Process_1 = setB1_true.TryToEnter_1 ; agent TryToEnter_1 = 'readB2_true.Wait_1 + 'readB2_false.Enter_1 ; agent Wait_1 = 'readK_2.Loop_1 + 'readK_1.loop_1.TryToEnter_1 ; agent Loop_1 = relax_1.setB1_false.'readK_1.setB1_true.TryToEnter_1 ; agent Enter_1 = enter.bell_1.leave.setK_2.setB1_false.Process_1 ; agent Process_2 = setB2_true.TryToEnter_2 ; agent TryToEnter_2 = 'readB1_true.Wait_2 + 'readB1_false.Enter_2 ; agent Wait_2 = 'readK_1.Loop_2 + 'readK_2.loop_2.TryToEnter_2 ; agent Loop_2 = relax_2.setB2_false.'readK_2.setB2_true.TryToEnter_2 ; agent Enter_2 = enter.bell_2.leave.setK_1.setB2_false.Process_2 ; set SyncActions = { readK_1, readK_2, setK_1, setK_2, readB1_false, readB1_true, setB1_false, setB1_true, readB2_false, readB2_true, setB2_false, setB2_true, enter, leave } ; agent System = ( Memory | Empty | Process_1 | Process_2 )\SyncActions ; ** **************************************** ** On the model: ** Process i has observable actions loop_i, relax_i, bell_i, corresponding ** each to a possible loop (bell_i is issued in the critical region). ** Entering and leaving the critical region is synchronized with a process ** "Empty", that mutates to "Occupied" and further to "Fail", if another ** enter happens before an exit. ** Fail can execute action "fail". ** Mutex holds, if "fail" is never (strongly) enabled: ** prop Mutex = max(X.([fail]F & [-]X)); ********************************************************************** ** Individual Starvation under Fairness assumption ********************************************************************** ** The following properties [inevitably bell_i will be rung] do not hold: ** prop No_Starve_1 = min(X.(T | (<->T & [-]X))); ** false prop No_Starve_2 = min(X.(T | (<->T & [-]X))); ** false ** ** It is always possible to _reach_ the critical region, but this does not ** suffice: ** prop Possibly_Bell_1 = min(X.(T | <-bell_1>X)); ** true prop Possibly_Bell_2 = min(X.(T | <-bell_2>X)); ** true prop Allways_Possibly_Bell_1 = max(Z.min(X.(T | <-bell_1>X)) & <->T & [-]Z); ** true prop Allways_Possibly_Bell_2 = max(Z.min(X.(T | <-bell_2>X)) & <->T & [-]Z); ** true ** ** **************************************** ** The crucial point is, that starvation freedom only holds under ** a fairness assumption which is captured as follows for Process_1 ** (for Process_2 it follows by symmetry). ** ** (I) ** The system is deadlock free: Always some observable action is possible ** prop DeadlockFree = max(Z.<->T & [-]Z); ** true ** ** ********** ** (II) ** For each single action, it is not possible to reach a state where ** only this action can be (weakly) observed henceforth: ** prop Only_loop_1 = min(Z.max(X.[[-loop_1]]F & [[loop_1]]X) | <->Z); ** false prop Only_loop_2 = min(Z.max(X.[[-loop_2]]F & [[loop_2]]X) | <->Z); ** false prop Only_relax_1 = min(Z.max(X.[[-relax_1]]F & [[relax_1]]X) | <->Z); ** false prop Only_relax_2 = min(Z.max(X.[[-relax_2]]F & [[relax_2]]X) | <->Z); ** false prop Only_bell_1 = min(Z.max(X.[[-bell_1]]F & [[bell_1]]X) | <->Z); ** false prop Only_bell_2 = min(Z.max(X.[[-bell_2]]F & [[bell_2]]X) | <->Z); ** false ** ** ********** ** (III) ** Two other actions happening infinitely often imply that bell_1 rings ** infinitely often: prop Imply_Bell_1_0 = max(Z.min(X.([loop_1](max(Y.([relax_1](max(W.(X & [-bell_1]W)))) & [-bell_1]Y)) & [-]Z))) ; ** true prop Imply_Bell_1_1 = max(Z.min(X.([loop_1](max(Y.([loop_2](max(W.(X & [-bell_1]W)))) & [-bell_1]Y)) & [-]Z))) ; ** true prop Imply_Bell_1_2 = max(Z.min(X.([loop_1](max(Y.([bell_2](max(W.(X & [-bell_1]W)))) & [-bell_1]Y)) & [-]Z))) ; ** true prop Imply_Bell_1_3 = max(Z.min(X.([loop_1](max(Y.([relax_2](max(W.(X & [-bell_1]W)))) & [-bell_1]Y)) & [-]Z))) ; ** true prop Imply_Bell_1_4 = max(Z.min(X.([relax_1](max(Y.([loop_2](max(W.(X & [-bell_1]W)))) & [-bell_1]Y)) & [-]Z))) ; ** true prop Imply_Bell_1_5 = max(Z.min(X.([relax_1](max(Y.([bell_2](max(W.(X & [-bell_1]W)))) & [-bell_1]Y)) & [-]Z))) ; ** true prop Imply_Bell_1_6 = max(Z.min(X.([relax_1](max(Y.([relax_2](max(W.(X & [-bell_1]W)))) & [-bell_1]Y)) & [-]Z))) ; ** true prop Imply_Bell_1_7 = max(Z.min(X.([loop_2](max(Y.([relax_2](max(W.(X & [-bell_1]W)))) & [-bell_1]Y)) & [-]Z))) ; ** true prop Imply_Bell_1_8 = max(Z.min(X.([loop_2](max(Y.([bell_2](max(W.(X & [-bell_1]W)))) & [-bell_1]Y)) & [-]Z))) ; ** true prop Imply_Bell_1_9 = max(Z.min(X.([relax_2](max(Y.([bell_2](max(W.(X & [-bell_1]W)))) & [-bell_1]Y)) & [-]Z))) ; ** true ** ** ********** ** (IV) Conclusion: ** The System is Deadlock-free (I); thus, at least one observation happens ** infinitely often. ** If only one action happens infinitely often, this is due to a cycle. The ** cycle is necessarily unfair, since it cannot happen that just one action is ** enabled henceforth (II). ** If we assume fairness, we can conclude that at least two different actions ** happen infinitely often. Due to (III), this implies that also bell_1 rings ** infinitely often, which subsumes freedom from individual starvation. ** **********************************************************************