Communicating Sequential Processes

A formal language for describing concurrent systems.

Processes

A process represents the behaviour pattern of an object. It consists of an alphabet, which is the set of the possible atomic events an object can engage on. There is no distinction between events originated by the user of the object or by the object itself.

The alphabet of process P is denoted as \alpha P and the set of traces of P is denoted as traces(P) . Two processes are considered independent if their alphabets are disjoint.

A process can be defined in terms of itself, like CLOCK = (tick \rightarrow CLOCK) .

A process can be defined as a function f : \Sigma \rightarrow (\Sigma, T) that takes an event and results in a process, and where its domain must be a subset of the alphabet. The function may return STOP_{\Sigma} to represent termination.

Two processes are equal if their event choices are the same and each resulting process is the same. The processes (x : A \rightarrow f(x)) and (y : B \rightarrow g(y)) are the same if A = B \land \forall \thinspace z \in A \bullet f(z) = g(z) .

If two objects define the same process, then they are considered equal, therefore there exists only one object that defines a process. A more formal definition for a process such as CLOCK = (tick \rightarrow CLOCK) is CLOCK = \mu X : \{ tick \} \bullet (tick \rightarrow X) . Given a function f that maps an event to a process, the unique-type definition can be generalized as \mu X : \Sigma \bullet (y : \Sigma \rightarrow f(y, X)) , where the second argument to f is the process itself, in order to support recursion.

Operators

The prefix operator ( \rightarrow ) takes an event and a process and describes the process that engages in a given event and then behaves like the subsequent process, for example (x \rightarrow P) . Notice that (x \rightarrow y \rightarrow z \rightarrow P) is equivalent to (x \rightarrow (y \rightarrow (z \rightarrow P))) .

The choice operator ( \mid ) takes two prefix applications (its not an operation on processes) and describes a process that has a choice over what event to engage on, for example (x \rightarrow P \mid y \rightarrow Q) . Notice that (x \rightarrow P \mid y \rightarrow Q) = (y \rightarrow Q \mid x \rightarrow P) . The events on the involved prefixes must be different, as (x \rightarrow P \mid x \rightarrow Q) is considered invalid.

The alphabet of the resulting process consists of the prefix events and the alphabets of the involved processes: \alpha(x \rightarrow P \mid y \rightarrow Q) = \{ x, y \} \cup \alpha P \cup \alpha Q .

There exists a shorthand to define choices over a set. Given A = \{ foo, bar \} , the shorthand (e: A \rightarrow P) evaluates to (foo \rightarrow P \mid bar \rightarrow P) . If the set of choices is the empty set, the resulting process is the broken process. Given (x : B \rightarrow P(x)) , if B \subseteq A where A = \alpha P(x) for all x , then \alpha (x : B \rightarrow P(x)) = A .

A process P is a subset of process Q if they share the same alphabets and the traces of P can all be consumed by Q . This is denoted as: P \sqsubseteq Q = (\alpha P = \alpha Q) \land (traces(P) \subseteq traces(Q)) . Of course, P \sqsubseteq P . If two processes are subsets of each other, then they must be equal: P \sqsubseteq Q \land Q \sqsubseteq P \implies P = Q . The subset operation is transitive: P \sqsubseteq Q \land Q \sqsubseteq R \implies P \sqsubseteq R . Finally, a process is always the superset of its broken process: STOP_{\alpha P} \sqsubseteq P .

Given a variable b that is either true or false , the process (P \thinspace{<}\llap{\mid}\thinspace b \thinspace\rlap{\mid}{>}\thinspace Q) behaves like P if b = true , and like Q otherwise. This operator obeys the following laws:

Given a boolean expression b and a process P , the process (b * P) is the machine that restarts P while b is true : (b * P) = \mu X \bullet ((P \thinspace ; \thinspace X) \thinspace{<}\llap{\mid}\thinspace b \thinspace\rlap{\mid}{>}\thinspace SKIP_{\alpha P}) .

Process Mapping (or Change of Symbol)

Given a function f that maps the alphabet (takes the alphabet of a process and returns a new set of the same size), a process P , and an event x \in \alpha P , then f(P) represents the process that engages in f(x) (the actual function application) whenever P engages in x . The function must be injective, so that f^{-1} makes functional sense.

