src/Pure/ML-Systems/multithreading_polyml.ML
author wenzelm
Tue, 24 Jul 2007 19:44:32 +0200
changeset 23961 9e7e1e309ebd
child 23973 b6ce6de5b700
permissions -rw-r--r--
Multithreading in Poly/ML (version 5.1).
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
23961
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/ML-Systems/multithreading_polyml.ML
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
     3
    Author:     Makarius
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
     4
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
     5
Multithreading in Poly/ML (version 5.1).
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
     6
*)
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
     7
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
     8
open Thread;
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
     9
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
    10
structure Multithreading: MULTITHREADING =
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
    11
struct
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
    12
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
    13
val number_of_threads = ref 0;
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
    14
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
    15
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
    16
(* FIXME tmp *)
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
    17
fun message s =
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
    18
  (TextIO.output (TextIO.stdErr, (">>> " ^ s ^ "\n")); TextIO.flushOut TextIO.stdErr);
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
    19
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
    20
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
    21
(* critical section -- may be nested within the same thread *)
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
    22
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
    23
local
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
    24
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
    25
val critical_lock = Mutex.mutex ();
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
    26
val critical_thread = ref (NONE: Thread.thread option);
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
    27
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
    28
in
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
    29
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
    30
fun self_critical () =
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
    31
  (case ! critical_thread of
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
    32
    NONE => false
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
    33
  | SOME id => Thread.equal (id, Thread.self ()));
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
    34
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
    35
fun CRITICAL e =
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
    36
  if self_critical () then e ()
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
    37
  else
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
    38
    let
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
    39
      val _ =
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
    40
        if Mutex.trylock critical_lock then ()
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
    41
        else
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
    42
          (message "Waiting for critical lock";
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
    43
           Mutex.lock critical_lock;
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
    44
           message "Obtained critical lock");
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
    45
      val _ = critical_thread := SOME (Thread.self ());
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
    46
      val result = Exn.capture e ();
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
    47
      val _ = critical_thread := NONE;
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
    48
      val _ = Mutex.unlock critical_lock;
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
    49
    in Exn.release result end;
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
    50
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
    51
end;
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
    52
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
    53
end;
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
    54
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
    55
val CRITICAL = Multithreading.CRITICAL;