4012 evaluate pattern pruning #4020
Conversation
geo2a
force-pushed
the
4012-evaluate-pattern-pruning
branch
from
71998b1
to
84b3b61
Compare
|
KEVM performance:
|
geo2a
force-pushed
the
4012-evaluate-pattern-pruning
branch
6 times, most recently
from
e8b111d
to
8312613
Compare
| @@ -93,7 +93,7 @@ | |||
| "name": "SortInt", | |||
| "args": [] | |||
| }, | |||
| "value": "6" | |||
| "value": "4" | |||
There was a problem hiding this comment.
The strange changes to this the output of test-collectiontest were caused by the reuse of .json output file by both kore-rpc-booster and booster-dev runs of the test. Since Booster's result is stuck (no more rules), kore-rpc-booster will fallback to Kore and the result will contain Kore's preferred set ordering.
There was a problem hiding this comment.
this diff really does not make much sense.
What happened to test-diamond is: the differences between booster-dev and kore-rpc-booster are mostly eliminated, but some test results have to be special-cased for kore-rpc-dev.
There was a problem hiding this comment.
This response (and response-branch-after-one.json) are now branching. Kore's simplifier is necessary to prune the state after jumpi.false. It is still unclear what it going on here.
There was a problem hiding this comment.
I would maybe just leave --post-exec-simplify on for this test instead...
| "predicate": { | ||
| "format": "KORE", |
There was a problem hiding this comment.
This is a bit weird... the updated output does not have any "predicate" any more?
|
There is a major slowdown in engagement proofs as a result of this PR. A I think that we might need to construct a more representative test suite. |
geo2a
force-pushed
the
4012-evaluate-pattern-pruning
branch
from
ceb3c1e
to
3f29753
Compare
geo2a
force-pushed
the
4012-evaluate-pattern-pruning
branch
from
3f29753
to
afaa394
Compare
|
I've removed the data in this comment as I've been running with an incorrect branch, sorry for the spam. |
|
I've run the
This proof seems to be special in the sense that it does not branch a single time and always stays in Booster, hence this change introduces a slowdown, as we start calling Z3 at the beginning of every execute request. It is not clear to me at that point why the slowdown is so massive. |
geo2a
force-pushed
the
4012-evaluate-pattern-pruning
branch
from
72d4801
to
cdce88c
Compare
|
With cdce88c the runtime of |
|
Just in case this could be useful. For me, the SAT checking points are:
I don't think there is a need to make additional checks at branching points, because there are already checks in place that Even if we cut both |
|
|
To measure the effect of this PR, I am running: I am running using commit With HB version 0.1.67, which comes with that version of K (it's a bit behind, isn't it?), the result is as follows: which is actually a record-breaking time by ~4 minutes. Using HB from this branch, commit and it is clear that having a SAT check at the start of each request causes a substantial overhead. Here, it means that ~560 extra checks were made with respect to the TL; DR: This does not look good for real-world proofs. I think we need to really understand do we want this at all, that is, what is the worst that could happen if we actually started a request from an UNSAT state in the booster. |
|
Thanks @PetarMax! I'd like to re-iterate on the ask to upstream this test, perhaps partially, as to KEVM as a claim, so that we can run is as part of out performance measurement. Regarding having an RPC parameter to turn the initial constraints check off: we actually already have one we could use. It is the |
…fault: no simplification) * Introduces options `--fallback-simplify` and `--post-exec-simplify` to perform said simplifications (before fallbacks and after execute) in `kore-rpc-booster` * The old `--no-fallback-simplify` and `--no-post-exec-simplify` options are still accepted but not doing anything any more.
Separate booster-dev and kore-rpc-booster responses for collectiontest.k Separate kore-rpc-dev and kore-rpc-booster responses for test-vacuous Separate kore-rpc-dev and kore-rpc-booster responses for test-diamond Separate kore-rpc-dev and kore-rpc-booster responses for test-substitution Remove redundant booster-dev responses for test-substitutions Update test-3934-smt Update test-issue3764-vacuous-branch Update output for test-log-simplify-json
geo2a
force-pushed
the
4012-evaluate-pattern-pruning
branch
from
0c92b66
to
9c07a05
Compare
geo2a
force-pushed
the
4012-evaluate-pattern-pruning
branch
from
2ad1c79
to
09d68bb
Compare
geo2a
force-pushed
the
4012-evaluate-pattern-pruning
branch
from
09d68bb
to
586589f
Compare
| (Left ApplyEquations.SideConditionFalse{}, _) -> do | ||
| let tSort = externaliseSort $ sortOfPattern pat | ||
| pure $ Right (addHeader $ KoreJson.KJBottom tSort) |
There was a problem hiding this comment.
...another place where we should probably catch UndefinedTerm and return KJBottom...
| (Left err, _) -> | ||
| pure . Left . RpcError.backendError $ RpcError.Aborted (Text.pack . constructorName $ err) |
There was a problem hiding this comment.
We should probably also catch UndefinedTerm here... (but for now the endpoint anyway returns errors when it is unsure)
There was a problem hiding this comment.
Was this file supposed to be renamed (to state-vacuous-not-rewritten) instead of deleted?
We have the renamed/new response files but no state- file for it
|
|
||
| If `assume-state-defined` is set to `true`, the all sub-terms of `state` will be assumed to be defined before attempting rewrite rules. | ||
| The `assume-defined` flag defaults to `false`. The `assume-defined` flag has different meaning in Booster and Kore. If set to `true`, Booster will not check the constraints of the initial pattern for satisfiability. It is the responsibility of the caller to ensure that the pattern is not vacuous. In Kore, if `assume-defined` is set to `true`, then all sub-terms of `state` will be assumed to be defined before attempting rewrite rules. |
There was a problem hiding this comment.
Maybe add (which is generally assumed bykore-rpc-booster) after the last sentence?
| The `assume-defined` flag defaults to `false`. The `assume-defined` flag has different meaning in Booster and Kore. If set to `true`, Booster will not check the constraints of the initial pattern for satisfiability. It is the responsibility of the caller to ensure that the pattern is not vacuous. In Kore, if `assume-defined` is set to `true`, then all sub-terms of `state` will be assumed to be defined before attempting rewrite rules. | |
| The `assume-defined` flag defaults to `false`. The `assume-defined` flag has different meaning in `kore-rpc-booster` and `kore-rpc`. If set to `true`, Booster will not check the constraints of the initial pattern for satisfiability. It is the responsibility of the caller to ensure that the pattern is not vacuous. In Kore, if `assume-defined` is set to `true`, then all sub-terms of `state` will be assumed to be defined before attempting rewrite rules (which is generally assumed by `kore-rpc-booster`). |
Fixes #4012
Subsumes #4013 and #4011
Summary of changes:
"simplify"endpoint in Booster, when given a pattern (term and predicate) now checks the predicate for SAT before attempting to evaluate the term, returning#Bottomif the constraints are UNSAT."execute"endpoint in Booster will now too check the constraints of the initial pattern for SAT before starting the rewriting loop. This initial check can be disabled by setting the execute request parameter"assume-defined"tofalsekore-rpc-boosterserver will now effectively have--no-post-exec-simplifyoption enabled as default, i.e. no simplification will be done at the Proxy level. The old behavior can be recovered by passing--post-exec-simplifytokore-rpc-booster