3.10 Scheduling and Fairness
The compiler and the runtime provide partial guarantee about fairness
in their scheduling strategies. As regards processes triggered in
independent definitions, the usual fairness properties apply.
On the contrary, the choice among join-patterns in conflict within the
same definition is mostly performed once for all at compile-time,
which allows the compiler to generate fewer threads for the processes
and more efficient representations for the definitions.
3.10.1 Guaranteed fairness properties
A definition is active when enough messages are present to match
at least one of its join-patterns; because these messages cannot be
consumed otherwise, an active definition remains active until one of
its patterns is actually triggered.
The current implementation guarantees that:
-
In an active definition, one join-pattern is eventually triggered
- If there are enough messages to trigger a join-pattern, then one pattern
with at least one name in common with the latter is eventually
triggered.
Apart from that, the join-calculus programmer should not rely on a
particular scheduling strategy, even if it appears to work.
For instance, the implementation guarantees that the following program
eventually prints its message:
let loop() = loop()
and done() = { print_string("over !!\n"); }
spawn { loop() | done() }
Conversely, the implementation does not guarantee that if there
are always enough messages to trigger a pattern, then it is eventually
triggered; for instance, when in a definition some pattern is included
in another, the latter pattern may never be triggered.
Indeed, the following program will probably run forever without
printing anything:
let loop() = loop()
and loop() | done() = { print_string("over !!\n"); }
spawn { loop() | done() }
In other words, there is no fairness between the matching join-patterns
of an active definition.
Also notice that every call to an external primitive defined in
Objective Caml should terminate. As there is no mechanism to enforce
it, an external call that runs forever can cause the whole program to
deadlock.
3.10.2 Distributed computation and fairness
Assuming that a message within a failed location is not considered
present anymore, the previous guarantees hold, no matter of the actual
localization of processes and definitions.
There are specific guarantees for the migration primitives:
-
If a halt process is running in a location, then its location
branch eventually stops.
- If a go process is running in a location that remains alive,
then eventually the migration succeeds (no matter whether its
destination is alive or not; in the latter case, the migration
succeeds in stopping the moving location).
A full-fledged implementation of failure-detection should also
guarantee that:
-
If a fail-guarded process is running in a location that remains
alive, and if the watched location has stopped, then eventually the
guarded process is triggered.
The current implementation enforces this last condition only as long
as none of the involved runtime terminates.
3.10.3 Termination
When running in local mode, a runtime stops as soon as no pattern may
be triggered anymore (i.e., no more active definitions); otherwise a
runtime never stops by itself.
A standard library is provided to explicitly perform distributed
termination when a program knows the computation is over (cf.
5.12).