Repository navigation
state_exec: max_memory counts the deep-data work a process waits on - #695
Merged
Merged
Conversation
Inside an evaluator step, the native function the step applies may call a native function itself; a native call asked for from deeper is deferred to step_data, which makes it at its own level (data_step_scope::calls_here). (apply apply L), send through itself and a constructor that is its own init are now loops of steps that max_steps and max_time stop the same way on every platform, instead of hitting the stack-dependent nesting limit. A forwarding call job gives its place to its callee's work, so such chains run in constant space. Inherited init/finalize and the constructor look up the inherited chain 64 classes a call instead of calling through it. pending_data_work chains are freed a link at a time. native_nesting stays the backstop for generators and native calls from C++ with no evaluator.
…ive-calls # Conflicts: # src/cvc/tests/state_exec_deep_data_test.cpp
A heap measurement could not start while a process waited on deep-data work, and it never looked at what that work held, so a process that never stops waiting (a class whose init is its own constructor, or a closure init that constructs again) was held only by max_steps/max_time. Now a measurement may start on top of work in flight and runs first; it counts each pending work and what its job holds (data_job::held_values/held_bytes, implemented by the call and generator jobs). A job left to run after its call reports its bytes with eval_alloc_note so a re-measure comes due. fork refuses while any work in the chain waits on a frame (waits_on_data_work), not only the innermost.
…p-data-work # Conflicts: # docs/STATE_EXEC_GRAMMAR.md # inc/cvc/state/state_exec/data_job.h # src/cvc/state/state_exec/data_job.cpp # src/cvc/state/state_exec/stackless_evaluator.cpp
transfix
enabled auto-merge (squash)
October 18, 2026 22:03
transfix
disabled auto-merge
October 18, 2026 22:03
transfix
enabled auto-merge (squash)
October 18, 2026 22:03
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Stacked on #689. Review the last commit, 26e0bf3. It targets master so CI runs; once #689 merges, master gets merged in here.
Why
max_memorycovers a process's measured heap (#667), but a measurement could not start while the process waited on deep-data work, and it never looked at what that work held. A process that never stops waiting was held only bymax_steps/max_time. Two cases:initis its own constructor,(begin (defclass P) (set-attr P.__cls_dict__ "init" P) (P)), which after state_exec: native calls past the first level are the evaluator's #689 is a loop of steps instead of a nesting error. Each level passesinitone argument more, so memory grows quadratically;initthat constructs again,(begin (defclass P (init (self) (P))) (P)). Master has this one too.What changed
data_jobhas two new virtuals:held_values(visit)visits the values a job owns copies of;held_bytes()gives the job's own size and buffers.call_walk: function, arguments, result) and the generator job (collect's gathered values) implement them. The stdlib jobs only borrow their caller's arguments or build results held to the allocation limit, so they don't need to.eval_alloc_noteinrun_data_job), so a re-measure comes due as waiting calls pile up.heap_after_stepnow starts a measurement during a call in flight: innermost, withouterset and waiting on no frame. It runs first, and the call goes on after it.heap_share_jobcounts each pending work and what its job holds.waits_on_data_work), not only when that work is innermost. So a fork during a measurement that runs on top of a call is still refused.Measured
Each runaway, with
max_memory= 2 MiB and no other limit hit (MSVC Release):initinitthat constructs againBefore this change, neither was ever measured: the first ran into
max_stepswith a quadratically growing argument chain, the second untilmax_steps/max_time.Tests
state_exec_heap_test:AMeasurementRunsOnTopOfACallInFlight: a measurement due whilecollections.mapcalls a lambda sits on top of the map's work, runs without stepping any frame, and then the map finishes with the right result.waits_on_data_workholds meanwhile, so no fork.TheWorkAProcessWaitsOnCounts: after 100 steps of the self-initrunaway, the measured share includes the waiting calls' arguments (over 10000 values).ACallChainThatNeverEndsRunsOutOfMemory: both scripts, on the async scheduler (exit errormemory_limit_exceeded) and the sync one (killed before the step backstop, measured heap at least the budget).Docs: the developer guide's "Memory: state-tree writes and the measured heap", "Native call nesting" in
docs/STATE_EXEC_GRAMMAR.md, and the pycvc parity table (waits_on_data_workis internal).Local results (MSVC 14.38 Release, Windows, cvcpkg prefix)
state_exec_deep_data_testpasses at 64 KiB.NativeCallThroughputandEvalFibonacciare within noise of state_exec: native calls past the first level are the evaluator's #689.