20 val id = serial_string (); |
20 val id = serial_string (); |
21 val script_path = File.tmp_path (Path.basic ("bash_script" ^ id)); |
21 val script_path = File.tmp_path (Path.basic ("bash_script" ^ id)); |
22 val out_path = File.tmp_path (Path.basic ("bash_out" ^ id)); |
22 val out_path = File.tmp_path (Path.basic ("bash_out" ^ id)); |
23 val err_path = File.tmp_path (Path.basic ("bash_err" ^ id)); |
23 val err_path = File.tmp_path (Path.basic ("bash_err" ^ id)); |
24 val pid_path = File.tmp_path (Path.basic ("bash_pid" ^ id)); |
24 val pid_path = File.tmp_path (Path.basic ("bash_pid" ^ id)); |
|
25 |
|
26 fun cleanup_files () = |
|
27 (try File.rm script_path; |
|
28 try File.rm out_path; |
|
29 try File.rm err_path; |
|
30 try File.rm pid_path); |
|
31 val _ = cleanup_files (); |
25 |
32 |
26 val system_thread = |
33 val system_thread = |
27 Simple_Thread.fork false (fn () => |
34 Simple_Thread.fork false (fn () => |
28 Multithreading.with_attributes Multithreading.private_interrupts (fn _ => |
35 Multithreading.with_attributes Multithreading.private_interrupts (fn _ => |
29 let |
36 let |
53 Result (512 + LargeWord.toInt (Posix.Signal.toWord s))); |
60 Result (512 + LargeWord.toInt (Posix.Signal.toWord s))); |
54 in Synchronized.change result (K res) end |
61 in Synchronized.change result (K res) end |
55 handle exn => |
62 handle exn => |
56 (Synchronized.change result (fn Wait => Signal | res => res); reraise exn))); |
63 (Synchronized.change result (fn Wait => Signal | res => res); reraise exn))); |
57 |
64 |
58 fun get_pid () = Int.fromString (File.read pid_path) handle IO.Io _ => NONE; |
65 fun read_pid 0 = NONE |
|
66 | read_pid count = |
|
67 (case (Int.fromString (File.read pid_path) handle IO.Io _ => NONE) of |
|
68 NONE => (OS.Process.sleep (seconds 0.1); read_pid (count - 1)) |
|
69 | some => some); |
59 |
70 |
60 fun terminate opt_pid = |
71 fun terminate NONE = () |
61 let |
72 | terminate (SOME pid) = |
62 val sig_test = Posix.Signal.fromWord 0w0; |
73 let |
|
74 val sig_test = Posix.Signal.fromWord 0w0; |
63 |
75 |
64 fun kill_group pid s = |
76 fun kill_group pid s = |
65 (Posix.Process.kill |
77 (Posix.Process.kill |
66 (Posix.Process.K_GROUP (Posix.Process.wordToPid (LargeWord.fromInt pid)), s); true) |
78 (Posix.Process.K_GROUP (Posix.Process.wordToPid (LargeWord.fromInt pid)), s); true) |
67 handle OS.SysErr _ => false; |
79 handle OS.SysErr _ => false; |
68 |
80 |
69 fun kill s = |
81 fun kill s = (kill_group pid s; kill_group pid sig_test); |
70 (case opt_pid of |
|
71 NONE => true |
|
72 | SOME pid => (kill_group pid s; kill_group pid sig_test)); |
|
73 |
82 |
74 fun multi_kill count s = |
83 fun multi_kill count s = |
75 count = 0 orelse |
84 count = 0 orelse |
76 kill s andalso (OS.Process.sleep (seconds 0.1); multi_kill (count - 1) s); |
85 kill s andalso (OS.Process.sleep (seconds 0.1); multi_kill (count - 1) s); |
77 val _ = |
86 val _ = |
78 multi_kill 10 Posix.Signal.int andalso |
87 multi_kill 10 Posix.Signal.int andalso |
79 multi_kill 10 Posix.Signal.term andalso |
88 multi_kill 10 Posix.Signal.term andalso |
80 multi_kill 10 Posix.Signal.kill; |
89 multi_kill 10 Posix.Signal.kill; |
81 in () end; |
90 in () end; |
82 |
91 |
83 fun cleanup () = |
92 fun cleanup () = |
84 (Simple_Thread.interrupt_unsynchronized system_thread; |
93 (Simple_Thread.interrupt_unsynchronized system_thread; |
85 try File.rm script_path; |
94 cleanup_files ()); |
86 try File.rm out_path; |
|
87 try File.rm err_path; |
|
88 try File.rm pid_path); |
|
89 in |
95 in |
90 let |
96 let |
91 val _ = |
97 val _ = |
92 restore_attributes (fn () => |
98 restore_attributes (fn () => |
93 Synchronized.guarded_access result (fn Wait => NONE | x => SOME ((), x))) (); |
99 Synchronized.guarded_access result (fn Wait => NONE | x => SOME ((), x))) (); |
94 |
100 |
95 val out = the_default "" (try File.read out_path); |
101 val out = the_default "" (try File.read out_path); |
96 val err = the_default "" (try File.read err_path); |
102 val err = the_default "" (try File.read err_path); |
97 val rc = (case Synchronized.value result of Signal => Exn.interrupt () | Result rc => rc); |
103 val rc = (case Synchronized.value result of Signal => Exn.interrupt () | Result rc => rc); |
98 val pid = get_pid (); |
104 val pid = read_pid 1; |
99 val _ = cleanup (); |
105 val _ = cleanup (); |
100 in {out = out, err = err, rc = rc, terminate = fn () => terminate pid} end |
106 in {out = out, err = err, rc = rc, terminate = fn () => terminate pid} end |
101 handle exn => (terminate (get_pid ()); cleanup (); reraise exn) |
107 handle exn => (terminate (read_pid 10); cleanup (); reraise exn) |
102 end); |
108 end); |
103 |
109 |
104 end; |
110 end; |
105 |
111 |