src/Pure/ML-Systems/multithreading_polyml.ML
author wenzelm
Sun, 31 May 2009 14:51:21 +0200
changeset 31312 1c00e4ff3c99
parent 31311 b82e55f51dcc
child 31630 2f8ed0dca3bd
permissions -rw-r--r--
more modular setup of runtime compilation;
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
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
    11
  val system_out: 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
24072
8b9e5d776ef3 dequeue: wait loop while PROTECTED -- avoids race condition;
wenzelm
parents: 24069
diff changeset
    30
(* options *)
24069
8a15a04e36f6 tuned msgs;
wenzelm
parents: 24066
diff changeset
    31
24119
06965b38c5e9 tracing: level;
wenzelm
parents: 24109
diff changeset
    32
val trace = ref 0;
28465
db8667d84dd2 tracing: ignore failure of any kind;
wenzelm
parents: 28443
diff changeset
    33
24119
06965b38c5e9 tracing: level;
wenzelm
parents: 24109
diff changeset
    34
fun tracing level msg =
28465
db8667d84dd2 tracing: ignore failure of any kind;
wenzelm
parents: 28443
diff changeset
    35
  if level > ! trace then ()
db8667d84dd2 tracing: ignore failure of any kind;
wenzelm
parents: 28443
diff changeset
    36
  else (TextIO.output (TextIO.stdErr, (">>> " ^ msg () ^ "\n")); TextIO.flushOut TextIO.stdErr)
db8667d84dd2 tracing: ignore failure of any kind;
wenzelm
parents: 28443
diff changeset
    37
    handle _ (*sic*) => ();
23961
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
    38
23981
03b71bf91318 added trace flag, official tracing operation;
wenzelm
parents: 23973
diff changeset
    39
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
    40
23973
b6ce6de5b700 renamed number_of_threads to max_threads;
wenzelm
parents: 23961
diff changeset
    41
val max_threads = ref 1;
b6ce6de5b700 renamed number_of_threads to max_threads;
wenzelm
parents: 23961
diff changeset
    42
25775
90525e67ede7 added Multithreading.max_threads_value, which maps a value of 0 to number of CPUs;
wenzelm
parents: 25735
diff changeset
    43
fun max_threads_value () =
90525e67ede7 added Multithreading.max_threads_value, which maps a value of 0 to number of CPUs;
wenzelm
parents: 25735
diff changeset
    44
  let val m = ! max_threads
28161
7718587e510e added sync_interrupts, regular_interrupts;
wenzelm
parents: 28150
diff changeset
    45
  in if m <= 0 then Int.max (Thread.numProcessors (), 1) else m end;
25775
90525e67ede7 added Multithreading.max_threads_value, which maps a value of 0 to number of CPUs;
wenzelm
parents: 25735
diff changeset
    46
28555
d59712ee942c added enabled;
wenzelm
parents: 28466
diff changeset
    47
fun enabled () = max_threads_value () > 1;
d59712ee942c added enabled;
wenzelm
parents: 28466
diff changeset
    48
23973
b6ce6de5b700 renamed number_of_threads to max_threads;
wenzelm
parents: 23961
diff changeset
    49
24069
8a15a04e36f6 tuned msgs;
wenzelm
parents: 24066
diff changeset
    50
(* misc utils *)
8a15a04e36f6 tuned msgs;
wenzelm
parents: 24066
diff changeset
    51
24208
f4cafbaa05e4 schedule: more precise task model;
wenzelm
parents: 24144
diff changeset
    52
fun show "" = "" | show name = " " ^ name;
f4cafbaa05e4 schedule: more precise task model;
wenzelm
parents: 24144
diff changeset
    53
fun show' "" = "" | show' name = " [" ^ name ^ "]";
f4cafbaa05e4 schedule: more precise task model;
wenzelm
parents: 24144
diff changeset
    54
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
    55
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
    56
  let val is = TextIO.openIn name
26504
6e87c0a60104 before close: Exn.capture/release;
wenzelm
parents: 26493
diff changeset
    57
  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
    58
b59d33f73aed added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents: 26083
diff changeset
    59
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
    60
  let val os = TextIO.openOut name
26504
6e87c0a60104 before close: Exn.capture/release;
wenzelm
parents: 26493
diff changeset
    61
  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
    62
24208
f4cafbaa05e4 schedule: more precise task model;
wenzelm
parents: 24144
diff changeset
    63
f4cafbaa05e4 schedule: more precise task model;
wenzelm
parents: 24144
diff changeset
    64
