C-c C-c does not immediately stop processing

[tchajed]

On macOS I've seen cancelling processing take a long time. Usually manually sending SIGKILL rather than SIGINT to the z3 process is immediate, though that will occasionally result in a strange error or fstar.exe crashing.

I don't currently have a small, self-contained example and haven't looked into detail into what's going on when I try to cancel a query, but wanted to record the issue nonetheless.

[cpitclaudel]

I think this works as expected. C-c C-c sends a SIGINT to z3, which is sometimes unreliable. I think we just need a better solution on the F* side.

[s-zanella]

This feature is extremely useful and the current solution of sending a SIGINT to Z3 is almost the best that can be done without extra support on the F* side.

The most annoying thing and what I believe @tchajed is experiencing is that sending a SIGINT to Z3 will interrupt any ongoing query but not any subsequent queries. If the fuel/ifuel settings are such that F retries after killing the current query, then one has to repeatedly hit C-c C-c until no more queries are pending. This is not quite satisfactory though, because hitting C-c C-c many times in quick succession is likely to crash the F process. This requires the user to be aware of how many queries will have to be interrupted and wait a bit between interrupting each.

[cpitclaudel]

This feature is extremely useful and the current solution of sending a SIGINT to Z3 is almost the best that can be done without extra support on the F* side.

Yes, indeed. I realize now my wording may not have been the best. I'm happy we have this feature, and I'm happy that it continues being useful. But I'd be even more happy to add specialized support on the F* side :)

[cpitclaudel]

This is not quite satisfactory though, because hitting C-c C-c many times in quick succession is likely to crash the F* process.

Looking at the code, the crash seems to be on purpose (Z3 exited unadvertedly …):

    proc.Exited.AddHandler(
            EventHandler(fun _ _ ->
            if !killed then ()
            else
                System.Threading.Monitor.Enter(signal);
                killed := true;
                Printf.fprintf stdout "%s exited inadvertently\n%s\n" prog (driverOutput.ToString());
                stdout.Flush();
                System.Threading.Monitor.Exit(signal);
                exit(1))); ///////////////////////////////////////// ← here

This comes from this commit:

commit cdd85ef2b0aeed602f9d11b26aab95cdbe6204a6
Author: Catalin Hritcu <catalin.hritcu@gmail.com>
Date:   Tue Oct 28 14:26:28 2014 +0100

    Z3 exit events and timeouts. Fixes #8.

[cpitclaudel]

https://github.com/FStarLang/FStar/issues/8

[cpitclaudel]

@tej can you confirm that this problem is F#-specific? The OCaml version should be better behaved wrt hard Z3 exits. More precisely, the "exited unadvertedly" message should be F#-specific.

[cpitclaudel]

Looking at the OCaml side, I'm surprised that we even have a problem with sending sigint (possibly multiple times) to Z3: AFAICT it should be handled gracefully by the following bit:

let ask_process (p:proc) (stdin:string) : string =
  let out = Buffer.create 16 in

  let rec read_out _ =
    let s, eof = (try
                    BatString.trim (input_line p.inc), false
                  with End_of_file ->
                    Buffer.add_string out ("\nkilled\n") ; "", true) in
    if not eof then
      if s = "Done!" then ()
      else (Buffer.add_string out (s ^ "\n"); read_out ())
  in

  let child_thread = Thread.create (fun _ -> read_out ()) () in
  output_string p.outc stdin;
  flush p.outc;
  Thread.join child_thread;
  Buffer.contents out

We could make things somewhat cleaner by making this code aware of sigint (which is supported on both Window and GNU/Linux), and sending the sigints to F instead of Z3. We'd ignore sigints in the rest of the F code.

[s-zanella]

I don't know either why F* doesn't handle multiple C-c C-c gracefully.

Making this code SIGINT-aware to let F* handle signals instead of Z3 sounds very promising. It has the nice side effect of getting rid of the complicated code to grep for Z3's PID on Emacs.

[cpitclaudel]

Making this code SIGINT-aware to let F* handle signals instead of Z3 sounds very promising. It has the nice side effect of getting rid of the complicated code to grep for Z3's PID on Emacs.

Ok, I think I may give it a try :) I'll do it on the OCaml side only, I think.

But first, Tej, can you show me the kind of error message that F* prints, so as to make sure I didn't miss something obvious?

[cpitclaudel]

Making this code SIGINT-aware to let F* handle signals instead of Z3 sounds very promising. It has the nice side effect of getting rid of the complicated code to grep for Z3's PID on Emacs.

Done on the F* side, and I've updated fstar-mode accordingly.
I've only tested the new feature on GNU/Linux for now, though, so please try it out on Windows if you can and report :)

[s-zanella]

It doesn't work on Mac OS X. It interrupts F* (e.g. an assert_norm) but not Z3.

[cpitclaudel]

Thanks for testing. Can you share the code sample that you're trying this on?

[cpitclaudel]

I think I can reproduce the issue, actually. It might be due to the way signals work in OCaml. Hmm.

With the example it sometimes takes a few seconds to interrupt, but it always seems to work eventually. Is that what you're seeing too?

[s-zanella]

I'm using this to reproduce it:

module M

val ack: nat -> nat -> nat
let rec ack m n =
  if m = 0 then n + 1
  else if n = 0 then ack (m - 1) 1
  else ack (m - 1) (ack m (n - 1))

#set-options "--initial_fuel 16 --max_fuel 16 --z3rlimit 2000"

let test =
  assert (ack 3 7 == 1021)

Sending a SIGINT directly to Z3 (fstar-subp-kill-z3) interrupts the assert. C-c C-c (fstar-subp-interrupt) doesn't, but it does interrupt the computation if I use assert_norm instead.

[s-zanella]

With the above example, fstar-subp-interrupt seems to never interrupt Z3. In an example with several (fuel,ifuel) combinations to try, I believe it does interrupt the computation after a Z3 query is done and before the next starts.

[cpitclaudel]

Thanks. Investigating this now.

I believe it does interrupt the computation after a Z3 query is done and before the next starts.

That sounds right.

[cpitclaudel]

With the above example, fstar-subp-interrupt seems to never interrupt Z3.

Thanks again for testing. You're were totally right. It's a surprisingly tricky matter, actually. There's a straightforward fix on Unix-style platforms, but not on Windows. I'm looking at a different fix.

[cpitclaudel]

Ok, I've pushed a second attempt. Please give it a go :)

[s-zanella]

Works brilliantly. Thanks!

[cpitclaudel]

Thanks for testing! I'm still seeing a few Z3 issues here and there (duplicate names), which I'll investigate. Many parts of F* are not happy when you throw random exceptions in them, and they are stateful :/

Closing this in the meantime, as the Emacs side is robust ^^