Heavily rewritten the coqtop management process of coqide. The coqtop

object is now responsible for restarting itself, and handles unexpected
crashes. Fixes a lot of errors in file descriptor management, but may
introduce lurking deadlocks and nasty bugs waiting to be discovered.

Only (quickly) tested under Linux, any callbacks from Windows are welcome.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15314 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 198 insertions, 36 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index bca972006..1ce9379d2 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -110,27 +110,64 @@ let check_connection args =
       List.iter Minilib.safe_prerr_endline lines;
       exit 1
 
+(** Useful stuff *)
+
+let atomically mtx f arg =
+  Mutex.lock mtx;
+  try
+    let ans = f arg in
+    Mutex.unlock mtx;
+    ans
+  with err ->
+    Mutex.unlock mtx;
+    raise err
+
+let ignore_error f arg =
+  try ignore (f arg) with _ -> ()
+
 (** * The structure describing a coqtop sub-process *)
 
+type handle = {
+  pid : int;
+  (* Unix process id *)
+  cout : in_channel;
+  cin : out_channel;
+  mutable alive : bool;
+}
+
 type coqtop = {
-  pid : int; (* Unix process id *)
-  cout : in_channel ;
-  cin : out_channel ;
+  (* lock managing coqtop access *)
+  lock : Mutex.t;
+  (* non quoted command-line arguments of coqtop *)
   sup_args : string list;
+  (* actual coqtop process *)
+  mutable handle : handle;
+  (* trigger called whenever coqtop dies abruptly *)
+  trigger : handle -> unit;
+  (* whether coqtop may be relaunched *)
+  mutable is_closed : bool;
+  (* whether coqtop is computing *)
+  mutable is_computing : bool;
+  (* whether coqtop is waiting to be resetted *)
+  mutable is_to_reset : bool;
 }
 
+(** Invariants:
+  - any outside request takes the coqtop.lock and is discarded when
+    [is_closed = true].
+  - coqtop.handle may be written ONLY when toplvl_ctr_mtx AND coqtop.lock is 
+    taken.
+*)
+
+exception DeadCoqtop
+
 (** * Count of all active coqtops *)
 
 let toplvl_ctr = ref 0
 
 let toplvl_ctr_mtx = Mutex.create ()
 
-let coqtop_zombies () =
-  Mutex.lock toplvl_ctr_mtx;
-  let res = !toplvl_ctr in
-  Mutex.unlock toplvl_ctr_mtx;
-  res
-
+let coqtop_zombies () = !toplvl_ctr
 
 (** * Starting / signaling / ending a real coqtop sub-process *)
 
@@ -161,38 +198,102 @@ let open_process_pid prog args =
   set_binary_mode_in ic true;
   (pid,ic,oc)
 
-let spawn_coqtop sup_args =
-  Mutex.lock toplvl_ctr_mtx;
-  try
-    let prog = coqtop_path () in
-    let args = Array.of_list (prog :: "-ideslave" :: sup_args) in
-    let (pid,ic,oc) = open_process_pid prog args in
-    incr toplvl_ctr;
-    Mutex.unlock toplvl_ctr_mtx;
-    { pid = pid; cin = oc; cout = ic ; sup_args = sup_args }
-  with e ->
-    Mutex.unlock toplvl_ctr_mtx;
-    raise e
-
-let respawn_coqtop coqtop = spawn_coqtop coqtop.sup_args
+(** This launches a fresh handle from its command line arguments. *)
+let unsafe_spawn_handle args =
+  let prog = coqtop_path () in
+  let args = Array.of_list (prog :: "-ideslave" :: args) in
+  let (pid, ic, oc) = open_process_pid prog args in
+  incr toplvl_ctr;
+  {
+    pid = pid;
+    cin = oc;
+    cout = ic;
+    alive = true;
+  }
+
+(** This clears any potentially remaining open garbage. *)
+let unsafe_clear_handle coqtop =
+  let handle = coqtop.handle in
+  if handle.alive then begin
+    (* invalidate the old handle *)
+    handle.alive <- false;
+    ignore_error close_out handle.cin;
+    ignore_error close_in handle.cout;
+    ignore_error (Unix.waitpid []) handle.pid;
+    decr toplvl_ctr
+  end
+
+let spawn_coqtop hook sup_args =
+  let handle =
+    atomically toplvl_ctr_mtx unsafe_spawn_handle sup_args
+  in
+  {
+    handle = handle;
+    lock = Mutex.create ();
+    sup_args = sup_args;
+    trigger = hook;
+    is_closed = false;
+    is_computing = false;
+    is_to_reset = false;
+  }
 
 let interrupter = ref (fun pid -> Unix.kill pid Sys.sigint)
 let killer = ref (fun pid -> Unix.kill pid Sys.sigkill)
 
+let is_computing coqtop = coqtop.is_computing
+
+let is_closed coqtop = coqtop.is_closed
+
+(** These are asynchronous signals *)
 let break_coqtop coqtop =
-  try !interrupter coqtop.pid
+  try !interrupter coqtop.handle.pid
   with _ -> prerr_endline "Error while sending Ctrl-C"
 
 let kill_coqtop coqtop =
-  let pid = coqtop.pid in
-  begin
-    try !killer pid
-    with _ -> prerr_endline "Kill -9 failed. Process already terminated ?"
-  end;
+  try !killer coqtop.handle.pid
+  with _ -> prerr_endline "Kill -9 failed. Process already terminated ?"
+
+let unsafe_process coqtop f =
+  coqtop.is_computing <- true;
   try
-    ignore (Unix.waitpid [] pid);
-    Mutex.lock toplvl_ctr_mtx; decr toplvl_ctr; Mutex.unlock toplvl_ctr_mtx
-  with _ -> prerr_endline "Error while waiting for child"
+    f coqtop.handle;
+    coqtop.is_computing <- false;
+    Mutex.unlock coqtop.lock
+  with
+  | DeadCoqtop ->
+    coqtop.is_computing <- false;
+    Mutex.lock toplvl_ctr_mtx;
+    (* Coqtop died from an non natural cause, we have the lock, so it's our duty 
+       to relaunch it here. *)
+    if not coqtop.is_closed && not coqtop.is_to_reset then begin
+      ignore_error unsafe_clear_handle coqtop;
+      let try_respawn () =
+      coqtop.handle <- unsafe_spawn_handle coqtop.sup_args;
+      in
+      ignore_error try_respawn ();
+      (* If respawning coqtop failed, there is not much we can do... *)
+      assert (coqtop.handle.alive = true);
+      (* Process the reset callback *)
+      ignore_error coqtop.trigger coqtop.handle;
+    end;
+    Mutex.unlock toplvl_ctr_mtx;
+    Mutex.unlock coqtop.lock;
+  | err ->
+    (* Another error occured, we propagate it. *)
+    coqtop.is_computing <- false;
+    Mutex.unlock coqtop.lock;
+    raise err
+
+let grab coqtop f =
+  Mutex.lock coqtop.lock;
+  if not coqtop.is_closed && not coqtop.is_to_reset then unsafe_process coqtop f
+  else Mutex.unlock coqtop.lock
+
+let try_grab coqtop f g =
+  if Mutex.try_lock coqtop.lock then
+    if not coqtop.is_closed && not coqtop.is_to_reset then unsafe_process coqtop f
+    else Mutex.unlock coqtop.lock
+  else g ()
 
 (** * Calls to coqtop *)
 
@@ -202,10 +303,22 @@ let p = Xml_parser.make ()
 let () = Xml_parser.check_eof p false
 
 let eval_call coqtop (c:'a Serialize.call) =
-  Xml_utils.print_xml coqtop.cin (Serialize.of_call c);
-  flush coqtop.cin;
-  let xml = Xml_parser.parse p (Xml_parser.SChannel coqtop.cout) in
-  (Serialize.to_answer xml : 'a Interface.value)
+  try
+    Xml_utils.print_xml coqtop.cin (Serialize.of_call c);
+    flush coqtop.cin;
+    let xml = Xml_parser.parse p (Xml_parser.SChannel coqtop.cout) in
+    (Serialize.to_answer xml : 'a Interface.value)
+  with
+  | Serialize.Marshal_error ->
+    (* the protocol was not respected... *)
+    raise Serialize.Marshal_error
+  | err ->
+    (* if anything else happens here, coqtop is most likely dead *)
+    let msg = Printf.sprintf "Error communicating with pid [%i]: %s"
+      coqtop.pid (Printexc.to_string err)
+    in
+    prerr_endline msg;
+    raise DeadCoqtop
 
 let interp coqtop ?(raw=false) ?(verbose=true) s =
   eval_call coqtop (Serialize.interp (raw,verbose,s))
@@ -215,6 +328,55 @@ let mkcases coqtop s = eval_call coqtop (Serialize.mkcases s)
 let status coqtop = eval_call coqtop Serialize.status
 let hints coqtop = eval_call coqtop Serialize.hints
 
+let unsafe_close coqtop =
+  if Mutex.try_lock coqtop.lock then begin
+    let () =
+      try
+        match eval_call coqtop.handle Serialize.quit with
+        | Interface.Good _ -> ()
+        | _ -> raise Exit
+      with err -> kill_coqtop coqtop
+    in
+    Mutex.unlock coqtop.lock
+  end else begin
+    (* bring me the chainsaw! *)
+    kill_coqtop coqtop
+  end
+
+let close_coqtop coqtop =
+  (* wait for acquiring the process management lock *)
+  atomically toplvl_ctr_mtx (fun _ -> coqtop.is_closed <- true) ();
+  (* try to quit coqtop gently *)
+  unsafe_close coqtop;
+  (* Finalize the handle *)
+  Mutex.lock coqtop.lock;
+  Mutex.lock toplvl_ctr_mtx;
+    ignore_error unsafe_clear_handle coqtop;
+  Mutex.unlock toplvl_ctr_mtx;
+  Mutex.unlock coqtop.lock
+
+let reset_coqtop coqtop hook =
+  (* wait for acquiring the process management lock *)
+  atomically toplvl_ctr_mtx (fun _ -> coqtop.is_to_reset <- true) ();
+  (* try to quit coqtop gently *)
+  unsafe_close coqtop;
+  (* Reset the handle *)
+  Mutex.lock coqtop.lock;
+  Mutex.lock toplvl_ctr_mtx;
+    ignore_error unsafe_clear_handle coqtop;
+    let try_respawn () =
+    coqtop.handle <- unsafe_spawn_handle coqtop.sup_args;
+    in
+    ignore_error try_respawn ();
+    (* If respawning coqtop failed, there is not much we can do... *)
+    assert (coqtop.handle.alive = true);
+    (* Reset done *)
+    coqtop.is_to_reset <- false;
+    (* Process the reset callback with the given hook *)
+    ignore_error hook coqtop.handle;
+  Mutex.unlock toplvl_ctr_mtx;
+  Mutex.unlock coqtop.lock
+
 module PrintOpt =
 struct
   type t = string list