Differences

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

Link to this comparison view

Both sides previous revision Previous revision
cs-486:spin-homework-1 [2020/01/06 11:33]
egm
cs-486:spin-homework-1 [2020/01/06 11:41] (current)
egm
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 +
-*/+
 </​code>​ </​code>​
  
cs-486/spin-homework-1.1578335633.txt.gz · Last modified: 2020/01/06 11:33 by egm
Back to top
CC Attribution-Share Alike 4.0 International
chimeric.de = chi`s home Valid CSS Driven by DokuWiki do yourself a favour and use a real browser - get firefox!! Recent changes RSS feed Valid XHTML 1.0