Session 1, 2004
The following exercises are based on the operational semantics
for IO
operations defined in Simon Peyton Jones'
Tackling the Awkward Squad.
IORef
sFor 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.
Assume the following program:
swap a b = readIORef a >>= \av -> readIORef b >>= \bv -> 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.
Formally prove that the execution of programs is deterministic. We use the following definitions in addition to those in the paper:
P →t* Q if P →α1 … →αn Q, where n ≥ 0 and t = α1 … αn.We call t the trace of →t*.
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.
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.