It follows that \alpha f(P) = f(\alpha P) . The traces of the mapped process are traces(f(P)) = \{ \thinspace f^{*}(t) \mid t \in traces(P) \thinspace \} . Notice the mapping function always preserves the broken process, as in that case it would map over an empty list of choices: \forall P \bullet f(STOP_{\alpha P}) = STOP_{\alpha f(P)} .

Notice that process mapping distributes over the composition operator: f(P \parallel Q) = f(P) \parallel f(Q) . When it comes to consuming a trace t , then f(P) \thinspace / \thinspace f^{*}(t) = f(P \thinspace / \thinspace t) .

Given the choices shorthand definition of a process non-recursive process: f(x : A \rightarrow P(x)) = (y : f(A) \rightarrow f(P(f^{-1}(y)))) .

For example, consider CLOCK = (tick \rightarrow CLOCK) and f(tick) = tock . In that case, f(CLOCK) = (tock \rightarrow f(CLOCK)) .

Given a sequential process P , then f(\checkmark) = \checkmark must hold.

Given an arbitrary interleaving (P \sqcap Q) , f(P \sqcap Q) = (f(P) \sqcap f(Q)) .

A process defined by mapping diverges when its original process diverges. Given f and P , divergences(f(P)) = \{ f^{*}(s) \mid s \in divergences(P) \} .

The failures of a mapped process are defined as failures(f(P)) = \{ (f^{*}(s), f(X)) \mid (s, X) \in failures(P) \} . The refusals of a mapped process are defined as refusals(f(P)) = \{ f(X) \mid X \in refusals(P) \} .

Concealing a mapped process is defined as f(P \setminus C) = (f(P) \setminus f(C)) .

Process Labelling

Labelling is a mapping technique to add prefix to all the events of a process. Its useful when constructing groups of processes, and where we need to make sure that they are independent (that their alphabets are disjoint). Process P labelled with foo is denoted as foo : P . The prefix is added before every event, separated by a period.

For any prefix p , there exists a function label_{p}(e) = p.e . The labelled process p : Q is equivalent to label_{p}(Q) . Notice labelling changes the alphabet: \alpha Q \neq \alpha (p : Q) .

For example, consider CLOCK = (tick \rightarrow CLOCK) . In that case, foo : CLOCK = (foo.tick \rightarrow CLOCK) .

Concealment

Concealment creates a new process that behaves like the new process but with certain events being hidden. This operation reduces the alphabet of a process and may introduce non-determinism. Concealing an infinite sequence of consecutive events leads to divergence.

This operation is defined as ((x \rightarrow P) \setminus C) = (x \rightarrow (P \setminus C)) if x \notin C , and as ((x \rightarrow P) \setminus C) = (P \setminus C) otherwise. Given the choice shorthand definition (x : B \rightarrow P(x)) , concealing such process with C expands to (x : B \rightarrow (P(x) \setminus C)) if B \cap C = \emptyset , otherwise it expands to (Q \sqcap (Q \thinspace \square \thinspace (x : (B - C) \rightarrow P(x)))) where Q = \sqcap_{x \in B \cap C} (P(x) \setminus C) , which introduces non-determinism.

The alphabet of a concealed process is \alpha (P \setminus C) = \alpha P - C . The traces of a concealed process are defined as traces(P \setminus C) = \{ t \restriction (\alpha P - C) \mid t \in traces(P) \} . The following laws apply: (P \setminus \emptyset) = P and ((P \setminus B) \setminus C) = (P \setminus (B \cup C)) .

Given a concealed process, its divergences consist its original divergences plus the new ones potentially created by the concealment operation:

