Introduction to processes

Basics

A function is a computation object which calculates a result given its
arguments. A procedure is a computation object which establishes a
postcondition provided that its precondition is satisfied. Functions and
procedures do not interact with their environment during their lifetime. They
just have an entry point and an exit point. What happens between is not
observable (at least if we abstract the duration).

A process can interact with its environment. A complete program is usually a
process, because in order to have some value it has to interact with its
environment, which can be a user (equipped with mouse, keyboard and monitor) or
a filesystem or other processes. This is the reason why in most operating
systems running programs are called processes.

The interactions between a process and its environment are called events. The
only thing an event can do is “happen”.

In this article we use Tony Hoare’s theory of “Communicating sequential
processes” presented in a book with the same title in 1985. We just adapt the
syntax to fit our programming language.

In the following description we use sets and relations extensively.

Remember: If T denotes a type then T? denotes the type of a predicate over
objects of type T. All objects which satisfy the predicate form a set. Since
the connection between predicates and sets of objects which satisfy the
predicate is so strong, we identify both concepts. I.e. the type T? denotes a
predicate over the type T and a set of objects of type T at the same time.

This notation is extended to relations. The type [T,U] denotes pairs of
objects of type T and type U. Consequently [T,U]? is a predicate with two free
variables or a set of pairs. I.e. we use the type [T,U]? to denote a relation
between objects of type T and objects of type U.

In order to understand the notation in this article fully it might be
convenient to read (at least the basic concepts) of the articles

– Functions, ghost functions and higher order functions

– Predicates as sets

– Complete lattices and closure systems

– Binary relations, endorelations and transitive closures

Some simple process examples

Consider a simple vending machine which sells chocolates. This vending machine
has two events:

– coin: The event of a coin being inserted in the slot of the machine

– choc: The event of extraction of a chocolate from the dispenser of the
machine

Events are treated as features in our programming language. Their declaration
is very simple

  feature
      coin
      choc
  end

I.e. events look like argument-less procedures without body. Since the only
thing an event can do is “happen”, there is neither an implementation nor a
postcondition (but events can have arguments and preconditions as we will see
later).

Having these two events we can define the process which represents a simple
vending machine.

  feature
      vm_choc
          ensure
              Process = (coin -> choc -> vm_choc)
          end
  end

I.e. a process looks syntactically like a procedure which gives in its
postcondition an expression which states the property of the process. The
variable ‘Process’ represents the process and is just a placeholder for
‘vm_choc’ i.e. for the process to be defined. Therefore the definition states
the equality

      vm_choc = (coin -> choc -> vm_choc)

which is a recursive equation. We can expand the recursive definition as often
as we like to get the equations

      vm_choc = (coin -> choc -> (coin -> choc -> vm_choc))

      vm_choc = (coin -> choc -> (coin -> choc -> (coin -> choc -> vm_choc)))

      ...

The above definition says that the process ‘vm_choc’ can engage first in the
event ‘coin’ then in the event ‘choc’ and then behaves like
‘vm_choc’. I.e. the process ‘vm_choc’ can engage in the potentially infinite
sequence of events

      coin, choc, coin, choc, ...

The prefix operator ‘->’ is a right associative binary operator which has
on its left side an event and on its right side a process. I.e. we have to
‘parse’ the above definition it the following way.

      vm_choc
          ensure
              Process = (coin -> (choc -> vm_choc))
          end

A process like ‘vm_choc’ alone does nothing because events are
interactions. Therefore the process has to be placed into an environment where
it can interact. An environment can be a customer which can engage in the same
events, i.e. a customer having a coin which he inserts into the slot of the
machine and wants to extract a chocolate from its dispenser.

A process can engage in events or refuse events. Initially the vending machine
‘vm_choc’ can engage in the event ‘choc’ and refuses to dispense a
chocolate. After having received the coin it can engage in the event ‘choc’
and refuses to accept a new coin until the chocolate has been dispensed. The
set of all events which a process can accept or refuse is called its
alphabet. The alphabet of a process is a constant through its lifetime. Events
outside its alphabet are not known to a process, i.e. it can neither engage in
nor refuse them.

