runtimeverification / avm-semantics

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

Use krun class, avoid stderr #197

Closed ehildenb closed 1 year ago

ehildenb commented 1 year ago

This is an attempt to switch the KAVM class over to using KRun class functionalities instead of manually calling krun.

Blocked on: https://github.com/runtimeverification/avm-semantics/pull/196 Blocked on: https://github.com/runtimeverification/avm-semantics/pull/189 Blocked on: https://github.com/runtimeverification/pyk/pull/105 Blocked on: https://github.com/runtimeverification/pyk/pull/104

Currently, we're seeing a slowdown using this technique:

image

image

Typically, I should be able to run each simulation in ~140-200ms, but now we're seeing ~700-1100ms. Most of the time is wasted in Kore -> Kast conversion in the pyk code. To improve this (by about 500ms I estimate), we should do:

geo2a commented 1 year ago

This design is definitely better, but we need to work on performance, as outlined. Thanks @ehildenb!

geo2a commented 1 year ago

@ehildenb I've cherry-picked most of your commits into #222, closing this one.