(* thread attributes *)
f4cafbaa05e4 schedule: more precise task model;
wenzelm
parents: 24144
diff changeset
    65
28161
7718587e510e added sync_interrupts, regular_interrupts;
wenzelm
parents: 28150
diff changeset
    66
val no_interrupts =
7718587e510e added sync_interrupts, regular_interrupts;
wenzelm
parents: 28150
diff changeset
    67
  [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptDefer];
7718587e510e added sync_interrupts, regular_interrupts;
wenzelm
parents: 28150
diff changeset
    68
7718587e510e added sync_interrupts, regular_interrupts;
wenzelm
parents: 28150
diff changeset
    69
val regular_interrupts =
7718587e510e added sync_interrupts, regular_interrupts;
wenzelm
parents: 28150
diff changeset
    70
  [Thread.EnableBroadcastInterrupt true, Thread.InterruptState Thread.InterruptAsynchOnce];
7718587e510e added sync_interrupts, regular_interrupts;
wenzelm
parents: 28150
diff changeset
    71
30612
cb6421b6a18f future_job: do not inherit attributes, but enforce restricted interrupts -- attempt to prevent interrupt race conditions;
wenzelm
parents: 30602
diff changeset
    72
val restricted_interrupts =
cb6421b6a18f future_job: do not inherit attributes, but enforce restricted interrupts -- attempt to prevent interrupt race conditions;
wenzelm
parents: 30602
diff changeset
    73
  [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
    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
24208
f4cafbaa05e4 schedule: more precise task model;
wenzelm
parents: 24144
diff changeset
    80
fun with_attributes new_atts f x =
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 () =>
1bd90b76477a with_attributes: canonical capture/release scheme (potentially iron out race condition);
wenzelm
parents: 29564
diff changeset
    84
      (Thread.setAttributes (safe_interrupts new_atts); f orig_atts x)) ();
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
28161
7718587e510e added sync_interrupts, regular_interrupts;
wenzelm
parents: 28150
diff changeset
    88
fun interruptible f = with_attributes regular_interrupts (fn _ => f);
28150
cbc2cbfc840c added no_interrupts;
wenzelm
parents: 28124
diff changeset
    89
26083
abb3f8dd66dc removed managed_process (cf. General/shell_process.ML);
wenzelm
parents: 26074
diff changeset
    90
fun uninterruptible f =
28150
cbc2cbfc840c added no_interrupts;
wenzelm
parents: 28124
diff changeset
    91
  with_attributes no_interrupts (fn atts => f (fn g => with_attributes atts (fn _ => g)));
24668
4058b7b0925c added interrupt_timeout;
wenzelm
parents: 24297
diff changeset
    92
24688
a5754ca5c510 replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);
wenzelm
parents: 24672
diff changeset
    93
a5754ca5c510 replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);
wenzelm
parents: 24672
diff changeset
    94
(* 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
    95
a5754ca5c510 replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);
wenzelm
parents: 24672
diff changeset
    96
structure TimeLimit =
a5754ca5c510 replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);
wenzelm
parents: 24672
diff changeset
    97
struct
a5754ca5c510 replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);
wenzelm
parents: 24672
diff changeset
    98
a5754ca5c510 replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);
wenzelm
parents: 24672
diff changeset
    99
exception TimeOut;
a5754ca5c510 replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);
wenzelm
parents: 24672
diff changeset
   100
26083
abb3f8dd66dc removed managed_process (cf. General/shell_process.ML);
wenzelm
parents: 26074
diff changeset
   101
