Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 9 additions & 0 deletions bindings/pycvc/test_pycvc_state_exec_eval.py
Original file line number Diff line number Diff line change
Expand Up @@ -152,6 +152,15 @@ def test_timeout_and_pause():
for ev in (pycvc.stackless_evaluator(_builtins()), pycvc.evaluator(_builtins())):
e = _raises(pycvc.evaluation_timeout, ev.evaluate_script, "(while 1 1)", None, 0.05)
assert isinstance(e, RuntimeError)
# A loop inside one step (a generator body that never yields) is cut the same way.
e = _raises(
pycvc.evaluation_timeout,
ev.evaluate_script,
"(next (generator (lambda () (while t 1))))",
None,
0.05,
)
assert "evaluation exceeded timeout" in str(e)
ev.pause()
assert ev.is_paused()
t = threading.Timer(0.1, ev.resume)
Expand Down
14 changes: 14 additions & 0 deletions bindings/pycvc/test_pycvc_state_exec_sched.py
Original file line number Diff line number Diff line change
Expand Up @@ -136,6 +136,20 @@ def test_a_python_fn_error_surfaces_as_each_scheduler_reports_it():
assert a.get_exit_error(999) is None


def test_a_time_budget_cut_inside_a_step_is_the_time_limit():
# A generator body that never yields loops inside one step until the step's deadline cuts
# it. Each scheduler reports that as it reports running out of time between steps.
never_yields = "(next (generator (lambda () (while t 1))))"
s = pycvc.scheduler()
pid = s.execute(never_yields, _opts(max_time=0.05))
s.run() # no error out of run()
assert s.get_process_info(pid).status is process_status.killed
a = pycvc.async_scheduler()
pid = a.execute(never_yields, _opts(max_time=0.05))
a.sync_run()
assert a.get_exit_error(pid) == "time_limit_exceeded"