Since our programming language is strongly typed all objects must have a
type. All event objects like ‘coin’ and ‘choc’ are of type EVENT, all process
objects like ‘vm_choc’ are of type PROCESS.

The vending machine vm_choc has just a linear sequence of events. It does not
offer its customers any choice. The customer just can insert a coin and
extract a chocolate. In the programming language it is easy to express
choice. A vending machine which offers its customers a chocolate or a toffee
after inserting a coin can be defined as

      vm_choc_toffee
          ensure
              Process = (coin -> ( choc -> vm_choc_toffee
                                 | toffee -> vm_choc_toffee))
          end

where the operator ‘|’ expresses a choice.

The processes vm_choc and vm_choc_toffee are defined by a recursion equation
of the form ‘p=f(p)’. The definitions

      proc
          ensure
              Process = f(proc)
          end

      proc
          ensure
              Process = x: f(x)         -- a fresh variable `x'
          end

are equivalent. With this notation we can express the definition of our two
vending machines in the following form.

      vm_choc
          ensure
              Process = x: coin -> choc -> x
          end

      vm_choc_toffee
          ensure
              Process = x: coin -> (choc -> x | toffee -> x)
          end

I.e. the expression x:f(x) defines a process if ‘f’ is a function of type
PROCESS->PROCESS (Note: The function ‘f’ has to be guarded, i.e. it has to
start with an event. The expression ‘x:x’ is not a proper process expression).

Traces

One important aspect of a process is the sequence of events in which it can
engage. At any point in time a process has a history of events in which it has
engaged up to this point in time. We use the type LIST[EVENT] to talk about
the sequence of events and call them traces.

  TRACE = LIST[EVENT]

The following are valid traces of vm_choc_toffee

      []
      [coin, toffee, coin]
      [coin]
      [coin, choc, coin choc, coin, toffee, coin]

We can define the set of all traces ts:TRACE? in which a process can engage.
Note that any prefix of a trace is a valid trace. Therefore the set of traces
of a process has to be prefixclosed.

      is_prefixclosed(ts:TRACE?): ghost BOOLEAN
          ensure
              Result = ts.is_closed({u,v: v.is_prefix(u)})
          end

Since the empty trace is a prefix of any trace, the empty trace is contained
in the trace set of any process.

Every traceset defines the set of events which occur in any of its traces

      alphabet(ts:TRACE?): ghost EVENT?
              -- The alphabet of the trace set `ts'.
          ensure
              Result = {e: some(t:TRACE) t in ts and e in t}
          end

With this function we get

     vm_choc.traces.alphabet = {coin, choc}

     vm_choc_toffee.traces.alphabet = {coin, choc, toffee}

where the function ‘traces’ returns the trace set of a process.

The set of all prefixclosed trace sets is a closure system. An arbitrary
traceset does not represent a valid traceset of a process. The closure of a
trace set with respect to the prefix relation is the smallest set which
contains the trace set and is prefixclosed. I.e. the set

      {[coin,choc,coin]}

is not a valid traceset. We can generate a valid trace set by closing the set.

      {[coin,choc,coin]}.closed(is_prefixclosed)
      =
      {[], [coin], [coin,choc], [coin,choc,coin]}

      -- Note: The expression is_prefixclosed is just a shorthand for
      --       {ts:TRACE?: ts.is_prefixclosed}

> For details on closures see the article “Complete lattices and closure
systems”.

Let us try to find a closed expression for the trace set of the process
vm_choc.

First we note: If t is a trace then [coin,choc]+t is a trace as well. The
expression {nil}.closed(t->[coin,choc]+t) therefore generates a set of valid
traces of vm_choc. This traceset is not yet prefixclosed. The full set of
valid traces can be generated by the formula

      vm_choc.traces = {nil}.closed(t->[coin,choc]+t)
                            .closed(is_prefixclosed)

      -- Note: t->[coin,choc]+t is the function which maps any trace t
      --       to the trace [coin,choc]+t

      -- The type checker of our programming language can resolve this
      -- ambiguity between function expressions and process expressions

In a similar manner we can give a closed expression for the traces of the
process ‘vm_choc_toffee’.

      vm_choc_toffee.traces = {nil}
                              .closed({u,v: v=[coin,choc  ]+u or
                                            v=[coin,toffee]+u})
                              .closed(is_prefixclosed)

