Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
21 commits
Select commit Hold shift + click to select a range
32bc3e3
state_exec: grammar spec, conformance cases and parse corpus (grammar…
transfix Oct 17, 2026
1381d6d
state_exec grammar: make the nesting limit configurable (default 256)
transfix Oct 17, 2026
c6486e2
state_exec grammar: parser settings live on the state tree
transfix Oct 17, 2026
e221ac7
state_exec: parser settings on the state tree, with a nesting limit (…
transfix Oct 17, 2026
7a4b4b1
state_exec: make the parser stackless (explicit frame stack, resumabl…
transfix Oct 17, 2026
c040bdd
state_exec: read submitted scripts inside the process, a slice per step
transfix Oct 17, 2026
97c2a92
state_exec: the app's exec scheduler reads scripts in steps (1024 tok…
transfix Oct 17, 2026
9ed8702
pycvc: give Exec the same state_exec defaults as the app's exec sched…
transfix Oct 17, 2026
753abb1
pycvc: expose the state_exec parser-settings surface under its C++ names
transfix Oct 17, 2026
4d3bc6b
state_exec: free, print, compare, copy and snapshot deep values witho…
transfix Oct 17, 2026
6f11d9e
state_exec: deep-data work a slice per step, and the budget by kind
transfix Oct 17, 2026
ffa9a26
pycvc: parse_options_from_state takes the State root, as in C++
transfix Oct 17, 2026
a65ed9e
Merge feat/state-exec-sliced-read: pycvc *_options_from_state take th…
transfix Oct 17, 2026
7419dd1
Merge remote-tracking branch 'origin/master' into HEAD
transfix Oct 17, 2026
bc20f8e
Merge remote-tracking branch 'origin/feat/state-exec-parse-settings' …
transfix Oct 17, 2026
ac5a35e
Merge feat/state-exec-sliced-read (now with master) into feat/state-e…
transfix Oct 17, 2026
ea8b77a
Merge remote-tracking branch 'origin/master' into HEAD
transfix Oct 18, 2026
6e0cf06
Merge remote-tracking branch 'origin/feat/state-exec-parse-settings' …
transfix Oct 18, 2026
f137f37
Merge feat/state-exec-sliced-read (now with #660) into feat/state-exe…
transfix Oct 18, 2026
8a7585f
Merge origin/master (#653 squashed) into feat/state-exec-data-steps
transfix Oct 18, 2026
a84d37e
Run the master CI on #658 after retargeting it to master
transfix Oct 18, 2026
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: 8 additions & 1 deletion bindings/pycvc/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -203,9 +203,16 @@ ex.parser_defaults() # == host_parser_defaults(
pycvc.state_set(app, "state_exec.defaults.parser.max_depth", "64") # tree overrides
root = pycvc.State.instance(app) # the tree root, as in C++
pycvc.parse_options_from_state(root, "", ex.parser_defaults()) # what Exec uses

# Deep-data settings ("Deep data on the executor"), the same way
pycvc.data_options() # step_nodes 0
pycvc.async_scheduler.host_data_defaults() # step_nodes 1024
ex.data_defaults() # == host_data_defaults()
pycvc.data_options_from_state(root, "", ex.data_defaults()) # what Exec uses
```

`Exec` starts from the same defaults as the app's exec scheduler (Ariadne), and
the same `state_exec.defaults.parser.*` keys override both. A syntax error
the same `state_exec.defaults.parser.*` and `state_exec.defaults.data.*` keys
override both. A syntax error
raises a `RuntimeError` with the parse error's message. Contract test:
`test_pycvc_exec.py`.
10 changes: 10 additions & 0 deletions bindings/pycvc/pycvc.i
Original file line number Diff line number Diff line change
Expand Up @@ -1445,8 +1445,11 @@ class AsyncStateObserver(state_observer):
// async_scheduler.h (value_t, the parser, the scheduler itself) is not wrapped
// yet, so async_scheduler has no Python constructor. Exec's parser_defaults /
// set_parser_defaults are in pycvc_exec.h.
// The deep-data settings (data_options, data_options_from_state, "Deep data on the
// executor") are wrapped the same way.
%{
#include <cvc/state/state_exec/async_scheduler.h>
#include <cvc/state/state_exec/data_job.h>
#include <cvc/state/state_exec/parser.h>
%}
namespace cvc {
Expand All @@ -1455,14 +1458,21 @@ struct parse_options {
size_t max_depth; // lists and quotes that may nest (default 256)
size_t step_tokens; // 0: parse at submit; N: read N tokens per process step
};
struct data_options {
size_t step_nodes; // 0: deep-data work in the step that needs it; N: N nodes per step
};
parse_options parse_options_from_state(cvc::state &root,
const std::string &scheduler_id = std::string(),
const parse_options &base = parse_options());
data_options data_options_from_state(cvc::state &root,
const std::string &scheduler_id = std::string(),
const data_options &base = data_options());
%nodefaultctor async_scheduler;
%nodefaultdtor async_scheduler;
class async_scheduler {
public:
static parse_options host_parser_defaults();
static data_options host_data_defaults();
};
}
}
Expand Down
12 changes: 10 additions & 2 deletions bindings/pycvc/pycvc_exec.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -379,9 +379,11 @@ Exec::Exec(const std::shared_ptr<cvc::app> &app) : impl_(std::make_shared<ExecIm
app->computePool();
impl_->sched.set_watch_root(impl_->root);
// The same state_exec defaults as the app's exec scheduler, so a program behaves the same from
// Python as from Ariadne: scripts are read inside the process (host_parser_defaults), and the
// app tree's state_exec.defaults.parser.* keys override them for both.
// Python as from Ariadne: scripts are read inside the process (host_parser_defaults) and deep
// data is handled a slice per step (host_data_defaults), and the app tree's
// state_exec.defaults.parser.* / data.* keys override them for both.
impl_->sched.set_parser_defaults(async_scheduler::host_parser_defaults());
impl_->sched.set_data_defaults(async_scheduler::host_data_defaults());

impl_->host_proc = make_process();
impl_->host_proc->pid = 0;
Expand Down Expand Up @@ -656,4 +658,10 @@ void Exec::set_parser_defaults(const cvc::state_exec::parse_options &defaults) {
impl_->sched.set_parser_defaults(defaults);
}

cvc::state_exec::data_options Exec::data_defaults() const { return impl_->sched.data_defaults(); }

void Exec::set_data_defaults(const cvc::state_exec::data_options &defaults) {
impl_->sched.set_data_defaults(defaults);
}

} // namespace pycvc
8 changes: 7 additions & 1 deletion bindings/pycvc/pycvc_exec.h
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,8 @@
// registered here becomes callable from DSL source like any builtin.
#pragma once

#include <cvc/state/state_exec/parser.h> // parse_options
#include <cvc/state/state_exec/data_job.h> // data_options
#include <cvc/state/state_exec/parser.h> // parse_options
#include <memory>
#include <string>

Expand Down Expand Up @@ -94,6 +95,11 @@ class Exec {
cvc::state_exec::parse_options parser_defaults() const;
void set_parser_defaults(const cvc::state_exec::parse_options &defaults);

// The deep-data settings, likewise: async_scheduler::data_defaults() / set_data_defaults(),
// starting as async_scheduler::host_data_defaults().
cvc::state_exec::data_options data_defaults() const;
void set_data_defaults(const cvc::state_exec::data_options &defaults);

private:
struct ExecImpl;
std::shared_ptr<ExecImpl> impl_;
Expand Down
57 changes: 57 additions & 0 deletions bindings/pycvc/test_pycvc_exec.py
Original file line number Diff line number Diff line change
Expand Up @@ -129,6 +129,63 @@ def test_set_parser_defaults_changes_how_exec_parses():
assert ex.run("(+ 1 (+ 2 3))") == "6"


# ── state_exec deep-data settings (docs/STATE_EXEC_GRAMMAR.md, "Deep data on
# the executor"), under the C++ names ────────────────────────────────────


def test_data_options_is_the_cpp_struct():
o = pycvc.data_options()
assert o.step_nodes == 0 # C++ default: deep-data work runs whole
o.step_nodes = 64
assert o.step_nodes == 64


def test_exec_starts_from_the_host_data_defaults():
# The same defaults as the app's exec scheduler:
# async_scheduler::host_data_defaults().
host = pycvc.async_scheduler.host_data_defaults()
assert host.step_nodes == 1024
ex = pycvc.Exec(pycvc.make_app())
assert ex.data_defaults().step_nodes == host.step_nodes


def test_data_options_from_state_resolves_like_cpp():
# The real C++ function: it takes the tree root, a State, as in C++.
app = pycvc.make_app()
root = pycvc.State.instance(app)
assert pycvc.data_options_from_state(root).step_nodes == 0
ex = pycvc.Exec(app)
assert pycvc.data_options_from_state(root, "", ex.data_defaults()).step_nodes == 1024
root.child("state_exec.defaults.data.step_nodes").value("16")
root.child("state_exec.schedulers.s1.data.step_nodes").value("8")
assert pycvc.data_options_from_state(root).step_nodes == 16
assert pycvc.data_options_from_state(root, "s1").step_nodes == 8
root.child("state_exec.defaults.data.step_nodes").value("lots") # bad: skipped
assert pycvc.data_options_from_state(root).step_nodes == 0
o = pycvc.data_options()
o.step_nodes = 0
ex.set_data_defaults(o)
assert ex.data_defaults().step_nodes == 0


def test_deep_data_gives_the_same_results_however_it_is_sliced():
# Compare and print values nested 3000 deep: whole in one step, 1024 nodes a step (the host
# default) or 4 nodes a step.
app = pycvc.make_app()
ex = pycvc.Exec(app)
prog = (
"(begin (set a 1) (set b 1) (set i 0)"
" (while (< i 3000) (begin (set a (list a)) (set b (list b)) (set i (+ i 1))))"
" (list (= a b) (length (str a))))"
)
sliced = ex.run(prog)
pycvc.state_set(app, "state_exec.defaults.data.step_nodes", "0")
whole = ex.run(prog)
pycvc.state_set(app, "state_exec.defaults.data.step_nodes", "4")
assert ex.run(prog) == whole == sliced
assert whole.startswith("(#t ")


# ── DSL <-> state <-> Python round trips (one shared app) ───────────────


Expand Down
58 changes: 58 additions & 0 deletions docs/STATE_EXEC_GRAMMAR.md
Original file line number Diff line number Diff line change
Expand Up @@ -208,6 +208,64 @@ scheduler can parse a script the same way it evaluates one: a slice per step. Wi
- **Snapshots.** A process snapshotted while reading stores its source and parser settings. After
a restore it reads the script again from the start.

### Deep data on the executor

Walking a nested value no longer recurses on the native stack: freeing, printing (`to_string`),
comparing (`values_equal`), copying (`state-data-get`), macro expansion and the snapshot codec
keep their work on the heap. That work is still proportional to the value's size, so a scheduler
can run it the way it reads a script: a slice per step, counted against the process's budget.

The setting is `data.step_nodes`, resolved like the parser's (`state_exec.schedulers.<id>.data.step_nodes`,
then `state_exec.defaults.data.step_nodes`, then the scheduler's built-in default;
`data_options_from_state()`):

| Key | Meaning | Default |
|---|---|---|
| `step_nodes` | 0: deep-data work runs whole, inside the step that needs it. N: a step does at most N nodes of it; the rest runs N per step in the steps after | 0; **1024** for the app's exec scheduler and pycvc's `Exec` |

A node is an element visited: a list element or a dict entry walked, or an element freed. With
`step_nodes` = N:

- **Native calls.** `=`, `!=`, `str`, `str-concat`, `print` and `state-data-get` hand their walk
to the evaluator (`run_data_job`). It does one slice inside the call's step; if the walk isn't
done, the call's frame waits and the following steps are **data steps** that each run N more
nodes. The step that finishes it completes the call. A walk under N nodes finishes in the
call's own step, so ordinary programs take no extra steps.
- **Macro expansion** works the same way, before the expansion is evaluated.
- **Freeing.** Last owners dropped during a step (a list, dict, closure, generator or scope)
go to the process's release backlog instead of being freed on the spot. The step frees up to
what is left of its N nodes at its end. If more is left, the next steps are data steps that
only free, and evaluation resumes once the backlog is empty.
- **Budgets.** Data steps are process steps. They count against `max_steps` and `max_time`, and
other processes run between them.
- **Signals and watch events** wait while a walk is pending, because the walk's call frame is
on top of the evaluation stack.
- **Snapshots** keep `step_nodes` but not a walk in flight: after a restore, the waiting call
or macro expansion runs again.
- **Values changed between slices.** A walk holds the lists and dicts it walks by owning
pointer and reads them by index, checking bounds at every node. A change between two slices
(by another process) changes the answer, never memory safety.

Other deep walks run whole inside one step, as before, but count their nodes. These are
`collections.*` helpers and string coercion for `state-set`.

Measured per node (MSVC Release, `state_exec_bench_test` `DataWalkThroughput`): ~45 ns to free,
~70 ns to print, ~250 ns to compare and ~380 ns to copy. So a 1024-node slice costs 0.05-0.4 ms.

### Budget by kind

Each process's steps are split by what they were spent on (`step_kind`):

- **read**: reading the script (`parser.step_tokens`);
- **data**: deep-data steps (`data.step_nodes`);
- **eval**: evaluating code.

`process_info` carries `read_steps`, `eval_steps`, `data_steps` (they add up to `step_count`),
`data_nodes` (deep-data nodes, whichever steps did them), and `read_time`, `eval_time`,
`data_time`. The times are the seconds of the steps a scheduler ran, charged to each step's kind.
`inspect` reports them for any pid, and `(budget-usage)` reports them, with `steps`, for the
running process.

## Data

| Production | Value (`value_t` alternative) |
Expand Down
25 changes: 25 additions & 0 deletions inc/cvc/state/state_exec/async_scheduler.h
Original file line number Diff line number Diff line change
Expand Up @@ -182,6 +182,30 @@ class async_scheduler : public scheduler_base {
return defaults;
}

/// This scheduler's built-in deep-data settings: what a submitted process runs with when the
/// watch root's `state_exec.defaults.data.*` keys don't say otherwise. data_options{} (no
/// slicing) unless the host sets it.
void set_data_defaults(const data_options &defaults) { data_defaults_ = defaults; }
const data_options &data_defaults() const { return data_defaults_; }

/// The deep-data settings a process submitted now gets: the watch root's keys over
/// data_defaults(). Read on every submit, like the parser settings.
data_options data_settings() const {
return watch_root_ ? data_options_from_state(*watch_root_, {}, data_defaults_) : data_defaults_;
}

/// The deep-data defaults libcvc's own hosts give their async schedulers (app::exec_scheduler()
/// and pycvc's Exec), next to host_parser_defaults(): deep-data work runs 1024 nodes per step
/// (docs/STATE_EXEC_GRAMMAR.md, "Deep data on the executor"). At the measured ~45 ns a node
/// to free, ~70 to print, ~250 to compare and ~380 to copy, a slice costs 0.05-0.4 ms, so a huge
/// value is spread over steps instead of stalling a drain, while the data of a normal program
/// (far under 1024 nodes a step) costs it no extra steps.
static data_options host_data_defaults() {
data_options defaults;
defaults.step_nodes = 1024;
return defaults;
}

private:
scheduling_policy policy_;
int next_pid_ = 1;
Expand All @@ -200,6 +224,7 @@ class async_scheduler : public scheduler_base {
memory_tracker mem_tracker_;
cvc::state *watch_root_ = nullptr;
parse_options parser_defaults_;
data_options data_defaults_;

std::unordered_map<int, process_ptr> processes_;

Expand Down
Loading
Loading