Multithreading in Poly/ML (version 5.1).
(* Title: Pure/ML-Systems/multithreading_polyml.ML
ID: $Id$
Author: Makarius
Multithreading in Poly/ML (version 5.1).
*)
open Thread;
structure Multithreading: MULTITHREADING =
struct
val number_of_threads = ref 0;
(* FIXME tmp *)
fun message s =
(TextIO.output (TextIO.stdErr, (">>> " ^ s ^ "\n")); TextIO.flushOut TextIO.stdErr);
(* critical section -- may be nested within the same thread *)
local
val critical_lock = Mutex.mutex ();
val critical_thread = ref (NONE: Thread.thread option);
in
fun self_critical () =
(case ! critical_thread of
NONE => false
| SOME id => Thread.equal (id, Thread.self ()));
fun CRITICAL e =
if self_critical () then e ()
else
let
val _ =
if Mutex.trylock critical_lock then ()
else
(message "Waiting for critical lock";
Mutex.lock critical_lock;
message "Obtained critical lock");
val _ = critical_thread := SOME (Thread.self ());
val result = Exn.capture e ();
val _ = critical_thread := NONE;
val _ = Mutex.unlock critical_lock;
in Exn.release result end;
end;
end;
val CRITICAL = Multithreading.CRITICAL;