1.1 --- a/src/Pure/Concurrent/bash.ML Sat Nov 27 16:29:53 2010 +0100
1.2 +++ b/src/Pure/Concurrent/bash.ML Sat Nov 27 19:17:55 2010 +0100
1.3 @@ -4,80 +4,67 @@
1.4 GNU bash processes, with propagation of interrupts.
1.5 *)
1.6
1.7 -local
1.8 +val bash_output = uninterruptible (fn restore_attributes => fn script =>
1.9 + let
1.10 + datatype result = Wait | Signal | Result of int;
1.11 + val result = Synchronized.var "bash_result" Wait;
1.12
1.13 -fun read_file name =
1.14 - let val is = TextIO.openIn name
1.15 - in Exn.release (Exn.capture TextIO.inputAll is before TextIO.closeIn is) end;
1.16 + val id = serial_string ();
1.17 + val script_path = File.tmp_path (Path.basic ("bash_script" ^ id));
1.18 + val output_path = File.tmp_path (Path.basic ("bash_output" ^ id));
1.19 + val pid_path = File.tmp_path (Path.basic ("bash_pid" ^ id));
1.20
1.21 -fun write_file name txt =
1.22 - let val os = TextIO.openOut name
1.23 - in Exn.release (Exn.capture TextIO.output (os, txt) before TextIO.closeOut os) end;
1.24 + val system_thread =
1.25 + Simple_Thread.fork false (fn () =>
1.26 + Multithreading.with_attributes Multithreading.private_interrupts (fn _ =>
1.27 + let
1.28 + val _ = File.write script_path script;
1.29 + val status =
1.30 + OS.Process.system
1.31 + ("exec \"$ISABELLE_HOME/lib/scripts/process\" group " ^
1.32 + File.shell_path pid_path ^ " script \"exec bash " ^
1.33 + File.shell_path script_path ^ " > " ^
1.34 + File.shell_path output_path ^ "\"");
1.35 + val res =
1.36 + (case Posix.Process.fromStatus status of
1.37 + Posix.Process.W_EXITED => Result 0
1.38 + | Posix.Process.W_EXITSTATUS 0wx82 => Signal
1.39 + | Posix.Process.W_EXITSTATUS w => Result (Word8.toInt w)
1.40 + | Posix.Process.W_SIGNALED s =>
1.41 + if s = Posix.Signal.int then Signal
1.42 + else Result (256 + LargeWord.toInt (Posix.Signal.toWord s))
1.43 + | Posix.Process.W_STOPPED s =>
1.44 + Result (512 + LargeWord.toInt (Posix.Signal.toWord s)));
1.45 + in Synchronized.change result (K res) end
1.46 + handle _ (*sic*) => Synchronized.change result (fn Wait => Signal | res => res)));
1.47
1.48 -in
1.49 + fun cleanup () =
1.50 + (Simple_Thread.interrupt system_thread;
1.51 + try File.rm script_path;
1.52 + try File.rm output_path;
1.53 + try File.rm pid_path);
1.54
1.55 -fun bash_output script =
1.56 - Multithreading.with_attributes Multithreading.no_interrupts (fn orig_atts =>
1.57 + fun kill n =
1.58 + (case Int.fromString (File.read pid_path) of
1.59 + SOME pid =>
1.60 + Posix.Process.kill
1.61 + (Posix.Process.K_GROUP (Posix.Process.wordToPid (LargeWord.fromInt pid)),
1.62 + Posix.Signal.int)
1.63 + | NONE => ())
1.64 + handle OS.SysErr _ => ()
1.65 + | IO.Io _ => (OS.Process.sleep (seconds 0.1); if n > 0 then kill (n - 1) else ());
1.66 + in
1.67 let
1.68 - val script_name = OS.FileSys.tmpName ();
1.69 - val _ = write_file script_name script;
1.70 + (*proxy for interrupts*)
1.71 + val _ =
1.72 + restore_attributes (fn () =>
1.73 + Synchronized.guarded_access result (fn Wait => NONE | x => SOME ((), x))) ()
1.74 + handle exn => (if Exn.is_interrupt exn then kill 10 else (); reraise exn);
1.75
1.76 - val pid_name = OS.FileSys.tmpName ();
1.77 - val output_name = OS.FileSys.tmpName ();
1.78 + val output = the_default "" (try File.read output_path);
1.79 + val rc = (case Synchronized.value result of Signal => Exn.interrupt () | Result rc => rc);
1.80 + val _ = cleanup ();
1.81 + in (output, rc) end
1.82 + handle exn => (cleanup (); reraise exn)
1.83 + end);
1.84
1.85 - (*result state*)
1.86 - datatype result = Wait | Signal | Result of int;
1.87 - val result = Unsynchronized.ref Wait;
1.88 - val lock = Mutex.mutex ();
1.89 - val cond = ConditionVar.conditionVar ();
1.90 - fun set_result res =
1.91 - (Mutex.lock lock; result := res; ConditionVar.signal cond; Mutex.unlock lock);
1.92 -
1.93 - val _ = Mutex.lock lock;
1.94 -
1.95 - (*system thread*)
1.96 - val system_thread = Thread.fork (fn () =>
1.97 - let
1.98 - val status =
1.99 - OS.Process.system ("exec \"$ISABELLE_HOME/lib/scripts/process\" group " ^ pid_name ^
1.100 - " script \"exec bash " ^ script_name ^ " > " ^ output_name ^ "\"");
1.101 - val res =
1.102 - (case Posix.Process.fromStatus status of
1.103 - Posix.Process.W_EXITED => Result 0
1.104 - | Posix.Process.W_EXITSTATUS 0wx82 => Signal
1.105 - | Posix.Process.W_EXITSTATUS w => Result (Word8.toInt w)
1.106 - | Posix.Process.W_SIGNALED s =>
1.107 - if s = Posix.Signal.int then Signal
1.108 - else Result (256 + LargeWord.toInt (Posix.Signal.toWord s))
1.109 - | Posix.Process.W_STOPPED s => Result (512 + LargeWord.toInt (Posix.Signal.toWord s)));
1.110 - in set_result res end handle _ (*sic*) => set_result (Result 2), []);
1.111 -
1.112 - (*main thread -- proxy for interrupts*)
1.113 - fun kill n =
1.114 - (case Int.fromString (read_file pid_name) of
1.115 - SOME pid =>
1.116 - Posix.Process.kill
1.117 - (Posix.Process.K_GROUP (Posix.Process.wordToPid (LargeWord.fromInt pid)),
1.118 - Posix.Signal.int)
1.119 - | NONE => ())
1.120 - handle OS.SysErr _ => () | IO.Io _ =>
1.121 - (OS.Process.sleep (seconds 0.1); if n > 0 then kill (n - 1) else ());
1.122 -
1.123 - val _ =
1.124 - while ! result = Wait do
1.125 - let val res =
1.126 - Multithreading.sync_wait (SOME orig_atts)
1.127 - (SOME (Time.+ (Time.now (), seconds 0.1))) cond lock
1.128 - in if Exn.is_interrupt_exn res then kill 10 else () end;
1.129 -
1.130 - (*cleanup*)
1.131 - val output = read_file output_name handle IO.Io _ => "";
1.132 - val _ = OS.FileSys.remove script_name handle OS.SysErr _ => ();
1.133 - val _ = OS.FileSys.remove pid_name handle OS.SysErr _ => ();
1.134 - val _ = OS.FileSys.remove output_name handle OS.SysErr _ => ();
1.135 - val _ = Thread.interrupt system_thread handle Thread _ => ();
1.136 - val rc = (case ! result of Signal => Exn.interrupt () | Result rc => rc);
1.137 - in (output, rc) end);
1.138 -
1.139 -end;
1.140 -
2.1 --- a/src/Pure/Concurrent/bash_sequential.ML Sat Nov 27 16:29:53 2010 +0100
2.2 +++ b/src/Pure/Concurrent/bash_sequential.ML Sat Nov 27 19:17:55 2010 +0100
2.3 @@ -5,39 +5,30 @@
2.4 could work via the controlling tty).
2.5 *)
2.6
2.7 -local
2.8 -
2.9 -fun read_file name =
2.10 - let val is = TextIO.openIn name
2.11 - in Exn.release (Exn.capture TextIO.inputAll is before TextIO.closeIn is) end;
2.12 -
2.13 -fun write_file name txt =
2.14 - let val os = TextIO.openOut name
2.15 - in Exn.release (Exn.capture TextIO.output (os, txt) before TextIO.closeOut os) end;
2.16 -
2.17 -in
2.18 -
2.19 fun bash_output script =
2.20 let
2.21 - val script_name = OS.FileSys.tmpName ();
2.22 - val _ = write_file script_name script;
2.23 + val id = serial_string ();
2.24 + val script_path = File.tmp_path (Path.basic ("bash_script" ^ id));
2.25 + val output_path = File.tmp_path (Path.basic ("bash_output" ^ id));
2.26 + fun cleanup () = (try File.rm script_path; try File.rm output_path);
2.27 + in
2.28 + let
2.29 + val _ = File.write script_path script;
2.30 + val status =
2.31 + OS.Process.system
2.32 + ("exec \"$ISABELLE_HOME/lib/scripts/process\" no_group /dev/null" ^
2.33 + " script \"exec bash " ^ File.shell_path script_path ^ " > " ^
2.34 + File.shell_path output_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 output_name = OS.FileSys.tmpName ();
2.43 + val output = the_default "" (try File.read output_path);
2.44 + val _ = cleanup ();
2.45 + in (output, rc) end
2.46 + handle exn => (cleanup (); reraise exn)
2.47 + end;
2.48
2.49 - val status =
2.50 - OS.Process.system ("exec \"$ISABELLE_HOME/lib/scripts/process\" no_group /dev/null" ^
2.51 - " script \"exec bash " ^ script_name ^ " > " ^ output_name ^ "\"");
2.52 - val rc =
2.53 - (case Posix.Process.fromStatus status of
2.54 - Posix.Process.W_EXITED => 0
2.55 - | Posix.Process.W_EXITSTATUS w => Word8.toInt w
2.56 - | Posix.Process.W_SIGNALED s => 256 + LargeWord.toInt (Posix.Signal.toWord s)
2.57 - | Posix.Process.W_STOPPED s => 512 + LargeWord.toInt (Posix.Signal.toWord s));
2.58 -
2.59 - val output = read_file output_name handle IO.Io _ => "";
2.60 - val _ = OS.FileSys.remove script_name handle OS.SysErr _ => ();
2.61 - val _ = OS.FileSys.remove output_name handle OS.SysErr _ => ();
2.62 - in (output, rc) end;
2.63 -
2.64 -end;
2.65 -