From: Stefano Zacchiroli Date: Mon, 19 Apr 2004 12:05:30 +0000 (+0000) Subject: added ExtThread module, ex Hbugs_deity (a Thread module with killing X-Git-Tag: dead_dir_walking~41 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=be4d9c44f4d9df070339da40aa82c8cb0cc6467c added ExtThread module, ex Hbugs_deity (a Thread module with killing capabilities) --- diff --git a/helm/ocaml/thread/.depend b/helm/ocaml/thread/.depend index 8838cb307..7759190c6 100644 --- a/helm/ocaml/thread/.depend +++ b/helm/ocaml/thread/.depend @@ -1,2 +1,4 @@ threadSafe.cmo: threadSafe.cmi threadSafe.cmx: threadSafe.cmi +extThread.cmo: extThread.cmi +extThread.cmx: extThread.cmi diff --git a/helm/ocaml/thread/Makefile b/helm/ocaml/thread/Makefile index 6a5dd3d84..9818e9a0e 100644 --- a/helm/ocaml/thread/Makefile +++ b/helm/ocaml/thread/Makefile @@ -1,7 +1,7 @@ PACKAGE = thread REQUIRES = threads -INTERFACE_FILES = threadSafe.mli +INTERFACE_FILES = threadSafe.mli extThread.mli IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) include ../Makefile.common diff --git a/helm/ocaml/thread/extThread.ml b/helm/ocaml/thread/extThread.ml new file mode 100644 index 000000000..1b34e09c7 --- /dev/null +++ b/helm/ocaml/thread/extThread.ml @@ -0,0 +1,108 @@ +(* + * Copyright (C) 2003-2004: + * 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/ + *) + +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 = + 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 *) +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 + 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 + +(* +(* FAKE IMPLEMENTATION *) +let create = Thread.create +let kill _ = () +*) + +let create body arg = + do_critical creation_mutex (lazy ( + 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 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 (thread_t, Printexc.to_string e)) + + (* "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 *) +let _ = ignore (Unix.sigprocmask Unix.SIG_BLOCK [ kill_signal ]) + diff --git a/helm/ocaml/thread/extThread.mli b/helm/ocaml/thread/extThread.mli new file mode 100644 index 000000000..5fb3bd487 --- /dev/null +++ b/helm/ocaml/thread/extThread.mli @@ -0,0 +1,35 @@ +(* + * 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/ + *) + +(** {2 Extended Thread module with killing capabilities} *) + +exception Can_t_kill of Thread.t * string + +val create: ('a -> 'b) -> 'a -> Thread.t +val kill: Thread.t -> unit +