##### Differences

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

 cs-486:spin-homework-1 [2020/01/06 11:29]egm created cs-486:spin-homework-1 [2020/01/06 11:41] (current)egm 2020/01/06 11:41 egm 2020/01/06 11:33 egm 2020/01/06 11:29 egm created Next revision Previous revision 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)''' ​This problem comes from [https://​d1b10bmlvqabco.cloudfront.net/​attach/​i4libjkuz9io1/​i4licnd7ihy2nh/​i5zqbdqd68yu/​Assignment_4_CS118_2015.pdf CalTech'​s CS 118 Assignment 4]. Consider ​the following ​concurrent ​algorithm ​for controlling access to the critical section of two processes, specified informally in the following table. + '''​2. (30 points)''' ​Model the following ​mutual exclusion ​algorithm ​with PROMELA ​(25 points) ​and prove its correctness or incorrectness ​with SPIN (5 points). - <​code>​ + - ​Process P                     ​Process Q + - | p1: while true              | q1: while true             | + - | p2:   ​non-critical section ​ | q2:   ​non-critical section | + - | p3:   wantp = true          | q3:   wantq = true         | + - | p4:   await wantq == false  | q4:   await wantp == false | + - | p5:   ​critical section ​     | q5:   ​critical section ​    | + - | p6:   wantp = false         | q6:   wantq = false        | + - ​ + - The algorithm relies on two global variables initialized to false: '''​bool wantp = false, wantq = false'''​. ​ Each numbered line corresponds to an indivisible statement execution. The keyword '''​await'''​ is used to indicate that the process will wait for the condition that follows it to become true before proceeding. Model the algorithm in PROMELA, and verify it with SPIN. Report the results of the verification ​(including errors if they exist). + - + - '''​3. (50 points)'''​ This problem comes from [https://​d1b10bmlvqabco.cloudfront.net/​attach/​i4libjkuz9io1/​i4licnd7ihy2nh/​i5zqbdqd68yu/​Assignment_4_CS118_2015.pdf CalTech'​s CS 118 Assignment 4]. Five concurrent algorithms are sketched below, each defining the behavior of two concurrent processes named p and q. There is an array of bit values called a[] with 8 elements. Assume that there is at least one integer value for which array element a[i] equals 0. Formalize each algorithm in Promela and use Spin to perform the verification. You will need to extend or modify each algorithm to prevent array indexing errors. You should also add an initial process that initializes the array a[] with nondeterministically chosen 0 or 1, while preventing that all eight array elements are set to 1. This initialization should be completed before processes p and q start executing. + - + - An algorithm is considered correct if for all possible scenarios, both processes terminate after one of them has found a zero. Each numbered line for each process corresponds to an indivisible action. For each algorithm, show that it is correct or find a counterexample. For each counterexample,​ explain what the problem is that causes it. + - + - These are the global variable declarations to be used for all five algorithms. + + '''​Hyman'​s Mutual Exclusion'''​ - bool found = false + void lock (int i) { - int i, j, turn = 1 // turn is only used in the last two algorithms ​ + int j = 1 - i; - bit a[8]       // to be initialized by you before p and q run + signal[i] = 1; - ​ + while (turn != i) { + while (signal[j]); + turn = i; + } + } - '''​Algorithm 1'''​ + void unlock(int i) { - + signal[i] = 0; - p0: i = 0 + } - p1: found = false + - p2: while !found { + - p3:   i++ + - p4:   found = (a[i] == 0) + - p5: } + - + - q0: j = 1 + - q1: found = false + - q2: while !found ​{ + - q3:   ​j-- + - q4:   found = (a[j] == 0) + - q5: } + ​ - '''​Algorithm 2'''​ + '''​3. (30 points)'''​ - + Write a Promela model for the below problem ​(25 point) and use SPIN to find a solution (5 points). - p0: i = 0 + - p1: while !found { + - p2:   i++ + - p3:   found = (a[i] == 0) + - p4: } + - q0: j = 1 + A farmer wants to cross a river and take with him a wolf, a goat, and a cabbage. There is a boat that can fit himself plus either the wolf, the goat, or the cabbage. If the wolf and the goat are alone on one shore, the wolf will eat the goat. If the goat and the cabbage are alone on the shore, the goat will eat the cabbage. How can the farmer bring the wolf, the goat, and the cabbage across the river? - q1: while !found { + - q2:   j-- + - q3:   found = (a[j] == 0) + - q4: } + - ​ + - '''​Algorithm 3'''​ - - p0: i = 0 - p1: while !found { - p2:   i++ - p3:   if a[i] == 0 - p4:     found = true - p5: } - - q0: j = 1 - q1: while !found { - q2:   j-- - q3:   if a[j] == 0 - q4:     found = true - q5: } - ​ - - '''​Algorithm 4'''​ - - p0: i = 0 - p1: while !found { - p2:   await turn == 1 -> turn = 2 - p3:   i++ - p4:   if a[i] == 0 - p5:     found = true - p6: } - - q0: j = 1 - q1: while !found { - q2:   await turn == 2 -> turn = 1 - q3:   j-- - q4:   if a[j] == 0 - q5:     found = true - q6: } - ​ - - '''​Algorithm 5'''​ - - p0: i = 0 - p1: while !found { - p2:   await turn == 1 -> turn = 2 - p3:   i++ - p4:   if a[i] == 0 - p5:     found = true - p6:   turn = 2 - p7: } - - q0: j = 1 - q1: while !found { - q2:   await turn == 2 -> turn = 1 - q3:   j-- - q4:   if a[j] == 0 - q5:     found = true - q6:   turn = 1 - q7: } -
cs-486/spin-homework-1.1578335375.txt.gz · Last modified: 2020/01/06 11:29 by egm
Back to top