Define reaching definitions for a parallel programming construct: (10pts)
Y := X;
Z := 1;
WHILE Y > 0 DO
Z := Z * Y; Y := Y - 1 || Y := Y - 1; Z := Z * Y;
SKIP;
This program includes a new construction, t1 || t2
, that executes t1
and t2
in parallel in the same memory space. Define a general procedure for defining reaching definitions for t1 || t2
terms. You need not redefine reaching definitions for other terms. (5pts)
In class we defined the language:
S ::= x := a | S1 ; S2 | if b then S1 else S2 fi | while b do S od
and an annotated type system that calculates reaching definitions. Add the t1 || t2
term from the previous exercise to this language and define a type rule for calculating reaching definitions. Only provide a definition for this construct, not the entire language. (5pts)
Let’s extend reaching analysis to determine both when a variable is set and when it is used. Our state for reaching analysis is the set of variable, label pairs that record where a variable was last set with the additional label ?
indicating a variable has not been set. Let’s add a new label, !
, that indicates a variable is used before being set. For example, {(X,!),(Y,1),(Z,?)}
indicates that X
is used prior to being set, Y
was last set at label 1
and Z
was never set.
RDEntry
and RDExit
for each construct. (5pts)Our last in-class example defined a parameterized counter. Thinking about that counter:
false
and down when true
. Use logic notation, not z3. (5pts)I
and P
do not change from the original counter definition, how would you determine if P
is invariant over this new system? (5pts)