School of Computer Science and Engineering, UNSW CRICOS Provider No. 00098G

Session 1, 2004

## Exercises: Semantics of IO, Part II

The following exercises are based on the operational semantics for IO operations defined in Simon Peyton Jones' Tackling the Awkward Squad.

### The Semantics of IORefs

For the first two exercises, the rules of up to and including Secton 3 are relevant; these are Figures 2-5. In other words, we don't consider concurrency and exceptions yet.

#### Program execution

Assume the following program:

swap a b = readIORef a >>= \av ->
writeIORef a bv
writeIORef b av

main = newIORef 14  >>= \r1 ->
newIORef 3   >>= \r2 ->
swap r1 r2

Use the transition semantics in the same way as it is done on Page 27 of Peyton Jones' paper to execute this program. Note the interaction between the evaluation function and the transition rules and also how ν (nu) ensures the uniqueness of reference names.

NB: In a "real" program, one would use the do notation, instead of explicitly using >>=, but for this exercise, I have avoided do to keep things a little simpler.

#### Determinism(*)

Formally prove that the execution of programs is deterministic. We use the following definitions in addition to those in the paper:

• We denote the transitive closure of the transition relation →α as →t*, where for two program states P and Q, we have
P →t* Q if P →α1 … →αn Q, where n ≥ 0 and t = α1 … αn.
We call t the trace of →t*.
• A program state P is final if there exists no program state Q, such that Pα Q.

Now show the following:

Given a program M with final program state P and trace t, for every final program state Q with {M} →s* Q, we have P = Q and t = s.

NB: You can assume that the evaluation function E of the inner denotational aspect of the semantics is deterministic.

### The Semantics of Concurrency

Assume the following program:

import Char

main = newEmptyMVar          >>= \in  ->
newEmptyMVar          >>= \out ->
forkIO (upper in out) >>
putMVar  in 'a'
takeMVar out	     >>= \c   ->
putChar c
where
upper i o = takeMVar i              >>= \c ->
putMVar  o (toUpper c)

Again, use the transition semantics to execute this program. Note in which way blocking of threads is achieved in the operational semantics.

(*)Challenging exercise