1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Pure/Concurrent/bash.ML Sat Nov 27 16:29:53 2010 +0100
1.3 @@ -0,0 +1,83 @@
1.4 +(* Title: Pure/Concurrent/bash.ML
1.5 + Author: Makarius
1.6 +
1.7 +GNU bash processes, with propagation of interrupts.
1.8 +*)
1.9 +
1.10 +local
1.11 +
1.12 +fun read_file name =
1.13 + let val is = TextIO.openIn name
1.14 + in Exn.release (Exn.capture TextIO.inputAll is before TextIO.closeIn is) end;
1.15 +
1.16 +fun write_file name txt =
1.17 + let val os = TextIO.openOut name
1.18 + in Exn.release (Exn.capture TextIO.output (os, txt) before TextIO.closeOut os) end;
1.19 +
1.20 +in
1.21 +
1.22 +fun bash_output script =
1.23 + Multithreading.with_attributes Multithreading.no_interrupts (fn orig_atts =>
1.24 + let
1.25 + val script_name = OS.FileSys.tmpName ();
1.26 + val _ = write_file script_name script;
1.27 +
1.28 + val pid_name = OS.FileSys.tmpName ();
1.29 + val output_name = OS.FileSys.tmpName ();
1.30 +
1.31 + (*result state*)
1.32 + datatype result = Wait | Signal | Result of int;
1.33 + val result = Unsynchronized.ref Wait;
1.34 + val lock = Mutex.mutex ();
1.35 + val cond = ConditionVar.conditionVar ();
1.36 + fun set_result res =
1.37 + (Mutex.lock lock; result := res; ConditionVar.signal cond; Mutex.unlock lock);
1.38 +
1.39 + val _ = Mutex.lock lock;
1.40 +
1.41 + (*system thread*)
1.42 + val system_thread = Thread.fork (fn () =>
1.43 + let
1.44 + val status =
1.45 + OS.Process.system ("exec \"$ISABELLE_HOME/lib/scripts/process\" group " ^ pid_name ^
1.46 + " script \"exec bash " ^ script_name ^ " > " ^ output_name ^ "\"");
1.47 + val res =
1.48 + (case Posix.Process.fromStatus status of
1.49 + Posix.Process.W_EXITED => Result 0
1.50 + | Posix.Process.W_EXITSTATUS 0wx82 => Signal
1.51 + | Posix.Process.W_EXITSTATUS w => Result (Word8.toInt w)
1.52 + | Posix.Process.W_SIGNALED s =>
1.53 + if s = Posix.Signal.int then Signal
1.54 + else Result (256 + LargeWord.toInt (Posix.Signal.toWord s))
1.55 + | Posix.Process.W_STOPPED s => Result (512 + LargeWord.toInt (Posix.Signal.toWord s)));
1.56 + in set_result res end handle _ (*sic*) => set_result (Result 2), []);
1.57 +
1.58 + (*main thread -- proxy for interrupts*)
1.59 + fun kill n =
1.60 + (case Int.fromString (read_file pid_name) of
1.61 + SOME pid =>
1.62 + Posix.Process.kill
1.63 + (Posix.Process.K_GROUP (Posix.Process.wordToPid (LargeWord.fromInt pid)),
1.64 + Posix.Signal.int)
1.65 + | NONE => ())
1.66 + handle OS.SysErr _ => () | IO.Io _ =>
1.67 + (OS.Process.sleep (seconds 0.1); if n > 0 then kill (n - 1) else ());
1.68 +
1.69 + val _ =
1.70 + while ! result = Wait do
1.71 + let val res =
1.72 + Multithreading.sync_wait (SOME orig_atts)
1.73 + (SOME (Time.+ (Time.now (), seconds 0.1))) cond lock
1.74 + in if Exn.is_interrupt_exn res then kill 10 else () end;
1.75 +
1.76 + (*cleanup*)
1.77 + val output = read_file output_name handle IO.Io _ => "";
1.78 + val _ = OS.FileSys.remove script_name handle OS.SysErr _ => ();
1.79 + val _ = OS.FileSys.remove pid_name handle OS.SysErr _ => ();
1.80 + val _ = OS.FileSys.remove output_name handle OS.SysErr _ => ();
1.81 + val _ = Thread.interrupt system_thread handle Thread _ => ();
1.82 + val rc = (case ! result of Signal => Exn.interrupt () | Result rc => rc);
1.83 + in (output, rc) end);
1.84 +
1.85 +end;
1.86 +
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/src/Pure/Concurrent/bash_sequential.ML Sat Nov 27 16:29:53 2010 +0100
2.3 @@ -0,0 +1,43 @@
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 +local
2.12 +
2.13 +fun read_file name =
2.14 + let val is = TextIO.openIn name
2.15 + in Exn.release (Exn.capture TextIO.inputAll is before TextIO.closeIn is) end;
2.16 +
2.17 +fun write_file name txt =
2.18 + let val os = TextIO.openOut name
2.19 + in Exn.release (Exn.capture TextIO.output (os, txt) before TextIO.closeOut os) end;
2.20 +
2.21 +in
2.22 +
2.23 +fun bash_output script =
2.24 + let
2.25 + val script_name = OS.FileSys.tmpName ();
2.26 + val _ = write_file script_name script;
2.27 +
2.28 + val output_name = OS.FileSys.tmpName ();
2.29 +
2.30 + val status =
2.31 + OS.Process.system ("exec \"$ISABELLE_HOME/lib/scripts/process\" no_group /dev/null" ^
2.32 + " script \"exec bash " ^ script_name ^ " > " ^ output_name ^ "\"");
2.33 + val rc =
2.34 + (case Posix.Process.fromStatus status of
2.35 + Posix.Process.W_EXITED => 0
2.36 + | Posix.Process.W_EXITSTATUS w => Word8.toInt w
2.37 + | Posix.Process.W_SIGNALED s => 256 + LargeWord.toInt (Posix.Signal.toWord s)
2.38 + | Posix.Process.W_STOPPED s => 512 + LargeWord.toInt (Posix.Signal.toWord s));
2.39 +
2.40 + val output = read_file output_name handle IO.Io _ => "";
2.41 + val _ = OS.FileSys.remove script_name handle OS.SysErr _ => ();
2.42 + val _ = OS.FileSys.remove output_name handle OS.SysErr _ => ();
2.43 + in (output, rc) end;
2.44 +
2.45 +end;
2.46 +
3.1 --- a/src/Pure/General/secure.ML Sat Nov 27 16:27:52 2010 +0100
3.2 +++ b/src/Pure/General/secure.ML Sat Nov 27 16:29:53 2010 +0100
3.3 @@ -15,8 +15,6 @@
3.4 val toplevel_pp: string list -> string -> unit
3.5 val PG_setup: unit -> unit
3.6 val commit: unit -> unit
3.7 - val bash_output: string -> string * int
3.8 - val bash: string -> int
3.9 end;
3.10
3.11 structure Secure: SECURE =
3.12 @@ -58,20 +56,6 @@
3.13 fun PG_setup () =
3.14 use_global "val change = Unsynchronized.change; structure ThyLoad = ProofGeneral.ThyLoad;";
3.15
3.16 -
3.17 -(* shell commands *)
3.18 -
3.19 -fun secure_shell () = deny_secure "Cannot execute shell commands in secure mode";
3.20 -
3.21 -val orig_bash_output = bash_output;
3.22 -
3.23 -fun bash_output s = (secure_shell (); orig_bash_output s);
3.24 -
3.25 -fun bash s =
3.26 - (case bash_output s of
3.27 - ("", rc) => rc
3.28 - | (out, rc) => (writeln (perhaps (try (unsuffix "\n")) out); rc));
3.29 -
3.30 end;
3.31
3.32 (*override previous toplevel bindings!*)
3.33 @@ -80,5 +64,4 @@
3.34 fun use s = Secure.use_file ML_Parse.global_context true s
3.35 handle ERROR msg => (writeln msg; error "ML error");
3.36 val toplevel_pp = Secure.toplevel_pp;
3.37 -val bash_output = Secure.bash_output;
3.38 -val bash = Secure.bash;
3.39 +
4.1 --- a/src/Pure/IsaMakefile Sat Nov 27 16:27:52 2010 +0100
4.2 +++ b/src/Pure/IsaMakefile Sat Nov 27 16:29:53 2010 +0100
4.3 @@ -22,7 +22,6 @@
4.4 BOOTSTRAP_FILES = \
4.5 General/exn.ML \
4.6 General/timing.ML \
4.7 - ML-Systems/bash.ML \
4.8 ML-Systems/compiler_polyml-5.2.ML \
4.9 ML-Systems/compiler_polyml-5.3.ML \
4.10 ML-Systems/ml_name_space.ML \
4.11 @@ -55,6 +54,8 @@
4.12 Pure: $(OUT)/Pure
4.13
4.14 $(OUT)/Pure: $(BOOTSTRAP_FILES) \
4.15 + Concurrent/bash.ML \
4.16 + Concurrent/bash_sequential.ML \
4.17 Concurrent/cache.ML \
4.18 Concurrent/future.ML \
4.19 Concurrent/lazy.ML \
5.1 --- a/src/Pure/ML-Systems/bash.ML Sat Nov 27 16:27:52 2010 +0100
5.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
5.3 @@ -1,43 +0,0 @@
5.4 -(* Title: Pure/ML-Systems/bash.ML
5.5 - Author: Makarius
5.6 -
5.7 -Generic GNU bash processes (no provisions to propagate interrupts, but
5.8 -could work via the controlling tty).
5.9 -*)
5.10 -
5.11 -local
5.12 -
5.13 -fun read_file name =
5.14 - let val is = TextIO.openIn name
5.15 - in Exn.release (Exn.capture TextIO.inputAll is before TextIO.closeIn is) end;
5.16 -
5.17 -fun write_file name txt =
5.18 - let val os = TextIO.openOut name
5.19 - in Exn.release (Exn.capture TextIO.output (os, txt) before TextIO.closeOut os) end;
5.20 -
5.21 -in
5.22 -
5.23 -fun bash_output script =
5.24 - let
5.25 - val script_name = OS.FileSys.tmpName ();
5.26 - val _ = write_file script_name script;
5.27 -
5.28 - val output_name = OS.FileSys.tmpName ();
5.29 -
5.30 - val status =
5.31 - OS.Process.system ("exec \"$ISABELLE_HOME/lib/scripts/process\" no_group /dev/null" ^
5.32 - " script \"exec bash " ^ script_name ^ " > " ^ output_name ^ "\"");
5.33 - val rc =
5.34 - (case Posix.Process.fromStatus status of
5.35 - Posix.Process.W_EXITED => 0
5.36 - | Posix.Process.W_EXITSTATUS w => Word8.toInt w
5.37 - | Posix.Process.W_SIGNALED s => 256 + LargeWord.toInt (Posix.Signal.toWord s)
5.38 - | Posix.Process.W_STOPPED s => 512 + LargeWord.toInt (Posix.Signal.toWord s));
5.39 -
5.40 - val output = read_file output_name handle IO.Io _ => "";
5.41 - val _ = OS.FileSys.remove script_name handle OS.SysErr _ => ();
5.42 - val _ = OS.FileSys.remove output_name handle OS.SysErr _ => ();
5.43 - in (output, rc) end;
5.44 -
5.45 -end;
5.46 -
6.1 --- a/src/Pure/ML-Systems/multithreading_polyml.ML Sat Nov 27 16:27:52 2010 +0100
6.2 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML Sat Nov 27 16:29:53 2010 +0100
6.3 @@ -8,7 +8,6 @@
6.4 sig
6.5 val interruptible: ('a -> 'b) -> 'a -> 'b
6.6 val uninterruptible: ((('c -> 'd) -> 'c -> 'd) -> 'a -> 'b) -> 'a -> 'b
6.7 - val bash_output: string -> string * int
6.8 structure TimeLimit: TIME_LIMIT
6.9 end;
6.10
6.11 @@ -42,20 +41,6 @@
6.12 fun enabled () = max_threads_value () > 1;
6.13
6.14
6.15 -(* misc utils *)
6.16 -
6.17 -fun show "" = "" | show name = " " ^ name;
6.18 -fun show' "" = "" | show' name = " [" ^ name ^ "]";
6.19 -
6.20 -fun read_file name =
6.21 - let val is = TextIO.openIn name
6.22 - in Exn.release (Exn.capture TextIO.inputAll is before TextIO.closeIn is) end;
6.23 -
6.24 -fun write_file name txt =
6.25 - let val os = TextIO.openOut name
6.26 - in Exn.release (Exn.capture TextIO.output (os, txt) before TextIO.closeOut os) end;
6.27 -
6.28 -
6.29 (* thread attributes *)
6.30
6.31 val no_interrupts =
6.32 @@ -156,71 +141,6 @@
6.33 end;
6.34
6.35
6.36 -(* GNU bash processes, with propagation of interrupts *)
6.37 -
6.38 -fun bash_output script = with_attributes no_interrupts (fn orig_atts =>
6.39 - let
6.40 - val script_name = OS.FileSys.tmpName ();
6.41 - val _ = write_file script_name script;
6.42 -
6.43 - val pid_name = OS.FileSys.tmpName ();
6.44 - val output_name = OS.FileSys.tmpName ();
6.45 -
6.46 - (*result state*)
6.47 - datatype result = Wait | Signal | Result of int;
6.48 - val result = ref Wait;
6.49 - val lock = Mutex.mutex ();
6.50 - val cond = ConditionVar.conditionVar ();
6.51 - fun set_result res =
6.52 - (Mutex.lock lock; result := res; ConditionVar.signal cond; Mutex.unlock lock);
6.53 -
6.54 - val _ = Mutex.lock lock;
6.55 -
6.56 - (*system thread*)
6.57 - val system_thread = Thread.fork (fn () =>
6.58 - let
6.59 - val status =
6.60 - OS.Process.system ("exec \"$ISABELLE_HOME/lib/scripts/process\" group " ^ pid_name ^
6.61 - " script \"exec bash " ^ script_name ^ " > " ^ output_name ^ "\"");
6.62 - val res =
6.63 - (case Posix.Process.fromStatus status of
6.64 - Posix.Process.W_EXITED => Result 0
6.65 - | Posix.Process.W_EXITSTATUS 0wx82 => Signal
6.66 - | Posix.Process.W_EXITSTATUS w => Result (Word8.toInt w)
6.67 - | Posix.Process.W_SIGNALED s =>
6.68 - if s = Posix.Signal.int then Signal
6.69 - else Result (256 + LargeWord.toInt (Posix.Signal.toWord s))
6.70 - | Posix.Process.W_STOPPED s => Result (512 + LargeWord.toInt (Posix.Signal.toWord s)));
6.71 - in set_result res end handle _ (*sic*) => set_result (Result 2), []);
6.72 -
6.73 - (*main thread -- proxy for interrupts*)
6.74 - fun kill n =
6.75 - (case Int.fromString (read_file pid_name) of
6.76 - SOME pid =>
6.77 - Posix.Process.kill
6.78 - (Posix.Process.K_GROUP (Posix.Process.wordToPid (LargeWord.fromInt pid)),
6.79 - Posix.Signal.int)
6.80 - | NONE => ())
6.81 - handle OS.SysErr _ => () | IO.Io _ =>
6.82 - (OS.Process.sleep (seconds 0.1); if n > 0 then kill (n - 1) else ());
6.83 -
6.84 - val _ =
6.85 - while ! result = Wait do
6.86 - let val res =
6.87 - sync_wait (SOME orig_atts)
6.88 - (SOME (Time.+ (Time.now (), seconds 0.1))) cond lock
6.89 - in if Exn.is_interrupt_exn res then kill 10 else () end;
6.90 -
6.91 - (*cleanup*)
6.92 - val output = read_file output_name handle IO.Io _ => "";
6.93 - val _ = OS.FileSys.remove script_name handle OS.SysErr _ => ();
6.94 - val _ = OS.FileSys.remove pid_name handle OS.SysErr _ => ();
6.95 - val _ = OS.FileSys.remove output_name handle OS.SysErr _ => ();
6.96 - val _ = Thread.interrupt system_thread handle Thread _ => ();
6.97 - val rc = (case ! result of Signal => Exn.interrupt () | Result rc => rc);
6.98 - in (output, rc) end);
6.99 -
6.100 -
6.101 (* critical section -- may be nested within the same thread *)
6.102
6.103 local
6.104 @@ -229,6 +149,9 @@
6.105 val critical_thread = ref (NONE: Thread.thread option);
6.106 val critical_name = ref "";
6.107
6.108 +fun show "" = "" | show name = " " ^ name;
6.109 +fun show' "" = "" | show' name = " [" ^ name ^ "]";
6.110 +
6.111 in
6.112
6.113 fun self_critical () =
7.1 --- a/src/Pure/ML-Systems/polyml_common.ML Sat Nov 27 16:27:52 2010 +0100
7.2 +++ b/src/Pure/ML-Systems/polyml_common.ML Sat Nov 27 16:29:53 2010 +0100
7.3 @@ -14,7 +14,6 @@
7.4 use "ML-Systems/multithreading.ML";
7.5 use "ML-Systems/time_limit.ML";
7.6 use "General/timing.ML";
7.7 -use "ML-Systems/bash.ML";
7.8 use "ML-Systems/ml_pretty.ML";
7.9 use "ML-Systems/use_context.ML";
7.10
8.1 --- a/src/Pure/ML-Systems/smlnj.ML Sat Nov 27 16:27:52 2010 +0100
8.2 +++ b/src/Pure/ML-Systems/smlnj.ML Sat Nov 27 16:29:53 2010 +0100
8.3 @@ -14,7 +14,6 @@
8.4 use "ML-Systems/thread_dummy.ML";
8.5 use "ML-Systems/multithreading.ML";
8.6 use "General/timing.ML";
8.7 -use "ML-Systems/bash.ML";
8.8 use "ML-Systems/ml_name_space.ML";
8.9 use "ML-Systems/ml_pretty.ML";
8.10 structure PolyML = struct end;
8.11 @@ -170,11 +169,6 @@
8.12 val pwd = OS.FileSys.getDir;
8.13
8.14
8.15 -(* system command execution *)
8.16 -
8.17 -val bash_output = (fn (output, rc) => (output, mk_int rc)) o bash_output;
8.18 -
8.19 -
8.20 (* getenv *)
8.21
8.22 fun getenv var =
9.1 --- a/src/Pure/ROOT.ML Sat Nov 27 16:27:52 2010 +0100
9.2 +++ b/src/Pure/ROOT.ML Sat Nov 27 16:29:53 2010 +0100
9.3 @@ -72,6 +72,15 @@
9.4 if Multithreading.available then ()
9.5 else use "Concurrent/synchronized_sequential.ML";
9.6
9.7 +if Multithreading.available
9.8 +then use "Concurrent/bash.ML"
9.9 +else use "Concurrent/bash_sequential.ML";
9.10 +
9.11 +fun bash s =
9.12 + (case bash_output s of
9.13 + ("", rc) => rc
9.14 + | (out, rc) => (writeln (perhaps (try (unsuffix "\n")) out); rc));
9.15 +
9.16 use "Concurrent/mailbox.ML";
9.17 use "Concurrent/task_queue.ML";
9.18 use "Concurrent/future.ML";