Iterating over sets in compiled code is slow

[robin-aws]

This is part of the motivation for the foreach loops and sequence comprehensions RFC, but since the issue is a bit subtle and largely orthogonal, I'm outlining it here separately. The goal here is to explain why this issue is not feasible to fix just by improving the efficiency of the compiler or runtimes, but is actually a more fundamental limitation on how the features of the language interact.

As explained in the reference manual, it is easy in a method context to iterate over the values in a set:

method PrintSet(s: set<int>) {
  var ss := s;
  while ss != {}
  {
    var i: int :| i in ss;
    ss := ss - {i};
    print i, "\n";
  }
}

With the current runtime implementation of sets, the expression ss - {i} takes O(|ss|) time to evaluate, since it creates an entirely fresh copy of the set with one element removed. This means the whole loop executes in quadratic time.

As @cpitclaudel correctly pointed out in the RFC, more efficient implementations of immutable sets exist that share subvalues and can implement removal in O(log |ss|) time, which would bring the runtime of the loop down to O(|s| log |s|). This may be a worthwhile optimization, although the downside is depending on such implementations in each target language, or (preferably) providing our own implementation in Dafny user code. Even then, log-linear time is disappointing and surprising for what should be a simple iteration over a collection.

The situation is much worse when trying to iterate over a set in an expression, though. We can define a ghost function that creates a sequence from a set:

function SetToSequence<A>(s: set<A>): seq<A>
  ensures var q := SetToSequence(s);
    forall i :: 0 <= i < |q| ==> q[i] in s
{
  if s == {} then [] else
    var x :| x in s;
    [x] + SetToSequence(s - {x})
}