\begin{align} divergences(P \setminus C) &= \{ (s \restriction (\alpha P - C)) \frown t \thinspace \mid \\ &t \in (\alpha P - C)^{*} \land (s \in divergences(P) \\ &\lor (\forall n \bullet \exists u \in C^{*} \bullet \#u > n \land (s \frown u) \in traces(P))) \} \end{align}

The alphabet of a concealed process is defined as \alpha (P \setminus C) = \alpha P - C .

The failures of a concealed process are defined as:

\begin{align} failures(P \setminus C) = \{ &(s \restriction (\alpha P - C), X) \mid (s, X \cup C) \in failures(P) \} \\ &\cup \{ (s, X) \mid s \in divergences(P \setminus C) \} \end{align}

Subordination

Given (P \parallel Q) , P is a slave or subordinate process of Q if \alpha P \subseteq \alpha Q , as each action of P can occur if Q permits it, while Q can freely engage on events of its own (where \alpha Q - \alpha P ). If we want to conceal communication between master and subordinate, then we can use the notation (P \thinspace // \thinspace Q) = (P \parallel Q) \setminus \alpha P . Its alphabet is \alpha (P \thinspace // \thinspace Q) = (\alpha Q - \alpha P) .

The subordinated process can be given a name in which case the master will communicate with it using a compound channel name, while the subordinated process will communicate with its master through a normal channel pair name. The benefit is that all communication between the master and the subordinate can’t be detected from outside as the new subordinate name acts as a local variable for the master.

For example, (m : P \thinspace // \thinspace Q(v)) = (m : (c!v \rightarrow P) \thinspace // \thinspace (m.c?x \rightarrow Q(x))) . Also consider (n : (m : (P \thinspace // \thinspace Q) \thinspace // \thinspace R)) . In this case, there is no way R can communicate with P as it doesn’t know about its existance or about its name, m .

Communication from the master to the slave looks like this: (m : (c?x \rightarrow P(x))) \thinspace // \thinspace (m.c!v \rightarrow Q) = (m : P(v)) \thinspace // \thinspace Q . Conversely, communication from the slave to the master: (m : (d!v \rightarrow P)) \thinspace // \thinspace (m.d?x \rightarrow Q(x)) = (m : P) \thinspace // \thinspace Q(v) .

Communication

Communication between processes is done using events that sets values on channels. This is described by the pair c.v where channel(c.v) = c and message(c.v) = v or the triplet m.c.v which includes the process as a prefix (a compound channel name). Notice that m.\checkmark = \checkmark for any m . A channel used by P only to send events is an output channel of P . A channel used by P only to receive events is an input channel of P .

Communication is unidirectional and only between two processes. Communication between two processes can only happen if both processes engage in the communication: one listens on a channel while the other one sends a message through that channel.

The set of all values that process P can communicate on a channel c is the alphabet of the channel: \alpha c(P) = \{ message(c.v) \mid c.v \in \alpha P \} . Given a compound channel name, \alpha \thinspace m.c(m : P) = \alpha \thinspace c(P) . Communication event pairs must be part of the alphabet of a process. For two processes to communicate over a channel c , they need to share the same alphabet on such channel: \alpha c(P) = \alpha c(Q) . Given P and Q communicate over channel c , all the possible communication events are inside \alpha P \cap \alpha Q .

Given proces P , the event c!v sends value v over channel c . For this to be valid, v \in \alpha c(P) . This event is defined as (c!v \rightarrow P) = (c.v \rightarrow P) . The communication message can be a more complex expression: c!(x + y) . The event to wait for a value on a channel is c?x , where x takes the value of the received message. This is defined as a choice over all the valid communication events of that channel: (c?x \rightarrow P(x)) = (e : \{ c \mid channel(e) = c \}) \rightarrow P(message(e)) . A process can wait in more than one channel using the choice operator: (c?x \rightarrow P(x) \mid d?y \rightarrow Q(y)) .

Variables

(x := e) is the process that sets x to e . Its defined as (x := e) = (x := e \thinspace ; \thinspace SKIP) . It follows that (x := x) = SKIP and that (x := e \thinspace ; \thinspace x := f(x)) = (x := f(e)) . The assignment operator can be used with multiple variables: (x, y, z := e, f, g) but keep in mind that (x := f \thinspace ; \thinspace y := g) \neq (x, y := f, g) as in the first case g may depend on the new value of x . With regards to the conditional operator: (x := e \thinspace ; \thinspace (P \thinspace{<}\llap{\mid}\thinspace b(x) \thinspace\rlap{\mid}{>}\thinspace Q)) = ((x := e \thinspace ; \thinspace P) \thinspace{<}\llap{\mid}\thinspace b(x) \thinspace\rlap{\mid}{>}\thinspace (x := e \thinspace ; \thinspace Q)) .

Given a process P , var(P) is the set of all variables that can be assigned within P , and acc(P) is the set of all the variables that P can access. Of course, all variables that can be set can be accessed: var(P) \subseteq acc(P) . Both sets are subsets of \alpha P .

No variable assigned in a process can be accessed by another concurrent process, so given P and Q , then var(P) \cap acc(Q) = var(Q) \cap acc(P) = \emptyset .

Deterministic Processes

A deterministic process is a tuple (\Sigma, T) consisting of two sets: an alphabet and a set of traces. These laws must be satisfied for a deterministic process to be valid:

A process P is deterministic if it can’t refuse any event in which it can engage: \forall s \in traces(P) \bullet X \in refusals(P \thinspace / \thinspace s) \iff (X \cap \{ x \mid \langle x \rangle \in traces(P \thinspace / \thinspace s) \} = \emptyset) .

Deterministic processes can unambiguously pick between events whenever there is a choice. These processes obey an extra law: given P then, P \parallel P = P .

The process that results by making a process consume a trace is a process with the same alphabet, and with all traces whose prefixes were consumed. Given process (\Sigma, T) and s \in T , then (\Sigma, T) \thinspace / \thinspace s = (\Sigma, \{ t \mid (s \frown t) \in T\}) . Of course, (x \rightarrow P) \thinspace / \thinspace \langle x \rangle = P , and given a function definition, (x : A \rightarrow f(x)) \thinspace / \thinspace \langle y \rangle = f(y) assuming y \in A .

The choice prefix shorthand notation works like this: given an alphabet \Sigma , a set of choices A \subseteq \Sigma , and a function f that maps over the set of traces, then (x : A \rightarrow (\Sigma, f(x))) = (\Sigma, \{ \langle \rangle \} \cup \{ \langle x \rangle \frown s \mid x \in A \land s \in f(x) \}) .

The process mapping operation using a function f is defined as f((\Sigma, T)) = (ran(f), \{ f^{*}(t) \mid t \in T \}) .

Special Processes

Every alphabet has a broken process that never engages in any event. Given alphabet \Sigma , the broken process is STOP_{\Sigma} = (\Sigma, \{ \langle \rangle \}) . Processes with different alphabets are always considered to be different, so given alphabets A and B , if A \neq B , then STOP_{A} \neq STOP_{B} . The traces of the broken object are defined as traces(STOP_{\Sigma}) = \{ \langle \rangle \} .

Every alphabet has a run process that can always engage, at any given point, in any event of its alphabet. Given alphabet \Sigma , the run process is RUN_{\Sigma} = (\Sigma, \Sigma^{*}) , or alternatively (x : \Sigma \rightarrow RUN_{\Sigma}) , and it follows that \alpha RUN_{\Sigma} = \Sigma . Notice that the run process behaves like a restart process: \forall s \in traces(RUN_{\Sigma}) \bullet \overset{\frown}{RUN_{\Sigma}} \thinspace / \thinspace (s \frown \langle \unicode{x21af} \rangle) = \overset{\frown}{RUN_{\Sigma}} .

Given alphabet \Sigma , the SKIP_{\Sigma} process does nothing and terminates successfully: \alpha SKIP_{\Sigma} = \Sigma \cup \{ \checkmark \} . A process can terminate successfully by behaving like SKIP . Notice SKIP_{A} \parallel SKIP_{B} = SKIP_{A \cup B} . Its traces are traces(SKIP_{\Sigma}) = \{ \langle \rangle, \langle \checkmark \rangle \} .

Concealing the broken process results in the broken process: \forall X, Y \bullet STOP_{X} \setminus Y = STOP_{X - Y} .

Properties

A process is cyclic if in all circumstances it can go back to its original state. Given process P , then \forall \thinspace s \in traces(P) \bullet \exists \thinspace t \bullet P \thinspace / \thinspace (s \frown t) = P . The broken process is a simple example.

A process P is free from deadlocks if none of its traces lead to the broken object: \forall \thinspace t \in traces(P) \bullet (P \thinspace / \thinspace t) \neq STOP_{\alpha P} .

Non-deterministic Processes

A non-deterministic process is defined as a triplet \Sigma, F, D that stands for the process alphabet, its failures, as a relation F \subseteq (\Sigma^{*} \times \wp(\Sigma)) where (\langle \rangle, \emptyset) \in F , and a set of divergences where D \subseteq \Sigma^{*} and D \subseteq dom(F) . The following laws must hold: