*.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
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
%_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:
--- /dev/null
+(*
+ * Copyright (C) 2003:
+ * Stefano Zacchiroli <zack@cs.unibo.it>
+ * 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 ]) ;;
+
--- /dev/null
+(*
+ * Copyright (C) 2003:
+ * Stefano Zacchiroli <zack@cs.unibo.it>
+ * 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
+
(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 ();
projects / helm.git / commitdiff