# 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.

- Define rules for each language construct that update state. Specifically, define
`RDEntry`

and `RDExit`

for each construct. (5pts)
- Define a trace-based gathering semantics for this analysis. Specifically, define how each language consruct adds to a program trace. (5pts)
- 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:

- 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)
- 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

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