src/Pure/ML-Systems/multithreading_polyml.ML
author wenzelm
Wed, 22 Sep 2010 18:21:48 +0200
changeset 39616 8052101883c3
parent 39583 c1e9c6dfeff8
child 40301 bf39a257b3d3
permissions -rw-r--r--
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
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
    Author:     Makarius
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
     3
31311
b82e55f51dcc more precise version information;
wenzelm
parents: 30612
diff changeset
     4
Multithreading in Poly/ML 5.2.1 or later (cf. polyml/basis/Thread.sml).
23961
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
     5
*)
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
     6
25704
df9c8074ff09 signature BASIC_MULTITHREADING;
wenzelm
parents: 24688
diff changeset
     7
signature MULTITHREADING_POLYML =
df9c8074ff09 signature BASIC_MULTITHREADING;
wenzelm
parents: 24688
diff changeset
     8
sig
26083
abb3f8dd66dc removed managed_process (cf. General/shell_process.ML);
wenzelm
parents: 26074
diff changeset
     9
  val interruptible: ('a -> 'b) -> 'a -> 'b
abb3f8dd66dc removed managed_process (cf. General/shell_process.ML);
wenzelm
parents: 26074
diff changeset
    10
  val uninterruptible: ((('c -> 'd) -> 'c -> 'd) -> 'a -> 'b) -> 'a -> 'b
35010
d6e492cea6e4 renamed system/system_out to bash/bash_output -- to emphasized that this is really GNU bash, not some undefined POSIX sh;
wenzelm
parents: 33219
diff changeset
    11
  val bash_output: string -> string * int
25704
df9c8074ff09 signature BASIC_MULTITHREADING;
wenzelm
parents: 24688
diff changeset
    12
  structure TimeLimit: TIME_LIMIT
df9c8074ff09 signature BASIC_MULTITHREADING;
wenzelm
parents: 24688
diff changeset
    13
end;
df9c8074ff09 signature BASIC_MULTITHREADING;
wenzelm
parents: 24688
diff changeset
    14
df9c8074ff09 signature BASIC_MULTITHREADING;
wenzelm
parents: 24688
diff changeset
    15
signature BASIC_MULTITHREADING =
df9c8074ff09 signature BASIC_MULTITHREADING;
wenzelm
parents: 24688
diff changeset
    16
sig
df9c8074ff09 signature BASIC_MULTITHREADING;
wenzelm
parents: 24688
diff changeset
    17
  include BASIC_MULTITHREADING
df9c8074ff09 signature BASIC_MULTITHREADING;
wenzelm
parents: 24688
diff changeset
    18
  include MULTITHREADING_POLYML
df9c8074ff09 signature BASIC_MULTITHREADING;
wenzelm
parents: 24688
diff changeset
    19
end;
df9c8074ff09 signature BASIC_MULTITHREADING;
wenzelm
parents: 24688
diff changeset
    20
24208
f4cafbaa05e4 schedule: more precise task model;
wenzelm
parents: 24144
diff changeset
    21
signature MULTITHREADING =
f4cafbaa05e4 schedule: more precise task model;
wenzelm
parents: 24144
diff changeset
    22
sig
f4cafbaa05e4 schedule: more precise task model;
wenzelm
parents: 24144
diff changeset
    23
  include MULTITHREADING
25704
df9c8074ff09 signature BASIC_MULTITHREADING;
wenzelm
parents: 24688
diff changeset
    24
  include MULTITHREADING_POLYML
24208
f4cafbaa05e4 schedule: more precise task model;
wenzelm
parents: 24144
diff changeset
    25
end;
f4cafbaa05e4 schedule: more precise task model;
wenzelm
parents: 24144
diff changeset
    26
23961
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
    27
structure Multithreading: MULTITHREADING =
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
    28
struct
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
    29
32185
57ecfab3bcfe added Multithreading.real_time;
wenzelm
parents: 32184
diff changeset
    30
(* options *)
32184
cfa0ef0c0c5f simplified/unified Multithreading.tracing_time;
wenzelm
parents: 32107
diff changeset
    31
23981
03b71bf91318 added trace flag, official tracing operation;
wenzelm
parents: 23973
diff changeset
    32