Note that we have used three possibilities to close a set: (a) close a set
with respect to a closure system, (b) close a set under a function and (c)
close a set under a relation. Let us shortly repeat what these closures
mean. Let c be a set, cs be a set of sets which are a closure system, f be a
function and r a relation. Then we have

     c.closed(cs) = ({x:c<=x}*cs).infimum  -- least set of cs which contains c

     c.closed(f)  = {c + c.image(f) + c.image(f).image(f) + ... }

     c.closed(r)  = {c + c.image(r) + c.image(r).image(r) + ... }

     -- Note: '<=' for sets is the subset relation i.e. {x:c<=x} is the set of
     --       all sets which contain c.

where c.image(f) is the image of the set c under the function f and c.image(r)
is the image of the set c under the relation r.

A specific trace t of a process characterizes in some way the state of a
process. We might be interested in the behaviour of a process after having
engaged in the events of the trace t. Clearly t must be a valid trace of the
process, otherwise this question does not make any sense. The behaviour of a
process after having engaged in t is characterized by a set of traces as well.

We define the function

      / (ts: TRACE?, t:TRACE): ghost TRACE?
              -- The traceset of a process with traceset `ts' after having
              -- engaged in the events of the trace `t'.
          ensure
              Result = ts.image(u -> u.without_prefix(t))
          end

Note that the function ‘image’ for a function f of type A->B is defined as

      image(p:A?, f:A->B): ghost B?
          ensure
              Result = {b:B: some(a:A) a in f.domain and b=f(a)}
          end

