4.2 Tuning for FDR

These sections discusses ways in which process descriptions can be tuned to get the best from the current version of FDR. Since some of these features can be detrimental to the overall readability of a script, they should be used with care and only when necessary.

4.2.1 Share components

When FDR builds state-machines from the CSP process descriptions, it does so as an acyclic graph of process operators where the leaves of the graph are simple transition systems. Although FDR can build the operator tree efficiently, construction of the leaves can be expensive. For example, it is much more efficient to build an N-place buffer as

BUFF(N,in,out) =
  let
    COPY = in?x->out!x->COPY
  within [out<->in] x : <1..N> @ COPY

than

BUFF(N,in,out) =
  let
    B(s) =
      not null(s) & out!head(s) -> B(tail(s))
    []
      #s < N & in?x -> B(s^<x>)
  within B(<>)

and it is more efficient (assuming P and Q are both used) to write

P = BUFF(10, in, out)
Q = P [[ in<-left, out<-right ]]

than to write

P = BUFF(10, in, out)
Q = BUFF(10, left, right)

since the renaming can be built directly and the leaf process is then shared between P and Q.

4.2.2 Factor state

The formulation of BUFF above (see section Share components) is not only more efficient because the COPY components are shared (and thus need only be calculated once), but also because the state of the buffer has been distributed across separate processes. In general, if we have a process P with two state variables x and y ranging over X and Y, so that

P(x, y) = f(P, x, y)

for some function f, and we can split the state so that

P(x, y) = Q(x) || R(y)

for some processes Q and R in parallel, then the time taken to build the state-machine corresponding to P can be reduced from #X*#Y in the first case to #X+#Y in the second. (Of course, the exploration of the product space still has to be performed, but it can be done more efficiently as the check proceeds.) Such a change may not improve performance if the state is not independent, for example if we write

BUFF(N,in,out) =
  let
    B(n, s) =
      n>0 & out!head(s) -> B(n-1,tail(s))
    []
      n<N & in?x -> B(n+1,s^<x>)
  within B(0, <>)

then separating n and s will not be productive.

4.2.3 Use local definitions

When constructing processes, the use of local definitions allows us to separate out those arguments which are passed in for configuration purposes (sizes, channels and so on) from those which represent process state and may need to modified on recursive calls. For example, in FDR1 we might have written

N = 6

BUFF(s) =
  not null(s) & out!head(s)->BUFF(tail(s))
[]
  #s<N & in?x->BUFF(s^<x>)

which ‘wires-in’ to the definition the name (and so type) of the channels along with the buffer size. It also requires users to know that the buffer must be given an initial argument of the empty sequence. With local definitons we can write

BUFF(N,in,out) = -- configuration arguments
  let
    B(s) = -- process state
      not null(s) & out!head(s) -> B(tail(s))
    []
      #s < N & in?x -> B(s^<x>)
  within B(<>) -- initialisation of process state

which generalises the definition so it can be used with different channels and sizes and also conceals the need for an initial argument.

This document was generated by Phil Armstrong on May 17, 2012 using texi2html 1.82.