speed up early exit

src/halmos/processes.py

@@ -66,8 +66,6 @@ def cancel(self):
         if not self.is_running():
             return
 
-        self.process.terminate()
-
         # use psutil to kill the entire process tree (including children)
         try:
             parent_process = psutil.Process(self.process.pid)
@@ -78,8 +76,9 @@ def cancel(self):
             for process in processes:
                 process.terminate()
 
-            # give them some time to terminate
-            time.sleep(0.5)
+            # termination grace period
+            with contextlib.suppress(TimeoutExpired):
+                parent_process.wait(timeout=0.5)
 
             # after grace period, force kill
             for process in processes:
@@ -161,9 +160,12 @@ def shutdown(self, wait=True, cancel_futures=False):
 
         # if asked for immediate shutdown we cancel everything
         else:
-            with self._lock:
-                for future in self._futures:
-                    future.cancel()
+            with self._lock, concurrent.futures.ThreadPoolExecutor() as executor:
+                # kick off all cancellations in parallel
+                cancel_tasks = [executor.submit(f.cancel) for f in self._futures]
+
+                # wait for them to finish
+                concurrent.futures.wait(cancel_tasks)
 
     def map(self, fn, *iterables, timeout=None, chunksize=1):
         raise NotImplementedError()

src/halmos/solve.py

@@ -10,7 +10,6 @@
 from halmos.config import Config as HalmosConfig
 from halmos.constants import VERBOSITY_TRACE_COUNTEREXAMPLE, VERBOSITY_TRACE_PATHS
 from halmos.logs import (
-    COUNTEREXAMPLE_INVALID,
     COUNTEREXAMPLE_UNKNOWN,
     debug,
     error,
@@ -19,7 +18,7 @@
 )
 from halmos.processes import PopenExecutor, PopenFuture, TimeoutExpired
 from halmos.sevm import Exec, SMTQuery
-from halmos.utils import con, red, stringify
+from halmos.utils import con, stringify
 
 
 @dataclass
@@ -468,16 +467,13 @@ def solve_end_to_end(ctx: PathContext) -> None:
         return
 
     if model.is_valid:
-        print(red(f"Counterexample: {model}"))
-
         fun_ctx.valid_counterexamples.append(model)
 
         # we have a valid counterexample, so we are eligible for early exit
         if args.early_exit:
+            debug(f"Shutting down {fun_ctx.info.name}'s solver executor")
             fun_ctx.solver_executor.shutdown(wait=False)
     else:
-        warn_str = f"Counterexample (potentially invalid): {model}"
-        warn_code(COUNTEREXAMPLE_INVALID, warn_str)
         fun_ctx.invalid_counterexamples.append(model)