src/Pure/ML-Systems/multithreading_polyml.ML
changeset 32295 400cc493d466
parent 32286 1fb5db48002d
child 32738 15bb09ca0378
     1.1 --- a/src/Pure/ML-Systems/multithreading_polyml.ML	Thu Jul 30 23:50:11 2009 +0200
     1.2 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Sat Aug 01 00:09:45 2009 +0200
     1.3 @@ -27,31 +27,6 @@
     1.4  structure Multithreading: MULTITHREADING =
     1.5  struct
     1.6  
     1.7 -(* tracing *)
     1.8 -
     1.9 -val trace = ref 0;
    1.10 -
    1.11 -fun tracing level msg =
    1.12 -  if level > ! trace then ()
    1.13 -  else (TextIO.output (TextIO.stdErr, (">>> " ^ msg () ^ "\n")); TextIO.flushOut TextIO.stdErr)
    1.14 -    handle _ (*sic*) => ();
    1.15 -
    1.16 -fun tracing_time detailed time =
    1.17 -  tracing
    1.18 -   (if not detailed then 5
    1.19 -    else if Time.>= (time, Time.fromMilliseconds 1000) then 1
    1.20 -    else if Time.>= (time, Time.fromMilliseconds 100) then 2
    1.21 -    else if Time.>= (time, Time.fromMilliseconds 10) then 3
    1.22 -    else if Time.>= (time, Time.fromMilliseconds 1) then 4 else 5);
    1.23 -
    1.24 -fun real_time f x =
    1.25 -  let
    1.26 -    val timer = Timer.startRealTimer ();
    1.27 -    val () = f x;
    1.28 -    val time = Timer.checkRealTimer timer;
    1.29 -  in time end;
    1.30 -
    1.31 -
    1.32  (* options *)
    1.33  
    1.34  val available = true;
    1.35 @@ -91,57 +66,76 @@
    1.36  val no_interrupts =
    1.37    [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptDefer];
    1.38  
    1.39 -val regular_interrupts =
    1.40 +val public_interrupts =
    1.41    [Thread.EnableBroadcastInterrupt true, Thread.InterruptState Thread.InterruptAsynchOnce];
    1.42  
    1.43 -val restricted_interrupts =
    1.44 +val private_interrupts =
    1.45    [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptAsynchOnce];
    1.46  
    1.47 +val sync_interrupts = map
    1.48 +  (fn x as Thread.InterruptState Thread.InterruptDefer => x
    1.49 +    | Thread.InterruptState _ => Thread.InterruptState Thread.InterruptSynch
    1.50 +    | x => x);
    1.51 +
    1.52  val safe_interrupts = map
    1.53    (fn Thread.InterruptState Thread.InterruptAsynch =>
    1.54        Thread.InterruptState Thread.InterruptAsynchOnce
    1.55      | x => x);
    1.56  
    1.57 -fun with_attributes new_atts f x =
    1.58 +fun with_attributes new_atts e =
    1.59    let
    1.60      val orig_atts = safe_interrupts (Thread.getAttributes ());
    1.61      val result = Exn.capture (fn () =>
    1.62 -      (Thread.setAttributes (safe_interrupts new_atts); f orig_atts x)) ();
    1.63 +      (Thread.setAttributes (safe_interrupts new_atts); e orig_atts)) ();
    1.64      val _ = Thread.setAttributes orig_atts;
    1.65    in Exn.release result end;
    1.66  
    1.67  
    1.68 -(* regular interruptibility *)
    1.69 +(* portable wrappers *)
    1.70 +
    1.71 +fun interruptible f x = with_attributes public_interrupts (fn _ => f x);
    1.72  
    1.73 -fun interruptible f x =
    1.74 -  (Thread.testInterrupt (); with_attributes regular_interrupts (fn _ => fn x => f x) x);
    1.75 -
    1.76 -fun uninterruptible f =
    1.77 -  with_attributes no_interrupts (fn atts => fn x =>
    1.78 -    f (fn g => with_attributes atts (fn _ => fn y => g y)) x);
    1.79 +fun uninterruptible f x =
    1.80 +  with_attributes no_interrupts (fn atts =>
    1.81 +    f (fn g => fn y => with_attributes atts (fn _ => g y)) x);
    1.82  
    1.83  
    1.84  (* synchronous wait *)
    1.85  
    1.86 -fun sync_attributes e =
    1.87 +fun sync_wait opt_atts time cond lock =
    1.88 +  with_attributes
    1.89 +    (sync_interrupts (case opt_atts of SOME atts => atts | NONE => Thread.getAttributes ()))
    1.90 +    (fn _ =>
    1.91 +      (case time of
    1.92 +        SOME t => Exn.Result (ConditionVar.waitUntil (cond, lock, t))
    1.93 +      | NONE => (ConditionVar.wait (cond, lock); Exn.Result true))
    1.94 +      handle exn => Exn.Exn exn);
    1.95 +
    1.96 +
    1.97 +(* tracing *)
    1.98 +
    1.99 +val trace = ref 0;
   1.100 +
   1.101 +fun tracing level msg =
   1.102 +  if level > ! trace then ()
   1.103 +  else uninterruptible (fn _ => fn () =>
   1.104 +    (TextIO.output (TextIO.stdErr, (">>> " ^ msg () ^ "\n")); TextIO.flushOut TextIO.stdErr)
   1.105 +      handle _ (*sic*) => ()) ();
   1.106 +
   1.107 +fun tracing_time detailed time =
   1.108 +  tracing
   1.109 +   (if not detailed then 5
   1.110 +    else if Time.>= (time, Time.fromMilliseconds 1000) then 1
   1.111 +    else if Time.>= (time, Time.fromMilliseconds 100) then 2
   1.112 +    else if Time.>= (time, Time.fromMilliseconds 10) then 3
   1.113 +    else if Time.>= (time, Time.fromMilliseconds 1) then 4 else 5);
   1.114 +
   1.115 +fun real_time f x =
   1.116    let
   1.117 -    val orig_atts = Thread.getAttributes ();
   1.118 -    val broadcast =
   1.119 -      (case List.find (fn Thread.EnableBroadcastInterrupt _ => true | _ => false) orig_atts of
   1.120 -        NONE => Thread.EnableBroadcastInterrupt false
   1.121 -      | SOME att => att);
   1.122 -    val interrupt_state =
   1.123 -      (case List.find (fn Thread.InterruptState _ => true | _ => false) orig_atts of
   1.124 -        NONE => Thread.InterruptState Thread.InterruptDefer
   1.125 -      | SOME (state as Thread.InterruptState Thread.InterruptDefer) => state
   1.126 -      | _ => Thread.InterruptState Thread.InterruptSynch);
   1.127 -  in with_attributes [broadcast, interrupt_state] (fn _ => fn () => e ()) () end;
   1.128 -
   1.129 -fun sync_wait time cond lock =
   1.130 -  sync_attributes (fn () =>
   1.131 -    (case time of
   1.132 -      SOME t => ConditionVar.waitUntil (cond, lock, t)
   1.133 -    | NONE => (ConditionVar.wait (cond, lock); true)));
   1.134 +    val timer = Timer.startRealTimer ();
   1.135 +    val () = f x;
   1.136 +    val time = Timer.checkRealTimer timer;
   1.137 +  in time end;
   1.138  
   1.139  
   1.140  (* execution with time limit *)
   1.141 @@ -169,7 +163,7 @@
   1.142  
   1.143  (* system shell processes, with propagation of interrupts *)
   1.144  
   1.145 -fun system_out script = uninterruptible (fn restore_attributes => fn () =>
   1.146 +fun system_out script = with_attributes no_interrupts (fn orig_atts =>
   1.147    let
   1.148      val script_name = OS.FileSys.tmpName ();
   1.149      val _ = write_file script_name script;
   1.150 @@ -180,13 +174,12 @@
   1.151      (*result state*)
   1.152      datatype result = Wait | Signal | Result of int;
   1.153      val result = ref Wait;
   1.154 -    val result_mutex = Mutex.mutex ();
   1.155 -    val result_cond = ConditionVar.conditionVar ();
   1.156 +    val lock = Mutex.mutex ();
   1.157 +    val cond = ConditionVar.conditionVar ();
   1.158      fun set_result res =
   1.159 -      (Mutex.lock result_mutex; result := res; Mutex.unlock result_mutex;
   1.160 -        ConditionVar.signal result_cond);
   1.161 +      (Mutex.lock lock; result := res; ConditionVar.signal cond; Mutex.unlock lock);
   1.162  
   1.163 -    val _ = Mutex.lock result_mutex;
   1.164 +    val _ = Mutex.lock lock;
   1.165  
   1.166      (*system thread*)
   1.167      val system_thread = Thread.fork (fn () =>
   1.168 @@ -216,11 +209,12 @@
   1.169        handle OS.SysErr _ => () | IO.Io _ =>
   1.170          (OS.Process.sleep (Time.fromMilliseconds 100); if n > 0 then kill (n - 1) else ());
   1.171  
   1.172 -    val _ = while ! result = Wait do
   1.173 -      restore_attributes (fn () =>
   1.174 -        (ignore (sync_wait (SOME (Time.+ (Time.now (), Time.fromMilliseconds 100)))
   1.175 -            result_cond result_mutex)
   1.176 -          handle Exn.Interrupt => kill 10)) ();
   1.177 +    val _ =
   1.178 +      while ! result = Wait do
   1.179 +        let val res =
   1.180 +          sync_wait (SOME orig_atts)
   1.181 +            (SOME (Time.+ (Time.now (), Time.fromMilliseconds 100))) cond lock
   1.182 +        in case res of Exn.Exn Exn.Interrupt => kill 10 | _ => () end;
   1.183  
   1.184      (*cleanup*)
   1.185      val output = read_file output_name handle IO.Io _ => "";
   1.186 @@ -229,7 +223,7 @@
   1.187      val _ = OS.FileSys.remove output_name handle OS.SysErr _ => ();
   1.188      val _ = Thread.interrupt system_thread handle Thread _ => ();
   1.189      val rc = (case ! result of Signal => raise Exn.Interrupt | Result rc => rc);
   1.190 -  in (output, rc) end) ();
   1.191 +  in (output, rc) end);
   1.192  
   1.193  
   1.194  (* critical section -- may be nested within the same thread *)