search

runtimeverification / k

K Framework Tools 7.0
BSD 3-Clause "New" or "Revised" License
452 stars 150 forks source link

Module helper functions should be recursive to avoid duplicating work #2221

Open radumereuta opened 3 years ago

radumereuta commented 3 years ago

Something like this https://github.com/kframework/k/blob/master/kore/src/main/scala/org/kframework/definition/outer.scala#L246 could be optimized if we compute the results for local sentences and then combine the results with the ones from the imports.

I don't know for sure what would be the impact of such a change but we already need to initialize some of the functions to reduce work being done: https://github.com/runtimeverification/k/blob/master/kernel/src/main/java/org/kframework/parser/inner/ParseInModule.java#L138

radumereuta commented 3 years ago

Let's keep this in mind when we modify the Module class so we don't make the same mistake again.

radumereuta commented 2 years ago

Provide some numbers. It take time in kompile, but it also takes some time when running proofs. Many proofs, lots of time spent.

radumereuta commented 2 years ago

Here are some numbers from evm proofs. Command: kserver ; make proofs -j 12

kompile driver.md -I /home/radu/work/evm-semantics/.build/usr/lib/kevm/include/kframework -I /home/radu/work/evm-semantics/.build/usr/lib/kevm/blockchain-k-plugin/include/kframework --hook-namespaces 'JSON KRYPTO BLOCKCHAIN' --emit-json --md-selector 'k & ! nobytes & ! node' --backend haskell --directory .build/usr/lib/kevm/haskell --main-module ETHEREUM-SIMULATION --syntax-module ETHEREUM-SIMULATION -v --debug -I /usr/lib/kevm/include/kframework -I /usr/lib/kevm/blockchain-k-plugin/include/kframework
Outer parsing [85 modules]                                   =  1.798s
  New scanner: STDOUT-STREAM-CONFIG-CELLS                    =  0.195s
  New scanner: STDIN-STREAM-CONFIG-CELLS                     =  0.227s
  New scanner: EVM-CONFIG-CELLS                              =  0.557s
Parse configurations [3/3 declarations]                      =  1.303s
  New scanner: ETHEREUM-SIMULATION-RULE-CELLS                =  1.148s
  New scanner: K-IO-RULE-CELLS                               =  0.378s
  New scanner: STDOUT-STREAM-RULE-CELLS                      =  0.391s
  New scanner: STDIN-STREAM-RULE-CELLS                       =  0.449s
  New scanner: ETHEREUM-SIMULATION-RULE-CELLS                =  2.609s
Parse rules [1545/1545 rules]                                =  9.535s
Validate definition                                          =  0.429s
Apply compile pipeline                                       =  4.479s
Kompile to kore                                              =  1.375s
Save to disk                                                 =  0.184s
Backend                                                      =  5.883s
Cleanup                                                      =  0.000s
Total                                                        = 25.000s
kprovex --directory tests/specs/benchmarks/verification/haskell tests/specs/benchmarks/staticarray00-spec.k -I /home/radu/work/evm-semantics/.build/usr/lib/kevm/include/kframework -I /home/radu/work/evm-semantics/.build/usr/lib/kevm/blockchain-k-plugin/include/kframework --profile-rule-parsing timings/tests/specs/benchmarks/staticarray00-spec.k.log --format-failures -v --dry-run
Outer parsing [100 modules]                                  =  2.342s
  New scanner: VERIFICATION-RULE-CELLS                       =  2.013s
  New scanner: STATICARRAY00-SPEC-RULE-CELLS                 =  1.712s