Changing this to a function method, however, generates the error message "to be compilable, the value of a let-such-that expression must be uniquely determined." This example is borrowed from this manuscript, which explains that the let-such-that expression var x :| x in s; ... must be deterministic, and hence needs extra constraints to specify a unique value. The final compilable version (with comments removed from the lemma as it isn't the focus here) ends up being:

function method SetToSequence(s: set<int>): seq<int>
  ensures var q := SetToSequence(s);
    forall i :: 0 <= i < |q| ==> q[i] in s
{
  if s == {} then [] else
    ThereIsAMinimum(s);
    var x :| x in s && forall y :: y in s ==> x <= y;
    [x] + SetToSequence(s - {x})
}

lemma ThereIsAMinimum(s: set<int>)
  requires s != {}
  ensures exists x :: x in s && forall y :: y in s ==> x <= y
{
  var x :| x in s;
  if s == {x} {
  } else {
    var s' := s - {x};
    assert s == s' + {x};
    ThereIsAMinimum(s');
  }
}

The extra conjunct on the let-such-that expression is very expensive in this case: the compiled implementation of this statement is equivalent to:

int x = 0;
foreach (int _assign_such_that_1 in (s).Elements) {
  x = _assign_such_that_1;
  if ((s).Contains(x) && (s).Elements.All(y => x < y)) {
    goto after__ASSIGN_SUCH_THAT_1;
  }
}
throw new System.Exception("assign-such-that search produced no value (line 17)");
after__ASSIGN_SUCH_THAT_1: ;
  // x is now assigned, continue with the program...

The call to Elements.All is a simplification of how the forall y :: y in s ==> x <= y expression is compiled, but is an equivalent search through all elements. Because selecting the minimum element is a naive, literal execution of the specification, it takes quadratic time, and so SetToSequence(s) evaluates in O(|s|³) time! It is difficult to imagine a practical compilation optimization that would recognize this pattern and produce better code, which would need to sort all the elements at once, possibly via a temporary ordered data structure such as a tree set, instead of attempting to pick each successive minimum one at a time.

Edit: @cpitclaudel provided a solution involving function by method which brings the runtime down to O(|s|²) with the current runtimes, which does improve the situation somewhat!

The features proposed in the RFC are one possible solution to these challenges, as they express ordering of results directly in their semantics. An expression like seq i: int | i in s would be interpreted as "the ordered domain of integers, restricted to those in the set s", which would be implemented at runtime by extracting and sorting the elements of s. This is not the only possible solution, but hopefully it is clear that any solution is better off proposing how to increase the expressivity of the Dafny language, rather than focussing on better compilation strategies.

[cpitclaudel]

hopefully it is clear that any solution is better off proposing how to increase the expressivity of the Dafny language, rather than focussing on better compilation strategies.

I think the situation isn't that dire :)

more efficient implementations of immutable sets exist that … would bring the runtime of the loop down to O(|s| log |s|). This may be a worthwhile optimization,

Can't we do O(|s|) amortized, rather than O(|s| lg |s|)? We'd need to be careful with the implementation, but I suspect it would be essentially isomorphic to the type or iterators over the set, and hence not super complicated (see below).

although the downside is depending on such implementations in each target language

But we already do for our current implementation of sets, so that's not a downside of that approach.

Coming back to the question of O(|s|) vs O(|s| lg |s|): the current proposal covers only built-in types, but how would user collections plug into that mechanism? My expectation would be that they do it through their own "iterator" type, which would support an iter method to create an iterator state from a collection, and a next method, which would take an iterator and would return a value (along with a new iterator state).

If that's what we're going to do in the long run, then we can do the same thing with sets. In fact, to make this concrete, consider building general iterators rather than plain sequence comprehensions. Suppose further that you're using an efficient set (because, O(|s|) for set removal is a bug that we have to fix in any case); for simplicity, let's say it's a binary search tree. How do you implement an iterator on that set? If you're doing it directly in C# you can write a recursive function that yields nodes in the order that they are traversed, which is very convenient; when you do that, though, under the hood the compiler will generate a stack machine whose state type is essentially the type of zippers over your datastructure (a location in the original datastructure, possibly with the difference that the compiler-generated state machine won't keep track of visited elements, whereas a zipper would).

I suspect this is more or less the way you would implement a generic iterator over tree-like datastructures in Dafny. In the binary search tree example, you have O(lg |s|) for iter, then O(1) amortized for next, and all of this is already expressible in Dafny (though not with the current set type, because we have no notion of iterators).

If we want to make the current iteration pattern as efficient as possible, then we could make any selection (x :| x in s) and set removal (s := x - {x}) construct a zipper, yielding a total cost of O(s) for iteration. At least, this is for methods.

This example is borrowed from this manuscript, which explains that the let-such-that expression var x :| x in s; ... must be deterministic, and hence needs extra constraints to specify a unique value.

Was this example written pre function-by-method? Now that we have that it's relatively easy to attach use a method and avoid the O(|s|³) (the implementation that I posted to the other thread does that).

[robin-aws]

hopefully it is clear that any solution is better off proposing how to increase the expressivity of the Dafny language, rather than focussing on better compilation strategies.

I think the situation isn't that dire :)

Oh I wouldn't even call the worst possible interpretation of this situation "dire", thankfully :)

Can't we do O(|s|) amortized, rather than O(|s| lg |s|)? We'd need to be careful with the implementation, but I suspect it would be essentially isomorphic to the type or iterators over the set, and hence not super complicated (see below).

I'm sure it's technically possible to choose a compilation/runtime strategy that makes the loop as written run in O(n) time. The extreme case would be using linked lists to represent set<T> values, in which case removing the first element takes O(1) time. Then of course x in s takes O(n) time, which is definitely not acceptable in general, so this alone wouldn't be a good choice for arbitrary Dafny code.

If I'm following the rest of your description correctly, you're imagining that we could have the equivalent of an AfterIteratorSet<T>(s, iter) implementation of the general Set<T> interface. If s was an instance of that case in the expresion s - {x}, and x was the next element produced by the iterator, then the result would be AfterIteratorSet<T>(s, iter) with the iterator advanced by one. Assuming that we can still test membership in O(log n) time by not descending to the left of the stack of nodes in the iterator, I agree this MIGHT work out. :) It still worries me that we'd be creating an optimization for a very particular pattern of using set operations, which would be easy for users to break with seemingly innocuous code changes.

Re: your point about wanting to have a general iterator concept, I completely agree! I'm really just proposing adding higher-level concepts that can be defined in terms of iterators first, because they will be useful for Dafny users by themselves on builtin datatypes right away, and provide much more succinct and easier-to-verify concepts than working with raw iterators. After all, it's generally a lot simpler to write a foreach loop than it is to create, advance and test an iterator directly. I absolutely intend to allow the c in an expression like seq x <- c :: x + 1 to be of a user-defined "enumerable" type in the future, meaning c provides a way to obtain an enumerator for the values it contains. My hope is just that enumerators will be a more advanced concept for contributors like us to use when implementing builtin collections in Dafny, or providing Dafny libraries with other enumerable datatypes.

This example is borrowed from this manuscript, which explains that the let-such-that expression var x :| x in s; ... must be deterministic, and hence needs extra constraints to specify a unique value.

Was this example written pre function-by-method? Now that we have that it's relatively easy to attach use a method and avoid the O(|s|³) (the implementation that I posted to the other thread does that).

That's an excellent point, and I hadn't fully read through your implementation until now (dafny-lang/rfcs#9 (comment)). That's another really nice feature of function-by-methods: not only does it enable more efficient implementations, it also allows you to use local non-determinism (via :| statements) when implementing a deterministic function! That does mean we can at least reduce the compiled expression case to O(n²) with the current simple runtime representation, or at worst O(n log n) with a better implementation. It might be worth adding your version to dafny-lang/libraries as I don't expect many Dafny users to immediately identify the cubic runtime of the original version, much less figure out your alternative.

[cpitclaudel]

My hope is just that enumerators will be a more advanced concept for contributors like us to use when implementing builtin collections in Dafny, or providing Dafny libraries with other enumerable datatypes.

Right. I don't have strong opinions on the high-level interface :)

It still worries me that we'd be creating an optimization for a very particular pattern of using set operations

That, and it sounds like a lot of work, too ^^

Assuming that we can still test membership in O(log n) time by not descending to the left of the stack of nodes in the iterator, I agree this MIGHT work out. :)

I suspect that we'll have to do something like that eventually (once/when we implement iterators). IOW the message above isn't anything about what interface we expose to users — more that whatever we have to do to support iterators down the line will require us to implement something that also gives fast iteration on sets, without having to make Dafny the language more expressive.

It might be worth adding your version to dafny-lang/libraries as I don't expect many Dafny users to immediately identify the cubic runtime of the original version, much less figure out your alternative.

👍, will do!

or at worst O(n log n) with a better implementation.

And even better: that's asymptotically optimal in this case, since we're actually sorting the output :)

[robin-aws]

My hope is just that enumerators will be a more advanced concept for contributors like us to use when implementing builtin collections in Dafny, or providing Dafny libraries with other enumerable datatypes.

Right. I don't have strong opinions on the high-level interface :)

Cool, I think we're on the same page. The features I'm proposing in the RFC will be able to use the existing target language datatype support for iterators as is, as they are already used in translating various uses of BoundedPools. I see you're thinking about how to provide the same functionality if and when we switch to pure Dafny implementations of types like set<T>, so we're nicely orthogonal!

or at worst O(n log n) with a better implementation.

And even better: that's asymptotically optimal in this case, since we're actually sorting the output :)

Right! :) I've added an edit since your observation changes the story a little, and thanks again!

[keyboardDrummer]

This example is borrowed from this manuscript, which explains that the let-such-that expression var x :| x in s; ... must be deterministic

I imagine that it only needs to be deterministic within a single program execution. Would an ordering based on hash codes, based on pointer values, that changes across executions, be okay?