From 45378acd1527d3b30fc8251929518875d2338328 Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 14 Aug 2026 01:27:35 +0000 Subject: [PATCH 1/4] Remove the pcsat container when the wrapper is killed Thrust gives up on a solver that exceeds its timeout by killing the wrapper with SIGKILL, which runs no trap and leaves the container behind: Docker keeps a container going after the client attached to it is gone, so the solver ran on in the background for as long as it took, or forever on an instance it cannot solve. Removing it has to be left to a process that outlives the wrapper. That process waits for the write end of a pipe, which the kernel closes however the wrapper dies, and then force-removes the container. It needs the container's id before the solver starts, hence `docker create` followed by `docker start --attach`, which reports the container's output and exit status just as `docker run` did. Only the wrapper may hold the pipe open; the subshell that starts the container closes its copy, or the removal would wait for the solver it is meant to stop. A container is still left behind if the wrapper is killed in the moment between `docker create` being asked for a container and the removal being set up, but it is one that never started, and Thrust's timeout does not expire that early. Closes #49 Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01Qpacd6KyiRsKFexkrgfX6Q --- tests/thrust-pcsat-wrapper | 16 ++++++++++++---- 1 file changed, 12 insertions(+), 4 deletions(-) diff --git a/tests/thrust-pcsat-wrapper b/tests/thrust-pcsat-wrapper index 448b0ea5..0674cbed 100755 --- a/tests/thrust-pcsat-wrapper +++ b/tests/thrust-pcsat-wrapper @@ -5,10 +5,18 @@ COAR_IMAGE=${COAR_IMAGE:-ghcr.io/hiroshi-unno/coar:main} smt2=$(mktemp -p . --suffix .smt2) trap "rm -f $smt2" EXIT cp "$1" "$smt2" -out=$( -docker run --rm -v "$PWD:/mnt" -w /root/coar "$COAR_IMAGE" \ - main.exe -c ./config/solver/pcsat_tbq_ar.json -p pcsp "/mnt/$smt2" -) + +container=$(docker create --rm -v "$PWD:/mnt" -w /root/coar "$COAR_IMAGE" \ + main.exe -c ./config/solver/pcsat_tbq_ar.json -p pcsp "/mnt/$smt2") + +# Thrust gives up on a slow solver by killing this script with SIGKILL: no trap runs, and +# Docker keeps the container going once the client attached to it is gone. Removing it is +# left to a process that outlives this one, waiting for the write end of a pipe that the +# kernel closes however this script dies. Every other process has to let go of that end -- +# hence the `exec 3>&-` below -- or the removal waits for as long as that process lives. +exec 3> >(cat > /dev/null; docker rm --force "$container" > /dev/null 2>&1) + +out=$(exec 3>&-; docker start --attach "$container") exit_code=$? echo "${out%,*}" exit "$exit_code" From d5c98a6f9f59b739ba2eafc6f448f9053df4819b Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 14 Aug 2026 02:45:36 +0000 Subject: [PATCH 2/4] Give a timed-out solver a chance to clean up after itself Thrust ended a solver that exceeded its timeout with SIGKILL, a signal the process cannot act on, and `tests/thrust-pcsat-wrapper` was therefore left no way to stop the Docker container it had started. Docker keeps a container running once the client attached to it is gone, so the solver went on in the background for as long as the instance took, or forever on one it cannot solve. Send SIGTERM instead, and kill only what has not exited two seconds later, so a solver command holding resources of its own can release them. The process is never reaped in between, so the system cannot hand its identifier to an unrelated process that the SIGKILL would then reach. The wrapper removes its container from a SIGTERM trap. It starts the container in the background and waits on it, because bash runs a trap only once the command in the foreground has finished -- which would be the very solver the signal is meant to stop. Closes #49 Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01Qpacd6KyiRsKFexkrgfX6Q --- Cargo.lock | 23 +++++++++++++++++++++-- Cargo.toml | 1 + README.md | 2 +- src/chc/solver.rs | 29 ++++++++++++++++++++++++++--- tests/thrust-pcsat-wrapper | 21 +++++++++++++-------- 5 files changed, 62 insertions(+), 14 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 00681410..d12ba165 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -142,6 +142,12 @@ version = "1.0.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd" +[[package]] +name = "cfg_aliases" +version = "0.2.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f079e83a288787bcd14a6aea84cee5c87a67c5a3e660c30f557a3d24761b3527" + [[package]] name = "color-eyre" version = "0.6.3" @@ -336,9 +342,9 @@ checksum = "db13adb97ab515a3691f56e4dbab09283d0b86cb45abd991d8634a9d6f501760" [[package]] name = "libc" -version = "0.2.183" +version = "0.2.189" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b5b646652bf6661599e1da8901b3b9522896f01e736bad5f723fe7a3a27f899d" +checksum = "3eaf3ede3fee6db1a4c2ee091bf8a8b4dccdc6d17f656fb07896ee72867612f2" [[package]] name = "linux-raw-sys" @@ -376,6 +382,18 @@ dependencies = [ "adler", ] +[[package]] +name = "nix" +version = "0.31.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "cf20d2fde8ff38632c426f1165ed7436270b44f199fc55284c38276f9db47c3d" +dependencies = [ + "bitflags", + "cfg-if", + "cfg_aliases", + "libc", +] + [[package]] name = "nu-ansi-term" version = "0.50.3" @@ -757,6 +775,7 @@ name = "thrust" version = "0.1.0" dependencies = [ "anyhow", + "nix", "pretty", "process_control", "tempfile", diff --git a/Cargo.toml b/Cargo.toml index 8aa6b979..e1f18a0f 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -30,6 +30,7 @@ thiserror = "2.0.18" tracing = "0.1.44" tracing-subscriber = { version = "0.3.23", features = ["env-filter"] } process_control = "5.2.0" +nix = { version = "0.31.3", default-features = false, features = ["signal"] } [dev-dependencies] ui_test = "0.30.6" diff --git a/README.md b/README.md index 99e66965..b03885c3 100644 --- a/README.md +++ b/README.md @@ -139,7 +139,7 @@ Several environment variables are used by Thrust to configure its behavior: - `THRUST_SOLVER`: A CHC solver command used to solve CHC constraints generated by Thrust. Default: `z3` - `THRUST_SOLVER_ARGS`: Whitespace-separated command-line flags passed to the solver. The default is `fp.spacer.global=true fp.validate=true` when the solver is `z3`. -- `THRUST_SOLVER_TIMEOUT_SECS`: Timeout for waiting on results from the solver. Default: `30` +- `THRUST_SOLVER_TIMEOUT_SECS`: Timeout for waiting on results from the solver. A solver that exceeds it is sent `SIGTERM` so that it can release what it holds, and is killed if it has not exited two seconds later. Default: `30` - `THRUST_OUTPUT_DIR`: When configured, Thrust outputs intermediate smtlib2 files into this directory. - `THRUST_ENUM_EXPANSION_DEPTH_LIMIT`: When Thrust works with enums, it "expands" the structure of the enum value onto its environment. This configuration value sets the limit on the depth of recursion during this expansion to handle enums that are defined recursively. It is our future work to discover a sensible value for this automatically. Default: `2` diff --git a/src/chc/solver.rs b/src/chc/solver.rs index 5792d756..1b376626 100644 --- a/src/chc/solver.rs +++ b/src/chc/solver.rs @@ -19,6 +19,25 @@ pub enum CheckSatError { Io(#[from] std::io::Error), } +/// Time a solver command that ran over its time limit is given to shut itself down. +const TERMINATION_GRACE: std::time::Duration = std::time::Duration::from_secs(2); + +/// Ends a solver command that ran over its time limit. +/// +/// A solver command may hold resources that outlive it and that only it knows how to +/// release -- `tests/thrust-pcsat-wrapper` leaves a Docker container running otherwise -- +/// so it is asked to exit with `SIGTERM` and killed only if it is still there once the +/// grace period is over. The process is never reaped here, so the system cannot hand its +/// identifier to an unrelated process in between. +fn terminate(pid: u32) { + use nix::sys::signal::{kill, Signal}; + + let pid = nix::unistd::Pid::from_raw(pid as i32); + let _ = kill(pid, Signal::SIGTERM); + std::thread::sleep(TERMINATION_GRACE); + let _ = kill(pid, Signal::SIGKILL); +} + /// A configuration for running a command-line CHC solver. #[derive(Debug, Clone)] pub struct CommandConfig { @@ -52,13 +71,17 @@ impl CommandConfig { use process_control::{ChildExt as _, Control as _}; let start = std::time::Instant::now(); - tracing::info!(timeout = ?self.timeout, pid = child.id(), "waiting"); - let mut child = child.controlled_with_output().terminate_for_timeout(); + let pid = child.id(); + tracing::info!(timeout = ?self.timeout, pid, "waiting"); + let mut child = child.controlled_with_output(); if let Some(timeout) = self.timeout { child = child.time_limit(timeout); } let output = match child.wait()? { - None => return Err(CheckSatError::Timeout(self.timeout.unwrap())), + None => { + terminate(pid); + return Err(CheckSatError::Timeout(self.timeout.unwrap())); + } Some(output) => output, }; let elapsed = std::time::Instant::now() - start; diff --git a/tests/thrust-pcsat-wrapper b/tests/thrust-pcsat-wrapper index 0674cbed..30316cde 100755 --- a/tests/thrust-pcsat-wrapper +++ b/tests/thrust-pcsat-wrapper @@ -3,20 +3,25 @@ COAR_IMAGE=${COAR_IMAGE:-ghcr.io/hiroshi-unno/coar:main} smt2=$(mktemp -p . --suffix .smt2) -trap "rm -f $smt2" EXIT +solver_out=$(mktemp) +trap 'rm -f "$smt2" "$solver_out"' EXIT cp "$1" "$smt2" container=$(docker create --rm -v "$PWD:/mnt" -w /root/coar "$COAR_IMAGE" \ main.exe -c ./config/solver/pcsat_tbq_ar.json -p pcsp "/mnt/$smt2") -# Thrust gives up on a slow solver by killing this script with SIGKILL: no trap runs, and -# Docker keeps the container going once the client attached to it is gone. Removing it is -# left to a process that outlives this one, waiting for the write end of a pipe that the -# kernel closes however this script dies. Every other process has to let go of that end -- -# hence the `exec 3>&-` below -- or the removal waits for as long as that process lives. -exec 3> >(cat > /dev/null; docker rm --force "$container" > /dev/null 2>&1) +# Thrust ends a solver that runs over its timeout with SIGTERM, and Docker keeps the +# container going once the client attached to it is gone, so the container is removed from +# here. Passing the signal on to the solver itself would achieve nothing: it runs as the +# container's PID 1, for which the kernel drops every signal that has no handler. +trap 'docker rm --force "$container" > /dev/null 2>&1; exit 143' TERM -out=$(exec 3>&-; docker start --attach "$container") +# Bash defers a trap until the command in the foreground finishes -- which would be the +# solver this one is meant to interrupt. `wait` is the exception, hence the background job. +docker start --attach "$container" > "$solver_out" & +wait $! exit_code=$? + +out=$(< "$solver_out") echo "${out%,*}" exit "$exit_code" From 4df5b7024e32792957752b5d339a8ff29ae52862 Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 14 Aug 2026 02:49:56 +0000 Subject: [PATCH 3/4] Trim the comments to what the code does not say The step-by-step account of `terminate` and of the wrapper's trap restated the lines they sat above; what is left is why a solver is signalled rather than killed, why its identifier is safe to signal, and why the container is removed rather than stopped. The grace period loses its doc comment along the same lines, matching the other constants in the crate. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01Qpacd6KyiRsKFexkrgfX6Q --- src/chc/solver.rs | 12 ++++++------ tests/thrust-pcsat-wrapper | 8 ++++---- 2 files changed, 10 insertions(+), 10 deletions(-) diff --git a/src/chc/solver.rs b/src/chc/solver.rs index 1b376626..6cff238e 100644 --- a/src/chc/solver.rs +++ b/src/chc/solver.rs @@ -19,16 +19,16 @@ pub enum CheckSatError { Io(#[from] std::io::Error), } -/// Time a solver command that ran over its time limit is given to shut itself down. const TERMINATION_GRACE: std::time::Duration = std::time::Duration::from_secs(2); /// Ends a solver command that ran over its time limit. /// -/// A solver command may hold resources that outlive it and that only it knows how to -/// release -- `tests/thrust-pcsat-wrapper` leaves a Docker container running otherwise -- -/// so it is asked to exit with `SIGTERM` and killed only if it is still there once the -/// grace period is over. The process is never reaped here, so the system cannot hand its -/// identifier to an unrelated process in between. +/// The command is given a chance to shut itself down first: it may hold resources that +/// outlive the process and that only it knows how to release, as +/// `tests/thrust-pcsat-wrapper` does with the Docker container it runs the solver in. +/// +/// A timed-out process is left unreaped, so the system cannot hand its identifier to an +/// unrelated process that the `SIGKILL` would then reach. fn terminate(pid: u32) { use nix::sys::signal::{kill, Signal}; diff --git a/tests/thrust-pcsat-wrapper b/tests/thrust-pcsat-wrapper index 30316cde..a8827ee1 100755 --- a/tests/thrust-pcsat-wrapper +++ b/tests/thrust-pcsat-wrapper @@ -11,13 +11,13 @@ container=$(docker create --rm -v "$PWD:/mnt" -w /root/coar "$COAR_IMAGE" \ main.exe -c ./config/solver/pcsat_tbq_ar.json -p pcsp "/mnt/$smt2") # Thrust ends a solver that runs over its timeout with SIGTERM, and Docker keeps the -# container going once the client attached to it is gone, so the container is removed from -# here. Passing the signal on to the solver itself would achieve nothing: it runs as the -# container's PID 1, for which the kernel drops every signal that has no handler. +# container going once the client attached to it is gone. Passing the signal on to the +# solver instead would achieve nothing: it runs as the container's PID 1, for which the +# kernel drops every signal that has no handler. trap 'docker rm --force "$container" > /dev/null 2>&1; exit 143' TERM # Bash defers a trap until the command in the foreground finishes -- which would be the -# solver this one is meant to interrupt. `wait` is the exception, hence the background job. +# solver the trap above is meant to interrupt. `wait` is the exception. docker start --attach "$container" > "$solver_out" & wait $! exit_code=$? From 06f8bd3a9259de47161b4cbdaa3558548dd38dab Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 15 Aug 2026 13:40:37 +0000 Subject: [PATCH 4/4] Leave a timed-out solver to exit on the SIGTERM it was sent Waiting out a grace period cost every timeout two seconds of doing nothing, and the SIGKILL that followed it was sent whether or not anything was still there to receive it. A solver command is expected to exit on the signal. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01Qpacd6KyiRsKFexkrgfX6Q --- README.md | 2 +- src/chc/solver.rs | 17 ++++++----------- 2 files changed, 7 insertions(+), 12 deletions(-) diff --git a/README.md b/README.md index b03885c3..bde4cd69 100644 --- a/README.md +++ b/README.md @@ -139,7 +139,7 @@ Several environment variables are used by Thrust to configure its behavior: - `THRUST_SOLVER`: A CHC solver command used to solve CHC constraints generated by Thrust. Default: `z3` - `THRUST_SOLVER_ARGS`: Whitespace-separated command-line flags passed to the solver. The default is `fp.spacer.global=true fp.validate=true` when the solver is `z3`. -- `THRUST_SOLVER_TIMEOUT_SECS`: Timeout for waiting on results from the solver. A solver that exceeds it is sent `SIGTERM` so that it can release what it holds, and is killed if it has not exited two seconds later. Default: `30` +- `THRUST_SOLVER_TIMEOUT_SECS`: Timeout for waiting on results from the solver. A solver that exceeds it is sent `SIGTERM`, and is expected to exit on it so that it can release what it holds. Default: `30` - `THRUST_OUTPUT_DIR`: When configured, Thrust outputs intermediate smtlib2 files into this directory. - `THRUST_ENUM_EXPANSION_DEPTH_LIMIT`: When Thrust works with enums, it "expands" the structure of the enum value onto its environment. This configuration value sets the limit on the depth of recursion during this expansion to handle enums that are defined recursively. It is our future work to discover a sensible value for this automatically. Default: `2` diff --git a/src/chc/solver.rs b/src/chc/solver.rs index 6cff238e..02aaa81e 100644 --- a/src/chc/solver.rs +++ b/src/chc/solver.rs @@ -19,23 +19,18 @@ pub enum CheckSatError { Io(#[from] std::io::Error), } -const TERMINATION_GRACE: std::time::Duration = std::time::Duration::from_secs(2); - -/// Ends a solver command that ran over its time limit. +/// Asks a solver command that ran over its time limit to shut itself down. /// -/// The command is given a chance to shut itself down first: it may hold resources that -/// outlive the process and that only it knows how to release, as -/// `tests/thrust-pcsat-wrapper` does with the Docker container it runs the solver in. +/// It is asked rather than killed because it may hold resources that outlive the process +/// and that only it knows how to release, as `tests/thrust-pcsat-wrapper` does with the +/// Docker container it runs the solver in. /// /// A timed-out process is left unreaped, so the system cannot hand its identifier to an -/// unrelated process that the `SIGKILL` would then reach. +/// unrelated process that this would then reach. fn terminate(pid: u32) { use nix::sys::signal::{kill, Signal}; - let pid = nix::unistd::Pid::from_raw(pid as i32); - let _ = kill(pid, Signal::SIGTERM); - std::thread::sleep(TERMINATION_GRACE); - let _ = kill(pid, Signal::SIGKILL); + let _ = kill(nix::unistd::Pid::from_raw(pid as i32), Signal::SIGTERM); } /// A configuration for running a command-line CHC solver.