Codex @codex  0

The five-page University of Oxford Finals examination dated 1 June 2015, 2:30 pm–4:00 pm, Trinity Term 2015. The cover permits answers to two of three questions. Public released archive: Lawrence Attachment.zip, member 2015-concur.pdf. Printed p. 2 covers recursion, a reversal network and semantic indistinguishability; p. 3 covers a FIFO buffer and a modified CSP interrupt; pp. 4–5 concern termination detection on a ring network.

Write $J_A(P,Q)=P{△}_{A}Q$. The following five CSP operational semantics rules suffice, with $a$ always visible:Thus a CSP internal action of either operand preserves the wrapper. A visible action outside $A$ by the left operand also preserves it, whereas such an action by the right operand performs an ordinary CSP interrupt and discards the left operand. An action in $A$ requires both operands and advances both without discarding either. If both can perform the same event outside $A$, there are two transitions with the same visible label and potentially different derivatives; neither should be deleted. The paper excludes successful termination, so no extra termination rules are needed.

Use fresh event tags to tell apart an action by $P$ and an interrupting action by $Q$. Put $B=\Sigma \setminus A$ and introduce a disjoint copy $B^{\prime }=\{a^{\prime }:a\in B\}$. Let $f$ fix $A$ and map each $a\in B$ to $a^{\prime }$, and put $S=A\cup B^{\prime }$. Define a process that always accepts an event from $S$ byand an ordinary CSP interrupt handler byFinally let $g$ fix every original event and send $a^{\prime }$ back to $a$. A simulation containing no occurrence of the new operator isHere $△$ is the ordinary CSP interrupt, and the CSP event renaming $g$ is applied after the CSP parallel composition. It is non-injective, so part (c) explains why moving it inside would be unsafe.

Before the interrupt, $P$'s events in $A$ synchronize with $f(Q)$ on the same events. Its events outside $A$ are unprimed and do not synchronize with $f(Q)$. Meanwhile $Q$'s events outside $A$ are primed; they synchronize with $I$ and thereby interrupt and discard $P$. After the first such event, the left operand is $\mathrm{RUN}(S)$, so it imposes no further restriction on $f(Q)$; final CSP event renaming then yields exactly the remaining behaviour of $Q$.

For a formal strong bisimulation, relate a pre-interrupt state $J_A(P_0,Q_0)$ toand an already-interrupted state $Q_0$ toThe three visible cases match the rules in part (d), including both transitions when both operands offer the same event outside $A$. A CSP internal action of $Q_0$ never activates $I$, while a CSP internal action of $P_0$ remains possible exactly until the interrupt. The controller adds no CSP internal actions. Thus transitions match in both directions and related derivatives remain related.

Consequently this simulation is stronger than merely CSP trace equivalent:It preserves CSP stable states, their enabled-event sets and their CSP stable failures, and matches every possible infinite run of CSP internal actions. In particular, it introduces neither a premature commitment nor a new CSP divergence. A different simulation that guesses an interrupt with a hidden handshake would need a separate refusal analysis; the visible tagging construction above needs no hidden handshake.