The initial events of a traceset are defined by the following function.

      initials(ts:TRACE?): ghost TRACE?
              -- The set of initial events of the traceset `ts'.
          ensure
              Result = {e: some(u:TRACE) e::u in ts}
          end

There might be traces in a traceset which do not have any continuation. These
are called endtraces.

      endtraces(ts:TRACE?): ghost TRACE?
          ensure
              Result = {t: t in ts and ts/t = 0}
          end

Any process after having engaged in the events of one of its endtraces cannot
continue to engage in events. There are two possible reasons for a process to
reach any of its endtraces: (a) The process has done what it is supposed to do
successfully and has therefore terminated. (b) The process has reached some
deadlock situation. Successful termination or deadlock cannot be
distinguished by the traces of a process.

The possibility of having endtraces reveals the fact that the alphabet of a
traceset as defined above cannot represent the alphabet of the
process. Consider a process with the traceset ts and an endtrace t. Then the
alphabet of the traceset ts/t is empty. This is not inline with the
requirement that the alphabet of a process has to be an invariant during its
lifetime.

Refusals and failures

If we have a traceset ts of a process we know a lot about the behaviour of the
process. The traceset defines the sequence of all possible events in which the
process can engage.

But we can look at a process as well by asking what it does not do, i.e. what
it refuses to do. E.g. our vending machine for chocolates refuses to dispense
a chocolate at the beginning. It expects first a coin to be inserted. After a
coin has been inserted the machine refuses the insertion of another
coin. Before the insertion of another coin the chocolate has to be extracted.

We define a refusal as a set of events which are refused by a process at a
certain state.

      REFUSAL = EVENT?

If the environment offers the events of a refusal then the combination of the
process with its environment cannot continue, it is blocked.

If r is a refusal (i.e. a set of events) and the environment offers a subset s
(i.e. s<=r) then s must be a refusal as well. Therefore at any state the
process has some set of refusals which is downclosed (i.e. with each set it
contains the subsets as well).

The state of a process is characterized by the sequence of events in which it
has engaged up to a certain point in time. The combination of a trace t and a
refusal r i.e. the pair [t,r] is called a failure of the process. We call
[t,r] a failure because the combination of the process with its environment
fails after engaging in the events of t if the environment offers the events
in r.

The set of all trace refusal pairs of a process is called its failure
relation (note that this a relation between traces and set of refusals,
i.e. set of sets).

Our intuition tells us that the refusals have to be in some way a complement
of what the traceset of a process is describing. This stems from the
conjecture that a process can either engage in an event or refuse an event and
both actions being mutually exclusive. This is in fact true for deterministic
processes.

Let us try to find an expression of the set of refusals of a process with the
traceset ts after having engaged in the events of the trace t. The process is
going to accept events of the set (ts/t).initials. The refusal sets have to be
subsets of the complement of (ts/t).initials. But complement with respect to
what? In order to answer this question the alphabet of a process enters the
scene.

Let a be the alphabet of a process described by the traceset ts. In order to
be a valid alphabet it has to be a superset of ts.alphabet. After having
engaged in the events of the trace t the set {r: r <= a-(ts/t).initials} is
the set of refusals which is inline with our intuition about deterministic
processes.

We can use this method to define a function which returns the failure relation
of a deterministic process with the traceset ts and the alphabet a.

      failures(ts:TRACE?, a:EVENT?): ghost [TRACE,REFUSAL]?
          ensure
              Result = {t,r: t in ts  and  r <= a - (ts/t).initials}
          end

The function failures calculates a meaningful failure relation of a process
only if the traceset is prefixclosed and the alphabet is a superset of the
alphabet defined by the traceset.

Note that the relation calculated by the function failures has a very specific
property. Any refusal after engaging in the trace t is a subset of
a-(ts/t).initials which is the greatest refusal after trace t. If fr is the
failure relation calculated by the function ‘failures’ then
t.image(fr).supremum is this greatest refusal. Note that this is not the most
general case. The most general case is that t.image(fr).supremum is not
contained in t.image(fr) which characterizes a non-deterministic process (see
next chapter).

The failure relation of a process contains more information than its
traceset. We can define some useful functions based on the failure relation of
a process.

      initials(fr:[TRACE,REFUSAL]?): ghost EVENT?
              -- The set of the initial events in which a process
              -- characterized by the failure relation `fr' can engage.
          ensure
              Result = fr.domain.initials
          end

      refusals(fr:[TRACE,REFUSAL]?): ghost REFUSAL?
              -- The set of all initial refusals of a process
              -- characterized by the failure relation `fr'.
          ensure
              Result = nil.image(fr)
          end

      events(fr:[TRACE,REFUSAL]?): ghost EVENT?
              -- The set of all events which a process characterized by
              -- the failure relation `fr' can initially engage in or refuse.
          ensure
              Result = fr.initials + fr.refusals.supremum
          end

      alphabet(fr:[TRACE,REFUSAL]?): ghost EVENT?
              -- The set of all events which can occur either in a trace or
              -- in a refusal of the failure relation `fr'.
          ensure
              Result = {e: some(t,r) [t,r] in fr and (e in t or e in r)}
          end
      / (fr:[TRACE,REFUSAL]?, t:TRACE): ghost [TRACE,REFUSAL]?
              -- The failure relation of a process characterized by the
              -- failure relation `fr' after having engaged in `t'.
          ensure
              Result = {u,r: t+u in fr.domain and r in (t+u).image(fr)}
          end

As we have seen above an arbitrary relation between traces and refusals is not
a valid failure relation of a process. With the defined functions we can
formulate the constraints of the failure relation precisely.

      is_process(fr:[TRACE,REFUSAL]?): ghost BOOLEAN
          ensure
              Result =
                ( fr.domain.is_prefixclosed
                  and
                  (all(t:TRACE) t.image(fr).is_downclosed)
                  and
                  (all(t:TRACE) t in fr.domain => fr.alphabet = (fr/t).events)
                )
          end

These conditions require that (a) the traceset characterized by the domain of
the relation has to be prefixclosed, (b) each subset of a refusal is a refusal
and (c) the alphabet is an invariant through the lifetime of a process.

It is interesting to note that the set of all failure relations which describe
a valid process is a closure system. I.e. we can use a arbitrary relation fr
between traces and refusals and form a valid one by building the closure
fr.closed(is_process). The relation ‘fr.closed(is_process)’ is the least
relation which contains ‘fr’ and satisfies the requirements to be a valid
process.

Non-deterministic processes

