src/HOL/Tools/ATP/watcher.ML
author paulson
Wed Oct 05 11:18:06 2005 +0200 (2005-10-05)
changeset 17764 fde495b9e24b
parent 17746 af59c748371d
child 17772 818cec5f82a4
permissions -rw-r--r--
improved process handling. tidied
     1 (*  Title:      Watcher.ML
     2     ID:         $Id$
     3     Author:     Claire Quigley
     4     Copyright   2004  University of Cambridge
     5  *)
     6 
     7 (*  The watcher process starts a resolution process when it receives a     *)
     8 (*  message from Isabelle                                                  *)
     9 (*  Signals Isabelle, puts output of child into pipe to Isabelle,          *)
    10 (*  and removes dead processes.  Also possible to kill all the resolution  *)
    11 (*  processes currently running.                                           *)
    12 
    13 signature WATCHER =
    14 sig
    15 
    16 (*  Send request to Watcher for multiple spasses to be called for filenames in arg       *)
    17 (* callResProvers (outstreamtoWatcher, prover name,prover-command, (settings,file) list *)
    18 
    19 val callResProvers :
    20     TextIO.outstream * (string*string*string*string*string) list 
    21     -> unit
    22 
    23 (* Send message to watcher to kill resolution provers *)
    24 val callSlayer : TextIO.outstream -> unit
    25 
    26 (* Start a watcher and set up signal handlers             *)
    27 val createWatcher : 
    28     thm * (ResClause.clause * thm) Array.array -> 
    29     TextIO.instream * TextIO.outstream * Posix.Process.pid
    30 val killWatcher : Posix.Process.pid -> unit
    31 val setting_sep : char
    32 end
    33 
    34 
    35 
    36 structure Watcher: WATCHER =
    37 struct
    38 
    39 (*Field separators, used to pack items onto a text line*)
    40 val command_sep = #"\t"
    41 and setting_sep = #"%";
    42 
    43 open Recon_Transfer
    44 
    45 val goals_being_watched = ref 0;
    46 
    47 val trace_path = Path.basic "watcher_trace";
    48 
    49 fun trace s = if !Output.show_debug_msgs then File.append (File.tmp_path trace_path) s 
    50               else ();
    51 
    52 (*  The result of calling createWatcher  *)
    53 datatype proc = PROC of {
    54         pid : Posix.Process.pid,
    55         instr : TextIO.instream,
    56         outstr : TextIO.outstream
    57       };
    58 
    59 (*  The result of calling executeToList  *)
    60 datatype cmdproc = CMDPROC of {
    61         prover: string,       (* Name of the resolution prover used, e.g. Vampire*)
    62         cmd:  string,         (* The file containing the goal for res prover to prove *)     
    63         goalstring: string,   (* string representation of subgoal*) 
    64         proc_handle : (TextIO.instream,TextIO.outstream) Unix.proc,
    65         instr : TextIO.instream,   (*  Input stream to child process *)
    66         outstr : TextIO.outstream};  (*  Output stream from child process *)
    67 
    68 type signal = Posix.Signal.signal
    69 datatype exit_status = datatype Posix.Process.exit_status
    70 
    71 val fromStatus = Posix.Process.fromStatus
    72 
    73 fun reap(pid, instr, outstr) =
    74   let val u = TextIO.closeIn instr;
    75       val u = TextIO.closeOut outstr;
    76       val (_, status) = Posix.Process.waitpid(Posix.Process.W_CHILD pid, [])
    77   in status end
    78 
    79 fun fdReader (name : string, fd : Posix.IO.file_desc) =
    80 	  Posix.IO.mkTextReader {initBlkMode = true,name = name,fd = fd };
    81 
    82 fun fdWriter (name, fd) =
    83           Posix.IO.mkTextWriter {
    84 	      appendMode = false,
    85               initBlkMode = true,
    86               name = name,  
    87               chunkSize=4096,
    88               fd = fd};
    89 
    90 fun openOutFD (name, fd) =
    91 	  TextIO.mkOutstream (
    92 	    TextIO.StreamIO.mkOutstream (
    93 	      fdWriter (name, fd), IO.BLOCK_BUF));
    94 
    95 fun openInFD (name, fd) =
    96 	  TextIO.mkInstream (
    97 	    TextIO.StreamIO.mkInstream (
    98 	      fdReader (name, fd), ""));
    99 
   100 fun childInfo (PROC{pid,instr,outstr }) = (pid,(instr,outstr));
   101 
   102 fun cmdstreamsOf (CMDPROC{instr,outstr,...}) = (instr, outstr);
   103 
   104 fun cmdInStream (CMDPROC{instr,outstr,...}) = instr;
   105 
   106 fun cmdchildInfo (CMDPROC{prover,cmd,proc_handle,goalstring,instr,outstr}) = 
   107   (prover,(cmd, (instr,outstr)));
   108 
   109 fun cmdchildHandle (CMDPROC{prover,cmd,goalstring,proc_handle,instr,outstr})  = 
   110   proc_handle;
   111 
   112 fun cmdProver (CMDPROC{prover,cmd,goalstring,proc_handle,instr,outstr})  =
   113   prover;
   114 
   115 fun cmdGoal (CMDPROC{prover,cmd,goalstring,proc_handle,instr,outstr})  =
   116   goalstring;
   117 
   118 
   119 (*    gets individual args from instream and concatenates them into a list      *)
   120 fun getArgs (fromParentStr, toParentStr, ys) =  
   121   let val thisLine = TextIO.input fromParentStr
   122   in ys@[thisLine] end
   123 
   124                             
   125 (*  Send request to Watcher for a vampire to be called for filename in arg      *)
   126                    
   127 fun callResProver (toWatcherStr,  arg) = 
   128       (TextIO.output (toWatcherStr, arg^"\n"); 
   129        TextIO.flushOut toWatcherStr)
   130 
   131 (*****************************************************************************************)
   132 (*  Send request to Watcher for multiple provers to be called for filenames in arg       *)
   133 (*  need to do the dfg stuff in the watcher, not here! send over the clasimp and stuff files too*)
   134 (*****************************************************************************************)
   135 
   136 fun callResProvers (toWatcherStr,  []) = 
   137       (TextIO.output (toWatcherStr, "End of calls\n");  TextIO.flushOut toWatcherStr)
   138 |   callResProvers (toWatcherStr,
   139                     (prover,goalstring, proverCmd,settings, 
   140                      probfile)  ::  args) =
   141       let val _ = trace (space_implode "\n" 
   142 		         (["\ncallResProvers:",prover,goalstring,proverCmd,settings,
   143 			  probfile]))
   144       in TextIO.output (toWatcherStr,
   145                         (*Uses a special character to separate items sent to watcher*)
   146       	                space_implode (str command_sep)
   147                           [prover, proverCmd, settings, probfile,
   148                            String.toString goalstring ^ "\n"]);
   149               (*goalstring is a single string literal, with all specials escaped.*)
   150          goals_being_watched := (!goals_being_watched) + 1;
   151 	 TextIO.flushOut toWatcherStr;
   152 	 callResProvers (toWatcherStr,args)
   153       end   
   154                                                 
   155                                     
   156  
   157 
   158 (*Send message to watcher to kill currently running vampires. NOT USED and possibly
   159   buggy. Note that killWatcher kills the entire process group anyway.*)
   160 fun callSlayer toWatcherStr = (TextIO.output (toWatcherStr, "Kill children\n"); 
   161                             TextIO.flushOut toWatcherStr)
   162 
   163                     
   164 (**************************************************************)
   165 (* Get commands from Isabelle                                 *)
   166 (**************************************************************)
   167 fun getCmds (toParentStr, fromParentStr, cmdList) = 
   168   let val thisLine = TextIO.inputLine fromParentStr 
   169   in
   170      trace("\nGot command from parent: " ^ thisLine);
   171      if thisLine = "End of calls\n" orelse thisLine = "" then cmdList
   172      else if thisLine = "Kill children\n"
   173      then (TextIO.output (toParentStr,thisLine); 
   174 	   TextIO.flushOut toParentStr;
   175 	   [("","","Kill children",[],"")])
   176      else
   177        let val [prover,proverCmd,settingstr,probfile,goalstring] = 
   178                    String.tokens (fn c => c = command_sep) thisLine
   179            val settings = String.tokens (fn c => c = setting_sep) settingstr
   180        in
   181            trace ("\nprover: " ^ prover ^ "  prover path: " ^ proverCmd^
   182                   "  problem file: " ^ probfile ^ 
   183 		  "\ngoalstring:  "^goalstring);
   184            getCmds (toParentStr, fromParentStr, 
   185                     (prover, goalstring, proverCmd, settings, probfile)::cmdList) 
   186        end
   187        handle Bind => 
   188           (trace "getCmds: command parsing failed!";
   189            getCmds (toParentStr, fromParentStr, cmdList))
   190   end
   191 	    
   192                                                                   
   193 (**************************************************************)
   194 (*  Get Io-descriptor for polling of an input stream          *)
   195 (**************************************************************)
   196 
   197 fun getInIoDesc someInstr = 
   198     let val (rd, buf) = TextIO.StreamIO.getReader(TextIO.getInstream someInstr)
   199         val _ = TextIO.output (TextIO.stdOut, buf)
   200         val ioDesc = 
   201 	    case rd
   202 	      of TextPrimIO.RD{ioDesc = SOME iod, ...} =>SOME iod
   203 	       | _ => NONE
   204      in (* since getting the reader will have terminated the stream, we need
   205 	 * to build a new stream. *)
   206 	TextIO.setInstream(someInstr, TextIO.StreamIO.mkInstream(rd, buf));
   207 	ioDesc
   208     end
   209 
   210 
   211 (*************************************)
   212 (*  Set up a Watcher Process         *)
   213 (*************************************)
   214 
   215 (* for tracing: encloses each string element in brackets. *)
   216 val concat_with_and = space_implode " & " o map (enclose "(" ")");
   217 
   218 fun prems_string_of th =
   219   concat_with_and (map (Sign.string_of_term (sign_of_thm th)) (prems_of th))
   220 
   221 fun killChild proc = (Unix.kill(proc, Posix.Signal.kill); Unix.reap proc);
   222 
   223 fun killChildren procs = List.app (ignore o killChild) procs;
   224 
   225  (*************************************************************)
   226  (* take an instream and poll its underlying reader for input *)
   227  (*************************************************************)
   228  
   229  fun pollParentInput (fromParentIOD, fromParentStr, toParentStr) = 
   230    case OS.IO.pollDesc fromParentIOD of
   231       SOME pd =>
   232 	 (case OS.IO.poll ([OS.IO.pollIn pd], SOME (Time.fromSeconds 2)) of
   233 	      [] => NONE
   234 	    | pd''::_ => if OS.IO.isIn pd''
   235 	 	         then SOME (getCmds (toParentStr, fromParentStr, []))
   236 	 	         else NONE)
   237    | NONE => NONE;
   238 
   239 (*get the number of the subgoal from the filename: the last digit string*)
   240 fun number_from_filename s =
   241   case String.tokens (not o Char.isDigit) s of
   242       [] => (trace "\nWatcher could not read subgoal nunber!!"; raise ERROR)
   243     | numbers => valOf (Int.fromString (List.last numbers));
   244 
   245 fun setupWatcher (thm,clause_arr) = 
   246   let
   247     val p1 = Posix.IO.pipe ()   (** pipes for communication between parent and watcher **)
   248     val p2 = Posix.IO.pipe ()
   249     fun closep () = 
   250 	 (Posix.IO.close (#outfd p1); Posix.IO.close (#infd p1);
   251 	  Posix.IO.close (#outfd p2); Posix.IO.close (#infd p2))
   252     (****** fork a watcher process and get it set up and going ******)
   253     fun startWatcher procList =
   254      (case  Posix.Process.fork() 
   255       of SOME pid => pid (* parent - i.e. main Isabelle process *)
   256        | NONE => let                (* child - i.e. watcher  *)
   257 	  val oldchildin = #infd p1  
   258 	  val fromParent = Posix.FileSys.wordToFD 0w0
   259 	  val oldchildout = #outfd p2
   260 	  val toParent = Posix.FileSys.wordToFD 0w1
   261 	  val fromParentIOD = Posix.FileSys.fdToIOD fromParent
   262 	  val fromParentStr = openInFD ("_exec_in_parent", fromParent)
   263 	  val toParentStr = openOutFD ("_exec_out_parent", toParent)
   264 	  val pid = Posix.ProcEnv.getpid()
   265 	  val () = Posix.ProcEnv.setpgid {pid = SOME pid, pgid = SOME pid}
   266                    (*set process group id: allows killing all children*)
   267 	  val () = debug ("subgoals forked to startWatcher: "^ prems_string_of thm);
   268 	 
   269 	  fun pollChildInput fromStr = 
   270 	     case getInIoDesc fromStr of
   271 	       SOME iod => 
   272 		 (case OS.IO.pollDesc iod of
   273 		    SOME pd =>
   274 			let val pd' = OS.IO.pollIn pd in
   275 			  case OS.IO.poll ([pd'], SOME (Time.fromSeconds 2)) of
   276 			      [] => false
   277 			    | pd''::_ => OS.IO.isIn pd''
   278 			end
   279 		   | NONE => false)
   280 	     | NONE => false
   281 
   282 	  (* Check all ATP processes currently running for output                 *)
   283 	  fun checkChildren ([], toParentStr) = []  (* no children to check *)
   284 	  |   checkChildren (childProc::otherChildren, toParentStr) = 
   285 	       let val _ = trace ("\nIn check child, length of queue:"^
   286 			          Int.toString (length (childProc::otherChildren)))
   287 		   val (childInput,childOutput) = cmdstreamsOf childProc
   288 		   val child_handle = cmdchildHandle childProc
   289 		   val childCmd = #1(#2(cmdchildInfo childProc)) (*name of problem file*)
   290 		   val _ = trace ("\nchildCmd = " ^ childCmd)
   291 		   val sg_num = number_from_filename childCmd
   292 		   val childIncoming = pollChildInput childInput
   293 		   val parentID = Posix.ProcEnv.getppid()
   294 		   val prover = cmdProver childProc
   295 		   val prems_string = prems_string_of thm
   296 		   val goalstring = cmdGoal childProc							
   297 	       in 
   298 		 trace("\nsubgoals forked to checkChildren: " ^ goalstring);
   299 		 if childIncoming
   300 		 then (* check here for prover label on child*)
   301 		   let val _ = trace ("\nInput available from child: " ^ childCmd ^ 
   302 				      "\ngoalstring is " ^ goalstring)
   303 		       val childDone = (case prover of
   304 			   "vampire" => AtpCommunication.checkVampProofFound(childInput, toParentStr, parentID,goalstring, childCmd, clause_arr)  
   305 			    | "E" => AtpCommunication.checkEProofFound(childInput, toParentStr, parentID,goalstring, childCmd, clause_arr)             
   306 			  |"spass" => AtpCommunication.checkSpassProofFound(childInput, toParentStr, parentID,goalstring, childCmd, thm, sg_num,clause_arr)  )
   307 		    in
   308 		     if childDone
   309 		     then (* child has found a proof and transferred it *)
   310 			(* Remove this child and go on to check others*)
   311 			(Unix.reap child_handle;
   312 			 OS.FileSys.remove childCmd;
   313 			 checkChildren(otherChildren, toParentStr))
   314 		     else (* Keep this child and go on to check others  *)
   315 		       childProc :: checkChildren (otherChildren, toParentStr)
   316 		  end
   317 		else (trace "\nNo child output";
   318 		      childProc::(checkChildren (otherChildren, toParentStr)))
   319 	       end
   320 
   321 	
   322 	(* call resolution processes                                        *)
   323 	(* settings should be a list of strings  ["-t 300", "-m 100000"]    *)
   324 	(* takes list of (string, string, string list, string)list proclist *)
   325 	fun execCmds [] procList = procList
   326 	|   execCmds ((prover, goalstring,proverCmd,settings,file)::cmds) procList  =
   327 	      let val _ = trace (space_implode "\n" 
   328 				 (["\nAbout to execute command for goal:",
   329 				   goalstring, proverCmd] @ settings @
   330 				  [file, Date.toString(Date.fromTimeLocal(Time.now()))]))
   331 	          val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc  = 
   332 		       Unix.execute(proverCmd, settings@[file])
   333 		  val (instr, outstr) = Unix.streamsOf childhandle
   334 		  val newProcList = CMDPROC{prover = prover,
   335 					    cmd = file,
   336 					    goalstring = goalstring,
   337 					    proc_handle = childhandle,
   338 					    instr = instr,
   339 					    outstr = outstr} :: procList
   340      
   341 		  val _ = trace ("\nFinished at " ^
   342 			         Date.toString(Date.fromTimeLocal(Time.now())))
   343 	      in execCmds cmds newProcList end
   344 
   345          (******** Watcher Loop ********)
   346          val limit = ref 500;  (*don't let it run forever*)
   347 
   348 	 fun keepWatching (procList) = 
   349 	   let fun loop procList =  
   350 	      let val _ = trace ("\nCalling pollParentInput: " ^ Int.toString (!limit));
   351 		  val cmdsFromIsa = pollParentInput 
   352 				     (fromParentIOD, fromParentStr, toParentStr)
   353 	      in 
   354 		 OS.Process.sleep (Time.fromMilliseconds 100);
   355 		 limit := !limit - 1;
   356 		 if !limit = 0 
   357 		 then 
   358 		  (trace "\nTimeout: Killing proof processes";
   359 		   TextIO.output(toParentStr, "Timeout: Killing proof processes!\n");
   360 		   TextIO.flushOut toParentStr;
   361 		   killChildren (map cmdchildHandle procList);
   362 		   exit 0)
   363 		 else case cmdsFromIsa of
   364 		     SOME [(_,_,"Kill children",_,_)] => 
   365 		       let val child_handles = map cmdchildHandle procList 
   366 		       in  killChildren child_handles; loop []  end
   367 		   | SOME cmds => (*  deal with commands from Isabelle process *)
   368 		       if length procList < 40
   369 		       then                        (* Execute locally  *)
   370 			 let 
   371 			   val newProcList = execCmds cmds procList
   372 			   val newProcList' = checkChildren (newProcList, toParentStr) 
   373 			 in
   374 			   trace "\nJust execed a child"; loop newProcList'
   375 			 end
   376 		       else  (* Execute remotely [FIXME: NOT REALLY]  *)
   377 			 let 
   378 			   val newProcList = execCmds cmds procList
   379 			   val newProcList' = checkChildren (newProcList, toParentStr) 
   380 			 in loop newProcList' end
   381 		   | NONE => (* No new input from Isabelle *)
   382 		       let val newProcList = checkChildren (procList, toParentStr)
   383 		       in
   384 			 trace "\nNo new input, still watching"; loop newProcList
   385 		       end
   386 	       end
   387 	   in  
   388 	       loop procList
   389 	   end
   390 	   
   391 
   392 	 in
   393 	  (*** Sort out pipes ********)
   394 	   Posix.IO.close (#outfd p1);
   395 	   Posix.IO.close (#infd p2);
   396 	   Posix.IO.dup2{old = oldchildin, new = fromParent};
   397 	   Posix.IO.close oldchildin;
   398 	   Posix.IO.dup2{old = oldchildout, new = toParent};
   399 	   Posix.IO.close oldchildout;
   400 
   401 	   (* start the watcher loop  *)
   402 	   keepWatching (procList);
   403 	   (* fake return value - actually want the watcher to loop until killed *)
   404 	   Posix.Process.wordToPid 0w0
   405 	 end);
   406      (* end case *)
   407 
   408 
   409     val _ = TextIO.flushOut TextIO.stdOut
   410 
   411     (*******************************)
   412     (***  set watcher going ********)
   413     (*******************************)
   414 
   415     val procList = []
   416     val pid = startWatcher procList
   417     (**************************************************)
   418     (* communication streams to watcher               *)
   419     (**************************************************)
   420 
   421     val instr = openInFD ("_exec_in", #infd p2)
   422     val outstr = openOutFD ("_exec_out", #outfd p1)
   423     
   424   in
   425    (*******************************)
   426    (* close the child-side fds    *)
   427    (*******************************)
   428     Posix.IO.close (#outfd p2);
   429     Posix.IO.close (#infd p1);
   430     (* set the fds close on exec *)
   431     Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
   432     Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
   433      
   434    (*******************************)
   435    (* return value                *)
   436    (*******************************)
   437     PROC{pid = pid, instr = instr, outstr = outstr}
   438   end;
   439 
   440 
   441 
   442 (**********************************************************)
   443 (* Start a watcher and set up signal handlers             *)
   444 (**********************************************************)
   445 
   446 fun killWatcher pid = Posix.Process.kill(Posix.Process.K_GROUP pid, Posix.Signal.kill);
   447 
   448 fun reapWatcher(pid, instr, outstr) =
   449   (TextIO.closeIn instr; TextIO.closeOut outstr;
   450    Posix.Process.waitpid(Posix.Process.W_CHILD pid, []); ())
   451 
   452 fun createWatcher (thm, clause_arr) =
   453  let val (childpid,(childin,childout)) = childInfo (setupWatcher(thm,clause_arr))
   454      fun decr_watched() =
   455 	  (goals_being_watched := !goals_being_watched - 1;
   456 	   if !goals_being_watched = 0
   457 	   then 
   458 	     (debug ("\nReaping a watcher, childpid = "^
   459 		     LargeWord.toString (Posix.Process.pidToWord childpid));
   460 	      killWatcher childpid; reapWatcher (childpid,childin, childout))
   461 	    else ())
   462      val _ = debug ("subgoals forked to createWatcher: "^ prems_string_of thm);
   463      fun proofHandler n = 
   464        let val outcome = TextIO.inputLine childin
   465 	   val goalstring = valOf (String.fromString (TextIO.inputLine childin))
   466 	   val _ = debug ("In signal handler. outcome = \"" ^ outcome ^ 
   467 		        "\"\ngoalstring = " ^ goalstring ^
   468 		        "\ngoals_being_watched: "^  Int.toString (!goals_being_watched))
   469        in 
   470 	 if String.isPrefix "[" outcome (*indicates a proof reconstruction*)
   471 	 then (priority (Recon_Transfer.apply_res_thm outcome goalstring);
   472 	       decr_watched())
   473 	 else if String.isPrefix "Invalid" outcome
   474 	 then (priority ("Subgoal is not provable:\n" ^ goalstring);
   475 	       decr_watched())
   476 	 else if String.isPrefix "Failure" outcome
   477 	 then (priority ("Proof attempt failed:\n" ^ goalstring);
   478 	       decr_watched()) 
   479 	(* print out a list of rules used from clasimpset*)
   480 	 else if String.isPrefix "Success" outcome
   481 	 then (priority (outcome ^ goalstring);
   482 	       decr_watched())
   483 	  (* if proof translation failed *)
   484 	 else if String.isPrefix "Translation failed" outcome
   485 	 then (priority (outcome ^ goalstring);
   486 	       decr_watched())
   487 	 else (priority "System error in proof handler";
   488 	       decr_watched())
   489        end
   490  in IsaSignal.signal (IsaSignal.usr2, IsaSignal.SIG_HANDLE proofHandler);
   491     (childin, childout, childpid)
   492   end
   493 
   494 end (* structure Watcher *)