From: Stefano Zacchiroli Date: Mon, 22 Mar 2004 17:47:13 +0000 (+0000) Subject: - implemented real thread killing (in place of the previous fake implementation) X-Git-Tag: v0_0_4~6 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1d08808239ea6db4c163d8377deecfeb4fa9afcd;p=helm.git - implemented real thread killing (in place of the previous fake implementation) --- diff --git a/helm/hbugs/tutors/Makefile b/helm/hbugs/tutors/Makefile index f0044dfc6..9e84bf4e6 100644 --- a/helm/hbugs/tutors/Makefile +++ b/helm/hbugs/tutors/Makefile @@ -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: diff --git a/helm/hbugs/tutors/hbugs_deity.ml b/helm/hbugs/tutors/hbugs_deity.ml index b1fa0f30d..1b34e09c7 100644 --- 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 * 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 ]) diff --git a/helm/hbugs/tutors/hbugs_deity.mli b/helm/hbugs/tutors/hbugs_deity.mli index f5f3dd5a4..8ec15c0fe 100644 --- a/helm/hbugs/tutors/hbugs_deity.mli +++ b/helm/hbugs/tutors/hbugs_deity.mli @@ -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 diff --git a/helm/hbugs/tutors/hbugs_tutors_common.ml b/helm/hbugs/tutors/hbugs_tutors_common.ml index 2f186c15d..dca58766a 100644 --- a/helm/hbugs/tutors/hbugs_tutors_common.ml +++ b/helm/hbugs/tutors/hbugs_tutors_common.ml @@ -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" diff --git a/helm/hbugs/tutors/search_pattern_apply_tutor.ml b/helm/hbugs/tutors/search_pattern_apply_tutor.ml index 26183e2b9..be2c68d70 100644 --- a/helm/hbugs/tutors/search_pattern_apply_tutor.ml +++ b/helm/hbugs/tutors/search_pattern_apply_tutor.ml @@ -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 *)