Significant slow-downs compared to fully dynamic approach at run time for static/more precise specs

[jennalwise]

After analyzing the new data after modifying our partial specification generating strategy, we are seeing dramatic slow-downs in the run-time performance of our tool compared to the fully dynamic approach. The below figures illustrate the problem:

In the above figures, we are seeing for all of the maximum plots (worst paths for gradual verification) and even for one of the median paths for BST large slow-downs (red spikes) at about 90% static completion, which is often where there are more mixtures of precise and imprecise specifications and continued increases of precise specifications. General data from Table 2 in our paper confirms the visual data, where there are extreme outliers in which gradual verification was 337-13131% (Table 2, Column 5) slower than dynamic verification. The table is shown below for reference.

In the plots below, we see that the most dramatic impacts on performance for both increasing and decreasing run-time overhead comes from removing ? from formulas---that is, going from an imprecise formula to a precise one. We see that dramatic increases in run-time overhead particularly comes from removing ? in predicate bodies and dramatic decreases comes from removing ? from preconditions. Therefore, I speculate that the slow-down problem is related to passing permissions at boundaries. For example, at method calls we look to see if the precondition is precise or imprecise. If it is precise (no ? in the formula or in containing predicates), then permissions are dynamically recreated from the precondition and passed to the callee. For recursive predicates this is expensive. This would not account for spikes above the fully dynamic approach, since it does the same thing (or should) for preconditions at method calls. However, it will account for some of the slow-downs we see in the plots below (for postconditions, preconditions, and pred bodies). Now, for postconditions the dynamic approach always returns all the permissions the callee owns (or should), so whether or not a formula is imprecise or precise has no run-time impact here. In contrast, Gradual C0 recreates permissions to pass around for precise formulas in postconditions as well. This has the same run-time overhead as passing permissions for preconditions, which should be very expensive for recursive predicates. This is likely the cause of the significant slow-downs experienced by Gradual C0 that the fully dynamic approach does not experience.

The goal of this issue is to figure out why Gradual C0 is performing significantly worse than the fully dynamic approach in the aforementioned cases. I've provided my speculation on the problem above, feel free to start there!

[jennalwise]

Notes on the solution that I proposed:

Cases for passing permissions at method calls:

• Imprecise precondition, imprecise post --> all perms passed to callee, all perms returned to caller, permission tracking in callee
• Imprecise pre, precise post --> all perms passed to callee, all perms returned to caller, permission tracking in callee
• Precise pre, imprecise post --> perms passed based on pre, all perms returned to caller, permission tracking in callee
• Precise pre, precise post, imprecision in callee/not fully statically verified callee --> perms passed based on pre, perms returned based on post, permission tracking in callee
• Precise pre, precise post, fully statically verified callee --> no perms passed or returned, no permission tracking in callee, current set of perms in caller unioned with post perms? for continuation in the caller; how is this case actually resolved in the caller?

When recursive predicates appear in postconditions it is very inefficient to recreate perms from the postcondition as our strategy does in the indicated cases. It is also inefficient to do this for preconditions, but we have to pass perm based on the pre to ensure soundness. In contrast, as long as we rely on the precondition in precise cases it is sound to not rely on the postcondition to return perms---we can always just return all the perms the callee has when it finishes execution and this is sound. So, ideally, the best strategy (in my opinion) is to wherever permission tracking in the callee is applied, the post condition should not be used to pass perms back to the caller but rather all the perms in the callee should be returned---this is sound, significantly more efficient when recursive preds are in the post, and more complete. In the fully static case, the solution can remain the same as it is simple and as efficient as the fully dynamic approach. A more complicated, but even more efficient approach in this case would be to:

• if the precondition does not contain a recursive predicate but the postcondition does --> pass perms based on pre, return all perms to caller, implement permission tracking in callee
• if the post does not contain recursive predicates, but the pre does --> keep the current strat
• if neither the pre or post contain recursive preds --> keep current strat
• if both contain recursive preds -> keep current strat

Can maybe go even further to be more efficient if we start to look at whether the predicate is created in the callee or passed to the callee for modification.

[jennalwise]

The implementation fix for the solution outlined in my previous comment should be located in Checker.scala in the frontend in the following case starting at line 248:

            case PreciseCallStyle => {
              // Always pass the instance counter
              call.ir.arguments :+= instanceCounter

              // If we need to track precise permissons, add the code at the call site
              if (needsToTrackPrecisePerms) {
                // Convert precondition into calls to removeAcc
                val context = new CallSiteContext(call.ir, method)
                call.ir.insertBefore(
                  callee.precondition.toSeq.flatMap(
                    implementation.translate(
                      RemoveMode,
                      _,
                      getPrimaryOwnedFields,
                      context
                    )
                  )
                )

                // Convert postcondition into calls to addAcc
                call.ir.insertAfter(
                  callee.postcondition.toSeq.flatMap(
                    implementation.translate(
                      AddMode,
                      _,
                      getPrimaryOwnedFields,
                      context
                    )
                  )
                )
              }
            }

Instead of adding perms based on the postcondition in the if statement, all the perms in the callee should be returned to the caller.

[etanter]

• Imprecise pre, precise post --> all perms passed to callee, all perms returned to caller, permission tracking in callee

shouldn't this say "..., perms returned based on post, ..." ?

[etanter]

reading further it seems you are indeed suggesting to return all perms despite the post being precise. I think that even though it's sound, it's a kind of abstraction breach, don't you think? (a bit like returning an object at an abstract type but the client that receives it "sees it" at a concrete subtype)

[jennalwise]

I do agree that it is an abstraction breach and makes it harder to indicate to a user that the postcondition is too weak for their client code if they were specifying it themselves. However, doing this new strategy should in theory significantly improve run-time performance, so it is an interesting trade-off.

Also, the other case you pointed out is nuanced since the precondition is imprecise. Here, we have to be careful to return all of the permissions passed to the callee back to the caller in case they were supposed to be framed off by the precondition had it been precise and kept by the caller. If the postcondition is too weak (which is should be, since those perms would be kept by the caller), then returning based on the post would break the gradual guarantee. For permissions created by the callee, the postcondition would be okay to use---but would be inefficient.

Do you think it would be better to keep the original approach, discuss how the performance is not ideal due to trying to preserve the abstraction, but if we allow for abstraction breaches we can improve performance and show new data for that along side the current data in our POPL submission?