]> matita.cs.unibo.it Git - helm.git/commitdiff
- implemented real thread killing (in place of the previous fake implementation)
authorStefano Zacchiroli <zack@upsilon.cc>
Mon, 22 Mar 2004 17:47:13 +0000 (17:47 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Mon, 22 Mar 2004 17:47:13 +0000 (17:47 +0000)
helm/hbugs/tutors/Makefile
helm/hbugs/tutors/hbugs_deity.ml
helm/hbugs/tutors/hbugs_deity.mli
helm/hbugs/tutors/hbugs_tutors_common.ml
helm/hbugs/tutors/search_pattern_apply_tutor.ml

index f0044dfc6ace1b922dd646705538c605097b171c..9e84bf4e671bae3c96dd05705b5aaf1d7ee690e2 100644 (file)
@@ -27,8 +27,8 @@ DEPSOPT = $(shell $(OCAMLFIND) query -recursive -predicates native -format "%d/%
 
 all: byte
 world: byte opt
-byte: $(TUTORS)
-opt: $(TUTORS_OPT)
+byte: $(COMMON) $(TUTORS)
+opt: $(COMMON_OPT) $(TUTORS_OPT)
 start:
        $(CTL) start
 stop:
index b1fa0f30db910f4d9759b124a14fcc1efd7ca7fc..1b34e09c7e5c9cef1177e3de86a90f2ce11b1483 100644 (file)
@@ -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/
  *
  *  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 ])
 
index f5f3dd5a48f55faa8b9a2aa55d6ef5832d50d1fd..8ec15c0fe0d853dbecc16e4097bffcbb3263fbe1 100644 (file)
@@ -26,8 +26,8 @@
  *  http://helm.cs.unibo.it/
  *)
 
-exception Can_t_kill of int * string
+exception Can_t_kill of Thread.t * string
 
-val create: ('a -> 'b) -> 'a -> int
-val kill: int -> unit
+val create: ('a -> 'b) -> 'a -> Thread.t
+val kill: Thread.t -> unit
 
index 2f186c15dcb1682906b38eda47f32734e594d7e9..dca58766a24900f743903bf9b45ddba50e90ac5a 100644 (file)
@@ -202,8 +202,8 @@ module BuildTutor (Dsc: HbugsTutorDescription) : HbugsTutor =
               Hbugs_deity.kill slave_thread;
               Hashtbl.remove slaves musing_id
             with
-            | Hbugs_deity.Can_t_kill (pid, reason) ->
-              prerr_endline (sprintf "Unable to kill slave %d: %s" pid reason)
+            | Hbugs_deity.Can_t_kill (_, reason) ->
+                prerr_endline (sprintf "Unable to kill slave: %s" reason)
             | Not_found ->
                 prerr_endline (sprintf
                   "Can't find slave corresponding to musing %s, can't kill it"
index 26183e2b97711e4a05c68facdc585e13256b5b88..be2c68d702c00b7d337a68f2e6bfe7e3446226c6 100644 (file)
@@ -72,9 +72,8 @@ let hbugs_callback mqi_handle =
         prerr_endline "received Start_musing";
         let new_musing_id = Hbugs_id_generator.new_musing_id () in
         let id = Hbugs_deity.create (slave mqi_handle) (state, new_musing_id) in
-        prerr_endline
-         (sprintf "starting a new musing (tid = %d, id = %s)" id new_musing_id);
-        Hashtbl.add ids new_musing_id id ;
+        prerr_endline (sprintf "starting a new musing (id = %s)" new_musing_id);
+        Hashtbl.add ids new_musing_id id;
         (*ignore (Thread.create slave (state, new_musing_id));*)
         Musing_started (my_own_id, new_musing_id)
       end else  (* broker unauthorized *)