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[2] = {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.

cs-486/homework-1-2016.txt · Last modified: 2017/01/11 16:39 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