val available = true;
25775
90525e67ede7 added Multithreading.max_threads_value, which maps a value of 0 to number of CPUs;
wenzelm
parents: 25735
diff changeset
    33
39616
8052101883c3 renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents: 39583
diff changeset
    34
val max_threads = ref 0;
23973
b6ce6de5b700 renamed number_of_threads to max_threads;
wenzelm
parents: 23961
diff changeset
    35
25775
90525e67ede7 added Multithreading.max_threads_value, which maps a value of 0 to number of CPUs;
wenzelm
parents: 25735
diff changeset
    36
fun max_threads_value () =
31630
2f8ed0dca3bd back to default -M max, with more robust interpretation of corresponding max_threads value;
wenzelm
parents: 31311
diff changeset
    37
  let val m = ! max_threads in
2f8ed0dca3bd back to default -M max, with more robust interpretation of corresponding max_threads value;
wenzelm
parents: 31311
diff changeset
    38
    if m > 0 then m
33180
e1b0280f0299 implicit default is 4 cores -- more cost-effective;
wenzelm
parents: 32738
diff changeset
    39
    else Int.min (Int.max (Thread.numProcessors (), 1), 4)
31630
2f8ed0dca3bd back to default -M max, with more robust interpretation of corresponding max_threads value;
wenzelm
parents: 31311
diff changeset
    40
  end;
25775
90525e67ede7 added Multithreading.max_threads_value, which maps a value of 0 to number of CPUs;
wenzelm
parents: 25735
diff changeset
    41
28555
d59712ee942c added enabled;
wenzelm
parents: 28466
diff changeset
    42
fun enabled () = max_threads_value () > 1;
d59712ee942c added enabled;
wenzelm
parents: 28466
diff changeset
    43
23973
b6ce6de5b700 renamed number_of_threads to max_threads;
wenzelm
parents: 23961
diff changeset
    44
24069
8a15a04e36f6 tuned msgs;
wenzelm
parents: 24066
diff changeset
    45
(* misc utils *)
8a15a04e36f6 tuned msgs;
wenzelm
parents: 24066
diff changeset
    46
24208
f4cafbaa05e4 schedule: more precise task model;
wenzelm
parents: 24144
diff changeset
    47
fun show "" = "" | show name = " " ^ name;
f4cafbaa05e4 schedule: more precise task model;
wenzelm
parents: 24144
diff changeset
    48
fun show' "" = "" | show' name = " [" ^ name ^ "]";
f4cafbaa05e4 schedule: more precise task model;
wenzelm
parents: 24144
diff changeset
    49
26098
b59d33f73aed added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents: 26083
diff changeset
    50
fun read_file name =
b59d33f73aed added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents: 26083
diff changeset
    51
  let val is = TextIO.openIn name
26504
6e87c0a60104 before close: Exn.capture/release;
wenzelm
parents: 26493
diff changeset
    52
  in Exn.release (Exn.capture TextIO.inputAll is before TextIO.closeIn is) end;
26098
b59d33f73aed added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents: 26083
diff changeset
    53
b59d33f73aed added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents: 26083
diff changeset
    54
fun write_file name txt =
b59d33f73aed added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents: 26083
diff changeset
    55
  let val os = TextIO.openOut name
26504
6e87c0a60104 before close: Exn.capture/release;
wenzelm
parents: 26493
diff changeset
    56
  in Exn.release (Exn.capture TextIO.output (os, txt) before TextIO.closeOut os) end;
26098
b59d33f73aed added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents: 26083
diff changeset
    57
24208
f4cafbaa05e4 schedule: more precise task model;
wenzelm
parents: 24144
diff changeset
    58
f4cafbaa05e4 schedule: more precise task model;
wenzelm
parents: 24144
diff changeset
    59
(* thread attributes *)
f4cafbaa05e4 schedule: more precise task model;
wenzelm
parents: 24144
diff changeset
    60
28161
7718587e510e added sync_interrupts, regular_interrupts;
wenzelm
parents: 28150
diff changeset
    61
