1. (10 points) Answer problems 1(a) through 1(e) from the SPIN Verification Examples and Exercises

2. (30 points) This problem comes from 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.

         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 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.

bool found = false
int i, j, turn = 1 // turn is only used in the last two algorithms 
bit a[8]       // to be initialized by you before p and q run

Algorithm 1

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

p0: i = 0
p1: while !found {
p2:   i++
p3:   found = (a[i] == 0)
p4: }
 
q0: j = 1
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: }