The guarded-command looping construct
do
Condition ⇒ Command
...
Condition ⇒ Command
od
involves nondeterministic choice, as explained in the text. An important theoretical concept related to potentially nonterminating nondeterministic computation is fairness. If a loop repeats indefinitely, then a fair nondeterministic choice must eventually select each command whose guard is true. For example, in the loop
do
true ⇒ x := x+1
true ⇒ x := x-1
od
both commands have guards that are always true. It would be unfair to execute x := x+1 repeatedly without ever executing x := x-1.
Most language implementations are
designed to provide fairness, usually by providing a bounded form. For example,
if there are n guarded commands, then the implementation may guarantee that
each enabled command will be executed at least once in every 2n or 3n times
through the loop.
Because the number 2n or 3n is implementation dependent,
though, programmers should assume only that each command with a true guard
will eventually be executed.
Is fairness easier to provide on a single-processor language implementation or on a multiprocessor?
Most languages have a serial model of execution, like machine code, not executing each statement in parallel with arbitrary ratios of executions. For example in C,
You'll always get output like
in that order.
Fair (or at least non-starving) thread-level parallelism is pretty easy on single or multi-core machines, with pre-emptive multi-tasking. Most languages with a thread model are designed around pre-emptive thread scheduling, where one thread running an infinite loop (even with no system calls) won't starve other threads.
Multi-core is harder to implement a correct OS for (e.g. you need locking, not just disabling interrupts), but does allow more threads to be running at once.