User Tools

Site Tools


cookbook:nondeterminism

Non-determinism

The word non-determinism means that something cannot be determined. In process algebra this means that the sequence of some event cannot be decided if both events take place at the same time instant. Non-determinism is different from randomness. Randomness implies that it is equal likely that events take place. We assume that in an alternative statement with two alternatives both alternatives can be selected. The following specification fragment makes this clear.

proc T(chan a?,b?,c!: lot) =
|[ var x: lot
:: *( ( a?x | b?x )
      ; delay ...
      ; c!x
      )
    )
]|

So, if a lot can be received from a or from b it is possible that channel a is selected. It also is possible that channel b is selected. In the next cycle if a lot can be received via channel a or channel b it is again possible that channel a is selected. Non-determinism means that for example in an alternative statement always the first alternative will be selected and never the second one. Or always the second alternative and never the first alternative. Randomness means that in 50 percent of the choices the first alternative is selected and 50 percent the second alternative. In other words non-determinism implies that the systems engineer has no control over the sequence of events.

An example

The following example illustrates the effect of non-determinism.

An example

We are interested in the flow time of lots in a system. Lots are defined by the following definition:

type lot = (nat, real)

A lot contains a sequence number and the time of generation.

The system is described by the following specification:

proc S() =
|[ chan a,b,c: lot
:: M(a,true) || M(b,false)|| T(a,b,c) || E(c)
]|

One process generates odd numbers 1,3, …, while the other process generates even numbers 2,4, …. Machine M is specified by:

proc M(chan a!: lot, val odd: bool) =
|[ id: nat = initId(odd), u: -> real = exponential(2.0), t: real
:: *( a!(id,time); t:= sample u; delay t; id:= id + 2 )
]|

with function initId:

func initId(odd: bool) -> nat =
|[ ( not even -> ret 1 | even -> ret 2 ) ]|

Transformer process T is specified by:

proc T(chan a?,b?,c!: lot) =
|[ var u: -> real = exponential(0.8), t: real
:: *( ( a?x | b?x )
      ; t:= sample u; delay t
      ; c!x
      )
    )
]|

The flow time of every lot, the mean flow time and the variance of the flow time are calculated in exit process E:

proc E(chan a?: lot) =
|[ i: nat = 0, x: lot, phi: real
 , s1: real = 0.0, s2,t: real
:: i < 100000
   *>( a?x
       ; phi:= time - x.1
       ; ( i <= 1 -> s2:= 0.0
         | i >  1 -> s2:= (i - 2) / (i - 1) * s2 + (phi - s1) ^ 2 / i        
         )
       ; s1:= (i - 1 / i) * s1 + phi / i
     )
  ; !!time, "\tE\t"
          , "\tMean flow time=\t", s1
          , "\tVariance =\t", s2
          , "\tTroughput=\t", i / time, "\n"
]|

In case the engineer likes to have some form of fairness in his specification, he has to specify this behavior.

An example with a dispatcher

In this example we demand that process T starts processing on the lot which waits the longest time for processing in a process M.

An example with dispatcher

We modify process M:

proc M(chan a!: lot, val odd: bool, p!,q?: void) =
|[ var id: nat = initId(odd), u: -> real = exponential(1.0), t: real
:: *( p!; q?; a!(id,time); t:= sample u; delay t; id:= id + 2 )
]|

Machine M sends a trigger to a dispatcher to denote that the process wants to send a lot to process T.

We modify process T in the following way. Before process T asks for a lot, the process sends a trigger to the dispatcher:

proc T(chan a?,b?,c!: lot, r: !void) =
|[ var u: -> real = exponential(0.8), t: real
:: *( r!
      ; ( a?x | b?x )
      ; t:= sample u; delay t
      ; c!x
      )
    )
]|

Dispatcher D determines which machine may continue by sending a trigger q back. The dispatcher is specified by:

proc D(chan p0?,p1?,r?,q0!,q1!: void) =
|[ var js: [nat], send: bool =false, j: nat
:: *( p0?; js:= js ++ [0]
    | p1?; js:= js ++ [1]
    | r?; send:= true
    | send and len(js) > 0 -> j:= hd(js)
      ; ( j = 0 -> q0! | j = 1 -> q1! )
      ; js:= tl(js); send:= false
    )
]|

We obtain the following process S:

proc S(chan c!: lot) =
|[ chan a,b,c: lot, p0,p1,q0,q1,r: void
:: M(a,true,p0,q0) || M(b,false,p1,q1)|| T(a,b,c,r) || E(c)
|| D(p0,p1,r,q0,q1)
]|

An example with a dispatcher and bundles

By using the full power of the channel concept (one channel can have two senders and one receiver) and by introducing bundles we can make this specification more elegant.

An example with dispatcher and bundles

We present process T:

proc T(chan a?,b!: lot, r: !void) =
|[ var u: -> real = exponential(0.8), t: real
:: *( r!
      ; a?x
      ; t:= sample u; delay t
      ; b!x
      )
    )
]|

We present dispatcher D:

proc D(chan p?: nat, r?: void, q!: 2 # void) =
|[ var js: [nat], send: bool =false, j: nat
:: *( p?j; js:= js ++ [j]
    | r?; send:= true
    | send and len(js) > 0 -> q.hd(js)!
      ; js:= tl(js); send:= false
    )
]|

And we present process S:

proc S() =
|[ chan a,b: lot, p: nat, q: 2 # void ,r: void
:: M(a,true,p,q.0) || M(a,false,p,q.1)|| T(a,b,r) || E(c)
|| D(p,r,q)
]|

Channel a is connected to the two machines M and process T.

cookbook/nondeterminism.txt · Last modified: Thursday, 12 February 2009 : 09:49:30 by hvrooy