Past exam of the computer science course of the University of Oxford 2015 Concurrent programming 3 a Solution by 
Codex 0 2026-10-31
Codex 0 2026-10-31A counting semaphore holds a nonnegative number of permits.
down waits until a permit is available and consumes one; up returns a permit and can release a waiting caller. A binary semaphore restricts the number available to zero or one. Unlike a mutex, a semaphore need not be released by the same software thread that acquired it; this permits producer-to-consumer signalling.Interpret
maxCount as the initial number of permits and, for this bounded implementation, the maximum permitted number of unmatched releases. An up beyond that capacity is a programming error, rather than a blocking operation. Clients obey this release discipline. If an unbounded counting semaphore is desired instead, remove the upper-bound requirement and use a sufficiently wide counter; a capacity-one instance is binary only under the corresponding balanced-use discipline.class CountingSemaphore(maxCount: Int) extends Semaphore {
require(maxCount > 0)
private var count = maxCount
def down: Unit = synchronized {
while (count == 0) wait()
count -= 1
}
def up: Unit = synchronized {
require(count < maxCount, "unmatched semaphore release")
count += 1
notify()
}
}All accesses to
count occur under the same monitor. wait atomically releases that monitor while sleeping, then reacquires it before returning. The while is needed because of spurious wakeups and because another caller can consume the returned permit before the notified caller reacquires the monitor. Only down callers wait here, and they all wait on the same predicate; hence waking one with notify is sufficient. A later up notifies another waiter if necessary. This use of notify will not be safe for the mixed predicates in the next part.[ref]Java 8 Object API documentation. notify and wait: arbitrary notification choice, monitor reacquisition and spurious wakeups
A binary semaphore initially available is
new CountingSemaphore(1). To initialize it unavailable, call its down once during construction, before publishing it to other software threads. Its state obeysThis implementation provides no first-come-first-served guarantee: a new caller can acquire the monitor before a notified waiter. The following examples assume ordinary successful execution without cancellation or interruption of a partially completed buffer operation. Past exam of the computer science course of the University of Oxford 2015 Concurrent programming 1 e Solution by Codex 0 2026-10-31
Codex 0 2026-10-31Use a return control channel to carry both cancellation and one-slot flow control. The latter is what prevents a silent consumer from obstructing other streams. Keep the preceding
MUX type and addsealed trait CTRL
final case class Grant(stream: Int) extends CTRL
final case class Cancel(stream: Int) extends CTRLHere is a precise event-loop specification of the modified generators.
choose means a fair Communicating Scala Objects guarded alternation over the listed input events, output events and a short closure-poll timer; every selected transition below is finite and contains no further blocking communication. An output transition commits its state change only after its selected send succeeds. The notation is operational pseudocode, with the requested signatures; it does not introduce an assumed nonblocking send primitive.def iMux[T](ins: Seq[?[T]], ctrl: ?[CTRL], mid: ![MUX[T]]): PROC
for each stream i:
credit[i] = true; inputOpen[i] = true; terminal[i] = false
pending[i] = None // Option[MUX[T]]
until every terminal[i]:
poll closures:
if !ins[i].canInput: inputOpen[i] = false
if !terminal[i] && !inputOpen[i] && pending[i].isEmpty:
pending[i] = Some(MUX(i, None)) // end follows earlier data
choose:
ctrl ? Grant(i):
if !terminal[i]: credit[i] = true
ctrl ? Cancel(i):
terminal[i] = true; pending[i] = None; ins[i].closeIn
ins[i] ? x, enabled when inputOpen[i] && !terminal[i]
&& credit[i] && pending[i].isEmpty:
credit[i] = false; pending[i] = Some(MUX(i, Some(x)))
mid ! pending[i].get, enabled when pending[i].nonEmpty:
if pending[i].get.item.isEmpty: terminal[i] = true
pending[i] = None
poll timer: no action
finally: close every ins[i] input; close mid output and ctrl input
def iDemux[T](ctrl: ![CTRL], mid: ?[MUX[T]], outs: Seq[![T]]): PROC
for each stream i:
slot[i] = None; ended[i] = false; cancelled[i] = false
replies = empty FIFO queue of CTRL
until every (cancelled[i] || (ended[i] && slot[i].isEmpty)):
poll closures:
if !cancelled[i] && !ended[i] && !outs[i].canOutput:
cancelled[i] = true; slot[i] = None
delete any queued Grant(i); append Cancel(i) to replies
if !cancelled[i] && ended[i] && slot[i].nonEmpty
&& !outs[i].canOutput:
cancelled[i] = true; slot[i] = None
if ended[i] && slot[i].isEmpty: outs[i].closeOut
choose:
mid ? MUX(i, Some(x)):
if !cancelled[i]: assert slot[i].isEmpty; slot[i] = Some(x)
mid ? MUX(i, None):
ended[i] = true
outs[i] ! slot[i].get, enabled when !cancelled[i] && slot[i].nonEmpty:
slot[i] = None
if !ended[i]: append Grant(i) to replies
ctrl ! replies.front, enabled when replies.nonEmpty:
remove replies.front
poll timer: no action
finally: close mid input, every output, and ctrl outputThere is one receive event on
mid, with the two packet forms dispatched in its body, and one send event on mid, offering a fairly chosen pending stream. There is likewise one send event on ctrl. If mid becomes exhausted, the channel demultiplexer marks any remaining streams ended, discards queued replies, and drains or cancels their slots; the sender has then finished and needs no more grants. If the control input closes, the channel multiplexer enters cleanup. If the receiver finds its control output closed, it discards queued replies and disables further control sends, but continues receiving end markers and draining its slots; sender completion must not discard already accepted values. A channel closing during an individual guarded operation is handled locally: a failed outs(i) send cancels that stream and queues Cancel(i) unless it had already ended; exhaustion of a shared port uses the cleanup rules just stated. Ports that closed while their data events were disabled are found by the poll. These rules specify closure handling as well as normal transitions.The credit starts at one and is consumed when an input is accepted. It is returned only after the corresponding output finishes. Thus the one permitted outstanding value for stream is either pending at the sender or stored at the receiver, never both. An end marker needs no credit and follows that stream's last data packet on the ordered shared message-passing channel. It can arrive while that value is still waiting for its consumer; the receiver then delays closing the output until its slot empties. The invariant isAs in a strict buffer, cancellation can discard the last outstanding value. A cancelled receiver ignores a data packet already in flight; a later grant cannot resurrect a cancelled sender. No selected data delivery blocks the event loop, and control replies are queued rather than sent inside a receive handler. In particular, there is no cycle in which the sender blocks sending data while the receiver blocks sending cancellation. Closing the control output at final receiver termination also releases the sender if a last cancellation was still queued.
Under fair event selection and eventual scheduling, an individual cancellation reaches its producer without waiting for any unrelated consumer. Producer closure similarly delivers its own end marker without waiting for another stream to drain. This gives finite flow control equivalent in ordering and termination to capacity-one strict buffers, with finite protocol delays. A physical shared message-passing channel necessarily serializes transfers, so instantaneous readiness and absolute real-time delay bounds are not identical to physically separate buffers.
Past exam of the computer science course of the University of Oxford 2015 Concurrent programming 1 d Solution by Codex 0 2026-10-31
Codex 0 2026-10-31A channel multiplexer adds a stream identity; a channel demultiplexer removes it and selects the corresponding output. Add an explicit per-stream end marker, since closing the shared message-passing channel cannot identify which producer has finished.
End(i) is represented by None; Some(x) represents a genuine value, including a null value if the application permits one.final case class MUX[T](stream: Int, item: Option[T])The following Communicating Scala Objects implementation uses a synchronous one-to-one
mid. As in part (a), a short timer detects closure even when no communication is enabled. Only the channel multiplexer owns the input ports, and only the channel demultiplexer owns the output ports. The channel multiplexer takes at most one input value before its corresponding mid write; it never accepts a second input while that write is pending.def iMux[T](ins: Seq[?[T]], mid: ![MUX[T]]): PROC = proc {
val ended = Array.fill(ins.length)(false)
val poll = 1000000L
try {
while (mid.canOutput && ended.contains(false)) {
for (i <- ins.indices if !ended(i) && !ins(i).canInput) {
mid ! MUX[T](i, None)
ended(i) = true
}
if (ended.contains(false)) {
alt(
(| (for (i <- ins.indices) yield
(!ended(i) && ins(i)) =?=> { x => mid ! MUX(i, Some(x)) }))
| after(poll) ==> { () }
)
}
}
} catch { case _: io.threadcso.process.Stopped => () }
finally { ins.foreach(_.closeIn); mid.closeOut }
}
def iDemux[T](mid: ?[MUX[T]], outs: Seq[![T]]): PROC = proc {
val ended = Array.fill(outs.length)(false)
val poll = 1000000L
try {
while (mid.canInput && ended.contains(false) &&
outs.indices.forall(i => ended(i) || outs(i).canOutput)) {
alt(
mid =?=> { packet =>
val i = packet.stream
require(i >= 0 && i < outs.length && !ended(i))
packet.item match {
case Some(x) => outs(i) ! x
case None => ended(i) = true; outs(i).closeOut
}
}
| after(poll) ==> { () }
)
}
} catch { case _: io.threadcso.process.Stopped => () }
finally { mid.closeIn; outs.foreach(_.closeOut) }
}For each stream, the output sequence remains a prefix of its accepted input sequence. One value can be pending in the channel demultiplexer, and one in the channel multiplexer, possibly from the same stream. Hence its discrepancy is at most two:There is a shared total of two pending values, so these processes do not supply the independent readiness of a parallel collection of capacity-two strict buffers. An unready consumer blocks the channel demultiplexer's ordinary send; the channel multiplexer can accept one further value and then blocks too. This is head-of-line blocking.
The alternation may choose an input unfairly; replacing its selection policy by round-robin selection helps among simultaneously ready producers. Even fair input choice cannot compensate for a consumer that blocks the entire channel demultiplexer. Closed-input scanning does allow a producer's end marker eventually to reach its consumer, but only after the shared transport and any earlier delivery become serviceable. Its own accepted values precede its end marker, so that consumer drains cleanly.
Consumer-driven closure is more restrictive. With no return message-passing channel, the sender cannot promptly learn which producer should stop. This implementation deliberately shuts down the whole multiplexed channel when it detects any unfinished consumer closing, thereby cancelling the other pairs too. If the channel demultiplexer is already blocked on some other consumer, even that detection waits for the blocked send. Thus producer-driven ends can be represented separately but need not be delivered promptly; consumer-driven cancellation is global and need not be detected promptly. Merely adding an end marker does not solve either delay.
Past exam of the computer science course of the University of Oxford 2015 Concurrent programming 1 c Solution by Codex 0 2026-10-31
Codex 0 2026-10-31Use a tagged union so that an idle indication cannot be confused with an actual value of type
T. Heartbeat messages are transport messages only and never reach the consumer.sealed trait InterPeer[+T]
final case class Data[T](value: T) extends InterPeer[T]
case object Idle extends InterPeer[Nothing]
case object EndPeer extends RuntimeException
case object PeerTimeout extends RuntimeExceptionHere are two small Communicating Scala Objects helpers. A timer expiring after a port has closed denotes orderly end-of-stream, rather than evidence of a silent peer. Closure can instead make the alternation throw
Stopped directly. sendWithin completes exactly one send, or throws; receiveWithin completes exactly one receive, or throws. Time arguments are positive nanosecond intervals.def sendWithin[A](p: ![A], value: A, t: Long): Unit = {
if (!p.canOutput) throw EndPeer
alt(
p =!=> { value }
| after(t) ==> {
if (!p.canOutput) throw EndPeer else throw PeerTimeout
}
)
}
def receiveWithin[A](p: ?[A], t: Long): A = {
if (!p.canInput) throw EndPeer
var result: Option[A] = None
alt(
p =?=> { x => result = Some(x) }
| after(t) ==> {
if (!p.canInput) throw EndPeer else throw PeerTimeout
}
)
result.get
}The sender waits only half the agreed interval before preparing an idle indication, leaving some scheduling allowance before the receiver's deadline. A pending data or idle send has its own deadline, so a failed receiver cannot strand the sender forever. An application with a guaranteed network-delay bound should subtract that bound, plus scheduling allowance, when choosing the heartbeat period.
def iPr[T](timeout: Long, in: ?[T], out: ![InterPeer[T]],
fail: ![Unit]): PROC = proc {
require(timeout >= 2)
var failed = false
try {
while (in.canInput && out.canOutput) {
var packet: InterPeer[T] = Idle
alt(
in =?=> { x => packet = Data(x) }
| after(timeout / 2) ==> { () }
)
// A just-accepted Data must survive a simultaneous upstream close.
if (packet != Idle || in.canInput) sendWithin(out, packet, timeout)
}
} catch {
case PeerTimeout => failed = out.canOutput
case EndPeer => ()
case _: io.threadcso.process.Stopped => ()
} finally { in.closeIn; out.closeOut }
try { if (failed) fail ! (()) }
catch { case _: io.threadcso.process.Stopped => () }
finally { fail.closeOut }
}
def iCon[T](timeout: Long, in: ?[InterPeer[T]], out: ![T],
fail: ![Unit]): PROC = proc {
require(timeout > 0)
var failed = false
try {
while (out.canOutput) {
receiveWithin(in, timeout) match {
case Idle => ()
case Data(x) => sendWithin(out, x, timeout)
}
}
} catch {
case PeerTimeout => failed = out.canOutput
case EndPeer => ()
case _: io.threadcso.process.Stopped => ()
} finally { in.closeIn; out.closeOut }
try { if (failed) fail ! (()) }
catch { case _: io.threadcso.process.Stopped => () }
finally { fail.closeOut }
}Each failure port has a supervising receiver that accepts its single notification; data-port cleanup occurs before that potentially blocking notification. The sender reports an interpeer send taking too long. The receiver reports an excessive interpeer receive delay or an excessive delay delivering a value to the consumer. Producer idleness alone is healthy and causes heartbeat messages, not a failure. A sufficiently slow consumer can ultimately cause both detectors to fire, since its backpressure reaches the sender.
Ignoring heartbeat messages, at most one genuine value is held by each intermediary with a synchronous interpeer message-passing channel; no value overtakes another. Normal upstream closure propagates after the last accepted genuine value is delivered, provided its delivery meets the deadline. The pair is not ready for another input while its sender is blocked sending, so it has the specified prefix and bounded-storage properties without every readiness property of an ideal strict buffer. Its useful guarantee isA timeout establishes suspicion, not proof of a crash: a live but delayed peer or an excessive network delay gives the same observation. There is no promise of bounded detection when the detector itself is never scheduled, nor of exact agreement between the two failure indications. A sender-side deadline measures completion of its own send: a network adapter that merely accepts values into local storage cannot confirm remote receipt. Detecting that remote failure at the sender would require confirmations over a return message-passing channel.
Past exam of the computer science course of the University of Oxford 2015 Concurrent programming 1 b Solution by Codex 0 2026-10-31
Codex 0 2026-10-31A cyclic Communicating Scala Objects component has a communication loop followed by a close-down phase.
repeat { ... } catches the library's normal Stopped family of exceptions, including closure, and leaves the loop; ordinary while code instead needs the explicit handler used above. In either case, cleanup closes every owned input port with closeIn and every owned output port with closeOut, preferably in finally. Reclosing a one-to-one port is harmless. A parallel composition completes only when every component has completed; one component returning does not automatically cancel all the others.The producer closes
left on return. The strict buffer observes this, drains its FIFO queue into a cooperating consumer, and closes right; the consumer's next read detects closure and enters its own cleanup. Conversely, the consumer closes right on return; the strict buffer then closes left, releasing a blocked producer write or causing its next write to stop. Thus,Eventual termination assumes that surviving components reach their next communication or closure check, and that the consumer keeps accepting a finite outstanding backlog after producer termination. A component stuck forever in unrelated computation cannot be stopped by closing a port alone. Past exam of the computer science course of the University of Oxford 2015 Concurrent programming 1 a Solution by Codex 0 2026-10-31
Codex 0 2026-10-31Store the accepted but undelivered values in an ordinary FIFO queue, owned exclusively by the Communicating Scala Objects process. An input event is enabled precisely when the FIFO queue is not full, and an output event precisely when it is not empty. An output event's expression is evaluated only after that event is selected; its epilogue runs after the output completes. The following uses no buffered communication message-passing channels.
def strictBuffer[T](capacity: Int, in: ?[T], out: ![T]): PROC = proc {
require(capacity > 0)
val q = scala.collection.mutable.Queue[T]()
val poll = 1000000L // nanoseconds
try {
while (out.canOutput && (in.canInput || q.nonEmpty)) {
alt(
(q.size < capacity && in) =?=> { x => q.enqueue(x) }
| (q.nonEmpty && out) =!=> { q.front } ==> { q.dequeue(); () }
| after(poll) ==> { () }
)
}
} catch { case _: io.threadcso.process.Stopped => () }
finally { in.closeIn; out.closeOut }
}Here
canInput and canOutput mean that the port has not become permanently unable to communicate; they are not instantaneous readiness tests. A closed input event is disabled by the Communicating Scala Objects guarded alternation. The timer periodically rechecks closure even when the affected port's data event is disabled, for example when the FIFO queue is empty and the downstream port closes. It neither transfers data nor imposes a deadline on a healthy producer. This avoids silently assuming that closure of a disabled event wakes an alternation. The relevant output-event and closure conventions are documented in [ref].Write and for the input and output sequences. The loop invariant is that is followed by the contents of the FIFO queue. An input appends one value to its rear; an output removes exactly its front. Consequently,The two data events remain offered whenever their respective size conditions hold. Under a fair choice policy, an endlessly ready event is eventually selected. The timer requires the usual assumption that expiry cannot starve a ready communication forever.
When the input closes, no more values are accepted, but all remaining values stay eligible for output. Once the FIFO queue empties, the process closes its output and terminates. If the output closes first, there is no recipient for those remaining values: the process abandons them, closes the input to release the producer, and terminates. Draining after upstream closure requires a consumer that continues receiving. The positive-capacity precondition is deliberate: two separate synchronous message passing events cannot provide a capacity-zero buffer with zero discrepancy after every event; that would require a simultaneous three-party transfer.
Past exam of the computer science course of the University of Oxford 2015 Concurrency 3 f Solution by Codex 0 2026-10-31
Codex 0 2026-10-31For a general ring, no. Being idle at the instant the coordinator starts is not the same as remaining idle until sampled. A downstream node that has not yet received the first-round message is still in its state and may become active.
For a concrete example, first perform , so all nodes are idle. Then take this CSP trace:At the first displayed event the coordinator has started and all nodes are idle. Node has received true and is frozen, but node can still activate before receiving the token. It forwards false, so the entire second round carries false and nobody shuts down. After the final , all nodes are idle again. The coordinator may then perform forever without starting another survey. This is an infinite execution with no shutdown and no assumption of fairness that would exclude it.
ThereforeThis does not contradict part (e): its stronger trigger, the true first-round return, never occurs in the failed survey. For the special ring, starting by already samples and freezes the only non-coordinator. If both nodes are idle at that event, this particular counterexample is impossible and the successful-survey progress argument applies. The general claim in the question must cover larger rings, where the unsampled downstream node exists.
Past exam of the computer science course of the University of Oxford 2015 Concurrency 3 e Solution by Codex 0 2026-10-31
Codex 0 2026-10-31The trigger is specifically the first-round reception . A CSP trace restriction cannot by itself guarantee progress after this event, because a finite prefix is compatible with both completion and an indefinitely delayed completion. We need to exclude both a stable refusal to continue and CSP divergence, so use the CSP failures-divergences model.
Here is an explicit conditional check that imposes no progress requirement before the trigger. Build the reachable labelled transition system of and observe coordinator rounds with a two-phase monitor: it starts in the first-return phase and toggles on each . Collect the set of system derivatives immediately after a true return in the first-return phase. This distinguishes the survey's return from the decision's return, without changing any system transitions. For fixed finite , the set is finite. DefineHere denotes CSP internal choice. Perform the single CSP refinement checkEquivalently, check each post-trigger derivative individually against after the displayed CSP hiding. If the trigger is unreachable, the conditional property is vacuously true and there is no post-trigger check to perform.
The CSP internal choice in deliberately permits any next shutdown, including an implementation that offers only one of the remaining shutdowns. It forbids a stable refusal of all remaining shutdowns, has no CSP divergence, and permits at most distinct shutdowns before . A CSP external choice over all remaining nodes would instead demand simultaneous readiness for every remaining shutdown and would unnecessarily reject the protocol's sequential delivery.
After hiding all other actions, endless internal work becomes a CSP divergence and a blocked unfinished state becomes a forbidden CSP stable failure. Since there are only possible shutdown actions and duplicates are excluded by CSP traces, every maximal progressing execution must complete all . As usual for untimed CSP, this progress claim assumes the environment allows shutdown signals to occur; it supplies no wall-clock deadline. No fairness assumption requiring the coordinator eventually to initiate a survey has been smuggled into this conditional check.
For the defined system the check succeeds. Immediately after the trigger all statuses are idle and frozen. The only message work left is the second round: node sends the decision to node , nodes through forward it, and node receives it. These are exactly more message transfers. Each node then has its one shutdown action, and the message can advance even while an earlier node's shutdown is pending. Thus there are no remaining status changes, no message cycle, and no unfinished global state in which every action is blocked. The measurestarts at , is nonnegative, and decreases on every subsequent transition. This excludes any hidden infinite run; before all shutdowns finish there is either an enabled message transfer or an enabled shutdown signal. The operational argument proves the conditional claim for every ; finite state enumeration is only a supporting check.
Past exam of the computer science course of the University of Oxford 2015 Concurrency 3 d Solution by Codex 0 2026-10-31
Codex 0 2026-10-31This is a safety property: a bad shutdown or a later reactivation has a finite bad CSP trace. Use the CSP traces model. Let , let track active nodes, and let track nodes that have announced shutdown. Let contain every message CSP event. Define the following specification over the status-signal alphabet:Use the CSP refinement checkThe specification offers a shutdown only if the active set is empty, and offers no activation once is nonempty. A trace violating either requirement is therefore absent from the specification. Recording also prevents duplicate shutdowns and any status change by an already shut-down node. CSP hiding removes message details irrelevant to this finite bad-prefix check; a CSP traces model check alone does not assert eventual progress.
The system satisfies the check. After the first message has passed nodes , its bit is the Boolean conjunction of their being idle when sampled. Every sampled node is then frozen until it forwards the second-round decision. A true bit returning to node therefore means that every non-coordinator is idle and still frozen; the coordinator has itself remained idle. A true decision consequently reaches only idle nodes, each of which proceeds to shutdown rather than returning to . No node can subsequently become active. A false decision permits no shutdown at all.
Past exam of the computer science course of the University of Oxford 2015 Concurrency 3 c Solution by Codex 0 2026-10-31
Codex 0 2026-10-31For each node letThe required CSP alphabetized parallel composition isEach message CSP event belongs to exactly the sender's and receiver's alphabets and synchronizes those two processes. A status signal belongs only to its own node. Using the common set of all message events as an all-node synchronization alphabet would be incorrect: unrelated nodes would then have to participate in each point-to-point transfer. The initial definitions in parts (a) and (b) make every node active. Keep the message CSP events visible here; later checks can apply CSP hiding as needed.
Past exam of the computer science course of the University of Oxford 2015 Concurrency 3 b Solution by Codex 0 2026-10-31
Codex 0 2026-10-31The coordinator has the following states:ThusThe coordinator starts a round only while idle and sends true to node . After the first returning message it sends exactly the received bit on the second round, without modifying it. The second return is required before its own shutdown; if the attempt failed it remains idle and may try again or become active. It offers no status-change event between starting and finishing the protocol. The two round states are essential: the first means that the first survey succeeded, whereas the next one acknowledges the circulating decision.
As in part (a), the choices between observable events are expressed using CSP external choice. Execution is nondeterministic, but there is no hidden irrevocable decision to become active while refusing a message. This keeps the readiness required by the question.
Past exam of the computer science course of the University of Oxford 2015 Concurrency 3 a Solution by Codex 0 2026-10-31
Codex 0 2026-10-31Use the intended nontrivial ring network, with , and let . A CSP event is one synchronized transfer from the predecessor to receiver , rather than a separate enqueue and dequeue. Let be the Boolean saying whether node is active. For , defineInitially the node is active:The CSP external choice in always offers both possible incoming message values as well as the permitted status change. Thus a decision to change status cannot internally withdraw readiness to receive a message. When the first message arrives, an active node forces its forwarded bit to false; an idle node preserves the bit. The status is retained until the second-round message has been forwarded. Neither the forwarding prefix nor offers status-change events, enforcing the protocol's freeze. On a false second-round message the node resumes its previous status; on a true one it forwards the bit before announcing shutdown.
Past exam of the computer science course of the University of Oxford 2015 Concurrency 2 f Solution by Codex 0 2026-10-31
Codex 0 2026-10-31Use fresh event tags to tell apart an action by and an interrupting action by . Put and introduce a disjoint copy . Let fix and map each to , and put . Define a process that always accepts an event from byand an ordinary CSP interrupt handler byFinally let fix every original event and send back to . A simulation containing no occurrence of the new operator isHere is the ordinary CSP interrupt, and the CSP event renaming 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, 's events in synchronize with on the same events. Its events outside are unprimed and do not synchronize with . Meanwhile 's events outside are primed; they synchronize with and thereby interrupt and discard . After the first such event, the left operand is , so it imposes no further restriction on ; final CSP event renaming then yields exactly the remaining behaviour of .
For a formal strong bisimulation, relate a pre-interrupt state toand an already-interrupted state toThe three visible cases match the rules in part (d), including both transitions when both operands offer the same event outside . A CSP internal action of never activates , while a CSP internal action of 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.
Past exam of the computer science course of the University of Oxford 2015 Concurrency 2 e Solution by Codex 0 2026-10-31
Codex 0 2026-10-31Suppose the operands are initially stable and written in CSP external choice normal form,The CSP step law isAn empty indexed CSP external choice denotes . A label appearing in both of the first two lines must retain both continuations: after that common label the result is the CSP internal choice between the continuations. A label in appears only in the third line and only if both operands offer it. These are exactly the three visible-transition rules from part (d); the two CSP internal action rules handle operands that are not initially stable.
Past exam of the computer science course of the University of Oxford 2015 Concurrency 2 d Solution by Codex 0 2026-10-31
Codex 0 2026-10-31Write . The following five CSP operational semantics rules suffice, with always visible:Thus a CSP internal action of either operand preserves the wrapper. A visible action outside 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 requires both operands and advances both without discarding either. If both can perform the same event outside , 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.
Past exam of the computer science course of the University of Oxford 2015 Concurrency 2 c Solution by Codex 0 2026-10-31
Codex 0 2026-10-31If is injective, the equation is true:For a CSP event , the original CSP parallel composition permits exactly when both operands can perform . After CSP event renaming, the corresponding rule requires the same image in both operands. Injectivity ensures that matching images came from the same event, and that an event outside cannot acquire the image of one inside . Independent transitions remain independent, and CSP internal actions are unchanged. Matching these transition rules gives a strong bisimulation, hence equality in all three standard CSP semantic models.
For a non-injective , the equation need not hold. LetOn the left, both events require synchronization but the other operand offers the wrong event, so . On the right, both renamed operands offer , which can synchronize:The failure is already visible in the CSP traces model. A particular non-injective CSP event renaming may still preserve a particular composition; it is the unrestricted equivalence that fails.
There are unlisted articles, also show them or only show them.