History log of /seL4-l4v-master/HOL4/tools/Holmake/poly/PMtest.ML
Revision Date Author Comments
# 36331080 28-Jul-2016 Michael Norrish <Michael.Norrish@nicta.com.au>

Rework poly/ml multi-plexing to use IO-polling

Old code used sleep to stop itself spin-polling on possible output from
sub-processes. The "right" approach to this is to use OS.IO.poll (which
will be a call to some version of select on Unix). Not only is this the
"right" solution, but it also seems to perform more reliably in the face
of subprocesses going into infinite loops or deep sulks. (The problem
with sleep is that the OS doesn't seem to want to guarantee that it will
ever come back.)

The new robustness should allow Holmake to display three red exclamation
marks as a signal that something is stalling more often than it has in
the past.

Also add a simple test-script for checking the multi-plexing.