##### Differences

This shows you the differences between two versions of the page.

 cs-486:spin-homework-1 [2020/01/06 11:33]egm cs-486:spin-homework-1 [2020/01/06 11:41] (current)egm Both sides previous revision Previous revision 2020/01/06 11:41 egm 2020/01/06 11:33 egm 2020/01/06 11:29 egm created 2020/01/06 11:41 egm 2020/01/06 11:33 egm 2020/01/06 11:29 egm created Line 8: Line 8: '''​1. (10 points)'''​ Answer problems 1(a) through 1(e) from the [http://​spinroot.com/​spin/​Man/​1_Exercises.html SPIN Verification Examples and Exercises] '''​1. (10 points)'''​ Answer problems 1(a) through 1(e) from the [http://​spinroot.com/​spin/​Man/​1_Exercises.html SPIN Verification Examples and Exercises] - '''​2. (30 points)'''​ Model the following mutual exclusion algorithm with Promela ​(25 points) and prove is correctness or incorrectness with SPIN (5 points). + '''​2. (30 points)'''​ Model the following mutual exclusion algorithm with PROMELA ​(25 points) and prove its correctness or incorrectness with SPIN (5 points). - <​code>​ + '''​Hyman'​s Mutual Exclusion'''​ - /* + <​code ​c> - R. W. Doran and L. K. Thomas. ​ Variants of the software solution to + void lock (int i) { - mutual exclusion. ​ Information Processing Letters 10(4--5):206--208, + int j = 1 - i; - 1980. + ​signal[i] = 1; + while (turn != i) { + while (signal[j]);​ + turn = i; + } + } - Process A                           ​Process B + void unlock(int i) { - 1. A_needs := true;                    B_needs :=  true; + signal[i] ​= 0; - 2. if B_needs then begin               if A_needs then begin + } - 3.   ​if turn = '​B'​ then begin            if turn = '​A'​ then begin + - 4.     ​A_needs := false;                   B_needs := false; + - 5.     wait until turn = '​A'; ​             wait until turn = '​B';​ + - 6.     ​A_needs := true;                    B_needs := true; + - 7.   ​end; ​                               end; + - 8.   wait until !B_needs; ​               wait until !A_needs; + - 9. end;                                end; + - 10. CRITICAL SECTION ​                   CRITICAL SECTION + - 11. turn := '​B'; ​                       turn := '​A';​ + - 12. A_needs := false; ​                  ​B_needs := false; + - 13. NON-CRITICAL SECTION ​               NON-CRITICAL SECTION + - */ +