val no_interrupts =
7718587e510e added sync_interrupts, regular_interrupts;
wenzelm
parents: 28150
diff changeset
    62
  [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptDefer];
7718587e510e added sync_interrupts, regular_interrupts;
wenzelm
parents: 28150
diff changeset
    63
32295
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
    64
val public_interrupts =
28161
7718587e510e added sync_interrupts, regular_interrupts;
wenzelm
parents: 28150
diff changeset
    65
  [Thread.EnableBroadcastInterrupt true, Thread.InterruptState Thread.InterruptAsynchOnce];
7718587e510e added sync_interrupts, regular_interrupts;
wenzelm
parents: 28150
diff changeset
    66
32295
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
    67
val private_interrupts =
30612
cb6421b6a18f future_job: do not inherit attributes, but enforce restricted interrupts -- attempt to prevent interrupt race conditions;
wenzelm
parents: 30602
diff changeset
    68
  [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptAsynchOnce];
cb6421b6a18f future_job: do not inherit attributes, but enforce restricted interrupts -- attempt to prevent interrupt race conditions;
wenzelm
parents: 30602
diff changeset
    69
32295
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
    70
val sync_interrupts = map
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
    71
  (fn x as Thread.InterruptState Thread.InterruptDefer => x
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
    72
    | Thread.InterruptState _ => Thread.InterruptState Thread.InterruptSynch
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
    73
    | x => x);
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
    74
28466
6e35fbfc32b8 with_attributes: enforces InterruptAsynch => InterruptAsynchOnce to avoid race condition;
wenzelm
parents: 28465
diff changeset
    75
val safe_interrupts = map
6e35fbfc32b8 with_attributes: enforces InterruptAsynch => InterruptAsynchOnce to avoid race condition;
wenzelm
parents: 28465
diff changeset
    76
  (fn Thread.InterruptState Thread.InterruptAsynch =>
6e35fbfc32b8 with_attributes: enforces InterruptAsynch => InterruptAsynchOnce to avoid race condition;
wenzelm
parents: 28465
diff changeset
    77
      Thread.InterruptState Thread.InterruptAsynchOnce
6e35fbfc32b8 with_attributes: enforces InterruptAsynch => InterruptAsynchOnce to avoid race condition;
wenzelm
parents: 28465
diff changeset
    78
    | x => x);
6e35fbfc32b8 with_attributes: enforces InterruptAsynch => InterruptAsynchOnce to avoid race condition;
wenzelm
parents: 28465
diff changeset
    79
32295
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
    80
fun with_attributes new_atts e =
24208
f4cafbaa05e4 schedule: more precise task model;
wenzelm
parents: 24144
diff changeset
    81
  let
29550
67ec51c032cb with_attributes: make double sure that unsafe attributes are avoided;
wenzelm
parents: 28555
diff changeset
    82
    val orig_atts = safe_interrupts (Thread.getAttributes ());
30602
1bd90b76477a with_attributes: canonical capture/release scheme (potentially iron out race condition);
wenzelm
parents: 29564
diff changeset
    83
    val result = Exn.capture (fn () =>
32295
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
    84
      (Thread.setAttributes (safe_interrupts new_atts); e orig_atts)) ();
30602
1bd90b76477a with_attributes: canonical capture/release scheme (potentially iron out race condition);
wenzelm
parents: 29564
diff changeset
    85
    val _ = Thread.setAttributes orig_atts;
28466
6e35fbfc32b8 with_attributes: enforces InterruptAsynch => InterruptAsynchOnce to avoid race condition;
wenzelm
parents: 28465
diff changeset
    86
  in Exn.release result end;
24208
f4cafbaa05e4 schedule: more precise task model;
wenzelm
parents: 24144
diff changeset
    87
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: 32230
diff changeset
    88
32295
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
    89
(* portable wrappers *)
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
    90
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
    91
fun interruptible f x = with_attributes public_interrupts (fn _ => f x);
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: 32230
diff changeset
    92
32295
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
    93
fun uninterruptible f x =
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
    94
  with_attributes no_interrupts (fn atts =>
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
    95
    f (fn g => fn y => with_attributes atts (fn _ => g y)) x);
24668
4058b7b0925c added interrupt_timeout;
wenzelm
parents: 24297
diff changeset
    96
