UNSW   Faculty of Engineering myCSEPRINT VERSIONSITE MAP  
cse | School of Computer Science and Engineering (CRICOS Provider No. 00098G)
    #About CSE     #Undergraduate Study     #Postgraduate Study     #Timetables & Courses     #Research & Publications     #People & Work Units     #Help & Resources     #News & Events     #High School Portal

Last updated 16.03.04

Advanced Functional Programming [COMP4132]

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.


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
         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
Top Of Page

Site maintained by webmistress@cse.unsw.edu.au
Please read the UNSW Copyright & Disclaimer Statement