**Objectives**:

- Predict the size of a state space in a PROMELA verification model
- Write simple PROMELA verification models that use shared variables for synchronization
- Use PROMELA to find solutions to brain-teasers

**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: }