key icon indicating copy to clipboard operation
key copied to clipboard

Published 20 hours ago • verified publisher icon KeYProject

key is too slow with large post-conditions

Open wadoon opened this issue 2 years ago • 0 comments

This issue was created at git.key-project.org where the discussions are preserved.

  • Mantis: MT-827
  • Submitted on: 2007-06-26 by (at)pruemmer
  • Updated: 2014-08-05

Description

When proving problems where a big formulas occurs behind a program block (i.e., <{prog}>big_phi), the performance of key is very bad. I think this is (in parts) caused by the fact that the rule matching cache (proof.TermTacletAppIndexCache) is currently not used for formulas underneath modal operators. It should be possible to enable the cache also for such cases (when being careful :-)).

Files

0827-symm.key

Notes

(at)most at 2007-06-26

I certainly agree and urge a fix ;)

(at)klebanov at 2007-07-16

How about this: 4853 rules (17 branches) in 172975,4 seconds with the attached problem. That's more or less exactly 48 hours. ;)

(at)most at 2007-07-16

Man, I adore your patience ;) What was the heap use for this thing?

(at)klebanov at 2007-07-16

g Oh, the heap use was not that terrible (it's not a long proof ;)) - about 1Gb I would say. Unfortunately, the system died a terrible swapping death when I was trying to examine what the proof actually looked like.

(at)pruemmer at 2007-07-22

There is a second reason for the bad performance: updates get too big when non-rigid predicates (in particular, inReachableState) are included in the post-condition. This happens in at least two situations: the JML/method contract mechanism seems to include inReachableState by default (which is pretty useless), and the JML/invariant mechanism adds inReachableState to invariants by default (which makes a bit more sense, but is unnecessary and devastating nevertheless). In the mondex read-visInv example, updates with around 150 assignments occur, most of the assignments describe temporary variables that are never needed again. The application rate for this example is poor 20 apps per second on my machine.

(at)pruemmer at 2007-07-22

0.2585 contains one optimisation for large post-conditions: when rewriting in an update that is in front of a program block, the post-condition of the program is not re-matched. ~10% speedup for the overflow_hija example

(at)pruemmer at 2007-07-23

Ah, only now I realised that Vladimir's example is Peter Baumgartner's infamous symmetry array case. The problem with your formalisation is that the quantified formula behind the program gets really bad once updates have been applied to it. Solution: don't do that. The distribution contains a different formalisation (examples/java_dl/symmArray.key) that works well even for 10 array updates. Of, course, Peter might call this cheating ... Btw, Rustan tried the same example with Spec# and could also solve it without problem. Only 3 orders of magnitude faster than key.

I'm just checking in the first version of a new cache architecture on side branch "ruemmerNewCache". But this one needs more testing, and the memory usage is probably too large for some example right now.

(at)most at 2007-07-23

Go, Philipp go! ;)

(at)klebanov at 2007-07-23

Heheh. Peter was here. The symmArray.key has the predicate already expanded. This was indeed my first formulation, but Peter claimed that it is cheating. We un-expanded the predicate ;) and then went through several stages:

  1. Very quick proofs. KeY judged the predicate as rigid and would remove the update at once. ;)

  2. Declared the predicate as non-rigid, but found that there is no way to use the definition, since it was only given in the pre-state. This is not surprising, but annoying. It would be nice to have some way to have global definitions valid in all states.

  3. Duplicated the definition, but then got the situation above. We would all be set if KeY could use the definition first, and then applied the updates. Unfortunately, the means to do reasoning on the postcondition are very limited.

So much for a quick report on this funny little problem.

(at)pruemmer at 2007-07-23

But Peter is also cheating, because there are no updates in his logic that could turn quantified formulas into a mess of if-then-else expressions.

There are two further ways to un-expand the symm-definition:

  • introduce a (state-independent) taclet for unfolding the definition.

  • use a query and formulate the definition completely in JML.

I tried both versions, and both work fine. I would actually prefer the first one, but unfortunately the taclet with the definition becomes pretty unreadable (because one cannot use concrete quantified variables in taclets, and because the attribute "length" cannot directly be used in taclets). I think we need a more userfriendly way to (recursively) define non-rigid predicates, maybe similarly to the contract-compartment in a .key-file. The definition could then be compiled to a taclet when loading the file.

