src/Pure/RAW/multithreading.ML
author wenzelm
Thu, 03 Mar 2016 11:12:02 +0100
changeset 62501 98fa1f9a292f
parent 62359 6709e51d5c11
permissions -rw-r--r--
discontinued polyml-5.3.0;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
61925
ab52f183f020 clarified directory structure;
wenzelm
parents: 59180
diff changeset
     1
(*  Title:      Pure/RAW/multithreading.ML
24690
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
     3
62359
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
     4
Multithreading in Poly/ML (cf. polyml/basis/Thread.sml).
24690
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
     5
*)
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
     6
62359
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
     7
signature BASIC_MULTITHREADING =
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
     8
sig
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
     9
  val interruptible: ('a -> 'b) -> 'a -> 'b
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    10
  val uninterruptible: ((('c -> 'd) -> 'c -> 'd) -> 'a -> 'b) -> 'a -> 'b
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    11
end;
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    12
24690
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
    13
signature MULTITHREADING =
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
    14
sig
62359
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    15
  include BASIC_MULTITHREADING
28149
26bd1245a46b added no_interrupts;
wenzelm
parents: 28123
diff changeset
    16
  val no_interrupts: Thread.threadAttribute list
32295
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
    17
  val public_interrupts: Thread.threadAttribute list
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
    18
  val private_interrupts: Thread.threadAttribute list
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
    19
  val sync_interrupts: Thread.threadAttribute list -> Thread.threadAttribute list
41713
a21084741b37 added Multithreading.interrupted (cf. java.lang.Thread.interrupted);
wenzelm
parents: 39616
diff changeset
    20
  val interrupted: unit -> unit  (*exception Interrupt*)
