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