src/Pure/ML-Systems/multithreading_polyml.ML
changeset 26098 b59d33f73aed
parent 26083 abb3f8dd66dc
child 26221 e557c20158e2
     1.1 --- a/src/Pure/ML-Systems/multithreading_polyml.ML	Tue Feb 19 20:34:29 2008 +0100
     1.2 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Tue Feb 19 20:34:30 2008 +0100
     1.3 @@ -11,6 +11,7 @@
     1.4  sig
     1.5    val interruptible: ('a -> 'b) -> 'a -> 'b
     1.6    val uninterruptible: ((('c -> 'd) -> 'c -> 'd) -> 'a -> 'b) -> 'a -> 'b
     1.7 +  val system_out: string -> string * int
     1.8    structure TimeLimit: TIME_LIMIT
     1.9  end;
    1.10  
    1.11 @@ -58,6 +59,14 @@
    1.12  fun show "" = "" | show name = " " ^ name;
    1.13  fun show' "" = "" | show' name = " [" ^ name ^ "]";
    1.14  
    1.15 +fun read_file name =
    1.16 +  let val is = TextIO.openIn name
    1.17 +  in TextIO.inputAll is before TextIO.closeIn is end;
    1.18 +
    1.19 +fun write_file name txt =
    1.20 +  let val os = TextIO.openOut name
    1.21 +  in TextIO.output (os, txt) before TextIO.closeOut os end;
    1.22 +
    1.23  
    1.24  (* thread attributes *)
    1.25  
    1.26 @@ -111,6 +120,70 @@
    1.27  end;
    1.28  
    1.29  
    1.30 +(* system shell processes, with propagation of interrupts *)
    1.31 +
    1.32 +fun system_out script = uninterruptible (fn restore_attributes => fn () =>
    1.33 +  let
    1.34 +    val script_name = OS.FileSys.tmpName ();
    1.35 +    val _ = write_file script_name script;
    1.36 +
    1.37 +    val pid_name = OS.FileSys.tmpName ();
    1.38 +    val output_name = OS.FileSys.tmpName ();
    1.39 +
    1.40 +    (*result state*)
    1.41 +    datatype result = Wait | Signal | Result of int;
    1.42 +    val result = ref Wait;
    1.43 +    val result_mutex = Mutex.mutex ();
    1.44 +    val result_cond = ConditionVar.conditionVar ();
    1.45 +    fun set_result res =
    1.46 +      (Mutex.lock result_mutex; result := res; Mutex.unlock result_mutex;
    1.47 +        ConditionVar.signal result_cond);
    1.48 +
    1.49 +    val _ = Mutex.lock result_mutex;
    1.50 +
    1.51 +    (*system thread*)
    1.52 +    val system_thread = Thread.fork (fn () =>
    1.53 +      let
    1.54 +        val status =
    1.55 +          OS.Process.system ("perl -w \"$ISABELLE_HOME/lib/scripts/system.pl\" group " ^
    1.56 +            script_name ^ " " ^ pid_name ^ " " ^ output_name);
    1.57 +        val res =
    1.58 +          (case Posix.Process.fromStatus status of
    1.59 +            Posix.Process.W_EXITED => Result 0
    1.60 +          | Posix.Process.W_EXITSTATUS 0wx82 => Signal
    1.61 +          | Posix.Process.W_EXITSTATUS w => Result (Word8.toInt w)
    1.62 +          | Posix.Process.W_SIGNALED s =>
    1.63 +              if s = Posix.Signal.int then Signal
    1.64 +              else Result (256 + LargeWord.toInt (Posix.Signal.toWord s))
    1.65 +          | Posix.Process.W_STOPPED s => Result (512 + LargeWord.toInt (Posix.Signal.toWord s)));
    1.66 +      in set_result res end handle _ => set_result (Result 2), []);
    1.67 +
    1.68 +    (*main thread -- proxy for interrupts*)
    1.69 +    fun kill n =
    1.70 +      (case Int.fromString (read_file pid_name) of
    1.71 +        SOME pid =>
    1.72 +          Posix.Process.kill
    1.73 +            (Posix.Process.K_GROUP (Posix.Process.wordToPid (LargeWord.fromInt pid)),
    1.74 +              Posix.Signal.int)
    1.75 +      | NONE => ())
    1.76 +      handle OS.SysErr _ => () | IO.Io _ =>
    1.77 +        (OS.Process.sleep (Time.fromMilliseconds 100); if n > 0 then kill (n - 1) else ());
    1.78 +
    1.79 +    val _ = while ! result = Wait do
    1.80 +      restore_attributes (fn () =>
    1.81 +        (ConditionVar.waitUntil (result_cond, result_mutex, Time.now () + Time.fromMilliseconds 100); ())
    1.82 +          handle Interrupt => kill 10) ();
    1.83 +
    1.84 +    (*cleanup*)
    1.85 +    val output = read_file output_name handle IO.Io _ => "";
    1.86 +    val _ = OS.FileSys.remove script_name handle OS.SysErr _ => ();
    1.87 +    val _ = OS.FileSys.remove pid_name handle OS.SysErr _ => ();
    1.88 +    val _ = OS.FileSys.remove output_name handle OS.SysErr _ => ();
    1.89 +    val _ = Thread.interrupt system_thread handle Thread _ => ();
    1.90 +    val rc = (case ! result of Signal => raise Interrupt | Result rc => rc);
    1.91 +  in (output, rc) end) ();
    1.92 +
    1.93 +
    1.94  (* critical section -- may be nested within the same thread *)
    1.95  
    1.96  local