def test_percent_encode_and_decode():
assert pycvc.percent_encode("a b/é~") == "a%20b%2F%C3%A9~"
assert pycvc.percent_decode("a%20b%2F%C3%A9~") == "a b/é~"
Expand Down
3 changes: 2 additions & 1 deletion docs/PYCVC_STATE_EXEC_PARITY.md
Original file line number Diff line number Diff line change
Expand Up @@ -91,7 +91,8 @@ are listed too. Status after PR 3:
| | `make_list`, `make_dict`, `make_bytes`, `nil_value`, `true_value`, `false_value` | `list`, `dict`, `bytes`, `None`, `True`, `False` | exception: the native Python values are the equivalents |
| | `environment` (`bindings`, `outer`, `frozen`, `lookup`, `set`, `set_existing`, `extend`) | `pycvc.environment` | wrapped (PR 2), shared like `environment_ptr`. `bindings` reads and writes as a dict (a copy); `lookup` raises `KeyError` where C++ returns nullptr; `set` on a frozen scope (#660) raises `RuntimeError` |
| | `closure`, `data_object`, `generator` | `pycvc.value` (opaque) | wrapped as opaque handles; no member access |
| | `time_budget`, `eval_deadline_guard`, `eval_deadline_expired`, `thread_cpu_seconds` | none | exception: thread-local evaluator internals |
| | `time_budget`, `eval_deadline_guard`, `eval_deadline_expired`, `eval_deadline_check`, `thread_cpu_seconds` | none | exception: thread-local evaluator internals |
| | `evaluation_interrupted`, `evaluation_timeout` (in types.h since 2026-10) | listed with evaluator.h below | |
| | `kDefaultMaxAllocBytes`, `eval_alloc_limit`, `eval_alloc_check`, `alloc_bytes` (#660) | the same names under `pycvc.` | wrapped (PR 3). A Python function a program calls runs on the stepping thread, where the step's limit is armed, so it can check the limit as a builtin does |
| | `eval_alloc_guard` (#660) | none | exception: RAII that must nest last-in first-out, which a Python object's lifetime doesn't promise |
| | `detail::release_nested`, `detail::drop_owner` (#657) | none | exception: internals of `value_t`'s destructor |
Expand Down
17 changes: 15 additions & 2 deletions docs/STATE_EXEC_DEVELOPER_GUIDE.md
Original file line number Diff line number Diff line change
Expand Up @@ -850,7 +850,19 @@ opts.max_messages = 100; // outbound msg-send calls
opts.max_message_bytes = 65536; // total outbound payload bytes
```

When a limit is exceeded, the process is killed (status becomes `killed`).
When a limit is exceeded, the process is killed (status becomes `killed`). The async scheduler
keeps the reason as its exit error: `max_steps_exceeded`, `time_limit_exceeded`,
`memory_limit_exceeded`, and so on.

`max_time` is checked between steps, and inside a step by the step's deadline. A long loop
inside one native call polls that deadline with `eval_deadline_check()`, which throws
`evaluation_timeout`. Examples are an unsliced data job, a generator body that never yields, and
a stdlib materializer. Either way the process is killed with `time_limit_exceeded`. On the sync
scheduler, a deadline armed outside it (its caller's) propagates out of `run()` instead.

Outside a scheduler, every evaluator's timeout arms the same deadline. A loop inside a step
throws `evaluation_timeout` (in pycvc, `pycvc.evaluation_timeout`), as the evaluator's own
check between steps does. An Ariadne predicate reports either one as the eval budget's time cap.

### Memory: state-tree writes and the measured heap

Expand Down Expand Up @@ -1491,7 +1503,8 @@ read. The document is held to the allocation limit as it grows.
- **Cost.** `collections.sort` is a stable merge sort, n log n nodes.
`collections.unique` costs a node per comparison, and compares lists and dicts with a sliced
equality walk. `collections.dict-merge` keeps a key index, so it is linear. Every job polls the
evaluation deadline (`max_time`) about every 64 nodes.
evaluation deadline (`max_time`) about every 64 nodes, and throws `evaluation_timeout` once it
has passed.
- **While a call runs.** Signals and watch events wait until the call is done, and `fork`
returns -1. A snapshot taken during it restores to the call's start: the call runs again, and
calls its function again from the first element.
Expand Down
12 changes: 1 addition & 11 deletions inc/cvc/state/state_exec/evaluator.h
Original file line number Diff line number Diff line change
Expand Up @@ -23,17 +23,7 @@

namespace cvc::state_exec {

/// Exception thrown when evaluation is interrupted.
class evaluation_interrupted : public std::runtime_error {
public:
using std::runtime_error::runtime_error;
};

/// Exception thrown when evaluation times out.
class evaluation_timeout : public std::runtime_error {
public:
using std::runtime_error::runtime_error;
};
// evaluation_interrupted and evaluation_timeout are in types.h, next to the evaluation deadline.

/// Exception used internally for (return ...) unwinding.
class return_exception : public std::exception {
Expand Down
3 changes: 1 addition & 2 deletions inc/cvc/state/state_exec/generator.h
Original file line number Diff line number Diff line change
Expand Up @@ -67,8 +67,7 @@ inline std::optional<value_t> generator_next(generator &gen) {
gen.state.yielded = false;
detail::native_nesting level("generator"); // a nested evaluator
while (!gen.state.done && !gen.state.yielded) {
if (eval_deadline_expired())
throw std::runtime_error("generator: evaluation exceeded time budget");
eval_deadline_check("generator");
gen.evaluator.step(gen.state);
}

Expand Down
26 changes: 24 additions & 2 deletions inc/cvc/state/state_exec/types.h
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,7 @@
#include <memory>
#include <optional>
#include <span>
#include <stdexcept>
#include <string>
#include <unordered_map>
#include <variant>
Expand Down Expand Up @@ -368,18 +369,39 @@ class eval_deadline_guard {
~eval_deadline_guard();
eval_deadline_guard(const eval_deadline_guard &) = delete;
eval_deadline_guard &operator=(const eval_deadline_guard &) = delete;
/// Whether this guard's own budget is spent (a check, like eval_deadline_expired()). Tells a
/// scheduler's step deadline from one armed outside it, both of which throw evaluation_timeout.
bool expired();

private:
friend bool eval_deadline_expired();
std::optional<time_budget> budget_;
eval_deadline_guard *outer_ = nullptr; // the next armed guard out
};

/// Exception thrown when evaluation is interrupted.
class evaluation_interrupted : public std::runtime_error {
public:
using std::runtime_error::runtime_error;
};

/// Exception thrown when evaluation times out: by the evaluator between steps, or by a long
/// loop inside one native step (eval_deadline_check). The schedulers kill a process whose step
/// throws it with time_limit_exceeded, as when the time runs out between steps.
class evaluation_timeout : public std::runtime_error {
public:
using std::runtime_error::runtime_error;
};

/// True iff a deadline is armed on this thread and its budget is spent; each call is a check
/// of every armed budget. Cheap (one steady-clock read until a budget is half spent);
/// long-running builtins call this in their loops so they too honour the budget.
/// of every armed budget. Cheap (one steady-clock read until a budget is half spent).
bool eval_deadline_expired();

/// Throws evaluation_timeout ("<what>: evaluation exceeded timeout") when eval_deadline_expired().
/// Long-running builtins and data jobs call this in their loops, so the budget cuts them the
/// same way it cuts a program.
void eval_deadline_check(const char *what);

// -- per-call allocation limit ----------------------------------------------
//
// A native call builds its whole result inside one evaluator step, where the per-process
Expand Down
3 changes: 3 additions & 0 deletions src/cvc/state/state_exec/async_evaluator.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -83,6 +83,9 @@ value_t async_evaluator::sync_evaluate(const value_t &expr, environment_ptr env,
std::optional<std::chrono::steady_clock::time_point> prev;
~deadline_restore() { self->deadline_ = prev; }
} restore{this, saved_deadline};
// The thread's evaluation deadline cuts a loop inside one native call, which never reaches
// check_interrupted_async (as stackless_evaluator::run arms it).
eval_deadline_guard deadline_guard(timeout_sec);

auto t = evaluate(expr, env);
// sync_wait drives the coroutine on both the trampoline (GCC/Clang) and the
Expand Down
6 changes: 5 additions & 1 deletion src/cvc/state/state_exec/async_scheduler.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -224,7 +224,11 @@ void async_scheduler::execute_process_step(process &proc) {
proc.accumulated_time +=
std::chrono::duration<double>(std::chrono::steady_clock::now() - proc.last_run_start)
.count();
kill_process(proc, e.what());
// The step's deadline (max_time, or the per-step cap) cutting a long loop inside the step is
// the process running out of time, reported as check_limits() reports it between steps.
const bool out_of_time =
dynamic_cast<const evaluation_timeout *>(&e) != nullptr && step_deadline.expired();
kill_process(proc, out_of_time ? "time_limit_exceeded" : e.what());
return;
}

Expand Down
5 changes: 5 additions & 0 deletions src/cvc/state/state_exec/async_stackless_evaluator.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -89,6 +89,10 @@ value_t async_stackless_evaluator::sync_evaluate(const value_t &expr, environmen
std::optional<double> timeout_sec,
std::function<void(const value_t &)> on_complete) {
auto st = create_state(expr, env);
// The thread's evaluation deadline cuts a loop inside one native call, which run() only
// checks between steps (as stackless_evaluator::run arms it). Armed here, not in the
// coroutine, so the guards on this thread are still released in order.
eval_deadline_guard deadline_guard(timeout_sec);
auto t = run(st, std::nullopt, timeout_sec, std::move(on_complete));
return t.sync_wait();
}
Expand All @@ -98,6 +102,7 @@ async_stackless_evaluator::sync_evaluate_script(const std::string &script, envir
std::optional<double> timeout_sec,
std::function<void(const value_t &)> on_complete) {
auto st = create_state(script, env);
eval_deadline_guard deadline_guard(timeout_sec); // see sync_evaluate
auto t = run(st, std::nullopt, timeout_sec, std::move(on_complete));
return t.sync_wait();
}
Expand Down
13 changes: 4 additions & 9 deletions src/cvc/state/state_exec/data_job.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -269,8 +269,7 @@ class equal_walk final : public data_job {
continue;
}
++nodes_;
if (eval_deadline_expired())
throw std::runtime_error("values_equal: structure too large to compare");
eval_deadline_check("values_equal");
bool equal;
// Element references stay valid through visit(), which only pushes onto open_.
if (ca.list) {
Expand Down Expand Up @@ -371,8 +370,7 @@ class copy_walk final : public data_job {
continue;
}
++nodes_;
if (eval_deadline_expired())
throw std::runtime_error("state-data-get: evaluation exceeded time budget");
eval_deadline_check("state-data-get");
if (src.list) {
list_ptr out = std::get<list_ptr>(dst.v);
const value_t &e = (*src.list)[i];
Expand Down Expand Up @@ -548,9 +546,7 @@ bool generator_walk::step(std::size_t nodes) {
if (g.native_step) { // range and friends: a value is a node
if (spent())
return false;
if (eval_deadline_expired()) // (collect (range 0 1e11)) when nothing slices
throw std::runtime_error(std::string(collect_ ? "collect" : "next") +
": evaluation exceeded time budget");
eval_deadline_check(collect_ ? "collect" : "next"); // (collect (range 0 1e11)) unsliced
std::optional<value_t> v = g.native_step();
++nodes_;
if (!v) {
Expand All @@ -571,8 +567,7 @@ bool generator_walk::step(std::size_t nodes) {
while (!g.state.done && !g.state.yielded) {
if (spent())
return false;
if (eval_deadline_expired())
throw std::runtime_error("generator: evaluation exceeded time budget");
eval_deadline_check("generator");
{
detail::native_nesting level("generator"); // its own evaluator, on this stack
g.evaluator.step(g.state);
Expand Down
3 changes: 3 additions & 0 deletions src/cvc/state/state_exec/evaluator.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -36,6 +36,9 @@ value_t evaluator::evaluate(const value_t &expr, environment_ptr env,
std::exception_ptr ex;
std::atomic<bool> done{false};
std::thread worker([&] {
// A loop inside one native call (a generator body, a data job) never sees interrupt():
// the thread's evaluation deadline cuts it, so join() below does not wait on it.
eval_deadline_guard deadline_guard(timeout_sec);
try {
bg_result = eval_internal(expr, run_env);
} catch (...) {
Expand Down
16 changes: 15 additions & 1 deletion src/cvc/state/state_exec/scheduler.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -276,7 +276,21 @@ void scheduler::execute_process_step(process &proc) {
proc.max_memory > 0 ? mem_tracker_.current_bytes(proc.pid) + proc.heap_bytes : 0));
const bool charge_cpu = proc.charges_cpu_time();
const double cpu0 = charge_cpu ? thread_cpu_seconds() : 0.0;
bool done = evaluator_.step(proc.state);
bool done = false;
try {
done = evaluator_.step(proc.state);
} catch (const evaluation_timeout &) {
// The step's deadline cut a long loop inside it (a data job, a generator, a stdlib call):
// the process ran out of time, as the between-steps check below would find. A deadline
// armed outside this scheduler is its caller's, so that one propagates like other errors.
if (!step_deadline.expired())
throw;
proc.accumulated_time +=
std::chrono::duration<double>(std::chrono::steady_clock::now() - proc.last_run_start)
.count();
kill_process(proc, "time_limit_exceeded");
return;
}

// 4. Accumulate running time, and charge it to what the step was spent on
auto now = std::chrono::steady_clock::now();
Expand Down
5 changes: 1 addition & 4 deletions src/cvc/state/state_exec/stdlib.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -70,10 +70,7 @@ std::size_t list_bytes(std::size_t n) {
}

// Long loops inside one native call honour the evaluation deadline (see collect in builtins.cpp).
void poll_deadline(const char *name) {
if (eval_deadline_expired())
throw std::runtime_error(std::string(name) + ": evaluation exceeded time budget");
}
void poll_deadline(const char *name) { eval_deadline_check(name); }

// A list argument by owning pointer (a null one reads as empty).
list_ptr as_list_ptr(const value_t &v, const char *name) {
Expand Down
7 changes: 7 additions & 0 deletions src/cvc/state/state_exec/types.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -124,6 +124,8 @@ eval_deadline_guard::~eval_deadline_guard() {
t_innermost = outer_;
}

bool eval_deadline_guard::expired() { return budget_ && budget_->spent(); }

bool eval_deadline_expired() {
if (!t_innermost)
return false;
Expand All @@ -134,6 +136,11 @@ bool eval_deadline_expired() {
return spent;
}

void eval_deadline_check(const char *what) {
if (eval_deadline_expired())
throw evaluation_timeout(std::string(what) + ": evaluation exceeded timeout");
}

// -- releasing nested values -------------------------------------------------

namespace {
Expand Down
10 changes: 4 additions & 6 deletions src/cvc/tests/ariadne_runtime_test.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -1679,12 +1679,10 @@ TEST(AriadneStdlib, PredicateMaterializerIsCutByTheEvalBudget) {
EXPECT_FALSE(mb.saw("text_line:big"));
auto warns = rt.take_reactive_warnings();
ASSERT_FALSE(warns.empty());
// Cut by the step cap or the time cap, whichever comes first. The time cap is reported as the
// eval budget when it expires between steps, and through the job's own error ("evaluation
// exceeded time budget") when the job's deadline poll sees it first, as on a slow Debug build.
EXPECT_TRUE(warns[0].find("exceeded the eval budget") != std::string::npos ||
warns[0].find("evaluation exceeded time budget") != std::string::npos)
<< warns[0];
// Cut by the step cap or the time cap, whichever comes first. The time cap reads the same
// whether it expires between steps or the job's own deadline poll sees it first, as on a slow
// Debug build: both throw evaluation_timeout.
EXPECT_NE(warns[0].find("exceeded the eval budget"), std::string::npos) << warns[0];

// A 0 here still slices, at the host's 1024 nodes a step, and an ordinary call finishes. It is
// kept small so it fits the 5 ms time cap in a Debug build on a loaded CI runner.
Expand Down
Loading
Loading