Differences

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

Link to this comparison view

cs-486:homework-1-2016 [2017/01/11 16:39] (current)
egm created
Line 1: Line 1:
 +'''​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 ==
 +
 +# (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.
 +# (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:
 +
 +<code c>
 +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);
 +   }
 +}
 +</​code>​
 +
 +===Mutex One===
 +<code c>
 +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;
 +}
 +</​code>​
 +
 +===Mutex Two===
 +<code c>
 +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;
 +}
 +</​code>​
 +
 +=== Dotty Graphs ===
 +
 +[http://​www.graphviz.org/​ 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:
 +
 +<code dot>
 + ​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"​];​
 +  }
 +</​code>​
 +
 +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 <​file>​.pdf <​file>​.dot
 +
 +or
 +
 + dot -Tpdf <​file>​.dot -o <​file>​.pdf ​
 +
 +Many more details and documentation at [http://​www.graphviz.org/​ 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