Improving execution time and memory consumption of invariant computation and assertion verification

[Maxime-Derri]

In this issue, I discuss possible ways to enhance the performance of invariant computation and assertion verification.

1. In recent versions, PREVAIL has been updated to verify assertions during the computation of invariants. In previous versions, PREVAIL had to store all invariants for the final step, where assertions were checked. This approach was highly memory-consuming. Now, pre- and post-invariants can be freed once their corresponding assertions have been verified. Two cases must be considered:
   1. Label: a label that is at the top level of the WTO, i.e. not part of any Bourdoncle component, reaches a fixpoint once its pre- and post-invariants have been computed. At that point, assertions can be checked immediately, and the invariants can be freed.
   2. Bourdoncle component: A Bourdoncle component reaches a fixpoint once all its labels and nested components have reached a fixpoint. However, if a Bourdoncle component is nested inside another, its invariants may still be updated until The Bourdoncle component that contains it also reaches a fixpoint. Starting from the top level of the WTO, a Bourdoncle component reaches a fixpoint once all its elements have reached a fixpoint. At that time, assertions can be checked. Let's consider two strategies: a. Free invariants just after assertions have been checked. Checks are performed once a fixpoint is reached for the current label or Bourdoncle component. b. While computing invariants, free the pre- and post-invariants of a label once the pre-invariants of its children have been updated. The invariants of the head of Bourdoncle components might need to be retained to detect when a fixpoint is reached. When a Bourdoncle component reaches a fixpoint, one final iteration could be performed to recompute invariants, verify assertions, and (re)free invariants. This approach requires one additional iteration but is memory efficient.
2. It may not be necessary to store post-invariants. When assertions are checked, the pre-invariants are typically copied. Therefore, the post-invariant of the current label can be directly used to compute the pre-invariants of its children. In other words, at each label is performed a part of join_all_prevs for its children:
   1. If the current label has one child and that child has one parent, current post-invariant = next pre-invariant.
   2. If a child has multiple parents, its pre-invariant can be updated by its parents by joining its pre-invariant with the post-invariant of the parent being processed.
   3. If the current label has n children, the post-invariant may need to be copied n−1 times to update the pre-invariants of the first n−1 children (std::move is used in the join operator). The last child can be updated directly using the post-invariant.

By reducing memory usage and minimizing the number of invariant copies, large programs can be verified more efficiently.

[elazarg]

Interesting!

It might be implementable by encoding invarniant ownership using shared pointers; unverified assertions own invariants that affect them. But note that invariants are also there to be printed, and it's possible that a second pass (e.g. lock-unlock check) would need them.

Related idea is https://github.com/vbpf/prevail/pull/266 - symbolically propagate assertions backwards. IIRC it greatly improved performance.