CS611 Preliminary Exam October 26, 2000Solutions1Domaintheorya. (10 pts.) Assume that f,g : D → D are continuous functions on a pointed cpo D with f(⊥)=g(⊥ )and f ◦ g = g ◦ f .Provethatfix f = fix g.Lemma: fn(⊥)=gn(⊥) (by induction on n)fn(⊥)=fn−1(f(⊥))= fn−1(g(⊥))= g(fn−1(⊥)) (by commutativity)= g(gn−1(⊥)) (induction hypothesis)= gn(⊥))Since fn(⊥)=gn(⊥) for all n,fn(⊥)=gn(⊥).b. (10 pts.) Given partial orders D1,... ,Dnwith respective bottom elements ⊥1,... ,⊥n,thesmashproduct D1⊗···⊗Dnis a partial order formed by taking tuples containing only non-bottom elementsfrom the Diplus a single new bottom element. Another way to think of it is as the ordinary productconstruction, but where all tuples containing any bottom component have been identified. Formally,(D1, 1) ⊗···⊗(Dn, n)=(D, )whereD = {d1,... ,dn|di∈ Di∧ di= ⊥ii∈1..n}∪{⊥}and the relation  is the least partial order relation containing at least the relationships defined bythe following two rules:diid ii∈1..nd1,... ,dnd 1,... ,d n⊥d1,... ,dnProve that the smash product of pointed cpos D1,... ,Dnis a pointed cpo.First, note that the ordering relation defined on the smash product is a partial or der (once all thereflexive relationships are added). The only non-trivial kind of ω-chain has the form...d 1,... ,d nd 1,... ,d nd 1,... ,d n ...where d i d i d i...Any upper bound of such a chain has the form d1,... ,dn where diis an upper b ound of d i,d i,etc.Therefore, the tuple whose components are the least upper bounds componentwise is no larger than anyother upper b ound and must be the le a st upper bound itself. This argument is of course exactly thesame as the argument for an ordinary product of cpos, which makes sense because the smash productis isomorphic to the lift of the product of the cpos minus their bottom elements.Finally, D is a pointed CPO because it has a bottom element, ⊥.12 Operational semantics for concurrent processesThe new concurrent programming language LIMPA extends IMP with support for multiple executing pro-cesses, each with their own state, and interprocess communication primitives. The IMP language is extendedwith the following new syntax:c ::= ...| fork c | send p, a | X := recv PP ::= {p1,... ,pn}The fork command executes the command c in a new process whose state is initially the same as that ofthe process executing the fo rk.Thesend command sends the value of the expression a to the port p.Portsare assumed to come from some countable set of port identifiers whose precise form is unimportant. Therecv command allows a process to read non-deterministically from any of a set of ports P . (The ability toread from a set of ports allows a receiver to multiplex multiple senders.) Both send and recv are blockingcommunication primitives: the sending process waits at a send until another process executes a matchingrecv, and vice versa. A given message is only delivered to a single process.For example, the following program ping-pongs an integer counter back and forth between two processes,such that one process only sees the even integers and the other the odd ones. The main process forks twoprocesses and then terminates, but the program executes until all processes are done.x:=0;fork (while x < 1000 do (send p1, x+1; x := recv {p1}));fork (while x < 1000 do (x := recv {p1}; send p1, x+1))The LIMPA designers need your ingenuity in designing the small-step operational semantics for thelanguage. They have managed to decide on a configuration for the semantics; a configuration t is defined as:t ::= c, σ | t1 t2A configuration is essentially an unordered collection of process configurations (c, σ pairs) and can bewritten as c1,σ1 ...  cn,σn. Note that the symbol  is not part of the LIMPA language syntax! To allowthe list of processes to be reordered and reassociated arbitrarily without destroying or creating processes,they have added the following rules already:t1 t2→ t2 t1t1 (t2 t3) → (t1 t2)  t3(t1 t2)  t3→ t1 (t2 t3)The LIMPA designers understand IMP pretty well, but they are having trouble defining the small-steprules for fork, send,andrecv.a. (3 pts.) Define what configurations you would like to consider final in LIMPA. What kinds of stuckconfigurations, if any, exist?One reasonable choice for a final configuration is a configuration of the form skip,σ.Because send and recv can block waiting for an appropriate process to exchange information with, aconfiguration c1,σ1 ...  cn,σnisstuckifeachofthecommandscihas the form send pi,n or send pi,n; cor X := recv Pior X := recv Pi; c, and none of the ports piis a member of any of the sets Pi.b. (5 pts.) Assuming p ∈ P , what should the configuration send pn, σ1 X := recv P, σ2step to inorder that progress is made and the message is transmitted to exactly one process?skip,σ1 skip,σ2[X → n]2How about send pn; c1,σ1 X := recv P ; c2,σ2,wherec1and c2are arbitrary commands?skip; c1,σ1 skip; c2,σ2[X → n]orc1,σ1 c2,σ2[X → n]To write the rules for more general uses of send, recv and the existing IMP commands, a more generaltechnique using evaluation contexts is needed. First of all, the designers would like to be able to express mostof the semantics by building on the IMP SOS with the following rule, in which the relation in the premise isthe original IMP small-step evaluation relation, and the function T is a suitably defined evaluation context.c, σ→c ,σ T [c, σ] → T [c ,σ ]c. (5 pts.) Write a BNF definition of the evaluation context T . It may be useful to define more than onekind of evaluation context.T ::= [·] | T  tC ::= [·] | C; cd. (5 pts.) Use your evaluation context T to write a small-step rule for send and recv.p ∈ PT [C1[send pn],σ1 C2[X := recv P ],σ2] → T [C1[skip],σ  C2[skip],σ2[X → n]]e. (5 pts.) Similarly, write a small-step rule for fork.T [C[fork c],σ] → T [C[skip],σ]  c, σf. (2 pts.) What other rules are needed to complete the LIMPA SOS?For termination:skip,σ  t → tFor evaluation of send:a, σ→a ,σT [C[send pa,σ]] → T [C[send pa ,σ]]3 A variation on continuation-passing styleIn class we talked about CPS conversion from a call-by-value lambda calculus to a simpler CPS languagein