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