Final Exam

Midterm

Date: 9 May - 16 May 2019

Exercise 1

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)

Exercise 2

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)

Exercise 3

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.

1. Define rules for each language construct that update state. Specifically, define RDEntry and RDExit for each construct. (5pts)
2. Define a trace-based gathering semantics for this analysis. Specifically, define how each language consruct adds to a program trace. (5pts)
3. Explain how to define α and γ so that we could derive a z3 analysis for our gather semantics. DO NOT ATTEMPT TO DO THE DERIVATION. (5pts)

Exercise 4

Our last in-class example defined a parameterized counter. Thinking about that counter:

1. Add a new boolean input, ‘d’, to the counter that causes the counter to go up when false and down when true. Use logic notation, not z3. (5pts)
2. Given that I and P do not change from the original counter definition, how would you determine if P is invariant over this new system? (5pts)

Resources

• PoPA - I used notes from Chapter 1
• Tinelli’s Notes - The counter example I referenced in class starts on page 22.

notes

1. Watch the class blog for updates.
2. Submit your solution using Blackboard.