more accurate timeout

autoverify/portfolio/portfolio.py

@@ -174,6 +174,7 @@ def get_costs(self, instances: Iterable[str]) -> dict[str, float]:
         return costs
 
     def get_all_costs(self) -> dict[str, float]:
+        """All the recorded costs."""
         return self._costs
 
     def get_mean_cost(self) -> float:

autoverify/portfolio/portfolio_runner.py

@@ -1,5 +1,4 @@
 """_summary_."""
-import concurrent.futures
 import logging
 from typing import TypeVar
 
@@ -124,14 +123,14 @@ def _vbs_from_cost_dict(cost_dict: _CostDict) -> _VbsResult:
 
         for cv, instance_costs in cost_dict.items():
             for instance, cost in instance_costs.items():
-                instance = str(instance)
+                str_inst = str(instance)
 
-                if instance not in vbs:
-                    vbs[instance] = (cost, cv.verifier)
+                if str_inst not in vbs:
+                    vbs[str_inst] = (cost, cv.verifier)
                     continue
 
-                if cost < vbs[instance][0]:
-                    vbs[instance] = (cost, cv.verifier)
+                if cost < vbs[str_inst][0]:
+                    vbs[str_inst] = (cost, cv.verifier)
 
         return vbs
 

autoverify/util/proc.py

@@ -5,6 +5,20 @@
 from typing import Iterable
 
 
+# Credits: @jfs
+def pid_exists(pid):
+    if pid < 0:
+        return False  # NOTE: pid == 0 returns True
+    try:
+        os.kill(pid, 0)
+    except ProcessLookupError:  # errno.ESRCH
+        return False  # No such process
+    except PermissionError:  # errno.EPERM
+        return True  # Operation not permitted (i.e., process exists)
+    else:
+        return True  # no error, we can send a signal to the process
+
+
 def pkill_match(pattern: str):
     """Kill processes matching the pattern."""
     cmd = f'pkill -f "{pattern}"'

autoverify/util/verification_instance.py

@@ -30,6 +30,7 @@ def __hash__(self):
         )
 
     def __str__(self):
+        """Short string representation of the `VerificationInstance`."""
         return f"{self.network.name} :: {self.property.name} :: {self.timeout}"
 
     def as_smac_instance(self) -> str:

autoverify/verifier/complete/abcrown/verifier.py

@@ -1,7 +1,6 @@
 """ab-crown verifier."""
 from collections.abc import Iterable
 from pathlib import Path
-from subprocess import CompletedProcess
 from typing import Any, ContextManager
 
 from ConfigSpace import Configuration, ConfigurationSpace

autoverify/verifier/complete/mnbab/verifier.py

@@ -1,6 +1,5 @@
 """Nnenum verifier."""
 from pathlib import Path
-from subprocess import CompletedProcess
 from typing import ContextManager
 
 from ConfigSpace import Configuration, ConfigurationSpace
@@ -54,7 +53,7 @@ def contexts(self) -> list[ContextManager[None]]:
 
     def _parse_result(
         self,
-        sp_result: CompletedProcess[bytes] | None,
+        _: str,
         result_file: Path | None,
     ) -> tuple[VerificationResultString, str | None]:
         # TODO:

autoverify/verifier/complete/nnenum/verifier.py

@@ -1,7 +1,6 @@
 """Nnenum verifier."""
 import shlex
 from pathlib import Path
-from subprocess import CompletedProcess
 from typing import Any, ContextManager, Iterable
 
 from ConfigSpace import Configuration, ConfigurationSpace

autoverify/verifier/complete/ovalbab/verifier.py

@@ -1,7 +1,6 @@
 """OvalBab verifier."""
 from collections.abc import Iterable
 from pathlib import Path
-from subprocess import CompletedProcess
 from typing import Any, ContextManager
 
 from ConfigSpace import Configuration, ConfigurationSpace

autoverify/verifier/complete/verinet/verifier.py

@@ -1,7 +1,6 @@
 """_summary_."""
 import shlex
 from pathlib import Path
-from subprocess import CompletedProcess
 from typing import Any, ContextManager, Iterable
 
 from ConfigSpace import Configuration, ConfigurationSpace

autoverify/verifier/verifier.py

@@ -20,7 +20,7 @@
 )
 from autoverify.util.env import environment
 from autoverify.util.path import check_file_extension
-from autoverify.util.proc import nvidia_gpu_count, taskset_cpu_range
+from autoverify.util.proc import nvidia_gpu_count, pid_exists, taskset_cpu_range
 from autoverify.util.verification_instance import VerificationInstance
 
 from .verification_result import (
@@ -316,26 +316,30 @@ def _run_verification(
                 preexec_fn=os.setsid,
             )
 
-            assert process.stdout
             before_t = time.time()
+            timeout_event = threading.Event()
 
-            # TODO: Make result a TIMEOUT
-            # FIXME: This is never called
             def _terminate(timeout_sec):
-                time.sleep(timeout_sec)
-                global result
-                result = "TIMEOUT"
-                os.killpg(os.getpgid(process.pid), signal.SIGTERM)
+                on_time = timeout_event.wait(timeout_sec)
+
+                if not on_time:
+                    global result
+                    result = "TIMEOUT"  # type: ignore
+
+                if pid_exists(process.pid):
+                    os.killpg(os.getpgid(process.pid), signal.SIGTERM)
 
             t = threading.Thread(target=_terminate, args=[timeout])
             t.start()
 
+            assert process.stdout
             for line in iter(process.stdout.readline, ""):
                 output_lines.append(line)
 
             process.stdout.close()
             return_code = process.wait()
             took_t = time.time() - before_t
+            timeout_event.set()
 
             output_str = "\n".join(output_lines)
             counter_example: str | None = None
@@ -349,7 +353,7 @@ def _terminate(timeout_sec):
                     )
 
             return CompleteVerificationData(
-                result,
+                result,  # type: ignore
                 took_t,
                 counter_example,
                 "",  # TODO: Remove err field; we pipe it to stdout