fun timeLimit time f x = uninterruptible (fn restore_attributes => fn () =>
abb3f8dd66dc removed managed_process (cf. General/shell_process.ML);
wenzelm
parents: 26074
diff changeset
   102
  let
abb3f8dd66dc removed managed_process (cf. General/shell_process.ML);
wenzelm
parents: 26074
diff changeset
   103
    val worker = Thread.self ();
abb3f8dd66dc removed managed_process (cf. General/shell_process.ML);
wenzelm
parents: 26074
diff changeset
   104
    val timeout = ref false;
abb3f8dd66dc removed managed_process (cf. General/shell_process.ML);
wenzelm
parents: 26074
diff changeset
   105
    val watchdog = Thread.fork (fn () =>
abb3f8dd66dc removed managed_process (cf. General/shell_process.ML);
wenzelm
parents: 26074
diff changeset
   106
      (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
   107
26083
abb3f8dd66dc removed managed_process (cf. General/shell_process.ML);
wenzelm
parents: 26074
diff changeset
   108
    val result = Exn.capture (restore_attributes f) x;
28443
de653f1ad78b more robust treatment of Interrupt (cf. exn.ML);
wenzelm
parents: 28398
diff changeset
   109
    val was_timeout = (case result of Exn.Exn Exn.Interrupt => ! timeout | _ => false);
24688
a5754ca5c510 replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);
wenzelm
parents: 24672
diff changeset
   110
26083
abb3f8dd66dc removed managed_process (cf. General/shell_process.ML);
wenzelm
parents: 26074
diff changeset
   111
    val _ = Thread.interrupt watchdog handle Thread _ => ();
abb3f8dd66dc removed managed_process (cf. General/shell_process.ML);
wenzelm
parents: 26074
diff changeset
   112
  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
   113
a5754ca5c510 replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);
wenzelm
parents: 24672
diff changeset
   114
end;
24668
4058b7b0925c added interrupt_timeout;
wenzelm
parents: 24297
diff changeset
   115
24069
8a15a04e36f6 tuned msgs;
wenzelm
parents: 24066
diff changeset
   116
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
   117
(* system shell processes, with propagation of 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
   118
28254
d67ba23e0277 multithreading for Poly/ML 5.1 is no longer supported;
wenzelm
parents: 28169
diff changeset
   119
fun system_out script = uninterruptible (fn restore_attributes => fn () =>
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
   120
  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
   121
    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
   122
    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
   123
b59d33f73aed added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents: 26083
diff changeset
   124
    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
   125
    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
   126
b59d33f73aed added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents: 26083
diff changeset
   127
    (*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
   128
    datatype result = Wait | Signal | Result of 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
   129
    val result = ref Wait;
b59d33f73aed added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents: 26083
diff changeset
   130
    val result_mutex = Mutex.mutex ();
b59d33f73aed added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents: 26083
diff changeset
   131
    val result_cond = ConditionVar.conditionVar ();
b59d33f73aed added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents: 26083
diff changeset
   132
    fun set_result 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
   133
      (Mutex.lock result_mutex; result := res; Mutex.unlock result_mutex;
b59d33f73aed added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents: 26083
diff changeset
   134
        ConditionVar.signal result_cond);
b59d33f73aed added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents: 26083
diff changeset
   135
b59d33f73aed added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents: 26083
diff changeset
   136
    val _ = Mutex.lock result_mutex;
b59d33f73aed added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents: 26083
diff changeset
   137
b59d33f73aed added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents: 26083
diff changeset
   138
    (*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
   139
    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
   140
      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
   141
        val status =
b59d33f73aed added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents: 26083
diff changeset
   142
          OS.Process.system ("perl -w \"$ISABELLE_HOME/lib/scripts/system.pl\" group " ^
b59d33f73aed added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents: 26083
diff changeset
   143
            script_name ^ " " ^ pid_name ^ " " ^ output_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
   144
        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
   145
          (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
   146
            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
   147
          | 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
   148
          | 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
   149
          | 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
   150
              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
   151
              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
   152
          | Posix.Process.W_STOPPED s => Result (512 + LargeWord.toInt (Posix.Signal.toWord s)));
28398
9aa3216e5f31 tuned comments;
wenzelm
parents: 28254
diff changeset
   153
      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
   154
b59d33f73aed added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents: 26083
diff changeset
   155
    (*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
   156
    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
   157
      (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
   158
        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
   159
          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
   160
            (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
   161
              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
   162
      | 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
   163
      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
   164
        (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
   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 _ = while ! result = Wait do
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
      restore_attributes (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
   168
        (ConditionVar.waitUntil (result_cond, result_mutex, Time.now () + Time.fromMilliseconds 100); ())
28443
de653f1ad78b more robust treatment of Interrupt (cf. exn.ML);
wenzelm
parents: 28398
diff changeset
   169
          handle Exn.Interrupt => kill 10) ();
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
   170
b59d33f73aed added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
wenzelm
parents: 26083
diff changeset
   171
    (*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
   172
    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
   173
    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
   174
    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
   175
    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
   176
    val _ = Thread.interrupt system_thread handle Thread _ => ();
28443
de653f1ad78b more robust treatment of Interrupt (cf. exn.ML);
wenzelm
parents: 28398
diff changeset
   177
    val rc = (case ! result of Signal => raise Exn.Interrupt | Result rc => rc);
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
  in (output, rc) end) ();
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
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
23961
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
   181
(* critical section -- may be nested within the same thread *)
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
   182
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
   183
local
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
   184
24063
736c03ae92f5 more informative tracing;
wenzelm
parents: 24060
diff changeset
   185
val critical_lock = Mutex.mutex ();
736c03ae92f5 more informative tracing;
wenzelm
parents: 24060
diff changeset
   186
val critical_thread = ref (NONE: Thread.thread option);
736c03ae92f5 more informative tracing;
wenzelm
parents: 24060
diff changeset
   187
val critical_name = ref "";
736c03ae92f5 more informative tracing;
wenzelm
parents: 24060
diff changeset
   188
23961
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
   189
in
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
   190
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
   191
fun self_critical () =
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
   192
  (case ! critical_thread of
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
   193
    NONE => false
28150
cbc2cbfc840c added no_interrupts;
wenzelm
parents: 28124
diff changeset
   194
  | SOME t => Thread.equal (t, Thread.self ()));
23961
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
   195
23991
d4417ba26706 renamed CRITICAL' to NAMED_CRITICAL;
wenzelm
parents: 23981
diff changeset
   196
fun NAMED_CRITICAL name e =
23961
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
   197
  if self_critical () then e ()
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
   198
  else
26083
abb3f8dd66dc removed managed_process (cf. General/shell_process.ML);
wenzelm
parents: 26074
diff changeset
   199
    uninterruptible (fn restore_attributes => fn () =>
24208
f4cafbaa05e4 schedule: more precise task model;
wenzelm
parents: 24144
diff changeset
   200
      let
f4cafbaa05e4 schedule: more precise task model;
wenzelm
parents: 24144
diff changeset
   201
        val name' = ! critical_name;
f4cafbaa05e4 schedule: more precise task model;
wenzelm
parents: 24144
diff changeset
   202
        val _ =
f4cafbaa05e4 schedule: more precise task model;
wenzelm
parents: 24144
diff changeset
   203
          if Mutex.trylock critical_lock then ()
f4cafbaa05e4 schedule: more precise task model;
wenzelm
parents: 24144
diff changeset
   204
          else
f4cafbaa05e4 schedule: more precise task model;
wenzelm
parents: 24144
diff changeset
   205
            let
f4cafbaa05e4 schedule: more precise task model;
wenzelm
parents: 24144
diff changeset
   206
              val timer = Timer.startRealTimer ();
f4cafbaa05e4 schedule: more precise task model;
wenzelm
parents: 24144
diff changeset
   207
              val _ = tracing 4 (fn () => "CRITICAL" ^ show name ^ show' name' ^ ": waiting");
f4cafbaa05e4 schedule: more precise task model;
wenzelm
parents: 24144
diff changeset
   208
              val _ = Mutex.lock critical_lock;
f4cafbaa05e4 schedule: more precise task model;
wenzelm
parents: 24144
diff changeset
   209
              val time = Timer.checkRealTimer timer;
26493
de4764e95166 CRITICAL: further trace levels for 1000ms and 100ms;
wenzelm
parents: 26390
diff changeset
   210
              val trace_time =
de4764e95166 CRITICAL: further trace levels for 1000ms and 100ms;
wenzelm
parents: 26390
diff changeset
   211
                if Time.>= (time, Time.fromMilliseconds 1000) then 1
de4764e95166 CRITICAL: further trace levels for 1000ms and 100ms;
wenzelm
parents: 26390
diff changeset
   212
                else if Time.>= (time, Time.fromMilliseconds 100) then 2
de4764e95166 CRITICAL: further trace levels for 1000ms and 100ms;
wenzelm
parents: 26390
diff changeset
   213
                else if Time.>= (time, Time.fromMilliseconds 10) then 3 else 4;
de4764e95166 CRITICAL: further trace levels for 1000ms and 100ms;
wenzelm
parents: 26390
diff changeset
   214
              val _ = tracing trace_time (fn () =>
24208
f4cafbaa05e4 schedule: more precise task model;
wenzelm
parents: 24144
diff changeset
   215
                "CRITICAL" ^ show name ^ show' name' ^ ": passed after " ^ Time.toString time);
f4cafbaa05e4 schedule: more precise task model;
wenzelm
parents: 24144
diff changeset
   216
            in () end;
f4cafbaa05e4 schedule: more precise task model;
wenzelm
parents: 24144
diff changeset
   217
        val _ = critical_thread := SOME (Thread.self ());
f4cafbaa05e4 schedule: more precise task model;
wenzelm
parents: 24144
diff changeset
   218
        val _ = critical_name := name;
26083
abb3f8dd66dc removed managed_process (cf. General/shell_process.ML);
wenzelm
parents: 26074
diff changeset
   219
        val result = Exn.capture (restore_attributes e) ();
24208
f4cafbaa05e4 schedule: more precise task model;
wenzelm
parents: 24144
diff changeset
   220
        val _ = critical_name := "";
f4cafbaa05e4 schedule: more precise task model;
wenzelm
parents: 24144
diff changeset
   221
        val _ = critical_thread := NONE;
f4cafbaa05e4 schedule: more precise task model;
wenzelm
parents: 24144
diff changeset
   222
        val _ = Mutex.unlock critical_lock;
f4cafbaa05e4 schedule: more precise task model;
wenzelm
parents: 24144
diff changeset
   223
      in Exn.release result end) ();
23961
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
   224
23991
d4417ba26706 renamed CRITICAL' to NAMED_CRITICAL;
wenzelm
parents: 23981
diff changeset
   225
fun CRITICAL e = NAMED_CRITICAL "" e;
23981
03b71bf91318 added trace flag, official tracing operation;
wenzelm
parents: 23973
diff changeset
   226
23961
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
   227
end;
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
   228
23973
b6ce6de5b700 renamed number_of_threads to max_threads;
wenzelm
parents: 23961
diff changeset
   229
25704
df9c8074ff09 signature BASIC_MULTITHREADING;
wenzelm
parents: 24688
diff changeset
   230
(* serial numbers *)
df9c8074ff09 signature BASIC_MULTITHREADING;
wenzelm
parents: 24688
diff changeset
   231
df9c8074ff09 signature BASIC_MULTITHREADING;
wenzelm
parents: 24688
diff changeset
   232
local
df9c8074ff09 signature BASIC_MULTITHREADING;
wenzelm
parents: 24688
diff changeset
   233
df9c8074ff09 signature BASIC_MULTITHREADING;
wenzelm
parents: 24688
diff changeset
   234
val serial_lock = Mutex.mutex ();
df9c8074ff09 signature BASIC_MULTITHREADING;
wenzelm
parents: 24688
diff changeset
   235
val serial_count = ref 0;
df9c8074ff09 signature BASIC_MULTITHREADING;
wenzelm
parents: 24688
diff changeset
   236
df9c8074ff09 signature BASIC_MULTITHREADING;
wenzelm
parents: 24688
diff changeset
   237
in
df9c8074ff09 signature BASIC_MULTITHREADING;
wenzelm
parents: 24688
diff changeset
   238
df9c8074ff09 signature BASIC_MULTITHREADING;
wenzelm
parents: 24688
diff changeset
   239
val serial = uninterruptible (fn _ => fn () =>
df9c8074ff09 signature BASIC_MULTITHREADING;
wenzelm
parents: 24688
diff changeset
   240
  let
df9c8074ff09 signature BASIC_MULTITHREADING;
wenzelm
parents: 24688
diff changeset
   241
    val _ = Mutex.lock serial_lock;
28124
10a1f1f4c6ae moved Multithreading.task/schedule to Concurrent/schedule.ML;
wenzelm
parents: 26504
diff changeset
   242
    val _ = serial_count := ! serial_count + 1;
10a1f1f4c6ae moved Multithreading.task/schedule to Concurrent/schedule.ML;
wenzelm
parents: 26504
diff changeset
   243
    val res = ! serial_count;
25704
df9c8074ff09 signature BASIC_MULTITHREADING;
wenzelm
parents: 24688
diff changeset
   244
    val _ = Mutex.unlock serial_lock;
df9c8074ff09 signature BASIC_MULTITHREADING;
wenzelm
parents: 24688
diff changeset
   245
  in res end);
df9c8074ff09 signature BASIC_MULTITHREADING;
wenzelm
parents: 24688
diff changeset
   246
23961
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
   247
end;
9e7e1e309ebd Multithreading in Poly/ML (version 5.1).
wenzelm
parents:
diff changeset
   248
25704
df9c8074ff09 signature BASIC_MULTITHREADING;
wenzelm
parents: 24688
diff changeset
   249
end;
24688
a5754ca5c510 replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);
wenzelm
parents: 24672
diff changeset
   250
25704
df9c8074ff09 signature BASIC_MULTITHREADING;
wenzelm
parents: 24688
diff changeset
   251
structure BasicMultithreading: BASIC_MULTITHREADING = Multithreading;
df9c8074ff09 signature BASIC_MULTITHREADING;
wenzelm
parents: 24688
diff changeset
   252
open BasicMultithreading;