(at)pruemmer at 2007-08-07

0.2599 contains the new cache architecture that, to some degree, solves this problem. Also the handling of quantified expressions should be faster. Apart from that, the TermTacletAppIndex is made more efficient in 2599 to reduce the amount of rematching in post-conditions.

For some examples, 2599 is close to twice as fast as earlier versions.

(at)most at 2007-08-16

Great, although for my problems the gain is not so big. But anything is good. I also did notice that the memory consumption decreased somewhow after all the recent hocus pocus. Could that be right?

(at)pruemmer at 2007-08-16

The performance gain depends very much on the shape of a problem, for the examples that are run with "runAllProofs", the gain is about 10% on average. It gets bigger when working on problems with large post-conditions.

I would expect that memory gets used more efficiently now when opening multiple proofs in one prover instance? (because the same cache is used for all proofs, i.e., no data is cached for proofs that have been inactive for a while)

(at)pruemmer at 2007-08-16

Oh, right, and the rule queue should generally get shorter and contain fewer obsolete entries, because rematching is done less often

(at)most at 2007-08-21

I was just wondering (aimlessly probably). I just produced a huge proof overnight (not the whole night, I just left it running and it was ready in the morning). The proof is circa 81000 steps, large postcondition, lots of updates, lots of possible aliasing, the usual ;) It loads in less than 2 minutes. Also the memory consumption stays stable, while when actually running the proof the whole heap of 1.8GB gets close to be filled up at times. So I just wonder - the difference in performance is huuuuuuuge - aren't we simply missing something, some small bit being unnecessairly complex, some memory being leaked, I don't know. It just contradicts my intuition ;)

History

  • (at)pruemmer -- (NEW_BUG) 2007-06-26

  • (at)most -- (BUGNOTE_ADDED) 2007-06-26

  • (at)klebanov -- (FILE_ADDED) 2007-07-16

  • (at)klebanov -- (BUGNOTE_ADDED) 2007-07-16

  • (at)most -- (BUGNOTE_ADDED) 2007-07-16

  • (at)klebanov -- (BUGNOTE_ADDED) 2007-07-16

  • (at)pruemmer -- (BUGNOTE_ADDED) 2007-07-22

  • (at)pruemmer -- (BUGNOTE_ADDED) 2007-07-22

  • (at)pruemmer -- (NORMAL_TYPE) 2007-07-23

  • (at)pruemmer -- (NORMAL_TYPE) 2007-07-23

  • (at)pruemmer -- (BUGNOTE_ADDED) 2007-07-23

  • (at)most -- (BUGNOTE_ADDED) 2007-07-23

  • (at)klebanov -- (BUGNOTE_ADDED) 2007-07-23

  • (at)pruemmer -- (BUGNOTE_ADDED) 2007-07-23

  • (at)pruemmer -- (BUGNOTE_ADDED) 2007-08-07

  • (at)most -- (BUGNOTE_ADDED) 2007-08-16

  • (at)pruemmer -- (BUGNOTE_ADDED) 2007-08-16

  • (at)pruemmer -- (BUGNOTE_ADDED) 2007-08-16

  • (at)most -- (BUGNOTE_ADDED) 2007-08-21

  • (at)klebanov -- (BUG_ADD_RELATIONSHIP) 2013-05-08

  • (at)grahl -- (NORMAL_TYPE) 2014-06-18

  • (at)grahl -- (NORMAL_TYPE) 2014-06-18

  • (at)grahl -- (TAG_ATTACHED) 2014-08-05

Attributes

  • Category: Prover Core
  • Status: ACKNOWLEDGED
  • Severity: MAJOR
  • OS:
  • Target Version:
  • Resolution: OPEN
  • Priority: NORMAL
  • Reproducibility: ALWAYS
  • Platform:
  • Commit: None
  • Build: 0.2560
  • Tags [{'name': 'performance'}]
  • Labels: ~Prover Core ~Bug ~NORMAL

View in Mantis

Information:

  • created_at: 2017-05-29T02:44:25.953Z
  • updated_at: 2017-05-29T02:44:25.953Z
  • closed_at: None (closed_by: )
  • milestone:
  • user_notes_count: 0

wadoon avatar Dec 23 '22 23:12 wadoon