Not enough time between SIGTERM and SIGKILL

[informarte]

When minizinc is used with the -t option, it sends SIGTERM after timeout and, about ~100ms later, SIGKILL:

    10.010 kill(-5774, SIGTERM)         = 0
           ...
     0.001 write(1, "...") = 391
     0.000 write(1, "----------\n", 11) = 11
           ...
     0.137 kill(-5774, SIGKILL)         = 0

In this case, the solver printed the solution and got killed in the further process of shutting down without finishing what it was supposed to do, namely to aggregate and print profiling metrics collected during search. The JVM loaded the classes and then ... boom.

So there is hardly any time for useful work apart from stopping the solver and printing the solution when optimizing, and even that might not always work.

I suggest to add one or both of the following timeout mechanisms:

1. Add a FlatZinc solver flag: If -t is supported according to the solver configuration, then launch the solver with whatever time is left after flattening and trust it to terminate after timeout.

2. Extend the solver configuration with the Boolean property terminatesOnInterrupt: If set, send SIGTERM on timeout and trust the solver to terminate as quickly as possible.

If none of the above is available, then use the existing mechanism.

[informarte]

I just noticed that the MiniZinc manual describes the -t option and I confirmed that minizinc uses it when declared in the solver configuration. However, minizinc does not deduct the time spent on flattening and it does not trust the solver to terminate in time: On timeout, it sends SIGTERM followed by SIGKILL as described above.

[cyderize]

Does this still cause problems when you have -t in your stdFlags?

MiniZinc does deduct the time spent on flattening if a solver configuration .msc file has -t in its stdFlags when running with --time-limit (for overall time limit, not when using -t which is shorthand for --solver-time-limit).

In addition, when a solver supports the -t stdFlag, MiniZinc won't actually try to terminate the solver until 1 second after when it was supposed to stop - so unless a solver takes more than 1 second to start and begin its own timer or stop clean up, MiniZinc shouldn't actually try to terminate it.

I do think we can also increase the interval between SIGTERM and SIGKILL this to 1 second (it's currently supposed to be 200ms) to give more time for clean up when the user does Ctrl+C to interrupt solving.

I can't imagine that a solver should need more than 1 second to do any clean up - is that the case here?