24688
a5754ca5c510 replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);
wenzelm
parents: 24672
diff changeset
    97
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: 32230
diff changeset
    98
(* synchronous wait *)
1fb5db48002d added Multithreading.sync_wait, which turns enabled interrupts to sync ones, to ensure that wait will reaquire its lock when interrupted;
wenzelm
parents: 32230
diff changeset
    99
32295
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
   100
fun sync_wait opt_atts time cond lock =
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
   101
  with_attributes
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
   102
    (sync_interrupts (case opt_atts of SOME atts => atts | NONE => Thread.getAttributes ()))
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
   103
    (fn _ =>
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
   104
      (case time of
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
   105
        SOME t => Exn.Result (ConditionVar.waitUntil (cond, lock, t))
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
   106
      | NONE => (ConditionVar.wait (cond, lock); Exn.Result true))
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
   107
      handle exn => Exn.Exn exn);
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
   108
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
   109
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
   110
(* tracing *)
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
   111
39616
8052101883c3 renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents: 39583
diff changeset
   112
val trace = ref 0;
32295
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
   113
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
   114
fun tracing level msg =
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
   115
  if level > ! trace then ()
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
   116
  else uninterruptible (fn _ => fn () =>
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
   117
    (TextIO.output (TextIO.stdErr, (">>> " ^ msg () ^ "\n")); TextIO.flushOut TextIO.stdErr)
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
   118
      handle _ (*sic*) => ()) ();
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
   119
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
   120
fun tracing_time detailed time =
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
   121
  tracing
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
   122
   (if not detailed then 5
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
   123
    else if Time.>= (time, Time.fromMilliseconds 1000) then 1
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
   124
    else if Time.>= (time, Time.fromMilliseconds 100) then 2
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
   125
    else if Time.>= (time, Time.fromMilliseconds 10) then 3
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
   126
    else if Time.>= (time, Time.fromMilliseconds 1) then 4 else 5);
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
fun real_time f x =
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: 32230
diff changeset
   129
  let
32295
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
   130
    val timer = Timer.startRealTimer ();
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
   131
    val () = f x;
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
   132
    val time = Timer.checkRealTimer timer;
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
   133
  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: 32230
diff changeset
   134
1fb5db48002d added Multithreading.sync_wait, which turns enabled interrupts to sync ones, to ensure that wait will reaquire its lock when interrupted;
wenzelm
parents: 32230
diff changeset
   135
24688
a5754ca5c510 replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);
wenzelm
parents: 24672
diff changeset
   136
(* execution with time limit *)
a5754ca5c510 replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);
wenzelm
parents: 24672
diff changeset
   137
a5754ca5c510 replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);
wenzelm
parents: 24672
diff changeset
   138
structure TimeLimit =
a5754ca5c510 replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);
wenzelm
parents: 24672
diff changeset
   139
struct
a5754ca5c510 replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);
wenzelm
parents: 24672
diff changeset
   140
a5754ca5c510 replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);
wenzelm
parents: 24672
diff changeset
   141
exception TimeOut;
a5754ca5c510 replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);
wenzelm
parents: 24672
diff changeset
   142
26083
abb3f8dd66dc removed managed_process (cf. General/shell_process.ML);
wenzelm
parents: 26074
diff changeset
   143
fun timeLimit time f x = uninterruptible (fn restore_attributes => fn () =>
abb3f8dd66dc removed managed_process (cf. General/shell_process.ML);
wenzelm
parents: 26074
diff changeset
   144
  let
abb3f8dd66dc removed managed_process (cf. General/shell_process.ML);
wenzelm
parents: 26074
diff changeset
   145
    val worker = Thread.self ();
39616
8052101883c3 renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents: 39583
diff changeset
   146
    val timeout = ref false;
26083
abb3f8dd66dc removed managed_process (cf. General/shell_process.ML);
wenzelm
parents: 26074
diff changeset
   147
    val watchdog = Thread.fork (fn () =>
abb3f8dd66dc removed managed_process (cf. General/shell_process.ML);
wenzelm
parents: 26074
diff changeset
   148
      (OS.Process.sleep time; timeout := true; Thread.interrupt worker), []);
24688
a5754ca5c510 replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);
wenzelm
parents: 24672
diff changeset
   149
