Past exam of the computer science course of the University of Oxford / 2015 / Concurrency / 2 / a / Solution

For a finite CSP trace $s$, let $L(s)$ be its sequence of values on $left$ and $O(s)$ its sequence of values on $right$, with channel names removed. Restrict the external alphabet to these two channels. The behavioural CSP trace specification for an unbounded FIFO buffer iswhere $⪯$ means prefix of a list, not merely subsequence. Outputs must therefore occur in input order, cannot duplicate or invent values, and cannot precede their inputs. Applying the condition to every CSP trace also checks every execution prefix.

For a legal $s$, write $L(s)=O(s)⌢q(s)$, so $q(s)$ is the pending FIFO queue content. Define the events that must remain available byIn addition to the CSP trace condition, require the behavioural CSP stable failure conditionThus an unbounded FIFO buffer cannot stably refuse any new input, and a nonempty FIFO buffer cannot stably refuse its oldest pending output. An empty FIFO buffer can refuse every output. Readiness of an input and readiness of an output are required together; the environment may choose either. These conditions do not require an output while the environment refuses to accept it. In a CSP failures-divergences model specification, also exclude CSP divergence; the stable-readiness condition alone does not rule out an implementation that loops internally forever without reaching a CSP stable state.