author | wenzelm |
Fri, 03 Dec 2010 17:16:53 +0100 | |
changeset 40896 | d9c112c587f9 |
parent 40783 | 21f7e8d66a39 |
child 43847 | 529159f81d06 |
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 |
|
40749 | 7 |
val bash_output = uninterruptible (fn restore_attributes => fn script => |
8 |
let |
|
9 |
datatype result = Wait | Signal | Result of int; |
|
10 |
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
|
11 |
|
40749 | 12 |
val id = serial_string (); |
13 |
val script_path = File.tmp_path (Path.basic ("bash_script" ^ id)); |
|
14 |
val output_path = File.tmp_path (Path.basic ("bash_output" ^ id)); |
|
15 |
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
|
16 |
|
40749 | 17 |
val system_thread = |
18 |
Simple_Thread.fork false (fn () => |
|
19 |
Multithreading.with_attributes Multithreading.private_interrupts (fn _ => |
|
20 |
let |
|
21 |
val _ = File.write script_path script; |
|
22 |
val status = |
|
23 |
OS.Process.system |
|
24 |
("exec \"$ISABELLE_HOME/lib/scripts/process\" group " ^ |
|
25 |
File.shell_path pid_path ^ " script \"exec bash " ^ |
|
26 |
File.shell_path script_path ^ " > " ^ |
|
27 |
File.shell_path output_path ^ "\""); |
|
28 |
val res = |
|
29 |
(case Posix.Process.fromStatus status of |
|
30 |
Posix.Process.W_EXITED => Result 0 |
|
31 |
| Posix.Process.W_EXITSTATUS 0wx82 => Signal |
|
32 |
| Posix.Process.W_EXITSTATUS w => Result (Word8.toInt w) |
|
33 |
| Posix.Process.W_SIGNALED s => |
|
34 |
if s = Posix.Signal.int then Signal |
|
35 |
else Result (256 + LargeWord.toInt (Posix.Signal.toWord s)) |
|
36 |
| Posix.Process.W_STOPPED s => |
|
37 |
Result (512 + LargeWord.toInt (Posix.Signal.toWord s))); |
|
38 |
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
|
39 |
handle exn => |
21f7e8d66a39
more conventional exception propagation -- taking into account Simple_Thread.fork wrapping;
wenzelm
parents:
40750
diff
changeset
|
40 |
(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
|
41 |
|
40750
2064991db2ac
more thorough process termination (cf. Scala version);
wenzelm
parents:
40749
diff
changeset
|
42 |
fun terminate () = |
2064991db2ac
more thorough process termination (cf. Scala version);
wenzelm
parents:
40749
diff
changeset
|
43 |
let |
2064991db2ac
more thorough process termination (cf. Scala version);
wenzelm
parents:
40749
diff
changeset
|
44 |
val sig_test = Posix.Signal.fromWord 0w0; |
2064991db2ac
more thorough process termination (cf. Scala version);
wenzelm
parents:
40749
diff
changeset
|
45 |
|
2064991db2ac
more thorough process termination (cf. Scala version);
wenzelm
parents:
40749
diff
changeset
|
46 |
fun kill_group pid s = |
2064991db2ac
more thorough process termination (cf. Scala version);
wenzelm
parents:
40749
diff
changeset
|
47 |
(Posix.Process.kill |
2064991db2ac
more thorough process termination (cf. Scala version);
wenzelm
parents:
40749
diff
changeset
|
48 |
(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
|
49 |
handle OS.SysErr _ => false; |
2064991db2ac
more thorough process termination (cf. Scala version);
wenzelm
parents:
40749
diff
changeset
|
50 |
|
2064991db2ac
more thorough process termination (cf. Scala version);
wenzelm
parents:
40749
diff
changeset
|
51 |
fun kill s = |
2064991db2ac
more thorough process termination (cf. Scala version);
wenzelm
parents:
40749
diff
changeset
|
52 |
(case Int.fromString (File.read pid_path) of |
2064991db2ac
more thorough process termination (cf. Scala version);
wenzelm
parents:
40749
diff
changeset
|
53 |
NONE => true |
2064991db2ac
more thorough process termination (cf. Scala version);
wenzelm
parents:
40749
diff
changeset
|
54 |
| SOME pid => (kill_group pid s; kill_group pid sig_test)) |
2064991db2ac
more thorough process termination (cf. Scala version);
wenzelm
parents:
40749
diff
changeset
|
55 |
handle IO.Io _ => true; |
2064991db2ac
more thorough process termination (cf. Scala version);
wenzelm
parents:
40749
diff
changeset
|
56 |
|
2064991db2ac
more thorough process termination (cf. Scala version);
wenzelm
parents:
40749
diff
changeset
|
57 |
fun multi_kill count s = |
2064991db2ac
more thorough process termination (cf. Scala version);
wenzelm
parents:
40749
diff
changeset
|
58 |
count = 0 orelse |
2064991db2ac
more thorough process termination (cf. Scala version);
wenzelm
parents:
40749
diff
changeset
|
59 |
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
|
60 |
val _ = |
2064991db2ac
more thorough process termination (cf. Scala version);
wenzelm
parents:
40749
diff
changeset
|
61 |
multi_kill 10 Posix.Signal.int andalso |
2064991db2ac
more thorough process termination (cf. Scala version);
wenzelm
parents:
40749
diff
changeset
|
62 |
multi_kill 10 Posix.Signal.term andalso |
2064991db2ac
more thorough process termination (cf. Scala version);
wenzelm
parents:
40749
diff
changeset
|
63 |
multi_kill 10 Posix.Signal.kill; |
2064991db2ac
more thorough process termination (cf. Scala version);
wenzelm
parents:
40749
diff
changeset
|
64 |
in () end; |
2064991db2ac
more thorough process termination (cf. Scala version);
wenzelm
parents:
40749
diff
changeset
|
65 |
|
40749 | 66 |
fun cleanup () = |
40896
d9c112c587f9
bash wrapper: terminate only in exceptional case, keep background processes running (e.g. 'thy_deps' or 'display_drafts');
wenzelm
parents:
40783
diff
changeset
|
67 |
(Simple_Thread.interrupt system_thread; |
40749 | 68 |
try File.rm script_path; |
69 |
try File.rm output_path; |
|
70 |
try File.rm pid_path); |
|
71 |
in |
|
72 |
let |
|
40748
591b6778d076
removed bash from ML system bootstrap, and past the Secure ML barrier;
wenzelm
parents:
diff
changeset
|
73 |
val _ = |
40749 | 74 |
restore_attributes (fn () => |
40750
2064991db2ac
more thorough process termination (cf. Scala version);
wenzelm
parents:
40749
diff
changeset
|
75 |
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
|
76 |
|
40749 | 77 |
val output = the_default "" (try File.read output_path); |
78 |
val rc = (case Synchronized.value result of Signal => Exn.interrupt () | Result rc => rc); |
|
79 |
val _ = cleanup (); |
|
80 |
in (output, rc) end |
|
40896
d9c112c587f9
bash wrapper: terminate only in exceptional case, keep background processes running (e.g. 'thy_deps' or 'display_drafts');
wenzelm
parents:
40783
diff
changeset
|
81 |
handle exn => (terminate(); cleanup (); reraise exn) |
40749 | 82 |
end); |
40748
591b6778d076
removed bash from ML system bootstrap, and past the Secure ML barrier;
wenzelm
parents:
diff
changeset
|
83 |