F* loops when Z3 times out or gets killed

[catalin-hritcu]

System.Threading.Monitor.Wait in ask_process in utils.fs gets stuck forever when Z3 times out or gets killed. Could this be some sort of deadlock?

[strub]

I noticed the same problem on my laptop - using the packaged mono. However, the continuous integration, that uses a up-to-date mono compiled from source, does not have this problem.

What are your system's specifications ?

[catalin-hritcu]

[hritcu@detained unit-tests]$ uname -a
Linux detained 3.16.4-1-ARCH #1 SMP PREEMPT Mon Oct 6 08:22:27 CEST 2014 x86_64 GNU/Linux
[hritcu@detained unit-tests]$ mono --version
Mono JIT compiler version 3.10.0 (tarball Mon Oct  6 20:46:04 UTC 2014)
...
[hritcu@detained unit-tests]$ fsharpc         
F# Compiler for F# 3.1 (Open Source Edition)
...

[catalin-hritcu]

I don't completely understand the code in ask_process. Why is System.Threading.Monitor.Wait called? Isn't it just silly to do a Wait right before an Exit?

And anyway, what other thread is supposed to be competing for this lock? :)

[catalin-hritcu]

[Sorry, posted this in the wrong bug report at first]
I think I now understand what the code is trying to do, wait for data from Z3 (the System.Threading.Monitor.Pulse in OutputDataReceived.AddHandler). If Z3 terminates without outputting any data (which seems to be the case for timeouts in 4.3.2 and always when Z3 gets killed) F* just waits forever for a signal. I'll try to fix this by adding one more event handler.

[strub]

Something like this ?

http://msdn.microsoft.com/en-us/library/system.diagnostics.process.exited(v=vs.110).aspx

[catalin-hritcu]

Yes.

[catalin-hritcu]

I've tried the following:

        proc.Exited.AddHandler(
             EventHandler(fun _ _ ->
               Printf.printf "exit handler invoked"; stdout.Flush();
               with_sig(fun () -> 
                 Printf.printf "exited - sending signal"; stdout.Flush();
                 System.Threading.Monitor.Pulse(signal);
                 Printf.printf "exited - signal sent"; stdout.Flush();
                )));

It just blocks at the "with_sig" and I don't see any reason for that.

[catalin-hritcu]

Since #6 just got fixed, to reproduce #8 we now need to replace Z3 with an infinite loop or with something that prints nothing using the --z3exe command line flag. I'm currently reliably reproducing this with "--z3exe true".

[catalin-hritcu]

I've been looking into this more, and it's a bit of a mess:

• On Windows the "z3 exited" handler above does not block without reason, as it does on Linux (mono). Still we should keep this kind of handling as a last resort thing, since (1) it doesn't seem portable and (2) when Z3 is dead there is little we can do beyond cleanly shutting down F*. The way things are setup currently it seems to me very hard to respawn another z3 instance, bring it to the state in which it was before, and continue processing new VCs.
• The -T:seconds option to Z3 is global (for all queries) an simply shuts down the whole Z3 process when time is up. Given that we might be feeding a large, unpredictable number of queries to Z3 and that we don't have a good way to deal with Z3 shutdown when time is up, I don't think we should be using this option at all.
• The -t:xxx soft timeout to Z3 is per-query and doesn't just shut down Z3 when time is up, which seems to be closest to what we actually need. Still, Z3 seems to be taking great liberties in interpreting this soft timeout, 5 seconds soft timeout often means 180 seconds in practice (I've just done a couple of experiments, and that's the average I got for 5 seconds soft timeout). Also we need to be aware that while Z3 4.3.1 was taking xxx in seconds, Z3 4.3.2 takes it in milliseconds.

I'll send in a patch that exits cleanly when Z3 is dead, and that changes from -T to -t. It's not ideal, but I think it's still better than what we have now.

[catalin-hritcu]

Asked for a better solution on the Z3 forum:
https://z3.codeplex.com/discussions/570731
Let's see what they propose.