CSE 635: Asynchronous Systems Homeworks, Spring 2003

[Announcements][Projects]  -  [Home]



Homework 1: Due Feb 18

1. SyncXor Gate

Define  zero-delay xor (exclusive or) gate with input signals in1 and in2 and output signal out:
  1. Directly, as an atomic module.
  2. As a composition, by using  the modules SyncNor, SyncAnd and SyncOr.

2. Composition

Let SyncNor implement a zero-delay nor (not or) gate. Why is the module defined by
hide x in SyncNor[in1, in2, out := set,ot, x] || SyncNor[in1, in2, out := x,  reset, ot]
not a correct implementation of an RS-Flip Flop?

3. Module properties

Define a module Nor such that the above definition is indeed an RS-Flip Flop.
  1. Give two initialized trajectories.
  2. Is the module finite? Closed? Deterministic? Asynchronous? Passive? Justify your answers.

4. Dining Philosophers

There are n philosophers (users) seated around a table, usually thinking (out of critical section). Between each pair of philosophers is a single fork (resource). From time to time, any philosopher might become hungry (requesting) and attempt to eat (enter critical section). In order to eat, the philosopher needs exclusive use of the two adjacent forks. After eating, the philosopher relinquishes the two forks (performs exit protocol) and resumes thinking (out of critical section).

Give a reactive modules solution for the above problem and for 4 philosophers that has the following properties:

  1. Mutual exclusion:  The (program counters of the) adjacent philosophers are not simultaneously in the critical section, i.e., the following invariant should hold:
      ~((pc1 = crit & pc2 = crit) | (pc2 = crit & pc3 = crit) | (pc3 = crit & pc4 = crit) | (pc4 = crit & pc1 = crit))
  1. Deadlock: There is no waiting ring of philosophers. Assuming that:
    1. To grab the left and the right fork the philosophers are in the states tstL and respectively tstR,
    2. The fork fk may have the states fr (free), lt (left) and rt (right) the following invariant should hold:
        ~((pc1 = tstL) & (pc2 = tstL) & (pc3 = tstL) & (pc4 = tstL) & (fk1 = rt) & (fk2 = rt) & (fk3 = rt) & (fk4 = rt))
Check your program with mocha. To check the invaruiants (e.g. the first) you have to write:
predicate mutex is ~((pc1 = crit & pc2 = crit) | (pc2 = crit & pc3 = crit) | (pc3 = crit & pc4 = crit) | (pc4 = crit & pc1 = crit))
judgment mutex is System |= mutex
First you have to succeed to parse, type check and construct the project window. Some of the programs are parsed, but the type checker might not detect a wrong name used instead of another name. This will crash the internal representation visitor (that assumes the program was type checked). Go gradually by commenting out parts of the program. Test your modules by simulating them. Alternatively, you might click the reach (mountains) button (you see how many states it has). Finally, test the judgments.

Your solution might not be fair, i.e., one of the philosopher may starve (never grab both forks). How should the data structure for the forks and the code for the philosopher be changed to assure fairness by construction? Explain in words.

Hints for the implementation in Reactive Modules

  1. Define a module for each fork, that takes requests (events) for the neighbors and grants access non deterministically to one of them. Use setL, setR, rstL, rstR for the input. The output fk (fork) is set accordingly (in the next clock). The values of fk  (the fork) should be: fr (free), rt (right), lt (left).
  2. Define a module for each philosopher. The module should contain only one lazy atom to account for the thinking, eating etc. time slots. The state of the philosopher should be: out, tstL (test left), tstR (test right), crit (critical section), drpL (drop left), drpR (drop right).
  3. A symmetric solution is wrong. Why? Break the symmetry and make an asymmetric solution.


 

Homework 2: Due Apr 8

1. (Transition graphs of compound modules)

Consider two compatible modules P and Q.
(10p) Assume that the two modules have no private variables (privXP =  privXQ = empty) and that the interface variables of one module are the external variables of the other module (intfXP =  extlXQ  and intfXQ =  extlXP ). Then the two modules and the compound module have the same state space SP = SQ = SP||Q. Prove that the transition action of the compound module P||Q is the intersection of the transition actions of the two component modules, i.e., s ->P||Q t iff s ->P t and s ->Q t. What can you say about the initial states of the compound module?

(10p) Assume that the two modules have no variables in common (XP  intersected with XQ  is empty). Then SP||Q = {(s1,s2)  |  s1 in SP  and s2 in SQ}. Prove that the transition action of the compound module is the cartesian product of the transition actions of the two component modules, i.e.,  (s1,s2) ->P||Q (t1,t2) iff  s1 ->P t1 and s2 ->Q t2. What can you say about the initial states of P||Q?

(10p) Now consider the general case. Consider two states s and t of the compound module P||Q. Prove that (1)  s is in P||Q.sI iff  s[XP] is in P.sI and s[XQ] is in Q.sI.  (2) s ->P||Q t iff s[XP] ->P t[XP]  and s[XQ] ->Q t[XQ].

Hint: Use in the argument the definition of a module (initial states and rounds) and of module composition.

2. (Fixpoint view of breadth-first search)

Let G = (S, sI, t) be a symbolic representation of a finite transition graph and let f and postG be defined as in the class:

 postG (s) = (EX. s & t)[X / X']
  f(s) = s |  postG (s)

where & and | are the boolean and and or operations, EX.s&t is existential quantification, i.e., exists(X, s&t)) and [X /X'] is renaming, i.e., rename(X',X). Show that:

(10p) f is monotonic, | continuous and & continuous.

(10p) What is the least fixpoint mf  and the greatest fixpoint nf ?

(10p) Explain in words why the symbolic search algorithm can be viewed as a fixpoint computation? Which fixpoint does it compute?

Hints:  You can identify & with intersection, | with union and => with subset. The empty set corresponds to false and the top set corresponds to true. Remember that a  function f is:

monotonic:       provided that    P1 => P2             implies that   f(P1) => f(P2)

| -continuous:   provided that    P1 => P =>...    implies that   f(|i Pi) = |i f(Pi)
&-continuous:   provided that    P1 <= P2 <=...     implies that   f(&i Pi) = &i f(Pi)

3. (Mutual exclusion)

(10p) Give the initial predicate and the transition predicate for the Peterson's protocol P1 || P2
(10p) Simulate the symbolic search algorithm for checking that Peterson's protocol satisfies the mutual exclusion requirement. For each iteration of the repeat loop give the state predicate sR after quantifier elimination and simplification.

4. (BDD for addition)

Let X = {x0,x1,y0,y1,o0,o1,c}.

(10p) Choose an appropriate ordering of the variables and construct the BDD for addition such that the output o1o0 together with the carry bit c is the sum of the inputs x1x0 and y1y0.


Homework 3: Due Apr 22

Solve problems 5.5, 5.9 from Chapter 5 and problems 6.2, 6.4 from Chapter 6.


Last updated on Mar 25, 2003 by Radu Grosu