src/Pure/Concurrent/multithreading.ML
author wenzelm
Sat, 09 Apr 2016 14:17:50 +0200
changeset 62925 f1bdf10f95d8
parent 62924 ce47945ce4fb
child 62926 9ff9bcbc2341
permissions -rw-r--r--
tuned signature;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
62508
d0b68218ea55 discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents: 62501
diff changeset
     1
(*  Title:      Pure/Concurrent/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
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
     7
signature MULTITHREADING =
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
     8
sig
62925
f1bdf10f95d8 tuned signature;
wenzelm
parents: 62924
diff changeset
     9
  val max_threads: unit -> int
62359
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    10
  val max_threads_update: int -> unit
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    11
  val enabled: unit -> bool
32295
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
    12
  val sync_wait: Thread.threadAttribute list option -> Time.time option ->
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
    13
    ConditionVar.conditionVar -> Mutex.mutex -> bool Exn.result
39616
8052101883c3 renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents: 32777
diff changeset
    14
  val trace: int ref
32295
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
    15
  val tracing: int -> (unit -> string) -> unit
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
    16
  val tracing_time: bool -> Time.time -> (unit -> string) -> unit
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
    17
  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
    18
  val synchronized: string -> Mutex.mutex -> (unit -> 'a) -> 'a
24690
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
    19
end;
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
    20
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
    21
structure Multithreading: MULTITHREADING =
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
    22
struct
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
    23
62925
f1bdf10f95d8 tuned signature;
wenzelm
parents: 62924
diff changeset
    24
(* max_threads *)
f1bdf10f95d8 tuned signature;
wenzelm
parents: 62924
diff changeset
    25
f1bdf10f95d8 tuned signature;
wenzelm
parents: 62924
diff changeset
    26
local
62359
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    27
62501
98fa1f9a292f discontinued polyml-5.3.0;
wenzelm
parents: 62359
diff changeset
    28
fun num_processors () =
98fa1f9a292f discontinued polyml-5.3.0;
wenzelm
parents: 62359
diff changeset
    29
  (case Thread.numPhysicalProcessors () of
98fa1f9a292f discontinued polyml-5.3.0;
wenzelm
parents: 62359
diff changeset
    30
    SOME n => n
98fa1f9a292f discontinued polyml-5.3.0;
wenzelm
parents: 62359
diff changeset
    31
  | NONE => Thread.numProcessors ());
98fa1f9a292f discontinued polyml-5.3.0;
wenzelm
parents: 62359
diff changeset
    32
62359
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    33
fun max_threads_result m =
62501
98fa1f9a292f discontinued polyml-5.3.0;
wenzelm
parents: 62359
diff changeset
    34
  if m > 0 then m else Int.min (Int.max (num_processors (), 1), 8);
62359
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    35
62925
f1bdf10f95d8 tuned signature;
wenzelm
parents: 62924
diff changeset
    36
val max_threads_state = ref 1;
f1bdf10f95d8 tuned signature;
wenzelm
parents: 62924
diff changeset
    37
f1bdf10f95d8 tuned signature;
wenzelm
parents: 62924
diff changeset
    38
in
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
    39
62925
f1bdf10f95d8 tuned signature;
wenzelm
parents: 62924
diff changeset
    40
fun max_threads () = ! max_threads_state;
f1bdf10f95d8 tuned signature;
wenzelm
parents: 62924
diff changeset
    41
fun max_threads_update m = max_threads_state := max_threads_result m;
f1bdf10f95d8 tuned signature;
wenzelm
parents: 62924
diff changeset
    42
fun enabled () = max_threads () > 1;
f1bdf10f95d8 tuned signature;
wenzelm
parents: 62924
diff changeset
    43
f1bdf10f95d8 tuned signature;
wenzelm
parents: 62924
diff changeset
    44
end;
28187
4062882c7df3 proper values of no_interrupts, regular_interrupts;
wenzelm
parents: 28169
diff changeset
    45
62359
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    46
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    47
(* synchronous wait *)
41713
a21084741b37 added Multithreading.interrupted (cf. java.lang.Thread.interrupted);
wenzelm
parents: 39616
diff changeset
    48
62359
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    49
fun sync_wait opt_atts time cond lock =
62923
3a122e1e352a clarified bootstrap;
wenzelm
parents: 62918
diff changeset
    50
  Thread_Attributes.with_attributes
3a122e1e352a clarified bootstrap;
wenzelm
parents: 62918
diff changeset
    51
    (Thread_Attributes.sync_interrupts
3a122e1e352a clarified bootstrap;
wenzelm
parents: 62918
diff changeset
    52
      (case opt_atts of SOME atts => atts | NONE => Thread.getAttributes ()))
62359
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    53
    (fn _ =>
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    54
      (case time of
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    55
        SOME t => Exn.Res (ConditionVar.waitUntil (cond, lock, t))
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    56
      | NONE => (ConditionVar.wait (cond, lock); Exn.Res true))
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    57
      handle exn => Exn.Exn exn);
32295
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
    58
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
    59
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
    60
(* tracing *)
30612
cb6421b6a18f future_job: do not inherit attributes, but enforce restricted interrupts -- attempt to prevent interrupt race conditions;
wenzelm
parents: 29564
diff changeset
    61
62359
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    62
val trace = ref 0;
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    63
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    64
fun tracing level msg =
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    65
  if level > ! trace then ()
62923
3a122e1e352a clarified bootstrap;
wenzelm
parents: 62918
diff changeset
    66
  else Thread_Attributes.uninterruptible (fn _ => fn () =>
62359
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    67
    (TextIO.output (TextIO.stdErr, (">>> " ^ msg () ^ "\n")); TextIO.flushOut TextIO.stdErr)
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    68
      handle _ (*sic*) => ()) ();
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    69
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    70
fun tracing_time detailed time =
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    71
  tracing
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    72
   (if not detailed then 5
62826
eb94e570c1a4 prefer infix operations;
wenzelm
parents: 62715
diff changeset
    73
    else if time >= seconds 1.0 then 1
eb94e570c1a4 prefer infix operations;
wenzelm
parents: 62715
diff changeset
    74
    else if time >= seconds 0.1 then 2
eb94e570c1a4 prefer infix operations;
wenzelm
parents: 62715
diff changeset
    75
    else if time >= seconds 0.01 then 3
eb94e570c1a4 prefer infix operations;
wenzelm
parents: 62715
diff changeset
    76
    else if time >= seconds 0.001 then 4 else 5);
62359
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    77
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    78
fun real_time f x =
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    79
  let
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    80
    val timer = Timer.startRealTimer ();
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    81
    val () = f x;
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    82
    val time = Timer.checkRealTimer timer;
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    83
  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
    84
25735
4d147263f71f added get/put_data;
wenzelm
parents: 25704
diff changeset
    85
59180
c0fa3b3bdabd discontinued central critical sections: NAMED_CRITICAL / CRITICAL;
wenzelm
parents: 59054
diff changeset
    86
(* synchronized evaluation *)
24690
c661dae1070a renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
wenzelm
parents:
diff changeset
    87
62359
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    88
fun synchronized name lock e =
62923
3a122e1e352a clarified bootstrap;
wenzelm
parents: 62918
diff changeset
    89
  Exn.release (Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
62359
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    90
    let
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    91
      val immediate =
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    92
        if Mutex.trylock lock then true
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    93
        else
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    94
          let
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    95
            val _ = tracing 5 (fn () => name ^ ": locking ...");
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    96
            val time = real_time Mutex.lock lock;
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    97
            val _ = tracing_time true time (fn () => name ^ ": locked after " ^ Time.toString time);
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    98
          in false end;
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
    99
      val result = Exn.capture (restore_attributes e) ();
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   100
      val _ = if immediate then () else tracing 5 (fn () => name ^ ": unlocking ...");
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   101
      val _ = Mutex.unlock lock;
6709e51d5c11 unconditional Multithreading;
wenzelm
parents: 61925
diff changeset
   102
    in result end) ());
59054
61b723761dff load simple_thread.ML later, such that it benefits from redefined print_exception_trace;
wenzelm
parents: 54717
diff changeset
   103
28123
53cd972d7db9 provide dummy thread structures, including proper Thread.getLocal/setLocal;
wenzelm
parents: 26082
diff changeset
   104
end;