Skip to content

Commit

Permalink
fix timing out [skip ci]
Browse files Browse the repository at this point in the history
  • Loading branch information
kw-corne committed Aug 31, 2023
1 parent 52fad1a commit 64e4447
Show file tree
Hide file tree
Showing 2 changed files with 21 additions and 16 deletions.
2 changes: 1 addition & 1 deletion autoverify/portfolio/portfolio_runner.py
Original file line number Diff line number Diff line change
Expand Up @@ -172,6 +172,6 @@ def verify_instances(
results: dict[_VI, VerificationDataResult] = {}

for cv in self._portfolio:
print(cv)
print(cv.verifier, cv.resources)

return results
35 changes: 20 additions & 15 deletions autoverify/verifier/verifier.py
Original file line number Diff line number Diff line change
@@ -1,6 +1,8 @@
"""TODO docstring."""
import sched
import os
import signal
import subprocess
import threading
import time
from abc import ABC, abstractmethod
from contextlib import ExitStack
Expand Down Expand Up @@ -295,6 +297,7 @@ def _run_verification(
"""_summary_."""
contexts = self.contexts or []
output_lines: list[str] = []
result: str = ""

if self._cpu_gpu_allocation is not None:
run_cmd = self._allocate_run_cmd(run_cmd, contexts)
Expand All @@ -310,38 +313,40 @@ def _run_verification(
stderr=subprocess.STDOUT,
shell=True,
universal_newlines=True,
preexec_fn=os.setsid,
)

assert process.stdout
before_t = time.time()

# TODO: Make result a TIMEOUT
def _terminate():
process.terminate()
# 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)

s = sched.scheduler(time.monotonic, time.sleep)
timeout_event = s.enter(timeout, 0, _terminate)
s.run(blocking=False)
t = threading.Thread(target=_terminate, args=[timeout])
t.start()

for line in iter(process.stdout.readline, ""):
output_lines.append(line)

if timeout_event in s.queue:
s.cancel(timeout_event)

process.stdout.close()
return_code = process.wait()
took_t = time.time() - before_t

output_str = "\n".join(output_lines)
counter_example: str | None = None

if return_code > 0:
result = "ERR"
else:
result, counter_example = self._parse_result(
output_str, result_file
)
if result != "TIMEOUT":
if return_code > 0:
result = "ERR"
else:
result, counter_example = self._parse_result(
output_str, result_file
)

return CompleteVerificationData(
result,
Expand Down

0 comments on commit 64e4447

Please sign in to comment.