(* Title: Watcher.ML
ID: $Id$
Author: Claire Quigley
Copyright 2004 University of Cambridge
*)
(* The watcher process starts a resolution process when it receives a *)
(* message from Isabelle *)
(* Signals Isabelle, puts output of child into pipe to Isabelle, *)
(* and removes dead processes. Also possible to kill all the resolution *)
(* processes currently running. *)
signature WATCHER =
sig
(* Send request to Watcher for multiple spasses to be called for filenames in arg *)
(* callResProvers (outstreamtoWatcher, prover name,prover-command, (settings,file) list *)
val callResProvers : TextIO.outstream * (string*string*string*string) list -> unit
(* Send message to watcher to kill resolution provers *)
val callSlayer : TextIO.outstream -> unit
(* Start a watcher and set up signal handlers*)
val createWatcher :
Proof.context * thm * string Vector.vector list ->
TextIO.instream * TextIO.outstream * Posix.Process.pid
val killWatcher : Posix.Process.pid -> unit
val killChild : ('a, 'b) Unix.proc -> OS.Process.status
val command_sep : char
val setting_sep : char
val reapAll : unit -> unit
end
structure Watcher: WATCHER =
struct
(*Field separators, used to pack items onto a text line*)
val command_sep = #"\t"
and setting_sep = #"%";
val goals_being_watched = ref 0;
val trace_path = Path.basic "watcher_trace";
fun trace s = if !Output.debugging then File.append (File.tmp_path trace_path) s
else ();
(*Representation of a watcher process*)
type proc = {pid : Posix.Process.pid,
instr : TextIO.instream,
outstr : TextIO.outstream};
(*Representation of a child (ATP) process*)
type cmdproc = {
prover: string, (* Name of the resolution prover used, e.g. "spass"*)
file: string, (* The file containing the goal for the ATP to prove *)
proc_handle : (TextIO.instream,TextIO.outstream) Unix.proc,
instr : TextIO.instream, (*Output of the child process *)
outstr : TextIO.outstream}; (*Input to the child process *)
fun fdReader (name : string, fd : Posix.IO.file_desc) =
Posix.IO.mkTextReader {initBlkMode = true,name = name,fd = fd };
fun fdWriter (name, fd) =
Posix.IO.mkTextWriter {
appendMode = false,
initBlkMode = true,
name = name,
chunkSize=4096,
fd = fd};
fun openOutFD (name, fd) =
TextIO.mkOutstream (
TextIO.StreamIO.mkOutstream (
fdWriter (name, fd), IO.BLOCK_BUF));
fun openInFD (name, fd) =
TextIO.mkInstream (
TextIO.StreamIO.mkInstream (
fdReader (name, fd), ""));
(* Send request to Watcher for a vampire to be called for filename in arg*)
fun callResProver (toWatcherStr, arg) =
(TextIO.output (toWatcherStr, arg^"\n");
TextIO.flushOut toWatcherStr)
(* Send request to Watcher for multiple provers to be called*)
fun callResProvers (toWatcherStr, []) =
(TextIO.output (toWatcherStr, "End of calls\n"); TextIO.flushOut toWatcherStr)
| callResProvers (toWatcherStr,
(prover,proverCmd,settings,probfile) :: args) =
(trace (space_implode ", " (["\ncallResProvers:", prover, proverCmd, probfile]));
(*Uses a special character to separate items sent to watcher*)
TextIO.output (toWatcherStr,
space_implode (str command_sep) [prover, proverCmd, settings, probfile, "\n"]);
inc goals_being_watched;
TextIO.flushOut toWatcherStr;
callResProvers (toWatcherStr,args))
(*Send message to watcher to kill currently running vampires. NOT USED and possibly
buggy. Note that killWatcher kills the entire process group anyway.*)
fun callSlayer toWatcherStr = (TextIO.output (toWatcherStr, "Kill children\n");
TextIO.flushOut toWatcherStr)
(* Get commands from Isabelle*)
fun getCmds (toParentStr, fromParentStr, cmdList) =
let val thisLine = the_default "" (TextIO.inputLine fromParentStr)
in
trace("\nGot command from parent: " ^ thisLine);
if thisLine = "End of calls\n" orelse thisLine = "" then cmdList
else if thisLine = "Kill children\n"
then (TextIO.output (toParentStr,thisLine);
TextIO.flushOut toParentStr;
[("","Kill children",[],"")])
else
let val [prover,proverCmd,settingstr,probfile,_] =
String.tokens (fn c => c = command_sep) thisLine
val settings = String.tokens (fn c => c = setting_sep) settingstr
in
trace ("\nprover: " ^ prover ^ " prover path: " ^ proverCmd ^
"\n problem file: " ^ probfile);
getCmds (toParentStr, fromParentStr,
(prover, proverCmd, settings, probfile)::cmdList)
end
handle Bind =>
(trace "\ngetCmds: command parsing failed!";
getCmds (toParentStr, fromParentStr, cmdList))
end
(*Get Io-descriptor for polling of an input stream*)
fun getInIoDesc someInstr =
let val (rd, buf) = TextIO.StreamIO.getReader(TextIO.getInstream someInstr)
val _ = TextIO.output (TextIO.stdOut, buf)
val ioDesc =
case rd
of TextPrimIO.RD{ioDesc = SOME iod, ...} => SOME iod
| _ => NONE
in (* since getting the reader will have terminated the stream, we need
* to build a new stream. *)
TextIO.setInstream(someInstr, TextIO.StreamIO.mkInstream(rd, buf));
ioDesc
end
fun pollChild fromStr =
case getInIoDesc fromStr of
SOME iod =>
(case OS.IO.pollDesc iod of
SOME pd =>
let val pd' = OS.IO.pollIn pd in
case OS.IO.poll ([pd'], SOME (Time.fromSeconds 2)) of
[] => false
| pd''::_ => OS.IO.isIn pd''
end
| NONE => false)
| NONE => false
(*************************************)
(* Set up a Watcher Process *)
(*************************************)
fun killChild proc = (Unix.kill(proc, Posix.Signal.kill); Unix.reap proc);
val killChildren = List.app (ignore o killChild o #proc_handle) : cmdproc list -> unit;
fun killWatcher (toParentStr, procList) =
(trace "\nWatcher timeout: Killing proof processes";
TextIO.output(toParentStr, "Timeout: Killing proof processes!\n");
TextIO.flushOut toParentStr;
killChildren procList;
Posix.Process.exit 0w0);
(* take an instream and poll its underlying reader for input *)
fun pollParentInput (fromParentIOD, fromParentStr, toParentStr) =
case OS.IO.pollDesc fromParentIOD of
SOME pd =>
(case OS.IO.poll ([OS.IO.pollIn pd], SOME (Time.fromSeconds 2)) of
[] => NONE
| pd''::_ => if OS.IO.isIn pd''
then SOME (getCmds (toParentStr, fromParentStr, []))
else NONE)
| NONE => NONE;
(*get the number of the subgoal from the filename: the last digit string*)
fun number_from_filename s =
case String.tokens (not o Char.isDigit) s of
[] => (trace ("\nWatcher could not read subgoal nunber! " ^ s);
error "")
| numbers => valOf (Int.fromString (List.last numbers));
(*Call ATP. Settings should be a list of strings ["-t 300", "-m 100000"],
which we convert below to ["-t", "300", "-m", "100000"] using String.tokens.
Otherwise, the SML/NJ version of Unix.execute will escape the spaces, and
Vampire will reject the switches.*)
fun execCmds [] procList = procList
| execCmds ((prover,proverCmd,settings,file)::cmds) procList =
let val _ = trace ("\nAbout to execute command: " ^ proverCmd ^ " " ^ file)
val settings' = List.concat (map (String.tokens Char.isSpace) settings)
val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc =
Unix.execute(proverCmd, settings' @ [file])
val (instr, outstr) = Unix.streamsOf childhandle
val newProcList = {prover=prover, file=file, proc_handle=childhandle,
instr=instr, outstr=outstr} :: procList
val _ = trace ("\nFinished at " ^
Date.toString(Date.fromTimeLocal(Time.now())))
in execCmds cmds newProcList end
fun checkChildren (ctxt, th, thm_names_list) toParentStr children =
let fun check [] = [] (* no children to check *)
| check (child::children) =
let val {prover, file, proc_handle, instr=childIn, ...} : cmdproc = child
val _ = trace ("\nprobfile = " ^ file)
val sgno = number_from_filename file (*subgoal number*)
val thm_names = List.nth(thm_names_list, sgno-1);
val ppid = Posix.ProcEnv.getppid()
in
if pollChild childIn
then (* check here for prover label on child*)
let val _ = trace ("\nInput available from child: " ^ file)
val childDone = (case prover of
"vampire" => ResReconstruct.checkVampProofFound
(childIn, toParentStr, ppid, file, ctxt, th, sgno, thm_names)
| "E" => ResReconstruct.checkEProofFound
(childIn, toParentStr, ppid, file, ctxt, th, sgno, thm_names)
| "spass" => ResReconstruct.checkSpassProofFound
(childIn, toParentStr, ppid, file, ctxt, th, sgno, thm_names)
| _ => (trace ("\nBad prover! " ^ prover); true) )
in
if childDone (*ATP has reported back (with success OR failure)*)
then (Unix.reap proc_handle;
if !Output.debugging then () else OS.FileSys.remove file;
check children)
else child :: check children
end
else (trace "\nNo child output"; child :: check children)
end
in
trace ("\nIn checkChildren, length of queue: " ^ Int.toString(length children));
check children
end;
fun setupWatcher (ctxt, th, thm_names_list) =
let
val checkc = checkChildren (ctxt, th, thm_names_list)
val p1 = Posix.IO.pipe() (*pipes for communication between parent and watcher*)
val p2 = Posix.IO.pipe()
(****** fork a watcher process and get it set up and going ******)
fun startWatcher procList =
case Posix.Process.fork() of
SOME pid => pid (* parent - i.e. main Isabelle process *)
| NONE =>
let (* child - i.e. watcher *)
val oldchildin = #infd p1
val fromParent = Posix.FileSys.wordToFD 0w0
val oldchildout = #outfd p2
val toParent = Posix.FileSys.wordToFD 0w1
val fromParentIOD = Posix.FileSys.fdToIOD fromParent
val fromParentStr = openInFD ("_exec_in_parent", fromParent)
val toParentStr = openOutFD ("_exec_out_parent", toParent)
val pid = Posix.ProcEnv.getpid()
val () = Posix.ProcEnv.setpgid {pid = SOME pid, pgid = SOME pid}
(*set process group id: allows killing all children*)
val () = trace "\nsubgoals forked to startWatcher"
val limit = ref 200; (*don't let watcher run forever*)
(*Watcher Loop : Check running ATP processes for output*)
fun keepWatching procList =
(trace ("\npollParentInput. Limit = " ^ Int.toString (!limit) ^
" length(procList) = " ^ Int.toString(length procList));
OS.Process.sleep (Time.fromMilliseconds 100); limit := !limit - 1;
if !limit < 0 then killWatcher (toParentStr, procList)
else
case pollParentInput(fromParentIOD, fromParentStr, toParentStr) of
SOME [(_,"Kill children",_,_)] =>
(trace "\nReceived Kill command";
killChildren procList; keepWatching [])
| SOME cmds => (* deal with commands from Isabelle process *)
if length procList < 40 then (* Execute locally *)
let val _ = trace("\nCommands from parent: " ^
Int.toString(length cmds))
val newProcList' = checkc toParentStr (execCmds cmds procList)
in trace "\nCommands executed"; keepWatching newProcList' end
else (* Execute remotely [FIXME: NOT REALLY] *)
let val newProcList' = checkc toParentStr (execCmds cmds procList)
in keepWatching newProcList' end
| NONE => (* No new input from Isabelle *)
(trace "\nNothing from parent...";
keepWatching(checkc toParentStr procList)))
handle exn => (*FIXME: exn handler is too general!*)
(trace ("\nkeepWatching exception handler: " ^ Toplevel.exn_message exn);
keepWatching procList);
in
(*** Sort out pipes ********)
Posix.IO.close (#outfd p1); Posix.IO.close (#infd p2);
Posix.IO.dup2{old = oldchildin, new = fromParent};
Posix.IO.close oldchildin;
Posix.IO.dup2{old = oldchildout, new = toParent};
Posix.IO.close oldchildout;
keepWatching (procList)
end;
val _ = TextIO.flushOut TextIO.stdOut
val pid = startWatcher []
(* communication streams to watcher*)
val instr = openInFD ("_exec_in", #infd p2)
val outstr = openOutFD ("_exec_out", #outfd p1)
in
(* close the child-side fds*)
Posix.IO.close (#outfd p2); Posix.IO.close (#infd p1);
(* set the fds close on exec *)
Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
{pid = pid, instr = instr, outstr = outstr}
end;
(**********************************************************)
(* Start a watcher and set up signal handlers *)
(**********************************************************)
(*Signal handler to tidy away zombie processes*)
fun reapAll() =
(case Posix.Process.waitpid_nh(Posix.Process.W_ANY_CHILD, []) of
SOME _ => reapAll() | NONE => ())
handle OS.SysErr _ => ()
(*FIXME: does the main process need something like this?
IsaSignal.signal (IsaSignal.chld, IsaSignal.SIG_HANDLE reap)??*)
fun killWatcher pid =
(goals_being_watched := 0;
Posix.Process.kill(Posix.Process.K_GROUP pid, Posix.Signal.kill);
reapAll());
fun reapWatcher(pid, instr, outstr) = ignore
(TextIO.closeIn instr; TextIO.closeOut outstr;
Posix.Process.waitpid(Posix.Process.W_CHILD pid, []))
handle OS.SysErr _ => ()
fun string_of_subgoal th i =
string_of_cterm (List.nth(cprems_of th, i-1))
handle Subscript => "Subgoal number out of range!"
fun prems_string_of th = space_implode "\n" (map string_of_cterm (cprems_of th))
fun createWatcher (ctxt, th, thm_names_list) =
let val {pid=childpid, instr=childin, outstr=childout} = setupWatcher (ctxt,th,thm_names_list)
fun decr_watched() =
(goals_being_watched := !goals_being_watched - 1;
if !goals_being_watched = 0
then
(Output.debug (fn () => ("\nReaping a watcher, childpid = " ^ string_of_pid childpid));
killWatcher childpid (*???; reapWatcher (childpid, childin, childout)*) )
else ())
fun proofHandler _ =
let val _ = trace("\nIn signal handler for pid " ^ string_of_pid childpid)
val outcome = ResReconstruct.restore_newlines (the_default "" (TextIO.inputLine childin))
val probfile = the_default "" (TextIO.inputLine childin)
val sgno = number_from_filename probfile
val text = string_of_subgoal th sgno
fun report s = priority ("Subgoal " ^ Int.toString sgno ^ ": " ^ s);
in
Output.debug (fn () => ("In signal handler. outcome = \"" ^ outcome ^
"\"\nprobfile = " ^ probfile ^
"\nGoals being watched: "^ Int.toString (!goals_being_watched)));
if String.isPrefix "Invalid" outcome
then (report ("Subgoal is not provable:\n" ^ text);
decr_watched())
else if String.isPrefix "Failure" outcome
then (report ("Proof attempt failed:\n" ^ text);
decr_watched())
(* print out a list of rules used from clasimpset*)
else if String.isPrefix "Success" outcome
then (report (outcome ^ text);
decr_watched())
(* if proof translation failed *)
else if String.isPrefix "Translation failed" outcome
then (report (outcome ^ text);
decr_watched())
else (report "System error in proof handler";
decr_watched())
end
in Output.debug (fn () => ("subgoals forked to createWatcher: "^ prems_string_of th));
IsaSignal.signal (IsaSignal.usr2, IsaSignal.SIG_HANDLE proofHandler);
(childin, childout, childpid)
end
end (* structure Watcher *)