26083
abb3f8dd66dc removed managed_process (cf. General/shell_process.ML);
wenzelm
parents: 26074
diff changeset
   150
    val result = Exn.capture (restore_attributes f) x;
39232
69c6d3e87660 more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents: 35023
diff changeset
   151
    val was_timeout = Exn.is_interrupt_exn result andalso ! timeout;
24688
a5754ca5c510 replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);
wenzelm
parents: 24672
diff changeset
   152
26083
abb3f8dd66dc removed managed_process (cf. General/shell_process.ML);
wenzelm
parents: 26074
diff changeset
   153
    val _ = Thread.interrupt watchdog handle Thread _ => ();
abb3f8dd66dc removed managed_process (cf. General/shell_process.ML);
wenzelm
parents: 26074
diff changeset
   154
  in if was_timeout then raise TimeOut else Exn.release result end) ();
24688
a5754ca5c510 replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);
wenzelm
parents: 24672
diff changeset
   155
a5754ca5c510 replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);
wenzelm
parents: 24672
diff changeset
   156
end;
24668
4058b7b0925c added interrupt_timeout;
wenzelm
parents: 24297
diff changeset
   157
24069
8a15a04e36f6 tuned msgs;
wenzelm
parents: 24066
diff changeset
   158
35010
d6e492cea6e4 renamed system/system_out to bash/bash_output -- to emphasized that this is really GNU bash, not some undefined POSIX sh;
wenzelm
parents: 33219
diff changeset
   159
(* GNU bash processes, with propagation of interrupts *)
26098
b59d33f73aed added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents: 26083
diff changeset
   160
35010
d6e492cea6e4 renamed system/system_out to bash/bash_output -- to emphasized that this is really GNU bash, not some undefined POSIX sh;
wenzelm
parents: 33219
diff changeset
   161
