SV-COMP Errors: `exception Sys_error("Mutex.lock: Resource deadlock avoided")`

[michael-schwarz]

Since updating the goblint-cil pin (#1780), we get new kinds of errors in SV-COMP:

./goblint --conf conf.json --sets ana.specification /home/goblint/sv-benchmarks/c/properties/termination.prp --sets exp.architecture 32bit /home/goblint/sv-benchmarks/c/uthash-2.0.2/uthash_SFH_test6-2.i
....
[Warning][Analyzer] Invariant Apron: coefficient is not int: 1.84467440695e+19
[Warning][Analyzer] Invariant Apron: coefficient is not int: 1.84467440764e+19
[Warning][Analyzer] Invariant Apron: coefficient is not int: 1.84467440711e+19

[Info] Fatal error: exception Sys_error("Mutex.lock: Resource deadlock avoided")

This seems to me to be unrelated to frontend changes and much more likely due to concurrency support. The diff between the CIL versions is: https://github.com/goblint/cil/compare/8385ab315bc7461f6801af57673c64731bfa036a..goblint:cil:c0b10d1848223a67de45ef608f4e05c082977ac1

CC: @arkocal

[michael-schwarz]

For other tasks, this happens while computation is still ongoing:

./goblint --conf conf.json --sets ana.specification /home/goblint/sv-benchmarks/c/properties/unreach-call.prp --sets exp.architecture 64bit /home/goblint/sv-benchmarks/c/goblint-coreutils/instrumented_du_comb.i
...
[Error][Analyzer] About to crash at mark transfer function at /home/goblint/sv-benchmarks/c/goblint-coreutils/instrumented_du_comb.i:53883:20-53883:45!
[Info] 
[Info] runtime: 00:06:01.741
[Info] vars: 1650852, evals: 2203937

[Info] |called|=356

Memory statistics: total=589994.43MB, max=3285.79MB, minor=589189.72MB, major=7080.40MB, promoted=6275.69MB
    minor collections=281229  major collections=26 compactions=0


Fatal error: exception Sys_error("Mutex.lock: Resource deadlock avoided")
Marked with transfer function at /home/goblint/sv-benchmarks/c/goblint-coreutils/instrumented_du_comb.i:53883:20-53883:45

[arkocal]

I will investigate. Curiously, the linked changes do not introduce mutexes but moves refs to DLS. Could be due to domain shims or a change introduced by another commit on goblint and did not triggered the error by luck.

[michael-schwarz]

It would be odd that the issue did not arise for any previous runs and now surfaces multiple times, so my money is on the shims.

[michael-schwarz]

Hypothesis: Is this related to interrupt handling for outputting timing? It seems possible that two print-related things may be going on at the same time, and that the eact interleaving depends on random things.

[michael-schwarz]

After reading up on it, it seems exceedingly likely that this is the problem:

In fact, OCaml does not treat signals in a strictly asynchronous fashion. On receiving a signal, OCaml records the receipt of the signal but the signal handling function will only be executed at certain checkpoints. These are frequent enough to provide the illusion of asynchronous execution. The checkpoints typically occur during allocations, loop controls, or interactions with the system (particularly system calls). OCaml guarantees that a program that does not loop, does not allocate, and does not interact with the system will not have its execution interleaved with that of a signal handler. In particular, storing an unallocated value (integer, boolean, etc. — but not a float!) in a reference cell cannot result in the race condition described above.

(from https://ocaml.github.io/ocamlunix/signals.html)

[sim642]

That sounds like a very reasonable hypothesis. In that case disabling the solver info every 10s should avoid the problem.

But the fact that this now causes a deadlock due to extra locking on Pretty internals means that some weird interactions must've been going on previously as well, just without a flat-out crash.

If this is the case, then moving printing out of the signal handler itself would be reasonable, although we'd have to think where exactly.
But the other worrying point is that we're apparently printing something during solving itself. That's unusual, because usually it's just one solver stats printout after another. Perhaps there's some internal unnecessary string conversion taking place as well.

[michael-schwarz]

let mtx = Mutex.create ()
let k = Domain.DLS.new_key (fun () -> 0)
let do_stuff _ =
  Mutex.lock mtx;
  Printf.printf "Doing stuff at %f\n" (Unix.gettimeofday ());
  Mutex.unlock mtx

let do_stuff2 _ =
  let i = Domain.DLS.get k in
  Domain.DLS.set k (i + 1)

let () =

  Sys.set_signal Sys.sigvtalrm (Signal_handle do_stuff2);
  ignore Unix.(setitimer ITIMER_VIRTUAL { it_interval = 0.001; it_value = 0.001 });

  while true do
    do_stuff2 ();
  done;

Indeed, this misbehaves with OCaml 4 and domain_shims but works with OCaml 5.

[michael-schwarz]

I filed an issue upstream: https://gitlab.com/gasche/domain-shims/-/issues/6

The question is if we can get rid of pretty-printing in the signal handler (hard, we also want stats when we're inside some (quasi-) infinite loop in an RHS). The alternative is providing a shim for DLS that does not attempt to be smart but just uses ordinary references in OCaml 4.

[sim642]

Regardless of how hard it is to move the printing out of the signal handler, I think it's still worth looking into:

But the other worrying point is that we're apparently printing something during solving itself. That's unusual, because usually it's just one solver stats printout after another. Perhaps there's some internal unnecessary string conversion taking place as well.

The analyses should not be using Pretty to convert things to strings during the analysis (unless warn_at is early at least). I may be wrong, but I can't currently think of a legitimate reason to do that.
It might help to do an sv-benchmarks run with -v to get the backtrace at that point. I think the backtrace should still contain the entire non-signal-handler stack, so it would expose where are we using Pretty during analysis.

Of course avoiding that isn't a particularly reliable fix, but it would make sense to avoid it anyway for performance reasons.

On another note, it might also be worth trying to reduce the amount of global DLS in Pretty. Each Pretty.doc → string conversion should be entirely self-contained and thus not need global state at all. It may just be that Pretty has been implemented with global state for convenience (not having to pass many arguments around).

[sim642]

I tried the case from the issue description and -v gives:

[Info] Fatal error: exception Sys_error("Mutex.lock: Resource deadlock avoided")
Raised by primitive operation at Mutex in file "mutex.ml" (inlined), line 18, characters 0-44
Called from Domain.atomically in file "lib/domain.ml" (inlined), line 35, characters 4-26
Called from Domain.DLS.set in file "lib/domain.ml", line 130, characters 4-63
Called from GoblintCil__Pretty.print_with_state in file "src/ocamlutil/pretty.ml", line 582, characters 2-22
Called from Messages.msg.finish in file "src/common/util/messages.ml", line 283, characters 17-35
Called from Goblint_lib__Maingoblint.do_analyze.control_analyze in file "src/maingoblint.ml", line 566, characters 8-73
Called from Goblint_timing.Make.wrap in file "src/util/timing/goblint_timing.ml", line 148, characters 10-13
Re-raised at Goblint_timing.Make.wrap in file "src/util/timing/goblint_timing.ml", line 154, characters 6-13
Called from Dune__exe__Goblint.main in file "src/goblint.ml", line 63, characters 6-35
Called from Stdlib.at_exit.new_exit in file "stdlib.ml", line 560, characters 59-63
Called from Stdlib.do_at_exit in file "stdlib.ml" (inlined), line 566, characters 20-61
Called from Std_exit in file "std_exit.ml", line 18, characters 8-20

Notably, Maingoblint.do_analyze.control_analyze in file "src/maingoblint.ml", line 566, characters 8-73 is itself in the global "About to crash" exception handler.
So in this case the issue happens when we're trying to print out some exception from the analysis.

The cases where this deadlock arose: did we use to normally terminate on them? Or did they all previously also crash with some other exception?

[sim642]

Another thing that I noticed a while ago, but what's relevant to the case from the issue description (where the deadlock is during warning output):
We never turn off the solver stats signal, so it keeps printing even after the solver has finished and we're doing some other (long) post-processing, e.g. g2html, witnesses, or I guess just printing warnings.
An obvious thing (but not complete fix) would be to actually remove the interval signaling after solving is done.