Parse spec modules [1/1 rules]                               = 13.734s
Apply prover steps                                           =  5.537s
kore-exec /home/radu/work/evm-semantics/./tests/specs/benchmarks/verification/haskell/verification-kompiled/definition.kore --module VERIFICATION --prove /home/radu/work/evm-semantics/./.kprove-2021-10-04-15-12-45-690-aa23c232-aac8-4527-ac2d-60075b0c5226/spec.kore --spec-module STATICARRAY00-SPEC --output /home/radu/work/evm-semantics/./.kprove-2021-10-04-15-12-45-690-aa23c232-aac8-4527-ac2d-60075b0c5226/result.kore
Backend                                                      =  3.057s
Cleanup                                                      =  1.184s
Total                                                        = 25.884s
time test
5.414s functional-spec.k
5.537s staticarray00-spec.k
5.795s bytes00-spec.k
5.274s overflow00-nooverflow-spec.k
5.610s address00-spec.k
5.632s encodepacked-keccak01-spec.k
5.877s requires01-a0gt0-spec.k
6.279s overflow00-overflow-spec.k
6.327s staticloop00-a0lt10-spec.k
6.521s encode-keccak00-spec.k
6.238s keccak00-spec.k
6.289s requires01-a0le0-spec.k
7.489s infinite-gas-spec.k
7.529s lemmas-no-smt-spec.k
7.853s storagevar02-nooverflow-spec.k
7.638s storagevar01-spec.k
7.893s storagevar02-overflow-spec.k
7.128s storagevar00-spec.k
6.508s merkle-spec.k
7.186s lemmas-spec.k
6.394s storageRoot-spec.k
6.620s storagevar03-spec.k
6.458s allowance-spec.k
5.921s approve-failure-spec.k
6.562s balanceOf-spec.k
5.954s approve-success-spec.k
6.210s totalSupply-spec.k
5.895s transfer-failure-2-b-spec.k
5.868s transfer-failure-2-a-spec.k
5.123s transfer-failure-1-a-spec.k
5.751s transferFrom-failure-2-a-spec.k
5.613s transferFrom-failure-2-b-spec.k
5.285s transfer-failure-1-c-spec.k
6.055s transfer-success-2-spec.k
6.233s transferFrom-failure-2-c-spec.k
6.276s transferFrom-success-1-spec.k
5.560s allowance-spec.k
5.562s transfer-success-1-spec.k
5.559s transferFrom-success-2-spec.k
5.976s balanceOf-spec.k
5.926s approve-spec.k
5.406s totalSupply-spec.k
6.148s transfer-failure-2-spec.k
5.413s transferFrom-failure-2-spec.k
5.847s transferFrom-success-2-spec.k
5.817s transferFrom-success-1-spec.k
6.054s transfer-failure-1-spec.k
5.520s transferFrom-failure-1-d-spec.k
6.190s transfer-success-1-spec.k
6.119s forwardToHotWallet-failure-1-spec.k
5.842s transfer-success-2-spec.k
6.566s transferFrom-failure-1-spec.k
6.720s forwardToHotWallet-failure-2-spec.k
6.708s functional-spec.k
6.355s sum-to-n-spec.k
5.843s solidity-code-spec.md
6.064s forwardToHotWallet-failure-3-spec.k
6.009s forwardToHotWallet-failure-4-spec.k
5.954s transferFrom-failure-1-c-spec.k
6.943s cat-exhaustiveness-spec.k
6.818s dai-symbol-pass-spec.k
7.100s dai-adduu-fail-rough-spec.k
6.715s dstoken-approve-fail-rough-spec.k
5.461s transferFrom-failure-1-a-spec.k
7.231s dsvalue-peek-pass-rough-spec.k
7.102s dsvalue-read-pass-spec.k
7.665s flipper-tau-pass-spec.k
7.721s flipper-ttl-pass-spec.k
6.835s end-subuu-pass-spec.k
7.656s functional-spec.k
5.762s flipper-addu48u48-fail-rough-spec.k
4.014s evm-optimizations-spec.md
4.936s vat-addui-fail-rough-spec.k
4.750s vat-subui-pass-rough-spec.k
4.850s vat-subui-pass-spec.k
4.724s vat-mului-pass-spec.k
4.294s dsvalue-read-pass-summarize-spec.k
gtrepta commented 11 months ago

The code links in the original post are outdated now, and don't reference anything interesting as far as I can tell.

radumereuta commented 11 months ago

It's about functions like this:

  lazy val productionsFor: Map[KLabel, Set[Production]] =
    productions
      .collect({ case p if p.klabel != None => p })
      .groupBy(_.klabel.get.head)
      .map { case (l, ps) => (l, ps) }

It calculates the map by looking at the entire list of productions from all the imported modules. If you take into consideration that we use these functions in visitors, then you can see the duplicated work. A visitor will start applying a transformation on the deepest module and calculate productionsFor. Then it's going to move to the siblings of that module and do the same thing. By looking again at the entire list of productions, which is recursive. And so on, until the root module. So the deepest nested productions are going to be calculated x no of modules.

I haven't measured the impact of this quadratic behavior recently (which should be linear). But it might matter in certain cases, especially when comparing large objects. I think it's mostly visible when you call ParseInModule::initialize().