+(*
+ * 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 ]) ;;
+