Optimize schedule.md #2349
Optimize schedule.md #2349
Conversation
dwightguth
force-pushed
the
schedule3
branch
13 times, most recently
from
f21c767 to
6c18cc7
Compare
…ich are total (#4118) As part of runtimeverification/evm-semantics#2349 we are trying to change how we implement the gas schedule in KEVM in order to improve performance. In order to do this, we introduce a new sort, ScheduleTuple, which has a single constructor with many arguments. We rely on projection functions for named nonterminals in order to extract those arguments. However, this confuses the booster because it is unable to determine that these functions are total. In general, they are not total, however, for the case where the sort they are defined over has a single constructor, they are total. Thus, we introduce logic into GenerateSortProjections which tags these productions as total in the cases where they are in fact total. This has been tested and shown to fix the performance regression in the booster introduced by the above change. It should be easy to see why this change is sound since it applies the `total` attribute only in the case where the production has a single constructor, and the rule matches unconditionally on any instance of that constructor.
dwightguth
force-pushed
the
schedule3
branch
4 times, most recently
from
52b5541 to
77a75e6
Compare
|
@dwightguth please post performance information about this vs master if it's supposed to be an optimization. |
|
I'd be great to ensure this change does not hinder the performance of symbolic execution. We run the It's worth noting that the test should be ideally run with 1 worker (i.e. passing |
|
Yes please, we sohuld check that it does not cause a regression in symbolic execution performance, using the same tables/techniques taht the HBB team uses. |
|
|
You requested the performance data regarding the impact this change has on the Haskell Backend. I ran the data, and it is attached. As you can see, we see on average about a 5% slowdown in the performance of the Haskell backend on these examples. Performance is a critical concern for Pi Squared because we need to execute EVM transactions with a level of performance within an order of magnitude of the performance of competitive EVM clients like Geth and Nethermind. Right now, 13% of the time spent executing KEVM transactions is spent looking up the gas costs of instructions, as compared to 2.5% with this change. It is critical that some version of this performance improvement be included in the EVM semantics so Pi Squared can move forward with development. We spent a significant amount of time iterating on this pull request. This is the third version of the pull request because the first two were rejected. We’ve spent the last two weeks attempting to construct a version of these changes that minimizes the disruption tor RV. This version of the pull request exists as a result of those iterations. It is a compromise between performance of concrete execution, performance on the Haskell backend, readability, and the degree to which it disrupts verification. I’m happy to go back to the original version of these changes, which optimizes for performance and lack of disruption at the expense of readability, but we do need some form of optimization to this cost center to be included in the change. We don’t know why this change reduces the performance of the Haskell backend. It doesn’t entirely make sense that it should, because from a purely theoretic standpoint, the semantics is now doing less work than it did before. We think it may be related to the implementation of the pattern matching algorithm but a definitive answer will require investigation. We suggest that we merge this change and, if you remain concerned about the performance impact, you can commence an investigation into why this change makes the Haskell backend slower. We welcome constructive suggestions on how to proceed, but some form of this change does need to be made in a timely manner. |
| @@ -35,6 +35,7 @@ In the comments next to each cell, we've marked which component of the YellowPap | |||
| <exit-code exit=""> 1 </exit-code> | |||
| <mode> $MODE:Mode </mode> | |||
| <schedule> $SCHEDULE:Schedule </schedule> | |||
| <scheduleTuple> getSchedule($SCHEDULE:Schedule) </scheduleTuple> | |||
There was a problem hiding this comment.
Can we drop the <schedule> cell and have only the <scheduleTuple>?
There was a problem hiding this comment.
No. Schedule is still used in some places, for example when calling precompiled contracts.
|
Closing this. Pi^2 is pursuing a different approach for right now. We will sync back up with you in the future about this change. |
This is a remake of #2335. That PR optimized the schedule lookup functions in schedule.md and deleted the DEFAULT schedule.
This PR takes a slightly different approach to get the same goal. We create a new sort, ScheduleTuple, which contains all of the values of all the schedule constants and schedule flags for a given schedule. We create an operator which computes a ScheduleTuple for a given Schedule via the existing code in schedule.md. Then we create getters for each individual member of the tuple (implicitly). Code that needs access to schedule data gets it by means of calling the getters on a value of sort
ScheduleTuplefrom throughout the semantics, thus considerably simplifying the hot path while maintaining the same code to compute the actual values for the schedule.Performance data:
On the master branch, we spend 35m21s executing the GeneralStateTests, of which 13% is spent in
_<_>. On this branch, we spend 26m46s executing the GeneralStateTests, of which 2.5% is spent in ScheduleTuple getters.