search

runtimeverification / haskell-backend

The symbolic execution engine powering the K Framework
BSD 3-Clause "New" or "Revised" License
212 stars 42 forks source link

[Haskell-Performance] kevm proof slow with extra side conditions #3286

Open ehildenb opened 2 years ago

ehildenb commented 2 years ago

Please Prepare Test Data

I have a specification on KEVM: https://github.com/runtimeverification/evm-semantics/blob/master/tests/specs/benchmarks/storagevar03-spec.k

This can be run with: make tests/specs/benchmarks/storagevar03-spec.k.prove after building KEVM.

It has some side-conditions for validity on the input state: https://github.com/runtimeverification/evm-semantics/blob/master/tests/specs/benchmarks/storagevar03-spec.k#L116. But these side-conditions are actually not needed (the lines CONTRACT_ID >Int 0 andBool notBool #isPrecompiledAccount(CONTRACT_ID, BYZANTIUM)), so I removed them.

Removing these 4 conditions (on CONTRACT_ID and CALLEE_ID) ends up improving the performance by ~2.5X.

So it seems that having these extra side-conditions is causing a big performance slowdown.

I've attached 2 bug reports:

These conditions should not change their simplification status through the whole proof beyond startup, so I guess I'm wondering why it takes so much longer to run with these extra conditions. We should try evaluating them once, and then basically know that they can't be simplified any further throughout the rest of execution (so should not try).

ehildenb commented 2 years ago

@F-WRunTime it seems that it cannot detect that I'm a member of the org? https://github.com/runtimeverification/haskell-backend/actions/runs/3148634684/jobs/5119382938

ehildenb commented 2 years ago

Also, it seems to create too many jobs: image

ehildenb commented 2 years ago

dummy comment to trigger workflow

ehildenb commented 2 years ago

Test me.

ehildenb commented 2 years ago

Test me.

jberthold commented 2 years ago

Ran the two tarballs in a separate ticket #3303 . Nothing immediately suspicious in the profiles, but the top consumers differ to significant extent:

with-conditions

COST CENTRE MODULE SRC %time %alloc
hashWithSalt Kore.Internal.TermLike.TermLike src/Kore/Internal/TermLike/TermLike.hs:698:5-77 4.7 4.7
hashWithSalt1 Data.Hashable.Class Data/Hashable/Class.hs:271:1-45 1.8 1.4
ravel Data.Generics.Internal.VL.Lens src/Data/Generics/Internal/VL/Lens.hs:66:1-42 1.8 1.6
guardAgainstBottom Kore.TopBottom src/Kore/TopBottom.hs:45:1-49 1.4 0.8
addConditionWithReplacements Kore.Internal.SideCondition src/Kore/Internal/SideCondition.hs:(310,1)-(333,29) 1.4 1.0
simplifySubstitutionWorker Kore.Simplify.SubstitutionSimplifier src/Kore/Simplify/SubstitutionSimplifier.hs:(267,1)-(399,78) 1.4 1.8
unionWith Data.Map.Strict.Internal src/Data/Map/Strict/Internal.hs:(990,1)-(996,35) 1.4 0.8
compare Data.InternedText src/Data/InternedText.hs:(82,5)-(86,61) 1.4 0.0
liftSimplifier Kore.Simplify.Simplify src/Kore/Simplify/Simplify.hs:192:5-42 1.3 1.7
compare Kore.Rewrite.RewritingVariable src/Kore/Rewrite/RewritingVariable.hs:75:25-27 1.2 0.0
fmap Kore.Internal.Predicate src/Kore/Internal/Predicate.hs:171:21-27 1.2 0.3
repIso Data.Generics.Internal.Profunctor.Iso src/Data/Generics/Internal/Profunctor/Iso.hs:38:1-20 1.1 2.6
substitute Kore.Internal.TermLike.TermLike src/Kore/Internal/TermLike/TermLike.hs:(850,5)-(948,57) 1.1 1.4

without-conditions

COST CENTRE MODULE SRC %time %alloc
hashWithSalt Kore.Internal.TermLike.TermLike src/Kore/Internal/TermLike/TermLike.hs:698:5-77 8.4 8.8
addConditionWithReplacements Kore.Internal.SideCondition src/Kore/Internal/SideCondition.hs:(310,1)-(333,29) 3.6 2.4
liftSimplifier Kore.Simplify.Simplify src/Kore/Simplify/Simplify.hs:192:5-42 3.0 4.3
hashWithSalt1 Data.Hashable.Class Data/Hashable/Class.hs:271:1-45 2.2 2.4
fmap Kore.Internal.Predicate src/Kore/Internal/Predicate.hs:171:21-27 1.5 0.5
ravel Data.Generics.Internal.VL.Lens src/Data/Generics/Internal/VL/Lens.hs:66:1-42 1.4 1.3
compare Data.InternedText src/Data/InternedText.hs:(82,5)-(86,61) 1.3 0.0
project Kore.Internal.Predicate src/Kore/Internal/Predicate.hs:(325,5)-(327,67) 1.2 4.8
compare Kore.Internal.TermLike.TermLike src/Kore/Internal/TermLike/TermLike.hs:(692,5)-(695,29) 1.2 0.0
simplifySubstitutionWorker Kore.Simplify.SubstitutionSimplifier src/Kore/Simplify/SubstitutionSimplifier.hs:(267,1)-(399,78) 1.1 1.3
ana-pantilie commented 2 years ago

Blocked on https://github.com/runtimeverification/haskell-backend/issues/3113, because the highest cost center is hashing. After that is fixed, we should reinvestigate.