implement parent monitoring thread

[karmacoma-eth]

fixes #7

[karmacoma-eth]

tested with:

# quickexit.py

import subprocess
import sys

proc = subprocess.Popen(
    ["rye", "run", "jsi", "--full-run", "--debug", "examples/unsat_div.smt2"]
)

print(f"started {proc.pid=}")
sys.exit(42)

[karmacoma-eth]

does not work as intended with halmos, and can repro the problem with the following snippet:

import subprocess
import sys
import time

timeout = int(sys.argv[1]) if len(sys.argv) > 1 else 5

try:
    cmd = ["jsi", "--full-run", "--debug", "examples/unsat_div.smt2"]
    output = subprocess.run(
        cmd, capture_output=False, text=True, timeout=timeout
    ).stdout.strip()
except KeyboardInterrupt:
    print("quickexit: caught KeyboardInterrupt")
    time.sleep(timeout)

sys.exit(42)

it is possible to get to quickexit: caught KeyboardInterrupt, but parent process died, exiting... is never printed by jsi and the solvers keep running 🤨

[karmacoma-eth]

does not work as intended with halmos, and can repro the problem with the following snippet:

import subprocess
import sys
import time

timeout = int(sys.argv[1]) if len(sys.argv) > 1 else 5

try:
    cmd = ["jsi", "--full-run", "--debug", "examples/unsat_div.smt2"]
    output = subprocess.run(
        cmd, capture_output=False, text=True, timeout=timeout
    ).stdout.strip()
except KeyboardInterrupt:
    print("quickexit: caught KeyboardInterrupt")
    time.sleep(timeout)

sys.exit(42)

it is possible to get to quickexit: caught KeyboardInterrupt, but parent process died, exiting... is never printed by jsi and the solvers keep running 🤨

that is because subprocess.run wraps communicate with an exception handler that can call process.kill() (SIGKILL, not SIGTERM), which kills the jsi process (and its parent monitor thread) but not the solvers. Out of scope for the thread -- this is something the reaper should be able to deal with.

Halmos should also be changed to avoid sending SIGKILL to jsi