author | wenzelm |
Mon, 16 Apr 2012 23:07:40 +0200 | |
changeset 47499 | 4b0daca2bf88 |
parent 44112 | ef876972fdc1 |
child 47764 | d141f1193789 |
permissions | -rw-r--r-- |
40748
591b6778d076
removed bash from ML system bootstrap, and past the Secure ML barrier;
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/Concurrent/bash.ML |
591b6778d076
removed bash from ML system bootstrap, and past the Secure ML barrier;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
591b6778d076
removed bash from ML system bootstrap, and past the Secure ML barrier;
wenzelm
parents:
diff
changeset
|
3 |
|
591b6778d076
removed bash from ML system bootstrap, and past the Secure ML barrier;
wenzelm
parents:
diff
changeset
|
4 |
GNU bash processes, with propagation of interrupts. |
591b6778d076
removed bash from ML system bootstrap, and past the Secure ML barrier;
wenzelm
parents:
diff
changeset
|
5 |
*) |
591b6778d076
removed bash from ML system bootstrap, and past the Secure ML barrier;
wenzelm
parents:
diff
changeset
|
6 |
|
44054 | 7 |
signature BASH = |
8 |
sig |
|
47499
4b0daca2bf88
redirect bash stderr to Isabelle warning as appropriate -- avoid raw process error output which may either get ignored or overload PIDE syslog in extreme cases;
wenzelm
parents:
44112
diff
changeset
|
9 |
val process: string -> {out: string, err: string, rc: int, terminate: unit -> unit} |
44054 | 10 |
end; |
11 |
||
12 |
structure Bash: BASH = |
|
43850
7f2cbc713344
moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents:
43847
diff
changeset
|
13 |
struct |
7f2cbc713344
moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents:
43847
diff
changeset
|
14 |
|
7f2cbc713344
moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents:
43847
diff
changeset
|
15 |
val process = uninterruptible (fn restore_attributes => fn script => |
40749 | 16 |
let |
17 |
datatype result = Wait | Signal | Result of int; |
|
18 |
val result = Synchronized.var "bash_result" Wait; |
|
40748
591b6778d076
removed bash from ML system bootstrap, and past the Secure ML barrier;
wenzelm
parents:
diff
changeset
|
19 |
|
40749 | 20 |
val id = serial_string (); |
21 |
val script_path = File.tmp_path (Path.basic ("bash_script" ^ id)); |
|
47499
4b0daca2bf88
redirect bash stderr to Isabelle warning as appropriate -- avoid raw process error output which may either get ignored or overload PIDE syslog in extreme cases;
wenzelm
parents:
44112
diff
changeset
|
22 |
val out_path = File.tmp_path (Path.basic ("bash_out" ^ id)); |
4b0daca2bf88
redirect bash stderr to Isabelle warning as appropriate -- avoid raw process error output which may either get ignored or overload PIDE syslog in extreme cases;
wenzelm
parents:
44112
diff
changeset
|
23 |
val err_path = File.tmp_path (Path.basic ("bash_err" ^ id)); |
40749 | 24 |
val pid_path = File.tmp_path (Path.basic ("bash_pid" ^ id)); |
40748
591b6778d076
removed bash from ML system bootstrap, and past the Secure ML barrier;
wenzelm
parents:
diff
changeset
|
25 |
|
40749 | 26 |
val system_thread = |
27 |
Simple_Thread.fork false (fn () => |
|
28 |
Multithreading.with_attributes Multithreading.private_interrupts (fn _ => |
|
29 |
let |
|
30 |
val _ = File.write script_path script; |
|
31 |
val status = |
|
32 |
OS.Process.system |
|
33 |
("exec \"$ISABELLE_HOME/lib/scripts/process\" group " ^ |
|
34 |
File.shell_path pid_path ^ " script \"exec bash " ^ |
|
47499
4b0daca2bf88
redirect bash stderr to Isabelle warning as appropriate -- avoid raw process error output which may either get ignored or overload PIDE syslog in extreme cases;
wenzelm
parents:
44112
diff
changeset
|
35 |
File.shell_path script_path ^ |
4b0daca2bf88
redirect bash stderr to Isabelle warning as appropriate -- avoid raw process error output which may either get ignored or overload PIDE syslog in extreme cases;
wenzelm
parents:
44112
diff
changeset
|
36 |
" > " ^ File.shell_path out_path ^ |
4b0daca2bf88
redirect bash stderr to Isabelle warning as appropriate -- avoid raw process error output which may either get ignored or overload PIDE syslog in extreme cases;
wenzelm
parents:
44112
diff
changeset
|
37 |
" 2> " ^ File.shell_path err_path ^ "\""); |
40749 | 38 |
val res = |
39 |
(case Posix.Process.fromStatus status of |
|
40 |
Posix.Process.W_EXITED => Result 0 |
|
41 |
| Posix.Process.W_EXITSTATUS 0wx82 => Signal |
|
42 |
| Posix.Process.W_EXITSTATUS w => Result (Word8.toInt w) |
|
43 |
| Posix.Process.W_SIGNALED s => |
|
44 |
if s = Posix.Signal.int then Signal |
|
45 |
else Result (256 + LargeWord.toInt (Posix.Signal.toWord s)) |
|
46 |
| Posix.Process.W_STOPPED s => |
|
47 |
Result (512 + LargeWord.toInt (Posix.Signal.toWord s))); |
|
48 |
in Synchronized.change result (K res) end |
|
40783
21f7e8d66a39
more conventional exception propagation -- taking into account Simple_Thread.fork wrapping;
wenzelm
parents:
40750
diff
changeset
|
49 |
handle exn => |
21f7e8d66a39
more conventional exception propagation -- taking into account Simple_Thread.fork wrapping;
wenzelm
parents:
40750
diff
changeset
|
50 |
(Synchronized.change result (fn Wait => Signal | res => res); reraise exn))); |
40748
591b6778d076
removed bash from ML system bootstrap, and past the Secure ML barrier;
wenzelm
parents:
diff
changeset
|
51 |
|
43847
529159f81d06
more general bash_process, which allows to terminate background processes as well;
wenzelm
parents:
40896
diff
changeset
|
52 |
fun get_pid () = Int.fromString (File.read pid_path) handle IO.Io _ => NONE; |
529159f81d06
more general bash_process, which allows to terminate background processes as well;
wenzelm
parents:
40896
diff
changeset
|
53 |
|
529159f81d06
more general bash_process, which allows to terminate background processes as well;
wenzelm
parents:
40896
diff
changeset
|
54 |
fun terminate opt_pid = |
40750
2064991db2ac
more thorough process termination (cf. Scala version);
wenzelm
parents:
40749
diff
changeset
|
55 |
let |
2064991db2ac
more thorough process termination (cf. Scala version);
wenzelm
parents:
40749
diff
changeset
|
56 |
val sig_test = Posix.Signal.fromWord 0w0; |
2064991db2ac
more thorough process termination (cf. Scala version);
wenzelm
parents:
40749
diff
changeset
|
57 |
|
2064991db2ac
more thorough process termination (cf. Scala version);
wenzelm
parents:
40749
diff
changeset
|
58 |
fun kill_group pid s = |
2064991db2ac
more thorough process termination (cf. Scala version);
wenzelm
parents:
40749
diff
changeset
|
59 |
(Posix.Process.kill |
2064991db2ac
more thorough process termination (cf. Scala version);
wenzelm
parents:
40749
diff
changeset
|
60 |
(Posix.Process.K_GROUP (Posix.Process.wordToPid (LargeWord.fromInt pid)), s); true) |
2064991db2ac
more thorough process termination (cf. Scala version);
wenzelm
parents:
40749
diff
changeset
|
61 |
handle OS.SysErr _ => false; |
2064991db2ac
more thorough process termination (cf. Scala version);
wenzelm
parents:
40749
diff
changeset
|
62 |
|
2064991db2ac
more thorough process termination (cf. Scala version);
wenzelm
parents:
40749
diff
changeset
|
63 |
fun kill s = |
43847
529159f81d06
more general bash_process, which allows to terminate background processes as well;
wenzelm
parents:
40896
diff
changeset
|
64 |
(case opt_pid of |
40750
2064991db2ac
more thorough process termination (cf. Scala version);
wenzelm
parents:
40749
diff
changeset
|
65 |
NONE => true |
43847
529159f81d06
more general bash_process, which allows to terminate background processes as well;
wenzelm
parents:
40896
diff
changeset
|
66 |
| SOME pid => (kill_group pid s; kill_group pid sig_test)); |
40750
2064991db2ac
more thorough process termination (cf. Scala version);
wenzelm
parents:
40749
diff
changeset
|
67 |
|
2064991db2ac
more thorough process termination (cf. Scala version);
wenzelm
parents:
40749
diff
changeset
|
68 |
fun multi_kill count s = |
2064991db2ac
more thorough process termination (cf. Scala version);
wenzelm
parents:
40749
diff
changeset
|
69 |
count = 0 orelse |
2064991db2ac
more thorough process termination (cf. Scala version);
wenzelm
parents:
40749
diff
changeset
|
70 |
kill s andalso (OS.Process.sleep (seconds 0.1); multi_kill (count - 1) s); |
2064991db2ac
more thorough process termination (cf. Scala version);
wenzelm
parents:
40749
diff
changeset
|
71 |
val _ = |
2064991db2ac
more thorough process termination (cf. Scala version);
wenzelm
parents:
40749
diff
changeset
|
72 |
multi_kill 10 Posix.Signal.int andalso |
2064991db2ac
more thorough process termination (cf. Scala version);
wenzelm
parents:
40749
diff
changeset
|
73 |
multi_kill 10 Posix.Signal.term andalso |
2064991db2ac
more thorough process termination (cf. Scala version);
wenzelm
parents:
40749
diff
changeset
|
74 |
multi_kill 10 Posix.Signal.kill; |
2064991db2ac
more thorough process termination (cf. Scala version);
wenzelm
parents:
40749
diff
changeset
|
75 |
in () end; |
2064991db2ac
more thorough process termination (cf. Scala version);
wenzelm
parents:
40749
diff
changeset
|
76 |
|
40749 | 77 |
fun cleanup () = |
44112
ef876972fdc1
more explicit Simple_Thread.interrupt_unsynchronized, to emphasize its meaning;
wenzelm
parents:
44054
diff
changeset
|
78 |
(Simple_Thread.interrupt_unsynchronized system_thread; |
40749 | 79 |
try File.rm script_path; |
47499
4b0daca2bf88
redirect bash stderr to Isabelle warning as appropriate -- avoid raw process error output which may either get ignored or overload PIDE syslog in extreme cases;
wenzelm
parents:
44112
diff
changeset
|
80 |
try File.rm out_path; |
4b0daca2bf88
redirect bash stderr to Isabelle warning as appropriate -- avoid raw process error output which may either get ignored or overload PIDE syslog in extreme cases;
wenzelm
parents:
44112
diff
changeset
|
81 |
try File.rm err_path; |
40749 | 82 |
try File.rm pid_path); |
83 |
in |
|
84 |
let |
|
40748
591b6778d076
removed bash from ML system bootstrap, and past the Secure ML barrier;
wenzelm
parents:
diff
changeset
|
85 |
val _ = |
40749 | 86 |
restore_attributes (fn () => |
40750
2064991db2ac
more thorough process termination (cf. Scala version);
wenzelm
parents:
40749
diff
changeset
|
87 |
Synchronized.guarded_access result (fn Wait => NONE | x => SOME ((), x))) (); |
40748
591b6778d076
removed bash from ML system bootstrap, and past the Secure ML barrier;
wenzelm
parents:
diff
changeset
|
88 |
|
47499
4b0daca2bf88
redirect bash stderr to Isabelle warning as appropriate -- avoid raw process error output which may either get ignored or overload PIDE syslog in extreme cases;
wenzelm
parents:
44112
diff
changeset
|
89 |
val out = the_default "" (try File.read out_path); |
4b0daca2bf88
redirect bash stderr to Isabelle warning as appropriate -- avoid raw process error output which may either get ignored or overload PIDE syslog in extreme cases;
wenzelm
parents:
44112
diff
changeset
|
90 |
val err = the_default "" (try File.read err_path); |
40749 | 91 |
val rc = (case Synchronized.value result of Signal => Exn.interrupt () | Result rc => rc); |
43847
529159f81d06
more general bash_process, which allows to terminate background processes as well;
wenzelm
parents:
40896
diff
changeset
|
92 |
val pid = get_pid (); |
40749 | 93 |
val _ = cleanup (); |
47499
4b0daca2bf88
redirect bash stderr to Isabelle warning as appropriate -- avoid raw process error output which may either get ignored or overload PIDE syslog in extreme cases;
wenzelm
parents:
44112
diff
changeset
|
94 |
in {out = out, err = err, rc = rc, terminate = fn () => terminate pid} end |
43847
529159f81d06
more general bash_process, which allows to terminate background processes as well;
wenzelm
parents:
40896
diff
changeset
|
95 |
handle exn => (terminate (get_pid ()); cleanup (); reraise exn) |
40749 | 96 |
end); |
40748
591b6778d076
removed bash from ML system bootstrap, and past the Secure ML barrier;
wenzelm
parents:
diff
changeset
|
97 |
|
43850
7f2cbc713344
moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents:
43847
diff
changeset
|
98 |
end; |
7f2cbc713344
moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents:
43847
diff
changeset
|
99 |