search

goblint / analyzer

Static analysis framework for C
https://goblint.in.tum.de
MIT License
185 stars 75 forks source link

Use SV-COMP time limit for soft exit #1221

Open sim642 opened 1 year ago

sim642 commented 1 year ago

SV-COMP and BenchExec can give the task time limit to the tool. Goblint doesn't use this information and just keeps running after the BenchExec soft time limit until it is killed at the hard time limit.

We should use this information to do a soft exit after the given time limit because continuing solving gives us nothing. It just wastes resources and makes benchmarks run longer.

sim642 commented 1 year ago

BenchExec should send SIGTERM on soft time limit and Goblint does react to it (and doesn't even override the signal handler), but somehow it doesn't work under BenchExec? SV-COMP 2023 results contain over 1416 instances of Goblint TIMEOUT with 960s CPU time.

sim642 commented 1 year ago

I couldn't reproduce this with runexec nor under BenchExec. Even with SV-COMP 2023 setup: BenchExec 3.16 and Goblint svcomp23.

michael-schwarz commented 1 year ago

If it cannot be reproduced, should we close it?

sim642 commented 1 year ago

It still happens in Dirk's preruns though.

It might depend on what exactly Goblint is doing at the time it gets the signal. OCaml's signal handling isn't necessarily immediate. If a signal is received, the signal handler just marks it as received but doesn't do anything else. Only at certain points in the OCaml runtime is this signal flag checked and handlers executed.

sim642 commented 1 week ago

SV-COMP 2025 prerun results contain 1298 instances of Goblint TIMEOUT with 960s CPU time, so the issue still remains after the catch-all exception handler fixes.