fun bash_output script = with_attributes no_interrupts (fn orig_atts =>
26098
b59d33f73aed added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents: 26083
diff changeset
   162
  let
b59d33f73aed added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents: 26083
diff changeset
   163
    val script_name = OS.FileSys.tmpName ();
b59d33f73aed added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents: 26083
diff changeset
   164
    val _ = write_file script_name script;
b59d33f73aed added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents: 26083
diff changeset
   165
b59d33f73aed added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents: 26083
diff changeset
   166
    val pid_name = OS.FileSys.tmpName ();
b59d33f73aed added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents: 26083
diff changeset
   167
    val output_name = OS.FileSys.tmpName ();
b59d33f73aed added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents: 26083
diff changeset
   168
b59d33f73aed added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents: 26083
diff changeset
   169
    (*result state*)
b59d33f73aed added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents: 26083
diff changeset
   170
    datatype result = Wait | Signal | Result of int;
39616
8052101883c3 renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents: 39583
diff changeset
   171
    val result = ref Wait;
32295
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
   172
    val lock = Mutex.mutex ();
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
   173
    val cond = ConditionVar.conditionVar ();
26098
b59d33f73aed added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents: 26083
diff changeset
   174
    fun set_result res =
32295
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
   175
      (Mutex.lock lock; result := res; ConditionVar.signal cond; Mutex.unlock lock);
26098
b59d33f73aed added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents: 26083
diff changeset
   176
32295
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
   177
    val _ = Mutex.lock lock;
26098
b59d33f73aed added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents: 26083
diff changeset
   178
b59d33f73aed added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents: 26083
diff changeset
   179
    (*system thread*)
b59d33f73aed added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents: 26083
diff changeset
   180
    val system_thread = Thread.fork (fn () =>
b59d33f73aed added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents: 26083
diff changeset
   181
      let
b59d33f73aed added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents: 26083
diff changeset
   182
        val status =
39576
48baf61cb888 refined ML/Scala bash wrapper, based on more general lib/scripts/process;
wenzelm
parents: 39232
diff changeset
   183
          OS.Process.system ("exec \"$ISABELLE_HOME/lib/scripts/process\" group " ^ pid_name ^
39583
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39576
diff changeset
   184
            " script \"exec bash " ^ script_name ^ " > " ^ output_name ^ "\"");
26098
b59d33f73aed added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents: 26083
diff changeset
   185
        val res =
b59d33f73aed added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents: 26083
diff changeset
   186
          (case Posix.Process.fromStatus status of
b59d33f73aed added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents: 26083
diff changeset
   187
            Posix.Process.W_EXITED => Result 0
b59d33f73aed added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents: 26083
diff changeset
   188
          | Posix.Process.W_EXITSTATUS 0wx82 => Signal
b59d33f73aed added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents: 26083
diff changeset
   189
          | Posix.Process.W_EXITSTATUS w => Result (Word8.toInt w)
b59d33f73aed added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents: 26083
diff changeset
   190
          | Posix.Process.W_SIGNALED s =>
b59d33f73aed added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents: 26083
diff changeset
   191
              if s = Posix.Signal.int then Signal
b59d33f73aed added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents: 26083
diff changeset
   192
              else Result (256 + LargeWord.toInt (Posix.Signal.toWord s))
b59d33f73aed added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents: 26083
diff changeset
   193
          | Posix.Process.W_STOPPED s => Result (512 + LargeWord.toInt (Posix.Signal.toWord s)));
28398
9aa3216e5f31 tuned comments;
wenzelm
parents: 28254
diff changeset
   194
      in set_result res end handle _ (*sic*) => set_result (Result 2), []);
26098
b59d33f73aed added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents: 26083
diff changeset
   195
b59d33f73aed added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents: 26083
diff changeset
   196
    (*main thread -- proxy for interrupts*)
b59d33f73aed added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents: 26083
diff changeset
   197
    fun kill n =
b59d33f73aed added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents: 26083
diff changeset
   198
      (case Int.fromString (read_file pid_name) of
b59d33f73aed added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents: 26083
diff changeset
   199
        SOME pid =>
b59d33f73aed added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents: 26083
diff changeset
   200
          Posix.Process.kill
b59d33f73aed added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents: 26083
diff changeset
   201
            (Posix.Process.K_GROUP (Posix.Process.wordToPid (LargeWord.fromInt pid)),
b59d33f73aed added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents: 26083
diff changeset
   202
              Posix.Signal.int)
b59d33f73aed added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents: 26083
diff changeset
   203
      | NONE => ())
b59d33f73aed added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents: 26083
diff changeset
   204
      handle OS.SysErr _ => () | IO.Io _ =>
b59d33f73aed added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents: 26083
diff changeset
   205
        (OS.Process.sleep (Time.fromMilliseconds 100); if n > 0 then kill (n - 1) else ());
b59d33f73aed added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents: 26083
diff changeset
   206
32295
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
   207
    val _ =
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
   208
      while ! result = Wait do
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
   209
        let val res =
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
   210
          sync_wait (SOME orig_atts)
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
   211
            (SOME (Time.+ (Time.now (), Time.fromMilliseconds 100))) cond lock
39232
69c6d3e87660 more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents: 35023
diff changeset
   212
        in if Exn.is_interrupt_exn res then kill 10 else () end;
26098
b59d33f73aed added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents: 26083
diff changeset
   213
b59d33f73aed added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents: 26083
diff changeset
   214
    (*cleanup*)
b59d33f73aed added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents: 26083
diff changeset
   215
    val output = read_file output_name handle IO.Io _ => "";
b59d33f73aed added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents: 26083
diff changeset
   216
    val _ = OS.FileSys.remove script_name handle OS.SysErr _ => ();
b59d33f73aed added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents: 26083
diff changeset
   217
    val _ = OS.FileSys.remove pid_name handle OS.SysErr _ => ();
b59d33f73aed added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents: 26083
diff changeset
   218
    val _ = OS.FileSys.remove output_name handle OS.SysErr _ => ();
b59d33f73aed added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents: 26083
diff changeset
   219
    val _ = Thread.interrupt system_thread handle Thread _ => ();
39232
69c6d3e87660 more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents: 35023
diff changeset
   220
    val rc = (case ! result of Signal => Exn.interrupt () | Result rc => rc);
32295
400cc493d466 renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
wenzelm
parents: 32286
diff changeset
   221
  in (output, rc) end);
