Compilation optimization idea: allocate varargs-style trailing sequence argument on the stack #2749
Labels
kind: enhancement
Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
part: runtime
Happens in Dafny's runtime (Add a `lang` tag if relevant)
Writing down some thoughts as I push this idea out of scope for #2390, to come back to later.
So far I've been able to implement the
seq<T>
type in native Dafny code, including optimized concatenation and slicing, based on a native implementation of a single-dimensionalNativeArray<T>
trait. It is very tempting to use this same technique to implement multi-dimensional arrays on top ofNativeArray<T>
as well, something like the following:This is appealing for the same reasons as implementing
seq<T>
in Dafny: the added assurance of verification, saving implementation effort per target language, and ensuring consistent runtime performance across backends. The last point is particularly applicable here: some backends allocate nested arrays instead of a single flat array, which is equally correct and simpler logic, but incurs a lot more allocations and memory traversals.The reason we should NOT do this yet is that allocating the
indices
sequence value for every access will be relatively expensive with the current set of backends. The manual implementations of multi-dimensional arrays in Go avoids this by using varargs, so the equivalentRead
method inDafnyRuntime.go
accepts aixs ...int
parameter.The best solution I can see is to find opportunities to compile a trailing sequence parameter to a varargs parameter where supported, and optimize calls to such methods that pass a sequence display literal. Another alternative is to generate multiple copies of such methods for low arities and unroll loops, which is essentially what the Java compiler does by generating multiple
Array*<T>
classes.The text was updated successfully, but these errors were encountered: