feat: Avoid boxing primitives in Go in sequence concatenations as well #6361
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
robin-aws
changed the title
robin-aws
added a commit
that referenced
this pull request
Oct 20, 2025
### What was changed?
There are two issues causing excessive memory usage when using Seq in
Dafny Go:
1. Dafny Go compiler uses an empty sequence whenever declaring a new
variable. It doesn't use the specific type for sequence, but rather an
`arrayStruct` which uses `interface{}` as the underlying type. While the
[Boxing Fix](#6361) addressed
the issue when converting from native Go types to dafny Go types (and
vice versa), it didn't fix the use of arrayStruct /
[EmptySeq](https://github.com/dafny-lang/DafnyRuntimeGo/blob/38e14aaf73eff74913a994ee80fd49edf5161c17/v4/dafny/dafny.go#L517)
in the compiler.
2. This issue gets compounded when using ConcatSequence for storing byte
sequences. The
[ToByteArray](https://github.com/dafny-lang/DafnyRuntimeGo/blob/38e14aaf73eff74913a994ee80fd49edf5161c17/v4/dafny/dafny.go#L710-L731)
method for concat seq delegates to ToArray which then uses a Vector to
flatten everything into arrayStruct, causing the same issue which was
fixed by the Boxing Fix. But since the ConcatSequence also has to use
ArraySequence as the final underlying type, delegating it to the
ToByteArray recursively ends up calling the optimized ToByteArrray for
ArraySequence, improving the performance from using 800MB for 50MB
sequence to ~100MB.
This PR fixes issue 2 since fixing 2 improves memory numbers AND 3x
boost in cpu efficiency / latency numbers.
NOTE: The numbers can be further optimized by optimizing the compiler to
use specific sequence instead of arrayStruct (Issue 1) but that might be
more involved changed. A PoC compiler fix shows marginal better memory
efficiency than the fix in this PR (which makes sense since recursive
call is expensive memory wise) but worse latency / CPU numbers. A full
fix might bring the CPU numbers in line as well but it's out of scope
for this PR.
---------
Co-authored-by: Shubham Chaturvedi <[email protected]>
Co-authored-by: Robin Salkeld <[email protected]>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
What was changed?
Continuing from #6353, this change ensures the same optimization to avoid boxing bytes, Chars and CodePoints in sequences is also used in the concatenation optimization implemented in
dafnyRuntime.dfy. In particular, it ensures the newArrays created to hold the result are also optimized for those types. This required modifying theSequence<T>implementation to expose aPrototypeArray()to indicate the array type at runtime. The overall solution mirrors the solution inDafnyRuntimeJavaquite closely.How has this been tested?
Existing tests. Performance improvement was measured using https://github.com/aws/aws-encryption-sdk/tree/mainline/esdk-performance-testing/benchmarks/go. On a payload of 100 MB, the peak memory usage before was 5822 MB, and after the optimization was 595 MB. The average latency also improved from 3652 ms to 2047 ms.
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.