# HG changeset patch # User wenzelm # Date 1290881875 -3600 # Node ID cb6698d2dbaf4292ba1f87b8792f97df7653cdf8 # Parent 591b6778d076658a1d31aaf639ec936cf6ee3411 prefer Isabelle/ML concurrency elements; more careful propagation of interrupts; diff -r 591b6778d076 -r cb6698d2dbaf src/Pure/Concurrent/bash.ML --- a/src/Pure/Concurrent/bash.ML Sat Nov 27 16:29:53 2010 +0100 +++ b/src/Pure/Concurrent/bash.ML Sat Nov 27 19:17:55 2010 +0100 @@ -4,80 +4,67 @@ GNU bash processes, with propagation of interrupts. *) -local - -fun read_file name = - let val is = TextIO.openIn name - in Exn.release (Exn.capture TextIO.inputAll is before TextIO.closeIn is) end; - -fun write_file name txt = - let val os = TextIO.openOut name - in Exn.release (Exn.capture TextIO.output (os, txt) before TextIO.closeOut os) end; - -in +val bash_output = uninterruptible (fn restore_attributes => fn script => + let + datatype result = Wait | Signal | Result of int; + val result = Synchronized.var "bash_result" Wait; -fun bash_output script = - Multithreading.with_attributes Multithreading.no_interrupts (fn orig_atts => - let - val script_name = OS.FileSys.tmpName (); - val _ = write_file script_name script; - - val pid_name = OS.FileSys.tmpName (); - val output_name = OS.FileSys.tmpName (); - - (*result state*) - datatype result = Wait | Signal | Result of int; - val result = Unsynchronized.ref Wait; - val lock = Mutex.mutex (); - val cond = ConditionVar.conditionVar (); - fun set_result res = - (Mutex.lock lock; result := res; ConditionVar.signal cond; Mutex.unlock lock); - - val _ = Mutex.lock lock; + val id = serial_string (); + val script_path = File.tmp_path (Path.basic ("bash_script" ^ id)); + val output_path = File.tmp_path (Path.basic ("bash_output" ^ id)); + val pid_path = File.tmp_path (Path.basic ("bash_pid" ^ id)); - (*system thread*) - val system_thread = Thread.fork (fn () => - let - val status = - OS.Process.system ("exec \"$ISABELLE_HOME/lib/scripts/process\" group " ^ pid_name ^ - " script \"exec bash " ^ script_name ^ " > " ^ output_name ^ "\""); - val res = - (case Posix.Process.fromStatus status of - Posix.Process.W_EXITED => Result 0 - | Posix.Process.W_EXITSTATUS 0wx82 => Signal - | Posix.Process.W_EXITSTATUS w => Result (Word8.toInt w) - | Posix.Process.W_SIGNALED s => - if s = Posix.Signal.int then Signal - else Result (256 + LargeWord.toInt (Posix.Signal.toWord s)) - | Posix.Process.W_STOPPED s => Result (512 + LargeWord.toInt (Posix.Signal.toWord s))); - in set_result res end handle _ (*sic*) => set_result (Result 2), []); + val system_thread = + Simple_Thread.fork false (fn () => + Multithreading.with_attributes Multithreading.private_interrupts (fn _ => + let + val _ = File.write script_path script; + val status = + OS.Process.system + ("exec \"$ISABELLE_HOME/lib/scripts/process\" group " ^ + File.shell_path pid_path ^ " script \"exec bash " ^ + File.shell_path script_path ^ " > " ^ + File.shell_path output_path ^ "\""); + val res = + (case Posix.Process.fromStatus status of + Posix.Process.W_EXITED => Result 0 + | Posix.Process.W_EXITSTATUS 0wx82 => Signal + | Posix.Process.W_EXITSTATUS w => Result (Word8.toInt w) + | Posix.Process.W_SIGNALED s => + if s = Posix.Signal.int then Signal + else Result (256 + LargeWord.toInt (Posix.Signal.toWord s)) + | Posix.Process.W_STOPPED s => + Result (512 + LargeWord.toInt (Posix.Signal.toWord s))); + in Synchronized.change result (K res) end + handle _ (*sic*) => Synchronized.change result (fn Wait => Signal | res => res))); - (*main thread -- proxy for interrupts*) - fun kill n = - (case Int.fromString (read_file pid_name) of - SOME pid => - Posix.Process.kill - (Posix.Process.K_GROUP (Posix.Process.wordToPid (LargeWord.fromInt pid)), - Posix.Signal.int) - | NONE => ()) - handle OS.SysErr _ => () | IO.Io _ => - (OS.Process.sleep (seconds 0.1); if n > 0 then kill (n - 1) else ()); + fun cleanup () = + (Simple_Thread.interrupt system_thread; + try File.rm script_path; + try File.rm output_path; + try File.rm pid_path); + fun kill n = + (case Int.fromString (File.read pid_path) of + SOME pid => + Posix.Process.kill + (Posix.Process.K_GROUP (Posix.Process.wordToPid (LargeWord.fromInt pid)), + Posix.Signal.int) + | NONE => ()) + handle OS.SysErr _ => () + | IO.Io _ => (OS.Process.sleep (seconds 0.1); if n > 0 then kill (n - 1) else ()); + in + let + (*proxy for interrupts*) val _ = - while ! result = Wait do - let val res = - Multithreading.sync_wait (SOME orig_atts) - (SOME (Time.+ (Time.now (), seconds 0.1))) cond lock - in if Exn.is_interrupt_exn res then kill 10 else () end; + restore_attributes (fn () => + Synchronized.guarded_access result (fn Wait => NONE | x => SOME ((), x))) () + handle exn => (if Exn.is_interrupt exn then kill 10 else (); reraise exn); - (*cleanup*) - val output = read_file output_name handle IO.Io _ => ""; - val _ = OS.FileSys.remove script_name handle OS.SysErr _ => (); - val _ = OS.FileSys.remove pid_name handle OS.SysErr _ => (); - val _ = OS.FileSys.remove output_name handle OS.SysErr _ => (); - val _ = Thread.interrupt system_thread handle Thread _ => (); - val rc = (case ! result of Signal => Exn.interrupt () | Result rc => rc); - in (output, rc) end); + val output = the_default "" (try File.read output_path); + val rc = (case Synchronized.value result of Signal => Exn.interrupt () | Result rc => rc); + val _ = cleanup (); + in (output, rc) end + handle exn => (cleanup (); reraise exn) + end); -end; - diff -r 591b6778d076 -r cb6698d2dbaf src/Pure/Concurrent/bash_sequential.ML --- a/src/Pure/Concurrent/bash_sequential.ML Sat Nov 27 16:29:53 2010 +0100 +++ b/src/Pure/Concurrent/bash_sequential.ML Sat Nov 27 19:17:55 2010 +0100 @@ -5,39 +5,30 @@ could work via the controlling tty). *) -local - -fun read_file name = - let val is = TextIO.openIn name - in Exn.release (Exn.capture TextIO.inputAll is before TextIO.closeIn is) end; - -fun write_file name txt = - let val os = TextIO.openOut name - in Exn.release (Exn.capture TextIO.output (os, txt) before TextIO.closeOut os) end; - -in - fun bash_output script = let - val script_name = OS.FileSys.tmpName (); - val _ = write_file script_name script; - - val output_name = OS.FileSys.tmpName (); + val id = serial_string (); + val script_path = File.tmp_path (Path.basic ("bash_script" ^ id)); + val output_path = File.tmp_path (Path.basic ("bash_output" ^ id)); + fun cleanup () = (try File.rm script_path; try File.rm output_path); + in + let + val _ = File.write script_path script; + val status = + OS.Process.system + ("exec \"$ISABELLE_HOME/lib/scripts/process\" no_group /dev/null" ^ + " script \"exec bash " ^ File.shell_path script_path ^ " > " ^ + File.shell_path output_path ^ "\""); + val rc = + (case Posix.Process.fromStatus status of + Posix.Process.W_EXITED => 0 + | Posix.Process.W_EXITSTATUS w => Word8.toInt w + | Posix.Process.W_SIGNALED s => 256 + LargeWord.toInt (Posix.Signal.toWord s) + | Posix.Process.W_STOPPED s => 512 + LargeWord.toInt (Posix.Signal.toWord s)); - val status = - OS.Process.system ("exec \"$ISABELLE_HOME/lib/scripts/process\" no_group /dev/null" ^ - " script \"exec bash " ^ script_name ^ " > " ^ output_name ^ "\""); - val rc = - (case Posix.Process.fromStatus status of - Posix.Process.W_EXITED => 0 - | Posix.Process.W_EXITSTATUS w => Word8.toInt w - | Posix.Process.W_SIGNALED s => 256 + LargeWord.toInt (Posix.Signal.toWord s) - | Posix.Process.W_STOPPED s => 512 + LargeWord.toInt (Posix.Signal.toWord s)); + val output = the_default "" (try File.read output_path); + val _ = cleanup (); + in (output, rc) end + handle exn => (cleanup (); reraise exn) + end; - val output = read_file output_name handle IO.Io _ => ""; - val _ = OS.FileSys.remove script_name handle OS.SysErr _ => (); - val _ = OS.FileSys.remove output_name handle OS.SysErr _ => (); - in (output, rc) end; - -end; -