Systems, Networks & Concurrency 2019
Non-determini4sm Uwe R. Zimmer – The Australian National University
[Ben-Ari06]
[AdaRM2012]
M. Ben-Ari
Ada Reference Manual – Lan- guage and Standard Libraries; ISO/IEC 8652:201x (E)
Principles of Concurrent and Dis- tributed Programming
2006, second edition, Prentice- Hall, ISBN 0-13-711821-X
[Barnes2006]
Barnes, John
Programming in Ada 2005
Addison-Wesley, Pearson education, ISBN- 13 978-0-321-34078-8, Harlow, England, 2006
© 2019 Uwe R. Zimmer, The Australian National University
page 370 of 757 (chapter 4: “Non-determinism” up to page 394)
Non-determinism
References for this chapter
Non-determinism
Non-determinism by design:
A property of a computation which
Definitions
may have more than one result.
Non-determinism by interaction:
A property of the operation environment which may
lead to different sequences of (concurrent) stimuli.
© 2019 Uwe R. Zimmer, The Australian National University page 371 of 757 (chapter 4: “Non-determinism” up to page 394)
if x <= y -> m := x x >= y -> m := y fi
Selection is non- deterministc for x=y
Non-determinism
Non-determinism by design
Dijkstra’s guarded commands (non-deterministic case statements):
The programmer needs to design the alternatives as ‘parallel’ options:
all cases need to be covered and overlapping conditions need to lead to the same result
All true case statements in any language are potentially concurrent and non-deterministic.
© 2019 Uwe R. Zimmer, The Australian National University page 372 of 757 (chapter 4: “Non-determinism” up to page 394)
Dijkstra’s guarded commands (non-deterministic case statements):
if x <= y -> m := x x >= y -> m := y fi
Selection is non- deterministc for x=y
Non-determinism
Non-determinism by design
The programmer needs to design the alternatives as ‘parallel’ options:
all cases need to be covered and overlapping conditions need to lead to the same result
All true case statements in any language are potentially concurrent and non-deterministic. Numerical non-determinism in concurrent statements (Chapel):
writeln (* reduce [i in 1..10] exp (i)); writeln (+ reduce [i in 1..1000000] i ** 2.0);
Results may be non-deterministc depending on numeric type
The programmer needs to understand the numerical implications of out-of-order expressions.
© 2019 Uwe R. Zimmer, The Australian National University
page 373 of 757 (chapter 4: “Non-determinism” up to page 394)
The compiler / runtime environment can directly (i.e. without any analy- sis) translate the source code into a concurrent implementation.
The implementation gains potentially significantly in performance
The programmer does not need to handle any of the details of a concur-
rent implementation (access locks, messages, synchronizations, …)
Non-determinism
Non-determinism by design
Motivation for non-deterministic design
By explicitly leaving the sequence of evaluation or execution undetermined:
A programming language which allows for those formulations is required!
current language support: Ada, X10, Chapel, Fortress, Haskell, OCaml, …
© 2019 Uwe R. Zimmer, The Australian National University page 374 of 757 (chapter 4: “Non-determinism” up to page 394)
ALT
…
Guard1
Process1
Guard2
Process2
Non-determinism
Non-determinism by interaction
Selective waiting in Occam2
• Guards are referring to boolean expressions and/or channel input operations.
• The boolean expressions are local expressions, i.e. if none of them evaluates to true
at the time of the evaluation of the ALT-statement, then the process is stopped. • If all triggered channel input operations evaluate to false, the process is sus-
pended until further activity on one of the named channels.
• Any Occam2 process can be employed in the ALT-statement
• The ALT-statement is non-deterministic (there is also a deterministic version: PRI ALT).
© 2019 Uwe R. Zimmer, The Australian National University page 375 of 757 (chapter 4: “Non-determinism” up to page 394)
•
Synchronization on input-channels only (channels are directed in Occam2): to initiate the sending of data (Take ! Buffer [Base]),
ALT
NumberInBuffer < Size & Append ? Buffer [Top]
SEQ
NumberInBuffer := NumberInBuffer + 1
Top := (Top + 1) REM Size
NumberInBuffer > 0 & Request ? ANY
SEQ
Take ! Buffer [Base]
NumberInBuffer := NumberInBuffer – 1
Base := (Base + 1) REM Size
Non-determinism
Non-determinism by interaction
Selective waiting in Occam2
a request need to be made first which triggers the condition: (Request ? ANY) CSP (Communicating Sequential Processes, Hoare 1978)
also supports non-deterministic selective waiting
© 2019 Uwe R. Zimmer, The Australian National University page 376 of 757 (chapter 4: “Non-determinism” up to page 394)
Non-determinism
Non-determinism by interaction
Select function in POSIX
int pselect(int n, fd_set *readfds, fd_set *writefds, fd_set *exceptfds, const struct timespec *ntimeout, sigset_t *sigmask);
with:
• n being one more than the maximum of any file descriptor in any of the sets.
• after return the sets will have been reduced to the channels which have been triggered.
• the return value is used as success / failure indicator.
The POSIX select function implements parts of general selective waiting:
• pselect returns if one or multiple I/O channels have been triggered or an error occured.
¬ Branching into individual code sections is not provided.
¬ Guards are not provided.
After return it is required that the following code
implements a sequential testing of all channels in the sets.
© 2019 Uwe R. Zimmer, The Australian National University page 377 of 757 (chapter 4: “Non-determinism” up to page 394)
select_statement ::= selective_accept |
conditional_entry_call |
timed_entry_call |
asynchronous_select
Non-determinism
Selective Synchronization
Message-based selective synchronization in Ada
Forms of selective waiting:
selective_accept implements …
… wait for more than a single rendezvous at any one time
… time-out if no rendezvous is forthcoming within a specified time
… withdraw its offer to communicate if no rendezvous is available immediately … terminate if no clients can possibly call its entries
… underlying concept: Dijkstra’s guarded commands
© 2019 Uwe R. Zimmer, The Australian National University page 378 of 757 (chapter 4: “Non-determinism” up to page 394)
end select;
Non-determinism
Selective Synchronization
Message-based selective synchronization in Ada
selective_accept ::= select
[guard] selective_accept_alternative
{ or [guard] selective_accept_alternative } [ else sequence_of_statements ]
guard ::= when
accept_alternative ::= accept_statement [ sequence_of_statements ] delay_alternative ::= delay_statement [ sequence_of_statements ] terminate_alternative ::= terminate;
accept_statement ::= accept entry_direct_name [(entry_index)] parameter_profile [do handled_sequence_of_statements
end [entry_identifier]];
delay_statement ::= delay until delay_expression; | delay delay_expression;
© 2019 Uwe R. Zimmer, The Australian National University page 379 of 757 (chapter 4: “Non-determinism” up to page 394)
select accept …
• If none of the entries have waiting calls the process is suspended
until a call arrives.
or
accept …
• If exactly one of the entries has waiting calls this entry is selected.
or
accept …
• If multiple entries have waiting calls
one of those is selected (non-determin- istically). The selection can be prioritized by means of the real-time-systems annex.
…
end select;
The code following the select-
ed entry (if any) is executed and the select statement completes.
© 2019 Uwe R. Zimmer, The Australian National University
page 380 of 757 (chapter 4: “Non-determinism” up to page 394)
Non-determinism
Selective Synchronization
Basic forms of selective synchronization
(select-accept)
select
when
• If some condition evaluate to ‘true’
the accept statement after those condi- tions are treated like in the previous form.
or
when
• If all conditions evaluate to ‘false’
Program_Error is raised.
Hence it is important that the set of con- ditions covers all possible states.
or
when
…
end select;
© 2019 Uwe R. Zimmer, The Australian National University
page 381 of 757 (chapter 4: “Non-determinism” up to page 394)
Non-determinism
Selective Synchronization
Basic forms of selective synchronization
(select-guarded-accept)
• If all conditions are ‘true’
identical to the previous form.
This form is identical to Dijkstra’s guarded commands.
or
when
the select statement completes.
• Otherwise one of the open entries
or
when
with waiting calls is chosen as above. This form never suspends the task.
…
else
This enables a task to withdraw its of- fer to accept a set of calls if no
tasks are currently waiting.
© 2019 Uwe R. Zimmer, The Australian National University
page 382 of 757 (chapter 4: “Non-determinism” up to page 394)
Non-determinism
Selective Synchronization
Basic forms of selective synchronization
select
when
• If all currently open entries have no waiting calls or all entries are closed
The else alternative is chosen, the as- sociated statements executed and
(select-guarded-accept-else)
select
when
or
when
• If none of the open entries have waiting calls before the deadline specified by the earliest open delay alternative
This earliest delay alternative is chosen and the statements associated with it executed.
or
when
…
or
when
• Otherwise one of the open entries with waiting calls is chosen as above.
or
when
This enables a task to withdraw its of- fer to accept a set of calls if no other task is calling after some time.
…
end select;
© 2019 Uwe R. Zimmer, The Australian National University
page 383 of 757 (chapter 4: “Non-determinism” up to page 394)
Non-determinism
Selective Synchronization
Basic forms of selective synchronization
(select-guarded-accept-delay)
terminate cannot be mixed with else or delay
or
when
chosen, i.e. the task is terminated. This situation occurs if:
or
when
… all tasks which can possibly call on any of the open entries are terminated.
…
or
when
or … all remaining tasks which can possibly call on any of the open entries are waiting on select-terminate statements themselves and none of their open entries can be called either. In this case all those waiting- for-termination tasks are terminated as well.
…
end select;
© 2019 Uwe R. Zimmer, The Australian National University
page 384 of 757 (chapter 4: “Non-determinism” up to page 394)
Non-determinism
Selective Synchronization
Basic forms of selective synchronization
select
when
• If none of the open entries have waiting calls and none of them can ever be called again
The terminate alternative is
(select-guarded-accept-terminate)
select_statement ::= selective_accept |
conditional_entry_call |
timed_entry_call |
asynchronous_select
conditional_entry_call and timed_entry_call implements …
… the possibility to withdraw an outgoing call.
… this might be restricted if calls have already been partly processed.
Non-determinism
Selective Synchronization
Message-based selective synchronization in Ada
Forms of selective waiting:
… underlying concept: Dijkstra’s guarded commands
© 2019 Uwe R. Zimmer, The Australian National University page 385 of 757 (chapter 4: “Non-determinism” up to page 394)
conditional_entry_call ::=
Example:
Even though it is tempting to use this statement in a “busy-waiting” seman- tic, there is usually no need to do so, as better alternatives are available.
else
There is only one entry-call and one else alternative.
select
• If the call is not accepted immediately The else alternative is chosen.
else
entry_call_statement
[sequence_of_statements]
This is e.g. useful to probe the state of a server before commit- ting to a potentially blocking call.
sequence_of_statements end select;
select
Light_Monitor.Wait_for_Light;
Lux := True;
Lux := False; end;
© 2019 Uwe R. Zimmer, The Australian National University
page 386 of 757 (chapter 4: “Non-determinism” up to page 394)
Non-determinism
Selective Synchronization
Conditional entry-calls
timed_entry_call ::=
Example:
This is e.g. useful to withdraw an entry call after some specified time-out.
select
or
entry_call_statement
[sequence_of_statements]
• If the call is not accepted before the dead- line specified by the delay alternative
The delay alternative is chosen.
delay_alternative end select;
select
Controller.Request (Some_Item);
There is only one entry-call and one delay alternative.
—— process data
or
delay 45.0; —— seconds —— try something else
end select;
© 2019 Uwe R. Zimmer, The Australian National University
page 387 of 757 (chapter 4: “Non-determinism” up to page 394)
Non-determinism
Selective Synchronization
Timed entry-calls
select_statement ::= selective_accept |
conditional_entry_call |
timed_entry_call |
asynchronous_select
Non-determinism
Selective Synchronization
Message-based selective synchronization in Ada
Forms of selective waiting:
… underlying concept: Dijkstra’s guarded commands … the possibility to escape a running code block due to an event from outside this task.
asynchronous_select implements …
(outside the scope of this course check: Real-Time Systems)
© 2019 Uwe R. Zimmer, The Australian National University page 388 of 757 (chapter 4: “Non-determinism” up to page 394)
• Operating systems / runtime environments:
Schedulers are often non-deterministic.
System load will have an influence on concurrent execution. Message passing systems react load depended.
• Networks & communication systems:
Traffic will arrive in an unpredictable way (non-deterministic).
Communication systems congestions are generally unpredictable.
• Computinghardware:
Timers drift and clocks have granularities. Processors have out-of-order units.
Non-determinism
Non-determinism
Sources of Non-determinism
As concurrent entities are not in “lockstep” synchronization, they “overtake” each other and arrive at synchronization points in non-deterministic order, due to (just a few):
• … basically: Physical systems (and computer systems connected to the physical world)
are intrinsically non-deterministic.
© 2019 Uwe R. Zimmer, The Australian National University page 389 of 757 (chapter 4: “Non-determinism” up to page 394)
Non-determinism
Non-determinism
Correctness of non-deterministic programs
Partial correctness:
(P (I) /terminates (Program (I, O) & Q (I, O)
Total correctness:
P (I) & (terminates (Program (I, O) /Q (I, O))
Safety properties: Liveness properties:
(P (I) /Processes (I, S)) & XQ (I, S)
where XQ means that Q does always hold
(P (I) /Processes (I, S)) & oQ (I, S)
where oQ means that Q does eventually hold (and will then stay true)
and S is the current state of the concurrent system © 2019 Uwe R. Zimmer, The Australian National University page 390 of 757 (chapter 4: “Non-determinism” up to page 394)
or
Non-determinism
Non-determinism
Correctness of non-deterministic programs
Correctness predicates need to hold true irrespective of the actual sequence of interaction points.
Correctness predicates need to hold true for all possible sequences of interaction points.
Therefore correctness predicates need to be based on invariants,
i.e. invariant predicates which are independent of the potential execution sequences, yet support the overall correctness predicates.
© 2019 Uwe R. Zimmer, The Australian National University page 391 of 757 (chapter 4: “Non-determinism” up to page 394)
An invariant would for instance be that the number of writing tasks inside a protected object is less or equal to one.
Non-determinism
Non-determinism
Correctness of non-deterministic programs
For example (in verbal form):
“Mutual exclusion accessing a specific resource holds true,
for all possible numbers, sequences or interleavings of requests to it”
Those invariants are the only practical way to guarantee (in a logical sense) correctness in concurrent / non-deterministic systems.
(as enumerating all possible cases and proving them individually is in general not feasible)
© 2019 Uwe R. Zimmer, The Australian National University page 392 of 757 (chapter 4: “Non-determinism” up to page 394)
or
when
Every time you formulate a non-de- terminstic statement like the one on the left you need to formulate an invariant which holds true whichever alternative will actually be chosen.
or
when
…
end select;
This is very similar to finding
loop invariants in sequential programs
© 2019 Uwe R. Zimmer, The Australian National University
page 393 of 757 (chapter 4: “Non-determinism” up to page 394)
Non-determinism
Non-determinism
Correctness of non-deterministic programs
select
when
Concrete:
• Non-determimism by design: • Benefits & considerations
• Non-determinism by interaction: • Selectivesynchronization
• Selectiveaccepts
• Selectivecalls
• Correctness of non-deterministic programs:
• Sources of non-determinism
• Predicates & invariants
© 2019 Uwe R. Zimmer, The Australian National University
page 394 of 757 (chapter 4: “Non-determinism” up to page 394)
Non-determinism
Summary
Non-Determinism