unconditional Multithreading;
authorwenzelm
Thu Feb 18 23:10:28 2016 +0100 (21 months ago)
changeset 623596709e51d5c11
parent 62357 ab76bd43c14a
child 62360 3fd79fcdb491
unconditional Multithreading;
clarified files;
lib/scripts/process
src/Pure/Concurrent/bash_sequential.ML
src/Pure/Concurrent/future.ML
src/Pure/Concurrent/lazy_sequential.ML
src/Pure/Concurrent/par_list_sequential.ML
src/Pure/Concurrent/single_assignment_sequential.ML
src/Pure/Concurrent/synchronized_sequential.ML
src/Pure/RAW/ROOT_polyml.ML
src/Pure/RAW/multithreading.ML
src/Pure/RAW/multithreading_polyml.ML
src/Pure/ROOT
src/Pure/ROOT.ML
src/Pure/System/message_channel.ML
     1.1 --- a/lib/scripts/process	Wed Feb 17 23:29:35 2016 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,46 +0,0 @@
     1.4 -#!/usr/bin/env perl
     1.5 -#
     1.6 -# Author: Makarius
     1.7 -#
     1.8 -# exec process - with optional process group and report of pid
     1.9 -#
    1.10 -
    1.11 -use warnings;
    1.12 -use strict;
    1.13 -
    1.14 -# process group
    1.15 -
    1.16 -my $group = $ARGV[0]; shift(@ARGV);
    1.17 -
    1.18 -if ($group eq "group") {
    1.19 -  use POSIX "setsid";
    1.20 -  POSIX::setsid || die $!;
    1.21 -}
    1.22 -
    1.23 -
    1.24 -# report pid
    1.25 -
    1.26 -my $pid_name = $ARGV[0]; shift(@ARGV);
    1.27 -
    1.28 -if ($pid_name eq "-") {
    1.29 -  print "$$\n";
    1.30 -}
    1.31 -else {
    1.32 -  open (PID_FILE, ">", $pid_name) || die $!;
    1.33 -  print PID_FILE "$$";
    1.34 -  close PID_FILE;
    1.35 -}
    1.36 -
    1.37 -
    1.38 -# exec process
    1.39 -
    1.40 -my $script = $ARGV[0]; shift(@ARGV);
    1.41 -
    1.42 -if ($script eq "script") {
    1.43 -  my $cmd_line = $ARGV[0]; shift(@ARGV);
    1.44 -  exec $cmd_line || die $!;
    1.45 -}
    1.46 -else {
    1.47 -  (exec { $ARGV[0] } @ARGV) || die $!;
    1.48 -}
    1.49 -
     2.1 --- a/src/Pure/Concurrent/bash_sequential.ML	Wed Feb 17 23:29:35 2016 +0100
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,47 +0,0 @@
     2.4 -(*  Title:      Pure/Concurrent/bash_sequential.ML
     2.5 -    Author:     Makarius
     2.6 -
     2.7 -Generic GNU bash processes (no provisions to propagate interrupts, but
     2.8 -could work via the controlling tty).
     2.9 -*)
    2.10 -
    2.11 -signature BASH =
    2.12 -sig
    2.13 -  val process: string -> {out: string, err: string, rc: int, terminate: unit -> unit}
    2.14 -end;
    2.15 -
    2.16 -structure Bash: BASH =
    2.17 -struct
    2.18 -
    2.19 -fun process script =
    2.20 -  let
    2.21 -    val id = serial_string ();
    2.22 -    val script_path = File.tmp_path (Path.basic ("bash_script" ^ id));
    2.23 -    val out_path = File.tmp_path (Path.basic ("bash_out" ^ id));
    2.24 -    val err_path = File.tmp_path (Path.basic ("bash_err" ^ id));
    2.25 -    fun cleanup () = (try File.rm script_path; try File.rm out_path; try File.rm err_path);
    2.26 -  in
    2.27 -    let
    2.28 -      val _ = File.write script_path script;
    2.29 -      val status =
    2.30 -        OS.Process.system
    2.31 -          ("exec \"$ISABELLE_HOME/lib/scripts/process\" no_group /dev/null" ^
    2.32 -            " script \"exec bash " ^ File.shell_path script_path ^
    2.33 -            " > " ^ File.shell_path out_path ^
    2.34 -            " 2> " ^ File.shell_path err_path ^ "\"");
    2.35 -      val rc =
    2.36 -        (case Posix.Process.fromStatus status of
    2.37 -          Posix.Process.W_EXITED => 0
    2.38 -        | Posix.Process.W_EXITSTATUS w => Word8.toInt w
    2.39 -        | Posix.Process.W_SIGNALED s => 256 + LargeWord.toInt (Posix.Signal.toWord s)
    2.40 -        | Posix.Process.W_STOPPED s => 512 + LargeWord.toInt (Posix.Signal.toWord s));
    2.41 -
    2.42 -      val out = the_default "" (try File.read out_path);
    2.43 -      val err = the_default "" (try File.read err_path);
    2.44 -      val _ = cleanup ();
    2.45 -    in {out = out, err = err, rc = rc, terminate = fn () => ()} end
    2.46 -    handle exn => (cleanup (); reraise exn)
    2.47 -  end;
    2.48 -
    2.49 -end;
    2.50 -
     3.1 --- a/src/Pure/Concurrent/future.ML	Wed Feb 17 23:29:35 2016 +0100
     3.2 +++ b/src/Pure/Concurrent/future.ML	Thu Feb 18 23:10:28 2016 +0100
     3.3 @@ -199,13 +199,11 @@
     3.4    broadcast scheduler_event);
     3.5  
     3.6  fun interruptible_task f x =
     3.7 -  (if Multithreading.available then
     3.8 -    Multithreading.with_attributes
     3.9 -      (if is_some (worker_task ())
    3.10 -       then Multithreading.private_interrupts
    3.11 -       else Multithreading.public_interrupts)
    3.12 -      (fn _ => f x)
    3.13 -   else interruptible f x)
    3.14 +  Multithreading.with_attributes
    3.15 +    (if is_some (worker_task ())
    3.16 +     then Multithreading.private_interrupts
    3.17 +     else Multithreading.public_interrupts)
    3.18 +    (fn _ => f x)
    3.19    before Multithreading.interrupted ();
    3.20  
    3.21  
    3.22 @@ -651,8 +649,7 @@
    3.23  (* shutdown *)
    3.24  
    3.25  fun shutdown () =
    3.26 -  if not Multithreading.available then ()
    3.27 -  else if is_some (worker_task ()) then
    3.28 +  if is_some (worker_task ()) then
    3.29      raise Fail "Cannot shutdown while running as worker thread"
    3.30    else
    3.31      SYNCHRONIZED "shutdown" (fn () =>
     4.1 --- a/src/Pure/Concurrent/lazy_sequential.ML	Wed Feb 17 23:29:35 2016 +0100
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,58 +0,0 @@
     4.4 -(*  Title:      Pure/Concurrent/lazy_sequential.ML
     4.5 -    Author:     Florian Haftmann and Makarius, TU Muenchen
     4.6 -
     4.7 -Lazy evaluation with memoing of results and regular exceptions
     4.8 -(sequential version).
     4.9 -*)
    4.10 -
    4.11 -structure Lazy: LAZY =
    4.12 -struct
    4.13 -
    4.14 -(* datatype *)
    4.15 -
    4.16 -datatype 'a expr =
    4.17 -  Expr of unit -> 'a |
    4.18 -  Result of 'a Exn.result;
    4.19 -
    4.20 -abstype 'a lazy = Lazy of 'a expr Unsynchronized.ref
    4.21 -with
    4.22 -
    4.23 -fun lazy e = Lazy (Unsynchronized.ref (Expr e));
    4.24 -fun value a = Lazy (Unsynchronized.ref (Result (Exn.Res a)));
    4.25 -
    4.26 -fun peek (Lazy r) =
    4.27 -  (case ! r of
    4.28 -    Expr _ => NONE
    4.29 -  | Result res => SOME res);
    4.30 -
    4.31 -fun is_running _ = false;
    4.32 -fun is_finished x = is_some (peek x);
    4.33 -val finished_result = peek;
    4.34 -
    4.35 -
    4.36 -(* force result *)
    4.37 -
    4.38 -fun force_result (Lazy r) =
    4.39 -  let
    4.40 -    val result =
    4.41 -      (case ! r of
    4.42 -        Expr e => Exn.capture e ()
    4.43 -      | Result res => res);
    4.44 -    val _ = if Exn.is_interrupt_exn result then () else r := Result result;
    4.45 -  in result end;
    4.46 -
    4.47 -fun force r = Exn.release (force_result r);
    4.48 -fun map f x = lazy (fn () => f (force x));
    4.49 -
    4.50 -
    4.51 -(* future evaluation *)
    4.52 -
    4.53 -fun future params x =
    4.54 -  if is_finished x then Future.value_result (force_result x)
    4.55 -  else (singleton o Future.forks) params (fn () => force x);
    4.56 -
    4.57 -end;
    4.58 -end;
    4.59 -
    4.60 -type 'a lazy = 'a Lazy.lazy;
    4.61 -
     5.1 --- a/src/Pure/Concurrent/par_list_sequential.ML	Wed Feb 17 23:29:35 2016 +0100
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,19 +0,0 @@
     5.4 -(*  Title:      Pure/Concurrent/par_list_sequential.ML
     5.5 -    Author:     Makarius
     5.6 -
     5.7 -Dummy version of parallel list combinators -- plain sequential evaluation.
     5.8 -*)
     5.9 -
    5.10 -structure Par_List: PAR_LIST =
    5.11 -struct
    5.12 -
    5.13 -fun managed_results _ f = map (Exn.capture f);
    5.14 -fun map_name _ = map;
    5.15 -val map = map;
    5.16 -val map_independent = map;
    5.17 -val get_some = get_first;
    5.18 -val find_some = find_first;
    5.19 -val exists = exists;
    5.20 -val forall = forall;
    5.21 -
    5.22 -end;
     6.1 --- a/src/Pure/Concurrent/single_assignment_sequential.ML	Wed Feb 17 23:29:35 2016 +0100
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,30 +0,0 @@
     6.4 -(*  Title:      Pure/Concurrent/single_assignment_sequential.ML
     6.5 -    Author:     Makarius
     6.6 -
     6.7 -Single-assignment variables (sequential version).
     6.8 -*)
     6.9 -
    6.10 -structure Single_Assignment: SINGLE_ASSIGNMENT =
    6.11 -struct
    6.12 -
    6.13 -abstype 'a var = Var of 'a SingleAssignment.saref
    6.14 -with
    6.15 -
    6.16 -fun var _ = Var (SingleAssignment.saref ());
    6.17 -
    6.18 -fun peek (Var var) = SingleAssignment.savalue var;
    6.19 -
    6.20 -fun await v =
    6.21 -  (case peek v of
    6.22 -    SOME x => x
    6.23 -  | NONE => Thread.unavailable ());
    6.24 -
    6.25 -fun assign (v as Var var) x =
    6.26 -  (case peek v of
    6.27 -    SOME _ => raise Fail "Duplicate assignment to variable"
    6.28 -  | NONE => SingleAssignment.saset (var, x));
    6.29 -
    6.30 -end;
    6.31 -
    6.32 -end;
    6.33 -
     7.1 --- a/src/Pure/Concurrent/synchronized_sequential.ML	Wed Feb 17 23:29:35 2016 +0100
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,28 +0,0 @@
     7.4 -(*  Title:      Pure/Concurrent/synchronized_sequential.ML
     7.5 -    Author:     Makarius
     7.6 -
     7.7 -Sequential version of state variables -- plain refs.
     7.8 -*)
     7.9 -
    7.10 -structure Synchronized: SYNCHRONIZED =
    7.11 -struct
    7.12 -
    7.13 -abstype 'a var = Var of 'a Unsynchronized.ref
    7.14 -with
    7.15 -
    7.16 -fun var _ x = Var (Unsynchronized.ref x);
    7.17 -fun value (Var var) = ! var;
    7.18 -
    7.19 -fun timed_access (Var var) _ f =
    7.20 -  (case f (! var) of
    7.21 -    SOME (y, x') => (var := x'; SOME y)
    7.22 -  | NONE => Thread.unavailable ());
    7.23 -
    7.24 -fun guarded_access var f = the (timed_access var (K NONE) f);
    7.25 -
    7.26 -fun change_result var f = guarded_access var (SOME o f);
    7.27 -fun change var f = change_result var (fn x => ((), f x));
    7.28 -
    7.29 -end;
    7.30 -
    7.31 -end;
     8.1 --- a/src/Pure/RAW/ROOT_polyml.ML	Wed Feb 17 23:29:35 2016 +0100
     8.2 +++ b/src/Pure/RAW/ROOT_polyml.ML	Thu Feb 18 23:10:28 2016 +0100
     8.3 @@ -75,7 +75,6 @@
     8.4  
     8.5  open Thread;
     8.6  use "RAW/multithreading.ML";
     8.7 -use "RAW/multithreading_polyml.ML";
     8.8  
     8.9  if ML_System.name = "polyml-5.6"
    8.10  then use "RAW/ml_stack_polyml-5.6.ML"
     9.1 --- a/src/Pure/RAW/multithreading.ML	Wed Feb 17 23:29:35 2016 +0100
     9.2 +++ b/src/Pure/RAW/multithreading.ML	Thu Feb 18 23:10:28 2016 +0100
     9.3 @@ -1,22 +1,28 @@
     9.4  (*  Title:      Pure/RAW/multithreading.ML
     9.5      Author:     Makarius
     9.6  
     9.7 -Dummy implementation of multithreading setup.
     9.8 +Multithreading in Poly/ML (cf. polyml/basis/Thread.sml).
     9.9  *)
    9.10  
    9.11 +signature BASIC_MULTITHREADING =
    9.12 +sig
    9.13 +  val interruptible: ('a -> 'b) -> 'a -> 'b
    9.14 +  val uninterruptible: ((('c -> 'd) -> 'c -> 'd) -> 'a -> 'b) -> 'a -> 'b
    9.15 +end;
    9.16 +
    9.17  signature MULTITHREADING =
    9.18  sig
    9.19 -  val available: bool
    9.20 -  val max_threads_value: unit -> int
    9.21 -  val max_threads_update: int -> unit
    9.22 -  val max_threads_setmp: int -> ('a -> 'b) -> 'a -> 'b
    9.23 -  val enabled: unit -> bool
    9.24 +  include BASIC_MULTITHREADING
    9.25    val no_interrupts: Thread.threadAttribute list
    9.26    val public_interrupts: Thread.threadAttribute list
    9.27    val private_interrupts: Thread.threadAttribute list
    9.28    val sync_interrupts: Thread.threadAttribute list -> Thread.threadAttribute list
    9.29    val interrupted: unit -> unit  (*exception Interrupt*)
    9.30    val with_attributes: Thread.threadAttribute list -> (Thread.threadAttribute list -> 'a) -> 'a
    9.31 +  val max_threads_value: unit -> int
    9.32 +  val max_threads_update: int -> unit
    9.33 +  val max_threads_setmp: int -> ('a -> 'b) -> 'a -> 'b
    9.34 +  val enabled: unit -> bool
    9.35    val sync_wait: Thread.threadAttribute list option -> Time.time option ->
    9.36      ConditionVar.conditionVar -> Mutex.mutex -> bool Exn.result
    9.37    val trace: int ref
    9.38 @@ -30,46 +36,156 @@
    9.39  structure Multithreading: MULTITHREADING =
    9.40  struct
    9.41  
    9.42 +(* thread attributes *)
    9.43 +
    9.44 +val no_interrupts =
    9.45 +  [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptDefer];
    9.46 +
    9.47 +val test_interrupts =
    9.48 +  [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptSynch];
    9.49 +
    9.50 +val public_interrupts =
    9.51 +  [Thread.EnableBroadcastInterrupt true, Thread.InterruptState Thread.InterruptAsynchOnce];
    9.52 +
    9.53 +val private_interrupts =
    9.54 +  [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptAsynchOnce];
    9.55 +
    9.56 +val sync_interrupts = map
    9.57 +  (fn x as Thread.InterruptState Thread.InterruptDefer => x
    9.58 +    | Thread.InterruptState _ => Thread.InterruptState Thread.InterruptSynch
    9.59 +    | x => x);
    9.60 +
    9.61 +val safe_interrupts = map
    9.62 +  (fn Thread.InterruptState Thread.InterruptAsynch =>
    9.63 +      Thread.InterruptState Thread.InterruptAsynchOnce
    9.64 +    | x => x);
    9.65 +
    9.66 +fun interrupted () =
    9.67 +  let
    9.68 +    val orig_atts = safe_interrupts (Thread.getAttributes ());
    9.69 +    val _ = Thread.setAttributes test_interrupts;
    9.70 +    val test = Exn.capture Thread.testInterrupt ();
    9.71 +    val _ = Thread.setAttributes orig_atts;
    9.72 +  in Exn.release test end;
    9.73 +
    9.74 +fun with_attributes new_atts e =
    9.75 +  let
    9.76 +    val orig_atts = safe_interrupts (Thread.getAttributes ());
    9.77 +    val result = Exn.capture (fn () =>
    9.78 +      (Thread.setAttributes (safe_interrupts new_atts); e orig_atts)) ();
    9.79 +    val _ = Thread.setAttributes orig_atts;
    9.80 +  in Exn.release result end;
    9.81 +
    9.82 +
    9.83 +(* portable wrappers *)
    9.84 +
    9.85 +fun interruptible f x = with_attributes public_interrupts (fn _ => f x);
    9.86 +
    9.87 +fun uninterruptible f x =
    9.88 +  with_attributes no_interrupts (fn atts =>
    9.89 +    f (fn g => fn y => with_attributes atts (fn _ => g y)) x);
    9.90 +
    9.91 +
    9.92  (* options *)
    9.93  
    9.94 -val available = false;
    9.95 -fun max_threads_value () = 1: int;
    9.96 -fun max_threads_update _ = ();
    9.97 -fun max_threads_setmp _ f x = f x;
    9.98 -fun enabled () = false;
    9.99 +fun max_threads_result m =
   9.100 +  if m > 0 then m else Int.min (Int.max (Thread.numProcessors (), 1), 8);
   9.101  
   9.102 +val max_threads = ref 1;
   9.103  
   9.104 -(* attributes *)
   9.105 +fun max_threads_value () = ! max_threads;
   9.106  
   9.107 -val no_interrupts = [];
   9.108 -val public_interrupts = [];
   9.109 -val private_interrupts = [];
   9.110 -fun sync_interrupts _ = [];
   9.111 +fun max_threads_update m = max_threads := max_threads_result m;
   9.112  
   9.113 -fun interrupted () = ();
   9.114 +fun max_threads_setmp m f x =
   9.115 +  uninterruptible (fn restore_attributes => fn () =>
   9.116 +    let
   9.117 +      val max_threads_orig = ! max_threads;
   9.118 +      val _ = max_threads_update m;
   9.119 +      val result = Exn.capture (restore_attributes f) x;
   9.120 +      val _ = max_threads := max_threads_orig;
   9.121 +    in Exn.release result end) ();
   9.122  
   9.123 -fun with_attributes _ e = e [];
   9.124 +fun enabled () = max_threads_value () > 1;
   9.125  
   9.126 -fun sync_wait _ _ _ _ = Exn.Res true;
   9.127 +
   9.128 +(* synchronous wait *)
   9.129 +
   9.130 +fun sync_wait opt_atts time cond lock =
   9.131 +  with_attributes
   9.132 +    (sync_interrupts (case opt_atts of SOME atts => atts | NONE => Thread.getAttributes ()))
   9.133 +    (fn _ =>
   9.134 +      (case time of
   9.135 +        SOME t => Exn.Res (ConditionVar.waitUntil (cond, lock, t))
   9.136 +      | NONE => (ConditionVar.wait (cond, lock); Exn.Res true))
   9.137 +      handle exn => Exn.Exn exn);
   9.138  
   9.139  
   9.140  (* tracing *)
   9.141  
   9.142 -val trace = ref (0: int);
   9.143 -fun tracing _ _ = ();
   9.144 -fun tracing_time _ _ _ = ();
   9.145 -fun real_time f x = (f x; Time.zeroTime);
   9.146 +val trace = ref 0;
   9.147 +
   9.148 +fun tracing level msg =
   9.149 +  if level > ! trace then ()
   9.150 +  else uninterruptible (fn _ => fn () =>
   9.151 +    (TextIO.output (TextIO.stdErr, (">>> " ^ msg () ^ "\n")); TextIO.flushOut TextIO.stdErr)
   9.152 +      handle _ (*sic*) => ()) ();
   9.153 +
   9.154 +fun tracing_time detailed time =
   9.155 +  tracing
   9.156 +   (if not detailed then 5
   9.157 +    else if Time.>= (time, seconds 1.0) then 1
   9.158 +    else if Time.>= (time, seconds 0.1) then 2
   9.159 +    else if Time.>= (time, seconds 0.01) then 3
   9.160 +    else if Time.>= (time, seconds 0.001) then 4 else 5);
   9.161 +
   9.162 +fun real_time f x =
   9.163 +  let
   9.164 +    val timer = Timer.startRealTimer ();
   9.165 +    val () = f x;
   9.166 +    val time = Timer.checkRealTimer timer;
   9.167 +  in time end;
   9.168  
   9.169  
   9.170  (* synchronized evaluation *)
   9.171  
   9.172 -fun synchronized _ _ e = e ();
   9.173 +fun synchronized name lock e =
   9.174 +  Exn.release (uninterruptible (fn restore_attributes => fn () =>
   9.175 +    let
   9.176 +      val immediate =
   9.177 +        if Mutex.trylock lock then true
   9.178 +        else
   9.179 +          let
   9.180 +            val _ = tracing 5 (fn () => name ^ ": locking ...");
   9.181 +            val time = real_time Mutex.lock lock;
   9.182 +            val _ = tracing_time true time (fn () => name ^ ": locked after " ^ Time.toString time);
   9.183 +          in false end;
   9.184 +      val result = Exn.capture (restore_attributes e) ();
   9.185 +      val _ = if immediate then () else tracing 5 (fn () => name ^ ": unlocking ...");
   9.186 +      val _ = Mutex.unlock lock;
   9.187 +    in result end) ());
   9.188  
   9.189  
   9.190  (* serial numbers *)
   9.191  
   9.192 -local val count = ref (0: int)
   9.193 -in fun serial () = (count := ! count + 1; ! count) end;
   9.194 +local
   9.195 +
   9.196 +val serial_lock = Mutex.mutex ();
   9.197 +val serial_count = ref 0;
   9.198 +
   9.199 +in
   9.200 +
   9.201 +val serial = uninterruptible (fn _ => fn () =>
   9.202 +  let
   9.203 +    val _ = Mutex.lock serial_lock;
   9.204 +    val _ = serial_count := ! serial_count + 1;
   9.205 +    val res = ! serial_count;
   9.206 +    val _ = Mutex.unlock serial_lock;
   9.207 +  in res end);
   9.208  
   9.209  end;
   9.210  
   9.211 +end;
   9.212 +
   9.213 +structure Basic_Multithreading: BASIC_MULTITHREADING = Multithreading;
   9.214 +open Basic_Multithreading;
    10.1 --- a/src/Pure/RAW/multithreading_polyml.ML	Wed Feb 17 23:29:35 2016 +0100
    10.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.3 @@ -1,172 +0,0 @@
    10.4 -(*  Title:      Pure/RAW/multithreading_polyml.ML
    10.5 -    Author:     Makarius
    10.6 -
    10.7 -Multithreading in Poly/ML (cf. polyml/basis/Thread.sml).
    10.8 -*)
    10.9 -
   10.10 -signature MULTITHREADING =
   10.11 -sig
   10.12 -  include MULTITHREADING
   10.13 -  val interruptible: ('a -> 'b) -> 'a -> 'b
   10.14 -  val uninterruptible: ((('c -> 'd) -> 'c -> 'd) -> 'a -> 'b) -> 'a -> 'b
   10.15 -end;
   10.16 -
   10.17 -structure Multithreading: MULTITHREADING =
   10.18 -struct
   10.19 -
   10.20 -(* thread attributes *)
   10.21 -
   10.22 -val no_interrupts =
   10.23 -  [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptDefer];
   10.24 -
   10.25 -val test_interrupts =
   10.26 -  [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptSynch];
   10.27 -
   10.28 -val public_interrupts =
   10.29 -  [Thread.EnableBroadcastInterrupt true, Thread.InterruptState Thread.InterruptAsynchOnce];
   10.30 -
   10.31 -val private_interrupts =
   10.32 -  [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptAsynchOnce];
   10.33 -
   10.34 -val sync_interrupts = map
   10.35 -  (fn x as Thread.InterruptState Thread.InterruptDefer => x
   10.36 -    | Thread.InterruptState _ => Thread.InterruptState Thread.InterruptSynch
   10.37 -    | x => x);
   10.38 -
   10.39 -val safe_interrupts = map
   10.40 -  (fn Thread.InterruptState Thread.InterruptAsynch =>
   10.41 -      Thread.InterruptState Thread.InterruptAsynchOnce
   10.42 -    | x => x);
   10.43 -
   10.44 -fun interrupted () =
   10.45 -  let
   10.46 -    val orig_atts = safe_interrupts (Thread.getAttributes ());
   10.47 -    val _ = Thread.setAttributes test_interrupts;
   10.48 -    val test = Exn.capture Thread.testInterrupt ();
   10.49 -    val _ = Thread.setAttributes orig_atts;
   10.50 -  in Exn.release test end;
   10.51 -
   10.52 -fun with_attributes new_atts e =
   10.53 -  let
   10.54 -    val orig_atts = safe_interrupts (Thread.getAttributes ());
   10.55 -    val result = Exn.capture (fn () =>
   10.56 -      (Thread.setAttributes (safe_interrupts new_atts); e orig_atts)) ();
   10.57 -    val _ = Thread.setAttributes orig_atts;
   10.58 -  in Exn.release result end;
   10.59 -
   10.60 -
   10.61 -(* portable wrappers *)
   10.62 -
   10.63 -fun interruptible f x = with_attributes public_interrupts (fn _ => f x);
   10.64 -
   10.65 -fun uninterruptible f x =
   10.66 -  with_attributes no_interrupts (fn atts =>
   10.67 -    f (fn g => fn y => with_attributes atts (fn _ => g y)) x);
   10.68 -
   10.69 -
   10.70 -(* options *)
   10.71 -
   10.72 -val available = true;
   10.73 -
   10.74 -fun max_threads_result m =
   10.75 -  if m > 0 then m else Int.min (Int.max (Thread.numProcessors (), 1), 8);
   10.76 -
   10.77 -val max_threads = ref 1;
   10.78 -
   10.79 -fun max_threads_value () = ! max_threads;
   10.80 -
   10.81 -fun max_threads_update m = max_threads := max_threads_result m;
   10.82 -
   10.83 -fun max_threads_setmp m f x =
   10.84 -  uninterruptible (fn restore_attributes => fn () =>
   10.85 -    let
   10.86 -      val max_threads_orig = ! max_threads;
   10.87 -      val _ = max_threads_update m;
   10.88 -      val result = Exn.capture (restore_attributes f) x;
   10.89 -      val _ = max_threads := max_threads_orig;
   10.90 -    in Exn.release result end) ();
   10.91 -
   10.92 -fun enabled () = max_threads_value () > 1;
   10.93 -
   10.94 -
   10.95 -(* synchronous wait *)
   10.96 -
   10.97 -fun sync_wait opt_atts time cond lock =
   10.98 -  with_attributes
   10.99 -    (sync_interrupts (case opt_atts of SOME atts => atts | NONE => Thread.getAttributes ()))
  10.100 -    (fn _ =>
  10.101 -      (case time of
  10.102 -        SOME t => Exn.Res (ConditionVar.waitUntil (cond, lock, t))
  10.103 -      | NONE => (ConditionVar.wait (cond, lock); Exn.Res true))
  10.104 -      handle exn => Exn.Exn exn);
  10.105 -
  10.106 -
  10.107 -(* tracing *)
  10.108 -
  10.109 -val trace = ref 0;
  10.110 -
  10.111 -fun tracing level msg =
  10.112 -  if level > ! trace then ()
  10.113 -  else uninterruptible (fn _ => fn () =>
  10.114 -    (TextIO.output (TextIO.stdErr, (">>> " ^ msg () ^ "\n")); TextIO.flushOut TextIO.stdErr)
  10.115 -      handle _ (*sic*) => ()) ();
  10.116 -
  10.117 -fun tracing_time detailed time =
  10.118 -  tracing
  10.119 -   (if not detailed then 5
  10.120 -    else if Time.>= (time, seconds 1.0) then 1
  10.121 -    else if Time.>= (time, seconds 0.1) then 2
  10.122 -    else if Time.>= (time, seconds 0.01) then 3
  10.123 -    else if Time.>= (time, seconds 0.001) then 4 else 5);
  10.124 -
  10.125 -fun real_time f x =
  10.126 -  let
  10.127 -    val timer = Timer.startRealTimer ();
  10.128 -    val () = f x;
  10.129 -    val time = Timer.checkRealTimer timer;
  10.130 -  in time end;
  10.131 -
  10.132 -
  10.133 -(* synchronized evaluation *)
  10.134 -
  10.135 -fun synchronized name lock e =
  10.136 -  Exn.release (uninterruptible (fn restore_attributes => fn () =>
  10.137 -    let
  10.138 -      val immediate =
  10.139 -        if Mutex.trylock lock then true
  10.140 -        else
  10.141 -          let
  10.142 -            val _ = tracing 5 (fn () => name ^ ": locking ...");
  10.143 -            val time = real_time Mutex.lock lock;
  10.144 -            val _ = tracing_time true time (fn () => name ^ ": locked after " ^ Time.toString time);
  10.145 -          in false end;
  10.146 -      val result = Exn.capture (restore_attributes e) ();
  10.147 -      val _ = if immediate then () else tracing 5 (fn () => name ^ ": unlocking ...");
  10.148 -      val _ = Mutex.unlock lock;
  10.149 -    in result end) ());
  10.150 -
  10.151 -
  10.152 -(* serial numbers *)
  10.153 -
  10.154 -local
  10.155 -
  10.156 -val serial_lock = Mutex.mutex ();
  10.157 -val serial_count = ref 0;
  10.158 -
  10.159 -in
  10.160 -
  10.161 -val serial = uninterruptible (fn _ => fn () =>
  10.162 -  let
  10.163 -    val _ = Mutex.lock serial_lock;
  10.164 -    val _ = serial_count := ! serial_count + 1;
  10.165 -    val res = ! serial_count;
  10.166 -    val _ = Mutex.unlock serial_lock;
  10.167 -  in res end);
  10.168 -
  10.169 -end;
  10.170 -
  10.171 -end;
  10.172 -
  10.173 -val interruptible = Multithreading.interruptible;
  10.174 -val uninterruptible = Multithreading.uninterruptible;
  10.175 -
    11.1 --- a/src/Pure/ROOT	Wed Feb 17 23:29:35 2016 +0100
    11.2 +++ b/src/Pure/ROOT	Thu Feb 18 23:10:28 2016 +0100
    11.3 @@ -25,7 +25,6 @@
    11.4      "RAW/ml_stack_polyml-5.6.ML"
    11.5      "RAW/ml_system.ML"
    11.6      "RAW/multithreading.ML"
    11.7 -    "RAW/multithreading_polyml.ML"
    11.8      "RAW/share_common_data_polyml-5.3.0.ML"
    11.9      "RAW/single_assignment_polyml.ML"
   11.10      "RAW/unsynchronized.ML"
   11.11 @@ -57,7 +56,6 @@
   11.12      "RAW/ml_stack_polyml-5.6.ML"
   11.13      "RAW/ml_system.ML"
   11.14      "RAW/multithreading.ML"
   11.15 -    "RAW/multithreading_polyml.ML"
   11.16      "RAW/share_common_data_polyml-5.3.0.ML"
   11.17      "RAW/single_assignment_polyml.ML"
   11.18      "RAW/unsynchronized.ML"
   11.19 @@ -65,24 +63,19 @@
   11.20      "RAW/windows_path.ML"
   11.21  
   11.22      "Concurrent/bash.ML"
   11.23 -    "Concurrent/bash_sequential.ML"
   11.24      "Concurrent/bash_windows.ML"
   11.25      "Concurrent/cache.ML"
   11.26      "Concurrent/counter.ML"
   11.27      "Concurrent/event_timer.ML"
   11.28      "Concurrent/future.ML"
   11.29      "Concurrent/lazy.ML"
   11.30 -    "Concurrent/lazy_sequential.ML"
   11.31      "Concurrent/mailbox.ML"
   11.32      "Concurrent/par_exn.ML"
   11.33      "Concurrent/par_list.ML"
   11.34 -    "Concurrent/par_list_sequential.ML"
   11.35      "Concurrent/random.ML"
   11.36      "Concurrent/single_assignment.ML"
   11.37 -    "Concurrent/single_assignment_sequential.ML"
   11.38      "Concurrent/standard_thread.ML"
   11.39      "Concurrent/synchronized.ML"
   11.40 -    "Concurrent/synchronized_sequential.ML"
   11.41      "Concurrent/task_queue.ML"
   11.42      "Concurrent/time_limit.ML"
   11.43      "General/alist.ML"
    12.1 --- a/src/Pure/ROOT.ML	Wed Feb 17 23:29:35 2016 +0100
    12.2 +++ b/src/Pure/ROOT.ML	Thu Feb 18 23:10:28 2016 +0100
    12.3 @@ -19,8 +19,6 @@
    12.4  use "General/table.ML";
    12.5  
    12.6  use "Concurrent/synchronized.ML";
    12.7 -if Multithreading.available then ()
    12.8 -else use "Concurrent/synchronized_sequential.ML";
    12.9  use "Concurrent/counter.ML";
   12.10  use "Concurrent/random.ML";
   12.11  
   12.12 @@ -106,13 +104,10 @@
   12.13  else use "ML/ml_statistics_dummy.ML";
   12.14  
   12.15  use "Concurrent/standard_thread.ML";
   12.16 +use "Concurrent/single_assignment.ML";
   12.17  
   12.18 -use "Concurrent/single_assignment.ML";
   12.19 -if Multithreading.available then ()
   12.20 -else use "Concurrent/single_assignment_sequential.ML";
   12.21 -
   12.22 -if not Multithreading.available then use "Concurrent/bash_sequential.ML"
   12.23 -else if ML_System.platform_is_windows then use "Concurrent/bash_windows.ML"
   12.24 +if ML_System.platform_is_windows
   12.25 +then use "Concurrent/bash_windows.ML"
   12.26  else use "Concurrent/bash.ML";
   12.27  
   12.28  use "Concurrent/par_exn.ML";
   12.29 @@ -120,14 +115,8 @@
   12.30  use "Concurrent/future.ML";
   12.31  use "Concurrent/event_timer.ML";
   12.32  use "Concurrent/time_limit.ML";
   12.33 -
   12.34  use "Concurrent/lazy.ML";
   12.35 -if Multithreading.available then ()
   12.36 -else use "Concurrent/lazy_sequential.ML";
   12.37 -
   12.38  use "Concurrent/par_list.ML";
   12.39 -if Multithreading.available then ()
   12.40 -else use "Concurrent/par_list_sequential.ML";
   12.41  
   12.42  use "Concurrent/mailbox.ML";
   12.43  use "Concurrent/cache.ML";
    13.1 --- a/src/Pure/System/message_channel.ML	Wed Feb 17 23:29:35 2016 +0100
    13.2 +++ b/src/Pure/System/message_channel.ML	Thu Feb 18 23:10:28 2016 +0100
    13.3 @@ -56,20 +56,14 @@
    13.4    in fn () => continue NONE end;
    13.5  
    13.6  fun make channel =
    13.7 -  if Multithreading.available then
    13.8 -    let
    13.9 -      val mbox = Mailbox.create ();
   13.10 -      val thread =
   13.11 -        Standard_Thread.fork {name = "channel", stack_limit = NONE, interrupts = false}
   13.12 -          (message_output mbox channel);
   13.13 -      fun send msg = Mailbox.send mbox (SOME msg);
   13.14 -      fun shutdown () =
   13.15 -        (Mailbox.send mbox NONE; Mailbox.await_empty mbox; Standard_Thread.join thread);
   13.16 -    in Message_Channel {send = send, shutdown = shutdown} end
   13.17 -  else
   13.18 -    let
   13.19 -      fun send msg = (output_message channel msg; flush channel);
   13.20 -    in Message_Channel {send = send, shutdown = fn () => ()} end;
   13.21 +  let
   13.22 +    val mbox = Mailbox.create ();
   13.23 +    val thread =
   13.24 +      Standard_Thread.fork {name = "channel", stack_limit = NONE, interrupts = false}
   13.25 +        (message_output mbox channel);
   13.26 +    fun send msg = Mailbox.send mbox (SOME msg);
   13.27 +    fun shutdown () =
   13.28 +      (Mailbox.send mbox NONE; Mailbox.await_empty mbox; Standard_Thread.join thread);
   13.29 +  in Message_Channel {send = send, shutdown = shutdown} end;
   13.30  
   13.31  end;
   13.32 -