search

vprover / vampire

The Vampire Theorem Prover
https://vprover.github.io/
Other
302 stars 52 forks source link

file-based portfolio synchronisation #540

Closed MichaelRawson closed 6 months ago

MichaelRawson commented 8 months ago

See #462. We currently synchronise child Vampires and their proof printing by UNIX semaphores, which are quite complex beasts. However, C11 (and therefore C++17) can synchronise on a file by passing an "x"clusive flag to fopen: if the file exists, fopen will fail. Note that the standard only says "to the extent the platform supports exclusive access", but it seems to work quite well in practice.

Therefore:

  1. We determine a path that should be written to. This is either what the user requested or a temporary file.
  2. We delete it if it exists!
  3. The first child to not find that file creates it and writes its proof there.
  4. Other children find the file and do not print a proof.
  5. The parent Vampire knows the path and reads from it once all children have finished (one way or another).

I think this is simpler and certainly more portable, but of course it needs lots of testing: it would be a silly way to lose problems.

MichaelRawson commented 7 months ago

To explain the signal-handling change: currently we handle many different signals with very similar but slightly different code. This looks more like organic growth over time rather than something intentionally complex, so I've streamlined it. There are now only two broad classes of signal we handle:

  1. Exit now, silently: SIGHUP (portfolio parent died), SIGINT (Ctrl-C), SIGTERM (polite termination), and SIGXCPU (we're being warned that we've used an external resource limit and are about to be killed). SIGXCPU has moved from the other class, I don't think we want to special-case this.
  2. Crash of some kind: everything else, including SIGQUIT as apparently that's an abnormal halt intended to be used for debugging. Here we print a stack trace, indicate something to Spider, etc.
quickbeam123 commented 7 months ago

Since you already polished the signals, could you please give me back the feature we used to have, that Vampire reports statistics (if asked) and termination reason on CTRL+C?

(This should be obvious in vampire mode, not sure how complex it is in portfolio mode? Does the CTRL+C reach the master if there are many competing workers spawned from it?)