26098
b59d33f73aed added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents: 26083
diff changeset
   222
b59d33f73aed added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents: 26083
diff changeset
   223
23961
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
   224
(* critical section -- may be nested within the same thread *)
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
   225
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
   226
local
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
   227
24063
736c03ae92f5 more informative tracing;
wenzelm
parents: 24060
diff changeset
   228
val critical_lock = Mutex.mutex ();
39616
8052101883c3 renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents: 39583
diff changeset
   229
val critical_thread = ref (NONE: Thread.thread option);
8052101883c3 renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents: 39583
diff changeset
   230
val critical_name = ref "";
24063
736c03ae92f5 more informative tracing;
wenzelm
parents: 24060
diff changeset
   231
23961
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
   232
in
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
   233
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
   234
fun self_critical () =
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
   235
  (case ! critical_thread of
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
   236
    NONE => false
28150
cbc2cbfc840c added no_interrupts;
wenzelm
parents: 28124
diff changeset
   237
  | SOME t => Thread.equal (t, Thread.self ()));
23961
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
   238
23991
d4417ba26706 renamed CRITICAL' to NAMED_CRITICAL;
wenzelm
parents: 23981
diff changeset
   239
fun NAMED_CRITICAL name e =
23961
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
   240
  if self_critical () then e ()
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
   241
  else
32184
cfa0ef0c0c5f simplified/unified Multithreading.tracing_time;
wenzelm
parents: 32107
diff changeset
   242
    Exn.release (uninterruptible (fn restore_attributes => fn () =>
24208
f4cafbaa05e4 schedule: more precise task model;
wenzelm
parents: 24144
diff changeset
   243
      let
f4cafbaa05e4 schedule: more precise task model;
wenzelm
parents: 24144
diff changeset
   244
        val name' = ! critical_name;
f4cafbaa05e4 schedule: more precise task model;
wenzelm
parents: 24144
diff changeset
   245
        val _ =
f4cafbaa05e4 schedule: more precise task model;
wenzelm
parents: 24144
diff changeset
   246
          if Mutex.trylock critical_lock then ()
f4cafbaa05e4 schedule: more precise task model;
wenzelm
parents: 24144
diff changeset
   247
          else
f4cafbaa05e4 schedule: more precise task model;
wenzelm
parents: 24144
diff changeset
   248
            let
32184
cfa0ef0c0c5f simplified/unified Multithreading.tracing_time;
wenzelm
parents: 32107
diff changeset
   249
              val _ = tracing 5 (fn () => "CRITICAL" ^ show name ^ show' name' ^ ": waiting");
32185
57ecfab3bcfe added Multithreading.real_time;
wenzelm
parents: 32184
diff changeset
   250
              val time = real_time Mutex.lock critical_lock;
32186
8026b73cd357 tuned tracing;
wenzelm
parents: 32185
diff changeset
   251
              val _ = tracing_time true time (fn () =>
24208
f4cafbaa05e4 schedule: more precise task model;
wenzelm
parents: 24144
diff changeset
   252
                "CRITICAL" ^ show name ^ show' name' ^ ": passed after " ^ Time.toString time);
f4cafbaa05e4 schedule: more precise task model;
wenzelm
parents: 24144
diff changeset
   253
            in () end;
f4cafbaa05e4 schedule: more precise task model;
wenzelm
parents: 24144
diff changeset
   254
        val _ = critical_thread := SOME (Thread.self ());
f4cafbaa05e4 schedule: more precise task model;
wenzelm
parents: 24144
diff changeset
   255
        val _ = critical_name := name;
26083
abb3f8dd66dc removed managed_process (cf. General/shell_process.ML);
wenzelm
parents: 26074
diff changeset
   256
        val result = Exn.capture (restore_attributes e) ();
24208
f4cafbaa05e4 schedule: more precise task model;
wenzelm
parents: 24144
diff changeset
   257
        val _ = critical_name := "";
f4cafbaa05e4 schedule: more precise task model;
wenzelm
parents: 24144
diff changeset
   258
        val _ = critical_thread := NONE;
f4cafbaa05e4 schedule: more precise task model;
wenzelm
parents: 24144
diff changeset
   259
        val _ = Mutex.unlock critical_lock;
32184
cfa0ef0c0c5f simplified/unified Multithreading.tracing_time;
wenzelm
parents: 32107
diff changeset
   260
      in result end) ());
