(* * 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 () ;; (* 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 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)) ;; *) (* FAKE IMPLEMENTATION *) let create x y = let _ = Thread.create x y in ~-1 ;; let kill _ = () ;; (* block kill signal in main process *) ignore (Unix.sigprocmask Unix.SIG_BLOCK [ kill_signal ]) ;;