STM: cancel slaves working on outdated jobs

I did not manage to make the slave manager use Unix.select to wait for a
response from the slave for a limited time and check for cancellation.

Hence the following semi-cooperative model:
- The slave has a thread that sends a Tick every second when the thread
  is working
- The slave_manager will then be unblocked periodically by this tick and
  check for cancellation
- Cancellation is, for the moment, implemented using kill.

To kill a process on windows one could bind TerminateProcess (>= WinXP)
or RegisterWindowMessage + BroadcastSystemMessage (>= Win2k).

See: http://msdn.microsoft.com/en-us/library/windows/desktop/ms686722%28v=vs.85%29.aspx

Another option is to make the slave_manager send to the tick thread on
the slave process a boolean answer to the Tick message, and the tick
thread could eventually bail out.  But to do that, it is way better
to have a second channel, used only by this tick thread.  This solution
sound very like the one proposed for windows, but requires more work.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16878 85f007b7-540e-0410-9357-904b9bb8a0f7

0 files changed, 0 insertions, 0 deletions