CSE 128 Spring
2004
Concurrency
Problem 2.3: For the
first part of the question, remember that "leads to" is typed as
"~>". For the book, the macro package changes the tilda to a space.
To solve the second part of this question, you need to define two
properties: one for the conjunction of two weak fairness properties and
one for weak fairness on the disjunction of the two actions. Call these
two properties F1 and F2. You will show that AltSpec
=> )F1 => F2) /\ (F2 => F1). That is, you show that of all the
behaviors of AltSpec (which includes no fairness), those that satisfy
F1 also satisfy F2 and vice versa.
Problem 2.8: For RelayRing,
use Call as the external
action, and have the parameter be a pair <i, v> where i is the process and v is a value from Input. For example, if Input is {0, 1} and N = 3, then a behavior
might be:
arg: <0, 0>
-> arg: <1, 1> -> arg: <2, 1>; arg: <0, 1>
-> ...
TokenPass will generate the
same external actions.