--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML Tue Jul 24 19:44:32 2007 +0200
@@ -0,0 +1,55 @@
+(* 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;