From: Stefano Zacchiroli Date: Tue, 15 Apr 2003 15:47:42 +0000 (+0000) Subject: added support for slaves killing X-Git-Tag: before_refactoring~22 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=1f9b11657c822cc762f808e0bfc5f5f2b4fb6ec7 added support for slaves killing --- diff --git a/helm/hbugs/tutors/.cvsignore b/helm/hbugs/tutors/.cvsignore index a3cccbc0c..7e2e0036f 100644 --- a/helm/hbugs/tutors/.cvsignore +++ b/helm/hbugs/tutors/.cvsignore @@ -4,3 +4,24 @@ *.cmx *.o *.a +ring_tutor.ml +fourier_tutor.ml +reflexivity_tutor.ml +symmetry_tutor.ml +assumption_tutor.ml +contradiction_tutor.ml +exists_tutor.ml +split_tutor.ml +left_tutor.ml +right_tutor.ml +ring_tutor +fourier_tutor +reflexivity_tutor +symmetry_tutor +assumption_tutor +contradiction_tutor +exists_tutor +split_tutor +left_tutor +right_tutor +search_pattern_apply_tutor diff --git a/helm/hbugs/tutors/Makefile b/helm/hbugs/tutors/Makefile index 6a3f718d5..65c559bd5 100644 --- a/helm/hbugs/tutors/Makefile +++ b/helm/hbugs/tutors/Makefile @@ -16,7 +16,7 @@ BUILD_TUTORS = ./build_tutors.ml CTL = ./sabba.sh TUTORS_OPT = $(patsubst %,%.opt,$(TUTORS)) GENERATED_TUTORS_SRC = $(patsubst %,%.ml,$(GENERATED_TUTORS)) -COMMON = hbugs_tutors_common.cmo +COMMON = hbugs_deity.cmo hbugs_tutors_common.cmo COMMON_OPT = $(patsubst %.cmo,%.cmx,$(COMMON)) all: byte @@ -35,11 +35,11 @@ $(GENERATED_TUTORS_SRC): $(TUTORS_TEMPLATE) $(TUTORS_INDEX) %_tutor.opt: $(COMMON_OPT) %_tutor.ml $(OCAMLOPT) $(LINK_OPTIONS) -o $@ $^ -hbugs_tutors_common.cmi: hbugs_tutors_common.mli +%.cmi: %.mli $(OCAMLC) -c $< -$(COMMON): hbugs_tutors_common.ml hbugs_tutors_common.cmi +%.cmo: %.ml %.cmi $(OCAMLC) -c $< -$(COMMON_OPT): hbugs_tutors_common.ml +%.cmx: %.ml %.cmi $(OCAMLOPT) -c $< clean: diff --git a/helm/hbugs/tutors/hbugs_deity.ml b/helm/hbugs/tutors/hbugs_deity.ml new file mode 100644 index 000000000..ba6caa478 --- /dev/null +++ b/helm/hbugs/tutors/hbugs_deity.ml @@ -0,0 +1,101 @@ +(* + * Copyright (C) 2003: + * Stefano Zacchiroli + * for the HELM Team http://helm.cs.unibo.it/ + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +exception Can_t_kill of int * string ;; (* pid, reason *) + + (* perform an action inside a critical section controlled by given mutex *) +let do_critical mutex = + fun action -> + try + Mutex.lock mutex; + let res = Lazy.force action in + 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 () + | _ -> ()))) +;; + + (* 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 + parent over "chan" *) +let wrap_thread body = + fun arg -> + ignore (Unix.sigprocmask Unix.SIG_UNBLOCK [ kill_signal ]); + Event.sync (Event.send chan (Unix.getpid ())); + body arg +;; + +let creation_mutex = Mutex.create () ;; + +let create body arg = + do_critical creation_mutex (lazy ( + ignore (Thread.create (wrap_thread body) arg); + Event.sync (Event.receive chan) + )) +;; +let kill pid = + add_to_dead_threads_walking pid; + try + Unix.kill pid kill_signal + with e -> raise (Can_t_kill (pid, Printexc.to_string e)) +;; + + (* block kill signal in main process *) +ignore (Unix.sigprocmask Unix.SIG_BLOCK [ kill_signal ]) ;; + diff --git a/helm/hbugs/tutors/hbugs_deity.mli b/helm/hbugs/tutors/hbugs_deity.mli new file mode 100644 index 000000000..f5f3dd5a4 --- /dev/null +++ b/helm/hbugs/tutors/hbugs_deity.mli @@ -0,0 +1,33 @@ +(* + * Copyright (C) 2003: + * Stefano Zacchiroli + * for the HELM Team http://helm.cs.unibo.it/ + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +exception Can_t_kill of int * string + +val create: ('a -> 'b) -> 'a -> int +val kill: int -> unit + diff --git a/helm/hbugs/tutors/hbugs_tutors_common.ml b/helm/hbugs/tutors/hbugs_tutors_common.ml index f00b17bc0..ca3de9fed 100644 --- a/helm/hbugs/tutors/hbugs_tutors_common.ml +++ b/helm/hbugs/tutors/hbugs_tutors_common.ml @@ -171,24 +171,41 @@ module BuildTutor (Dsc: HbugsTutorDescription) : HbugsTutor = (sprintf "Bye, I've completed my duties (success = %b)" success) let hbugs_callback = + (* hashtbl mapping musings ids to PID of threads doing the related (dirty) + work *) + let slaves = Hashtbl.create 17 in let forbidden () = prerr_endline "ignoring request from unauthorized broker"; Exception ("forbidden", "") in - function + function (* _the_ callback *) | Start_musing (broker_id, state) -> if is_authenticated broker_id then begin prerr_endline "received Start_musing"; let new_musing_id = Hbugs_id_generator.new_musing_id () in prerr_endline (sprintf "starting a new musing (id = %s)" new_musing_id); - ignore (Thread.create slave (state, new_musing_id)); +(* let slave_thread = Thread.create slave (state, new_musing_id) in *) + let slave_thread = + Hbugs_deity.create slave (state, new_musing_id) + in + Hashtbl.add slaves new_musing_id slave_thread; Musing_started (my_own_id, new_musing_id) end else (* broker unauthorized *) forbidden (); | Abort_musing (broker_id, musing_id) -> if is_authenticated broker_id then begin - prerr_endline "Ignoring 'Abort_musing' message ..."; + (try (* kill thread responsible for "musing_id" *) + let slave_thread = Hashtbl.find slaves musing_id in + 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) + | Not_found -> + prerr_endline (sprintf + "Can't find slave corresponding to musing %s, can't kill it" + musing_id)); Musing_aborted (my_own_id, musing_id) end else (* broker unauthorized *) forbidden ();