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