runtimeverification / avm-semantics

BSD 3-Clause "New" or "Revised" License
15 stars 4 forks source link

Investigate performance of `#initTxnIndexMap()` #287

Closed geo2a closed 1 year ago

geo2a commented 1 year ago

The #initTxnIndexMap() rule traverses the <transaction> cell and builds the <txnIndexMap>, a service cell which clusters the transactions by their groups and maintains a reverse index from group indices to transaction ids.

The #initTxnIndexMap() rule will be executed when a transaction group evaluation is triggered by the #evalTxGroup() rule, which fires both when the initial (outer) group is evaluated and an inner group is evaluated.

We suspect that this rule is expensive to execute, and we would like to determine how, in fact, expensive it is.

As an initial step, we should investigate the tests/specs/calls/buy-asset-spec.md:

nwatson22 commented 1 year ago

I tried the test you suggested in the linked branch. There seems to be about a 10 second speedup between the two (160 vs. 170 seconds). There are about 300 rewrites in this (non-forking) proof with about 10 steps of #initTxnIndexMap I'm guessing this means that these steps are collectively a bit slower than the average rewrite, but not that much worse. Was there an example where it seemed to be causing problems?

geo2a commented 1 year ago

Thanks @nwatson22. OK, I'll be closing it for now.