Optimising Rewrite Performance

[DavePearce]

In exploring #18, an important discovery was made:

• Incremental maintenance of reachability information is crucial for performance

In fact, in exploring the substitution approach versus the rewrite-based approach to handling inferences, it had become apparent to me that this would be especially true. However, the very surprising verification performance of Whiley v0.3.36 appears to stem specifically from the use of an incremental algorithm. One which, unfortunately, was removed at some point for reasons unknown.

Therefore, the goal of this issue is to reconsider the incremental approach in the context of the new Rewriter API.

[DavePearce]

The latest version of the algorithm in question I can find is in RevertingBatchRewriter in commit 15041f8 on 14th August:

https://github.com/Whiley/WhileyRewriteLanguage/blob/15041f8d06947f6e677651eb9736c2fc6f8557bf/src/wyrw/util/RevertingBatchRewriter.java

This is not the implementation used in v0.3.36, though it was most likely the basis for it.

I think the main thing this algorithm does is:

1. Reduce the amount of time spent on finding reachable states and compacting and minimising the automaton.

2. Implement the oneStepUndo which is necessary in the rewrite-based approach to implementing inference rules (though not for the substitution-based approach).

[DavePearce]

Strategies for improving performance using incremental algorithms:

1. Eliminate need for compaction during reduction rewrites. To do this, we need to incrementally maintain reachability information. The key thing we know is that after a rewrite has occurred, the target of the rewrite is guaranteed to be unreachable.

2. Prevent unnecessary reprobing of states. To do this, we need to incrementally maintain knowledge of which states are "dirty". That is, after a rewrite has occurred, some states need to be reprobed and some don't.

To fully implement (1) it would probably help if the Automaton was bidirectional. This would reduce the cost of identifying unreachable states.

[DavePearce]

What's the goal?

• To incrementally compact and minimise the automaton during reduction. This means maintaining and updating reachability information? Note that, with substitution applied for inference rules, we need to consider reachability information from multiple roots.
• When a reduction is successfully applied the target of that reduction is guaranteed to be unreachable. A naive approach is to simply "null" out any state which is eliminated in this way. However, this does not account for items reachable from the state which are now unreachable.
• A better approach is perhaps to maintain a reference count for each state, so that we can tell when one has become truly unreachable. Cycles are perhaps a problem here because the elimination of one state could then leave a cycle with each node having reference count 1 (i.e. the classic reference count problem).
• A simpler approach is just to simply work done during compaction by nullifying states in the automaton but not shifting. This does reduce work, for sure --- but it's still linear in the number of states.
• The ideal solution is to maintain reachability in a specific manner. That is, reachability from a root without traversing a "back-edge". In contrast, cross-edges are permitted. This information can easily be computed, but can it be maintained?
• What about minimisation? Is it really a problem? This boils down to the question as to whether a singe rewrite can introduce a new cycle. I think the answer is that it cannot. Eliminating minimise() from Reduction doesn't seem to have any adverse effects.

[DavePearce]

Continuing to think about incrementalisation. What are we trying to achieve?

• Compaction. To prevent the automaton from expanding aggressively and consuming available RAM, we compact. However, this is done strictly but could be done in a more lazy fashion by looking at the state-2-null ratio.
• Unreachable States. We need to identify unreachable states to avoid needlessly applying rewrites to them which could result in an infinite loop (though perhaps not if each rewrite nullifies at least one state).
• Reprobing. After a rewrite is applied need to update the set of activations which may apply. Doing this incrementally can prevent a lot of work.

The question is: how to address these requirements. Some obvious ideas:

• Least Common Ancestor (LCA). Maintaining the least common ancestor for each node would help us quickly identify the set of unreachable nodes after a rewrite. The key challenge is that after a rewrite we need to update the LCAs for affected nodes.
• Organise Rules by Root Type. This is a simple trick which can potentially reduce the overall amount of work.
• Activation Invalidation. After a rewrite, the trick is to try and invalidate activations rather than recomputing all activations. To do this, we need to consider the maximum depth for a given rule. That is, the maximum distance from the root of a node which could affect the decision to accept or reject. Then, after a rewrite we can identify the set of affected nodes which should be invalidated.
• Batch State Addition. A single rewrite can result in multiple new states being added to the automaton which could be expensive. This is because every addition requires checking whether an identical state already exists. Providing a way to cheaply add states in batches would help.

Another important consideration is to maintain information across reduction / inferences. At the moment, all information is destroyed once a reduction is completed, etc. Also, should not forget the cost of adding a new vertex to the automaton, etc.

[DavePearce]

A little bit of instrumentation has proved to be quite interesting. In particular, here are the three things I instrumented:

• Probing. After each sucessful rewrite is applied, we must reprobe the automaton. This measures the time spent doing this.
• Rewriting. This measures the time spent performing applying an activation, in both the successful and unsuccessful cases.
• Compaction. This measures the time spent identifying unreachable states and compacting the automaton.

Overall, the results indicates the time spent rewriting significantly dwarfs the time spent on the other two aspects. This raises the question as to which aspect of rewriting is expensive?

There are a couple of hypotheses:

1. This simply reflects the fact that the rewrite() method is called much more often. This is true because it is called regardless of whether a rewrite is successful or not. However, the new requires clause should have helped here.
2. The time spent on substitution is very expensive. This is currently performing some kind of depth-first search from a root. This involves adding a bunch of new states, and also the search itself. Only applies to inferences
3. The time spent adding states to the automaton is expensive. This is because a lot of time is spent looking for identical states to new states.

... I guess we'd better find out which it is!

[DavePearce]

A few things. Firstly, a large amount of time is spent in the method Automaton.rewrite(). There are also a reasonable number of unsuccessful applications of rewrite() (more than double the number of successful ones).

NOTE: the Automaton.rewrite() method calls minimise() ... ?

[DavePearce]

UPDATE: commenting out minimise() from Automaton.rewrite() has a profound effect on performance. However, at the same time, it actually doesn't work properly anymore :(

UPDATE: The version of Automaton using in v0.3.36 does appear to call minimise() and, indeed, this call appears to have been there for a very long time.

[DavePearce]

Right, so here is the minimal test case which illustrates why minimisation is necessary after rewriting:

G = { 1->2, 3->4 }
Rewrite 2 => 4

In this case, we now need to merge 1 with 3. Some obvious thoughts:

1. Only parents of both nodes are candidates for minimisation. Unsure in the presence of cycles though?
2. Targets with no parents (i.e. fresh nodes) never require minimisation.
3. Parents need to be otherwise identical. As soon as we encounter a parent which is somehow different, we can stop.

I guess this leaves open a few questions as to how best to proceed.

[DavePearce]

What we really want is an efficient incremental minimisation algorithm. Some notes:

1. Parent Pointers. This will require knowledge of the state parents to work efficiently.

2. Lock-step parent traversal. After a rewrite it will traverse the parents of the original and target states in lockstep. All non-identical pairs are eliminated immediately, and the traversal continues until no further pairs remain to be explored.

We could simulate (1) in order to test whether or not it works.