added proper implementation of self_critical, CRITICAL;
authorwenzelm
Mon Jul 23 22:18:05 2007 +0200 (2007-07-23)
changeset 239475e396bcf749e
parent 23946 4fbb1ff12337
child 23948 261bd4678076
added proper implementation of self_critical, CRITICAL;
src/Pure/ML-Systems/polyml-5.1.ML
     1.1 --- a/src/Pure/ML-Systems/polyml-5.1.ML	Mon Jul 23 22:18:03 2007 +0200
     1.2 +++ b/src/Pure/ML-Systems/polyml-5.1.ML	Mon Jul 23 22:18:05 2007 +0200
     1.3 @@ -39,3 +39,54 @@
     1.4      val instream = TextIO.openIn name;
     1.5      val txt = TextIO.inputAll instream before TextIO.closeIn instream;
     1.6    in use_text name output verbose txt end;
     1.7 +
     1.8 +
     1.9 +
    1.10 +(** multithreading **)
    1.11 +
    1.12 +open Thread;
    1.13 +
    1.14 +local
    1.15 +
    1.16 +datatype 'a result =
    1.17 +  Result of 'a |
    1.18 +  Exn of exn;
    1.19 +
    1.20 +fun capture f x = Result (f x) handle e => Exn e;
    1.21 +
    1.22 +fun release (Result y) = y
    1.23 +  | release (Exn e) = raise e;
    1.24 +
    1.25 +fun message s =
    1.26 +  (TextIO.output (TextIO.stdErr, (">>> " ^ s ^ "\n")); TextIO.flushOut TextIO.stdErr);
    1.27 +
    1.28 +
    1.29 +val critical_lock = Mutex.mutex ();
    1.30 +val critical_thread = ref (NONE: Thread.thread option);
    1.31 +
    1.32 +in
    1.33 +
    1.34 +(* critical section -- may be nested within the same thread *)
    1.35 +
    1.36 +fun self_critical () =
    1.37 +  (case ! critical_thread of
    1.38 +    NONE => false
    1.39 +  | SOME id => Thread.equal (id, Thread.self ()));
    1.40 +
    1.41 +fun CRITICAL e =
    1.42 +  if self_critical () then e ()
    1.43 +  else
    1.44 +    let
    1.45 +      val _ =
    1.46 +        if Mutex.trylock critical_lock then ()
    1.47 +        else
    1.48 +          (message "Waiting for critical lock";
    1.49 +           Mutex.lock critical_lock;
    1.50 +           message "Obtained critical lock");
    1.51 +      val _ = critical_thread := SOME (Thread.self ());
    1.52 +      val res = capture e ();
    1.53 +      val _ = critical_thread := NONE;
    1.54 +      val _ = Mutex.unlock critical_lock;
    1.55 +    in release res end;
    1.56 +
    1.57 +end;