search

fbrausse / smlp

Symbolic ML Prover
https://fbrausse.github.io/smlp/
Apache License 2.0
4 stars 1 forks source link

v2: Timeouts #2

Open fbrausse opened 2 years ago

fbrausse commented 2 years ago

As per the discussion on 2021-10-25: timeouts are to be implemented by aborting a running worker.

This is a different solution to what is already implemented in the fb/v2 branch: Apriori timeouts encoded within the SMT-LIB instance sent to workers.

In fb/v2, asnchronous tasks corresponding to active workers can already be terminated by sending a Type.CLIENT_QUIT message, but this also closes the connection. A new message type Type.CLIENT_ABORT_SOLVER, say, could be added that makes a worker terminate its child process (if running at that point).

The server would keep track of timeouts and send such messages to workers as appropriate.

fbrausse commented 2 years ago

Today briefly an alternative was discussed, but dismissed as too complicated for now: interruptable workers maintaing a set of stopped (possibly by SIGSTOP/SIGCONT signals) child processes in addition to the optional currently active one.