32295
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
    21
  val with_attributes: Thread.threadAttribute list -> (Thread.threadAttribute list -> 'a) -> 'a
62359
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    22
  val max_threads_value: unit -> int
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    23
  val max_threads_update: int -> unit
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    24
  val max_threads_setmp: int -> ('a -> 'b) -> 'a -> 'b
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    25
  val enabled: unit -> bool
32295
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
    26
  val sync_wait: Thread.threadAttribute list option -> Time.time option ->
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
    27
    ConditionVar.conditionVar -> Mutex.mutex -> bool Exn.result
39616
8052101883c3 renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents: 32777
diff changeset
    28
  val trace: int ref
32295
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
    29
  val tracing: int -> (unit -> string) -> unit
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
    30
  val tracing_time: bool -> Time.time -> (unit -> string) -> unit
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
    31
  val real_time: ('a -> unit) -> 'a -> Time.time
59054
61b723761dff load simple_thread.ML later, such that it benefits from redefined print_exception_trace;
wenzelm
parents: 54717
diff changeset
    32
  val synchronized: string -> Mutex.mutex -> (unit -> 'a) -> 'a
25704
df9c8074ff09 signature BASIC_MULTITHREADING;
wenzelm
parents: 24690
diff changeset
    33
  val serial: unit -> int
24690
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
    34
end;
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
    35
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
    36
structure Multithreading: MULTITHREADING =
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
    37
struct
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
    38
62359
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    39
(* thread attributes *)
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    40
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    41
val no_interrupts =
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    42
  [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptDefer];
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    43
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    44
val test_interrupts =
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    45
  [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptSynch];
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    46
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    47
val public_interrupts =
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    48
  [Thread.EnableBroadcastInterrupt true, Thread.InterruptState Thread.InterruptAsynchOnce];
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    49
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    50
val private_interrupts =
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    51
  [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptAsynchOnce];
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    52
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    53
val sync_interrupts = map
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    54
  (fn x as Thread.InterruptState Thread.InterruptDefer => x
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    55
    | Thread.InterruptState _ => Thread.InterruptState Thread.InterruptSynch
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    56
    | x => x);
24690
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
    57
62359
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    58
val safe_interrupts = map
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    59
  (fn Thread.InterruptState Thread.InterruptAsynch =>
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    60
      Thread.InterruptState Thread.InterruptAsynchOnce
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    61
    | x => x);
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    62
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    63
fun interrupted () =
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    64
  let
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    65
    val orig_atts = safe_interrupts (Thread.getAttributes ());
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    66
    val _ = Thread.setAttributes test_interrupts;
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    67
    val test = Exn.capture Thread.testInterrupt ();
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    68
    val _ = Thread.setAttributes orig_atts;
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    69
  in Exn.release test end;
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    70
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    71
fun with_attributes new_atts e =
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    72
  let
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    73
    val orig_atts = safe_interrupts (Thread.getAttributes ());
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    74
    val result = Exn.capture (fn () =>
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    75
      (Thread.setAttributes (safe_interrupts new_atts); e orig_atts)) ();
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    76
    val _ = Thread.setAttributes orig_atts;
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    77
  in Exn.release result end;
24690
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
    78
32286
1fb5db48002d added Multithreading.sync_wait, which turns enabled interrupts to sync ones, to ensure that wait will reaquire its lock when interrupted;
wenzelm
parents: 32186
diff changeset
    79
62359
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    80
(* portable wrappers *)
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    81
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    82
fun interruptible f x = with_attributes public_interrupts (fn _ => f x);
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    83
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    84
fun uninterruptible f x =
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    85
  with_attributes no_interrupts (fn atts =>
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    86
    f (fn g => fn y => with_attributes atts (fn _ => g y)) x);
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    87
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    88
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    89
(* options *)
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    90
62501
98fa1f9a292f discontinued polyml-5.3.0;
wenzelm
parents: 62359
diff changeset
    91
fun num_processors () =
98fa1f9a292f discontinued polyml-5.3.0;
wenzelm
parents: 62359
diff changeset
    92
  (case Thread.numPhysicalProcessors () of
98fa1f9a292f discontinued polyml-5.3.0;
wenzelm
parents: 62359
diff changeset
    93
    SOME n => n
98fa1f9a292f discontinued polyml-5.3.0;
wenzelm
parents: 62359
diff changeset
    94
  | NONE => Thread.numProcessors ());
98fa1f9a292f discontinued polyml-5.3.0;
wenzelm
parents: 62359
diff changeset
    95
62359
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    96
fun max_threads_result m =
62501
98fa1f9a292f discontinued polyml-5.3.0;
wenzelm
parents: 62359
diff changeset
    97
  if m > 0 then m else Int.min (Int.max (num_processors (), 1), 8);
62359
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    98
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    99
val max_threads = ref 1;
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   100
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   101
fun max_threads_value () = ! max_threads;
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   102
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   103
fun max_threads_update m = max_threads := max_threads_result m;
32286
1fb5db48002d added Multithreading.sync_wait, which turns enabled interrupts to sync ones, to ensure that wait will reaquire its lock when interrupted;
wenzelm
parents: 32186
diff changeset
   104
62359
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   105
fun max_threads_setmp m f x =
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   106
  uninterruptible (fn restore_attributes => fn () =>
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   107
    let
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   108
      val max_threads_orig = ! max_threads;
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   109
      val _ = max_threads_update m;
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   110
      val result = Exn.capture (restore_attributes f) x;
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   111
      val _ = max_threads := max_threads_orig;
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   112
    in Exn.release result end) ();
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   113
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   114
fun enabled () = max_threads_value () > 1;
28187
4062882c7df3 proper values of no_interrupts, regular_interrupts;
wenzelm
parents: 28169
diff changeset
   115
62359
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   116
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   117
(* synchronous wait *)
41713
a21084741b37 added Multithreading.interrupted (cf. java.lang.Thread.interrupted);
wenzelm
parents: 39616
diff changeset
   118
62359
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   119
fun sync_wait opt_atts time cond lock =
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   120
  with_attributes
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   121
    (sync_interrupts (case opt_atts of SOME atts => atts | NONE => Thread.getAttributes ()))
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   122
    (fn _ =>
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   123
      (case time of
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   124
        SOME t => Exn.Res (ConditionVar.waitUntil (cond, lock, t))
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   125
      | NONE => (ConditionVar.wait (cond, lock); Exn.Res true))
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   126
      handle exn => Exn.Exn exn);
32295
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
   127
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
   128
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
   129
(* tracing *)
30612
cb6421b6a18f future_job: do not inherit attributes, but enforce restricted interrupts -- attempt to prevent interrupt race conditions;
wenzelm
parents: 29564
diff changeset
   130
62359
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   131
val trace = ref 0;
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   132
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   133
fun tracing level msg =
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   134
  if level > ! trace then ()
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   135
  else uninterruptible (fn _ => fn () =>
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   136
    (TextIO.output (TextIO.stdErr, (">>> " ^ msg () ^ "\n")); TextIO.flushOut TextIO.stdErr)
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   137
      handle _ (*sic*) => ()) ();
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   138
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   139
fun tracing_time detailed time =
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   140
  tracing
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   141
   (if not detailed then 5
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   142
    else if Time.>= (time, seconds 1.0) then 1
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   143
    else if Time.>= (time, seconds 0.1) then 2
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   144
    else if Time.>= (time, seconds 0.01) then 3
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   145
    else if Time.>= (time, seconds 0.001) then 4 else 5);
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   146
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   147
fun real_time f x =
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   148
  let
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   149
    val timer = Timer.startRealTimer ();
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   150
    val () = f x;
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   151
    val time = Timer.checkRealTimer timer;
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   152
  in time end;
32286
1fb5db48002d added Multithreading.sync_wait, which turns enabled interrupts to sync ones, to ensure that wait will reaquire its lock when interrupted;
wenzelm
parents: 32186
diff changeset
   153
25735
4d147263f71f added get/put_data;
wenzelm
parents: 25704
diff changeset
   154
59180
c0fa3b3bdabd discontinued central critical sections: NAMED_CRITICAL / CRITICAL;
wenzelm
parents: 59054
diff changeset
   155
(* synchronized evaluation *)
24690
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
   156
62359
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   157
fun synchronized name lock e =
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   158
  Exn.release (uninterruptible (fn restore_attributes => fn () =>
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   159
    let
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   160
      val immediate =
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   161
        if Mutex.trylock lock then true
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   162
        else
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   163
          let
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   164
            val _ = tracing 5 (fn () => name ^ ": locking ...");
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   165
            val time = real_time Mutex.lock lock;
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   166
            val _ = tracing_time true time (fn () => name ^ ": locked after " ^ Time.toString time);
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   167
          in false end;
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   168
      val result = Exn.capture (restore_attributes e) ();
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   169
      val _ = if immediate then () else tracing 5 (fn () => name ^ ": unlocking ...");
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   170
      val _ = Mutex.unlock lock;
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   171
    in result end) ());
59054
61b723761dff load simple_thread.ML later, such that it benefits from redefined print_exception_trace;
wenzelm
parents: 54717
diff changeset
   172
25735
4d147263f71f added get/put_data;
wenzelm
parents: 25704
diff changeset
   173
4d147263f71f added get/put_data;
wenzelm
parents: 25704
diff changeset
   174
(* serial numbers *)
4d147263f71f added get/put_data;
wenzelm
parents: 25704
diff changeset
   175
62359
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   176
local
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   177
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   178
val serial_lock = Mutex.mutex ();
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   179
val serial_count = ref 0;
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   180
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   181
in
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   182
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   183
val serial = uninterruptible (fn _ => fn () =>
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   184
  let
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   185
    val _ = Mutex.lock serial_lock;
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   186
    val _ = serial_count := ! serial_count + 1;
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   187
    val res = ! serial_count;
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   188
    val _ = Mutex.unlock serial_lock;
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   189
  in res end);
25704
df9c8074ff09 signature BASIC_MULTITHREADING;
wenzelm
parents: 24690
diff changeset
   190
28123
53cd972d7db9 provide dummy thread structures, including proper Thread.getLocal/setLocal;
wenzelm
parents: 26082
diff changeset
   191
end;
53cd972d7db9 provide dummy thread structures, including proper Thread.getLocal/setLocal;
wenzelm
parents: 26082
diff changeset
   192
62359
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   193
end;
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   194
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   195
structure Basic_Multithreading: BASIC_MULTITHREADING = Multithreading;
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   196
open Basic_Multithreading;