23961
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
   261
23991
d4417ba26706 renamed CRITICAL' to NAMED_CRITICAL;
wenzelm
parents: 23981
diff changeset
   262
fun CRITICAL e = NAMED_CRITICAL "" e;
23981
03b71bf91318 added trace flag, official tracing operation;
wenzelm
parents: 23973
diff changeset
   263
23961
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
   264
end;
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
   265
23973
b6ce6de5b700 renamed number_of_threads to max_threads;
wenzelm
parents: 23961
diff changeset
   266
25704
df9c8074ff09 signature BASIC_MULTITHREADING;
wenzelm
parents: 24688
diff changeset
   267
(* serial numbers *)
df9c8074ff09 signature BASIC_MULTITHREADING;
wenzelm
parents: 24688
diff changeset
   268
df9c8074ff09 signature BASIC_MULTITHREADING;
wenzelm
parents: 24688
diff changeset
   269
local
df9c8074ff09 signature BASIC_MULTITHREADING;
wenzelm
parents: 24688
diff changeset
   270
df9c8074ff09 signature BASIC_MULTITHREADING;
wenzelm
parents: 24688
diff changeset
   271
val serial_lock = Mutex.mutex ();
39616
8052101883c3 renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents: 39583
diff changeset
   272
val serial_count = ref 0;
25704
df9c8074ff09 signature BASIC_MULTITHREADING;
wenzelm
parents: 24688
diff changeset
   273
df9c8074ff09 signature BASIC_MULTITHREADING;
wenzelm
parents: 24688
diff changeset
   274
in
df9c8074ff09 signature BASIC_MULTITHREADING;
wenzelm
parents: 24688
diff changeset
   275
df9c8074ff09 signature BASIC_MULTITHREADING;
wenzelm
parents: 24688
diff changeset
   276
val serial = uninterruptible (fn _ => fn () =>
df9c8074ff09 signature BASIC_MULTITHREADING;
wenzelm
parents: 24688
diff changeset
   277
  let
df9c8074ff09 signature BASIC_MULTITHREADING;
wenzelm
parents: 24688
diff changeset
   278
    val _ = Mutex.lock serial_lock;
28124
10a1f1f4c6ae moved Multithreading.task/schedule to Concurrent/schedule.ML;
wenzelm
parents: 26504
diff changeset
   279
    val _ = serial_count := ! serial_count + 1;
10a1f1f4c6ae moved Multithreading.task/schedule to Concurrent/schedule.ML;
wenzelm
parents: 26504
diff changeset
   280
    val res = ! serial_count;
25704
df9c8074ff09 signature BASIC_MULTITHREADING;
wenzelm
parents: 24688
diff changeset
   281
    val _ = Mutex.unlock serial_lock;
df9c8074ff09 signature BASIC_MULTITHREADING;
wenzelm
parents: 24688
diff changeset
   282
  in res end);
df9c8074ff09 signature BASIC_MULTITHREADING;
wenzelm
parents: 24688
diff changeset
   283
23961
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
   284
end;
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
   285
25704
df9c8074ff09 signature BASIC_MULTITHREADING;
wenzelm
parents: 24688
diff changeset
   286
end;
24688
a5754ca5c510 replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);
wenzelm
parents: 24672
diff changeset
   287
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: 32230
diff changeset
   288
structure Basic_Multithreading: BASIC_MULTITHREADING = Multithreading;
1fb5db48002d added Multithreading.sync_wait, which turns enabled interrupts to sync ones, to ensure that wait will reaquire its lock when interrupted;
wenzelm
parents: 32230
diff changeset
   289
open Basic_Multithreading;