The processes we have seen up to now are all deterministic. The environment
has full control over the behaviour via the events it offers. E.g. interacting
with the vending machine vm_choc_toffee the customer can insert a coin and can
decide whether to extract a chocolate or a toffee.

      vm_choc_toffee
          ensure
              Process = x: coin -> (choc -> x | toffee -> x)
          end

The choice after inserting the coin is done by the environment.

Let us construct a machine like vm_choc which dispenses only toffees.

      vm_toffee
          ensure
              Process = x: coin -> toffee -> x
          end

We can combine vm_choc and vm_toffee with the choice operator.

      vm_choc | vm_toffee

> Note: In Tony Hoare’s book about CSP this operator has been displayed as a
small square. Since squares are difficult to display in ASCII we use the |
operator.

The choice operator | suggests that the environment has a choice like in the
machine vm_choc_toffee after inserting the coin. But there is no real choice
here because both processes vm_choc and vm_toffee require a coin to be
inserted at the beginning. However the expression vm_choc|vm_toffee requires
a choice to be made. The only reasonable solution is to say that the process
described by the expression vm_choc|vm_toffee makes this choice
nondeterministically.

Once the choice has been made the process behaves subsequently either like
vm_choc or vm_toffee. The environment can note the consequence of this choice
after having inserted a coin and extracted one of the two possibilities. From
this point on the process behaves deterministic like a vm_choc or a
vm_toffee.

Note that the environment (i.e. a potential customer) has to be prepared for
both possibilities. If the customer insists to extract a toffee and the
process has made the non-deterministic choice to behave like a vm_choc then the
system of process and environment is deadlocked and cannot continue.

Some possible traces of vm_choc|vm_toffee are

  { [],
    [coin],
    [coin, choc],
    [coin, choc, coin, choc, coin, choc],
    [coin, toffee],
    [coin, toffee, coin, toffee, coin, toffee],
    ...
  }

The traceset of vm_choc|vm_toffee is the union of the tracesets of the
components.

It is interesting to look at the initial events and the refusal set of the
combined machine after having engaged in the first insertion of a coin

      ((vm_choc|vm_tofffee)/[coin]).initials = {choc,toffee}



      ((vm_choc|vm_tofffee)/[coin]).refusals = {
          0,
          {coin},
          {choc},
          {coin,choc},
          {toffee},
          {coin,toffee}
      }

The combination might accept the extraction of a chocolate and it might accept
the extraction of a toffee. The internal choice made by the process is not yet
visible to the environment.

The set of refusals does not have a greatest element. The complement of the
initials with respect to the alphabet which is the one element set {coin} is
no longer the greatest refusal like it would be if the process were
deterministic. We can use this observation to formally define deterministic
and non-deterministic processes.

      is_deterministic(fr:[TRACE,REFUSAL]?): ghost BOOLEAN
          ensure
              Result = all(t,r)
                           require
                               [t,r] in fr
                           ensure
                               r <= fr.alphabet - (fr/t).initials
                           end
          end

In this basic discussion about non-deterministic processes we have glossed over
an important detail. The expression vm_choc|vm_toffee is illegal because the |
operator requires identical alphabets of both operands. The process vm_choc
has the alphabet {coin,choc} and the process vm_toffee has the alphabet
{coin,toffee}. Therefore the above is valid only if we augment the alphabet of
vm_choc by the set {toffee} and the alphabet of vm_toffee by {choc}. The
augmentation of alphabets of a process is treated formally later. But the
basic semantics is that augmentation does not change the traces. It adds some
refusals to convert the alphabet into the augmented alphabet.

Terminations

The failure relation does not describe a process completely. The missing
information is obvious if we look at endtraces of a process. By definition an
endtrace has no continuation. A process in this situation can be either
deadlocked or might have terminated successfully.

Termination can be deterministic or nondeterminisitic, i.e. a process might
make some internal choices to terminate or not terminate after engaging in
some trace. In order to treat non-determinism properly for terminations as well
we have to partition the set of traces into

      terminations: TRACE?

      nonterminations: TRACE?

with the obvious constraint

      fr.domain = terminations + nonterminations

For a deterministic process we require that both sets are disjoint.

The combination of the failure relation the termination and nontermination
traces is sufficient to describe the behaviour of a process.

Advertisements

  1. Leave a comment

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: