- implemented real thread killing (in place of the previous fake implementation)

[helm.git] / helm / hbugs / tutors / hbugs_deity.ml

diff --git a/helm/hbugs/tutors/hbugs_deity.ml b/helm/hbugs/tutors/hbugs_deity.ml
index b1fa0f30db910f4d9759b124a14fcc1efd7ca7fc..1b34e09c7e5c9cef1177e3de86a90f2ce11b1483 100644 (file)
--- a/helm/hbugs/tutors/hbugs_deity.ml
+++ b/helm/hbugs/tutors/hbugs_deity.ml
@@ -1,5 +1,5 @@
 (*
- * Copyright (C) 2003:
+ * Copyright (C) 2003-2004:
  *    Stefano Zacchiroli <zack@cs.unibo.it>
  *    for the HELM Team http://helm.cs.unibo.it/
  *
@@ -26,7 +26,18 @@
  *  http://helm.cs.unibo.it/
  *)
 
-exception Can_t_kill of int * string ;; (* pid, reason *)
+let debug = true
+let debug_print s = if debug then prerr_endline s
+
+exception Can_t_kill of Thread.t * string (* thread, reason *)
+exception Thread_not_found of Thread.t
+
+module OrderedPid =
+  struct
+    type t = int
+    let compare = Pervasives.compare
+  end
+module PidSet = Set.Make (OrderedPid)
 
  (* perform an action inside a critical section controlled by given mutex *)
 let do_critical mutex =
@@ -37,39 +48,12 @@ let do_critical mutex =
       Mutex.unlock mutex;
       res 
     with e -> Mutex.unlock mutex; raise e
-;;
 
-let kill_signal = Sys.sigusr2 ;;    (* signal used to kill children *)
-let chan = Event.new_channel () ;;  (* communication channel between threads *)
-
-  (* functions mangling "must die" PID list *)
-let (add_to_dead_threads_walking, remove_from_dead_threads_walking, must_die) =
-  let dead_threads_walking = ref [] in
-  let mutex = Mutex.create () in
-  let add pid = do_critical mutex (lazy (
-      dead_threads_walking := pid :: !dead_threads_walking;
-  )) in
-  let remove pid = do_critical mutex (lazy (
-      dead_threads_walking := List.filter ((<>) pid) !dead_threads_walking
-  )) in
-  let is_in pid = do_critical mutex (lazy (
-      List.exists ((=) pid) !dead_threads_walking
-  )) in
-  (add, remove, is_in)
-;;
-
-  (* "kill_signal" handler, check if current process must die, if this is the
-  case exits with Thread.exit *)
-ignore (Sys.signal kill_signal (Sys.Signal_handle
-  (fun signal ->
-    let myself = Unix.getpid () in
-    match signal with
-    | sg when (sg = kill_signal) && (must_die myself) ->
-        remove_from_dead_threads_walking myself;
-        prerr_endline "AYEEEEH!";
-        Thread.exit ()
-    | _ -> ())))
-;;
+let kill_signal = Sys.sigusr2   (* signal used to kill children *)
+let chan = Event.new_channel () (* communication channel between threads *)
+let creation_mutex = Mutex.create ()
+let dead_threads_walking = ref PidSet.empty
+let pids: (Thread.t, int) Hashtbl.t = Hashtbl.create 17
 
   (* given a thread body (i.e. first argument of a Thread.create invocation)
   return a new thread body which unblock the kill signal and send its pid to
@@ -79,30 +63,46 @@ let wrap_thread body =
     ignore (Unix.sigprocmask Unix.SIG_UNBLOCK [ kill_signal ]);
     Event.sync (Event.send chan (Unix.getpid ()));
     body arg
-;;
 
-let creation_mutex = Mutex.create () ;;
+(*
+(* FAKE IMPLEMENTATION *)
+let create = Thread.create
+let kill _ = ()
+*)
 
-(* REAL IMPLEMENTATION NOT YET WORKING --ZACK
 let create body arg =
   do_critical creation_mutex (lazy (
-      ignore (Thread.create (wrap_thread body) arg);
-      Event.sync (Event.receive chan)
+    let thread_t = Thread.create (wrap_thread body) arg in
+    let pid = Event.sync (Event.receive chan) in
+    Hashtbl.add pids thread_t pid;
+    thread_t
   ))
-;;
 
-let kill pid =
-  add_to_dead_threads_walking pid;
+let kill thread_t =
   try
+    let pid =
+      try
+        Hashtbl.find pids thread_t
+      with Not_found -> raise (Thread_not_found thread_t)
+    in
+    dead_threads_walking := PidSet.add pid !dead_threads_walking;
     Unix.kill pid kill_signal
-  with e -> raise (Can_t_kill (pid, Printexc.to_string e))
-;;
-*)
+  with e -> raise (Can_t_kill (thread_t, Printexc.to_string e))
 
-(* FAKE IMPLEMENTATION *)
-let create x y = let _ = Thread.create x y in ~-1 ;;
-let kill _ = () ;;
+  (* "kill_signal" handler, check if current process must die, if this is the
+  case exits with Thread.exit *)
+let _ =
+  ignore (Sys.signal kill_signal (Sys.Signal_handle
+    (fun signal ->
+      let myself = Unix.getpid () in
+      match signal with
+      | sg when (sg = kill_signal) &&
+                (PidSet.mem myself !dead_threads_walking) ->
+          dead_threads_walking := PidSet.remove myself !dead_threads_walking;
+          debug_print "AYEEEEH!";
+          Thread.exit ()
+      | _ -> ())))
 
   (* block kill signal in main process *)
-ignore (Unix.sigprocmask Unix.SIG_BLOCK [ kill_signal ]) ;;
+let _ = ignore (Unix.sigprocmask Unix.SIG_BLOCK [ kill_signal ])