Differences

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

 — cs-486:homework-1-2016 [2017/01/11 16:39] (current)egm created 2017/01/11 16:39 egm created 2017/01/11 16:39 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: + + + 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 === + + [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: + + + ​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 <​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 