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