Multithreading in Poly/ML (version 5.1).
authorwenzelm
Tue Jul 24 19:44:32 2007 +0200 (2007-07-24)
changeset 239619e7e1e309ebd
parent 23960 c07ae96cbfc4
child 23962 e0358fac0541
Multithreading in Poly/ML (version 5.1).
src/Pure/ML-Systems/multithreading_polyml.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Tue Jul 24 19:44:32 2007 +0200
     1.3 @@ -0,0 +1,55 @@
     1.4 +(*  Title:      Pure/ML-Systems/multithreading_polyml.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Makarius
     1.7 +
     1.8 +Multithreading in Poly/ML (version 5.1).
     1.9 +*)
    1.10 +
    1.11 +open Thread;
    1.12 +
    1.13 +structure Multithreading: MULTITHREADING =
    1.14 +struct
    1.15 +
    1.16 +val number_of_threads = ref 0;
    1.17 +
    1.18 +
    1.19 +(* FIXME tmp *)
    1.20 +fun message s =
    1.21 +  (TextIO.output (TextIO.stdErr, (">>> " ^ s ^ "\n")); TextIO.flushOut TextIO.stdErr);
    1.22 +
    1.23 +
    1.24 +(* critical section -- may be nested within the same thread *)
    1.25 +
    1.26 +local
    1.27 +
    1.28 +val critical_lock = Mutex.mutex ();
    1.29 +val critical_thread = ref (NONE: Thread.thread option);
    1.30 +
    1.31 +in
    1.32 +
    1.33 +fun self_critical () =
    1.34 +  (case ! critical_thread of
    1.35 +    NONE => false
    1.36 +  | SOME id => Thread.equal (id, Thread.self ()));
    1.37 +
    1.38 +fun CRITICAL e =
    1.39 +  if self_critical () then e ()
    1.40 +  else
    1.41 +    let
    1.42 +      val _ =
    1.43 +        if Mutex.trylock critical_lock then ()
    1.44 +        else
    1.45 +          (message "Waiting for critical lock";
    1.46 +           Mutex.lock critical_lock;
    1.47 +           message "Obtained critical lock");
    1.48 +      val _ = critical_thread := SOME (Thread.self ());
    1.49 +      val result = Exn.capture e ();
    1.50 +      val _ = critical_thread := NONE;
    1.51 +      val _ = Mutex.unlock critical_lock;
    1.52 +    in Exn.release result end;
    1.53 +
    1.54 +end;
    1.55 +
    1.56 +end;
    1.57 +
    1.58 +val CRITICAL = Multithreading.CRITICAL;