Objectives:

• Practice compilation
• Understand the relation between a first-order representation of the Kripke structure and the Kripke structure itself.

See chapter 2 of course text for details.

## Paper Pencil Problems

1. (10 points) Consider the two mutual exclusion algorithms below. Use the translation function in Section 2.2.2 to translate the program to a first-order logic representation. You only need to translate the lock() methods. Be sure to do a translation for each version: mutex one and mutex two.
2. (10 points) Create the Kripke structure for Mutex One from the first-order representation in the first problem. Express the first 10 states of the Kripke as a dotty graph (see below). Use a depth first search to generate the 10 states always preferring the first thread in the transition.

## Kripke Structures

Below are two different algorithms for mutual exclusion. That are called in the following way from two threads:

cobegin run() || run() coend

The global variable initialization and code for run follows:

int turn = 0;
int signal = {0, 0};

void run() {
int i = getpid();  //Only returns 0 or 1
while(1) {
lock(i);
CriticalSection();
unlock(i);
}
}

### Mutex One

void lock (int i) {
int j = 1 - i;
signal[i] = 1;
while (turn != i) {
while (signal[j]);
turn = i;
}
}

void unlock(int i) {
signal[i] = 0;
}

### Mutex Two

void lock (int i) {
int j = 1 - i;
signal[i] = 1;
turn = j;
while (signal[j] && turn != i);
}

void unlock(int i) {
signal[i] = 0;
}

### Dotty Graphs

Graphviz is a tool set for graph layout and manipulation. We will use the tool set from time to time to visualize different Kripke structures and graphs. Below is a an example input file for a Kripke:

 digraph massive_output {
0 -> 1;
0 -> 2;
1 -> 4;
2 -> 0;
2 -> 5;
3 -> 3;
3 -> 2;
3 -> 0;
4 -> 1;
4 -> 2;
5 -> 6;
6 -> 3;
0 [label="0\n"+"~Start\n"+"~Close\n"+"~Heat\n" + "~Error\n"];
1 [label="1\n"+"Start\n"+"~Close\n"+"~Heat\n" + "Error\n"];
2 [label="2\n"+"~Start\n"+"Close\n"+"~Heat\n" + "~Error\n"];
3 [label="3\n"+"~Start\n"+"Close\n"+"Heat\n" + "~Error\n"];
4 [label="4\n"+"Start\n"+"Close\n"+"~Heat\n" + "Error\n"];
5 [label="5\n"+"Start\n"+"Close\n"+"~Heat\n" + "~Error\n"];
6 [label="6\n"+"Start\n"+"Close\n"+"Heat\n" + "~Error\n"];
}

Notice that the description language is simple: edge list followed by labels. To render the file as a PDF graph, use the following command:

dot -Tpdf -o .pdf .dot

or

dot -Tpdf .dot -o .pdf

Many more details and documentation at Graphviz. 