cookbook:nondeterminism

This shows you the differences between two versions of the page.

cookbook:nondeterminism [Monday, 04 December 2006 : 11:18:48] 127.0.0.1 external edit |
cookbook:nondeterminism [Thursday, 12 February 2009 : 09:49:30] (current) hvrooy |
||
---|---|---|---|

Line 1: | Line 1: | ||

+ | ====== 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. | ||

+ | <code chi> | ||

+ | proc T(chan a?,b?,c!: lot) = | ||

+ | |[ var x: lot | ||

+ | :: *( ( a?x | b?x ) | ||

+ | ; delay ... | ||

+ | ; c!x | ||

+ | ) | ||

+ | ) | ||

+ | ]| | ||

+ | </code> | ||

+ | 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. | ||

+ | |||

+ | {{ :cookbook:nondeterminism.png |An example}} | ||

+ | |||

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

+ | <code chi> | ||

+ | type lot = (nat, real) | ||

+ | </code> | ||

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

+ | |||

+ | The system is described by the following specification: | ||

+ | <code chi> | ||

+ | proc S() = | ||

+ | |[ chan a,b,c: lot | ||

+ | :: M(a,true) || M(b,false)|| T(a,b,c) || E(c) | ||

+ | ]| | ||

+ | </code> | ||

+ | |||

+ | One process generates odd numbers 1,3, ..., while the other process generates even numbers 2,4, .... | ||

+ | Machine ''M'' is specified by: | ||

+ | <code chi> | ||

+ | 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 ) | ||

+ | ]| | ||

+ | </code> | ||

+ | with function ''initId'': | ||

+ | <code chi> | ||

+ | func initId(odd: bool) -> nat = | ||

+ | |[ ( not even -> ret 1 | even -> ret 2 ) ]| | ||

+ | </code> | ||

+ | |||

+ | Transformer process ''T'' is specified by: | ||

+ | <code chi> | ||

+ | 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 | ||

+ | ) | ||

+ | ) | ||

+ | ]| | ||

+ | </code> | ||

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

+ | <code chi> | ||

+ | 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" | ||

+ | ]| | ||

+ | </code> | ||

+ | 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''. | ||

+ | |||

+ | {{ :cookbook:nondeterminismdisp0.png |An example with dispatcher}} | ||

+ | |||

+ | |||

+ | We modify process ''M'': | ||

+ | <code chi> | ||

+ | 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 ) | ||

+ | ]| | ||

+ | </code> | ||

+ | 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: | ||

+ | <code chi> | ||

+ | 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 | ||

+ | ) | ||

+ | ) | ||

+ | ]| | ||

+ | </code> | ||

+ | |||

+ | Dispatcher ''D'' determines which machine may continue by sending a trigger ''q'' back. | ||

+ | The dispatcher is specified by: | ||

+ | <code chi> | ||

+ | 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 | ||

+ | ) | ||

+ | ]| | ||

+ | </code> | ||

+ | |||

+ | We obtain the following process ''S'': | ||

+ | <code chi> | ||

+ | 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) | ||

+ | ]| | ||

+ | </code> | ||

+ | |||

+ | |||

+ | ===== 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. | ||

+ | |||

+ | {{ :cookbook:nondeterminismdisp2.png |An example with dispatcher and bundles}} | ||

+ | |||

+ | We present process ''T'': | ||

+ | <code chi> | ||

+ | 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 | ||

+ | ) | ||

+ | ) | ||

+ | ]| | ||

+ | </code> | ||

+ | |||

+ | We present dispatcher ''D'': | ||

+ | <code chi> | ||

+ | 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 | ||

+ | ) | ||

+ | ]| | ||

+ | </code> | ||

+ | |||

+ | And we present process ''S'': | ||

+ | <code chi> | ||

+ | 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) | ||

+ | ]| | ||

+ | </code> | ||

+ | 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

Except where otherwise noted, content on this wiki is licensed under the following license: CC Attribution-Noncommercial-Share Alike 4.0 International