UnderstandingAbortionsAndTimers

Abortions and Timers

AProVE uses a CPU-time-based abortion system to prevent processors from running indefinitely. The core classes live in aprove.strategies.Abortions.

Goal

Strategies often run many processors in parallel (via Any()). To avoid waiting too long on a fruitless processor before moving on, each processor is given a time budget. When that budget is exceeded, the processor is aborted.

There are two kinds of timers available in strategy files:

• Timer(ms, ...) — CPU-time based. Measures actual CPU time consumed by the processor thread. More predictable across different hardware and load situations.
• WallTimer(ms, ...) — Wall-clock based. Measures real elapsed time using Thread.sleep. Useful for external processes or theorem provers that spend most of their time waiting (and thus consume little CPU time, which would fool a CPU timer).

The main current.strategy uses Timer() throughout. Other strategies (e.g. cdt.strategy, competition.strategy) also use WallTimer() for specific sub-strategies like theorem provers.

Core Classes

Abortion

The central class. Each processor receives an Abortion instance in its process() method and is expected to call abortion.checkAbortion() periodically. When the abortion has been triggered, this throws an AbortionException, which can safely propagate up to the caller.

Key methods:

• checkAbortion() — throws AbortionException if aborted, otherwise does nothing.
• isAborted() — returns true if already aborted.
• abort(String reason) — triggers the abortion and notifies all listeners.
• createChild() — creates a child abortion that is automatically aborted when the parent is, but can also be aborted independently (useful for sub-calculations).
• createChild(int milliSec) — like createChild(), but the child also aborts after the given number of CPU milliseconds.

Abortions are one-shot: once aborted, they stay aborted.

Clock

Tracks accumulated CPU time for a set of calculations. A Clock is created with a maximum time limit; once that limit is exceeded, it notifies its ClockListener, which in turn triggers the relevant Abortion.

Each Timer() in the strategy allocates a new Clock and adds it to the RuntimeInformation. Processors report their CPU time usage to the abortion, which forwards it to all attached clocks via increaseTime(long millis).

WallTimer() works differently — it does not use a Clock at all. Instead, ExecWallTimer spawns a daemon thread that sleeps for the given duration and then calls asyncStop() directly, bypassing the CPU-time tracking machinery entirely.

AbortionFactory

Used to create top-level Abortion instances outside the regular framework (e.g. in tests or custom mains). Within the framework, abortions are created by Executor using the clocks registered in RuntimeInformation.

AbortionListener

Implement this to receive immediate notification when an abortion fires. Most processors should prefer calling checkAbortion() periodically instead.

Execution Flow

1. Executor.start() creates an Abortion (with clocks from RuntimeInformation) and starts a Runner (a PooledJob) in a thread pool.
2. A TrackThreadPool monitors the runner thread's CPU time and reports it to the abortion via increaseTime().
3. Once a Clock limit is reached, the clock's listener calls abortion.abort(...).
4. On the next call to checkAbortion(), the processor receives an AbortionException and terminates cleanly.
5. If the processor does not terminate within MIN_MILLIS_TO_STOP (currently 5000ms) of the abortion being triggered, Thread.stop() is called, forcing a ThreadDeath. This is a last resort — it can leave locks unreleased or classes half-initialized, which can confuse the JVM.

The grace period exists to give the processor a chance to stop cleanly and avoid such interference. Importantly, the grace period only consumes CPU time in the background — after the abortion is triggered, the processor is already considered done (with a result of Fail) from the strategy framework's perspective. The framework does not wait for the thread to finish; it moves on to the next processor(s) immediately.

Tracking External Threads and Processes

The abortion system only works automatically for the main processor thread. If a processor spawns additional threads or external processes, their CPU time must be tracked explicitly:

• Thread-based solvers: Attach a TrackThread to the spawned thread so its CPU time is reported to the abortion.
• External processes (e.g. minisat): Use a process timer that reads CPU time from /proc/$PID. Note that this only works on Linux, only tracks direct child processes, and will appear to use zero CPU time if the process is launched via a shell script rather than directly.
• Nested Machine runs: Use the dedicated Machine.start methods that accept the current RuntimeInformation, so that time spent in the sub-run is counted against the same clocks.

Failure to track external CPU usage means that thread or process will never appear to hit its time limit and will run forever.

Abortion Hierarchy

Child abortions form a tree: aborting a parent automatically aborts all its children. Children can be aborted independently without affecting the parent. This is used, for example, when a processor tries multiple approaches in parallel — each approach gets a child abortion so it can be stopped individually when another approach succeeds.

Notes and Caveats

• Thread.stop() is deprecated in modern Java for good reasons. If it fires during a class initializer, that class will be permanently marked as failed to load. Processors should always call checkAbortion() frequently enough to avoid this.
• CPU time tracking (Timer()) requires JVM support via ThreadMXBean. If unavailable (checked at startup in developer builds; assumed available in production builds), the system falls back to measuring wall time of RUNNABLE threads as an approximation.
• There is a known risk of deadlock in the time-tracking code. When in doubt, let the TimeRefresherThread handle time checks rather than doing so directly.