#3143 rewrite graph traversal + output unexplored leaves #3168
Conversation
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
4 tasks
|
|
|
|
|
3 tasks
|
New traversal models required functionality in data types rather than using exceptions and monad stack layers to add functionality. The `graphTraversal` function operates with a list of "steps" (sequences of "instructions") that take a configuration to a result containing new configurations. The traversal is parameterised with a specific transition function `([Step instr],config) -> m (TransitionResult ([Step instr],config))` which interprets step results. `TransitionResult` can indicate to continue with one (`Continuing`) or more (`Branch`) new configurations, or that the configuration is final, stuck, or should be stopped. One reason to stop is when the list of steps runs empty, other reasons could be to stop execuction on the application of certain rules. The transition function can be constructed from one that operates on the primitive instructions, together with an interpretation function that differs depending on the use case (proving or executing).
jberthold
force-pushed
the
3119-rewrite-graph-traversal-output-unexplored-leaves
branch
from
466f594 to
1662e72
Compare
jberthold
changed the title
|
Contributor
ana-pantilie
left a comment
ana-pantilie
left a comment
There was a problem hiding this comment.
This approach is definitely friendlier than the old one, but I think it's still a bit hard to understand just by reading the code, so my suggestions currently concern readability.
I also noticed that allocation has decreased a bit. Should we expect some performance improvements as well? That would be amazing. 😁
| import Kore.Simplify.Data (Simplifier) | ||
| import Prelude.Kore | ||
| import Pretty | ||
|
|
Contributor
There was a problem hiding this comment.
I think this module would benefit from some extra documentation. My first thought was, how do TransitionResult, StepResult and TraversalResult all relate to eachother?
Member
Author
There was a problem hiding this comment.
I have added documentation that describes all these types together, in a haddock comment on graphTraversal. Is this what you had in mind?
| -- execution is not a generic tree, but a cofree comonad with exactly the | ||
| -- branching structure described by the strategy algebra. | ||
| data Strategy prim where | ||
| -- The recursive arguments of these constructors are /intentionally/ lazy to |
Contributor
There was a problem hiding this comment.
This is probably out of scope for this PR, but we should probably keep in mind that we'd like to get rid of this type in the near future. Maybe a subsequent PR could take care of that?
Member
Author
There was a problem hiding this comment.
Yes, this type (and maybe even the whole module Strategy) is on the list of things to remove. I would think we lift everything worth keeping into the new GraphTraversal module.
Currently the Prove module still uses Strategy for the single-step function, and the repl uses the computation graph directly. Removing this and consolidating the parts we need from Strategy into GraphTraversal would be follow-up work in a new ticket and PR.
Member
Author
The new version is a bit faster, yes. My experiment PR had some KEVM timing comparisons - around 3% faster overall, most of it probably because of using |
Command > nix run .#update-cabal-ghc9
jberthold
commented
Jul 29, 2022
Comment on lines
+101
to
+105
| "flake-utils_2": { | ||
| "locked": { | ||
| "lastModified": 1642700792, | ||
| "narHash": "sha256-XqHrk7hFb+zBvRg6Ghl+AZDq03ov6OshJLiSWOoX5es=", | ||
| "owner": "numtide", |
Member
Author
There was a problem hiding this comment.
Changes here were auto-generated from running command nix run .#update-cabal-ghc9 (as instructed by @goodlyrottenapple )
|
|
…traversal-output-unexplored-leaves
|
rv-jenkins
deleted the
3119-rewrite-graph-traversal-output-unexplored-leaves
branch
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.
Related to #3119
Part of #3143
Scope:
Rewrite of graph traversal used by Kore.Exec and Kore.Reachability.Prove
New traversal models required functionality in data types rather than using exceptions and monad stack layers to add functionality.
The
graphTraversalfunction operates with a list of "steps" (sequences of "instructions") that take a configuration to a result containing new configurations.The traversal is parameterised with a specific transition function
([Step instr],config) -> m (TransitionResult ([Step instr],config))which interprets step results.
TransitionResultcan indicate to continue with one (Continuing) or more (Branch) new configurations, or that the configuration is final, stuck, or should be stopped.One reason to stop is when the list of steps runs empty, other reasons could be to stop execuction on the application of certain rules.
The transition function can be constructed from one that operates on the primitive instructions, together with an interpretation function that differs depending on the use case (proving or executing).
Estimate:
Review checklist
The author performs the actions on the checklist. The reviewer evaluates the work and checks the boxes as they are completed.