Skip to content

Conversation

@fabiomadge
Copy link
Collaborator

@fabiomadge fabiomadge commented Aug 31, 2025

(new description by @robin-aws who has taken over the PR :)

Refactors GoNativeArray, the Go implementation of the dafnyRuntime.dfy NativeArray implementation, to be a wrapper around the existing Array interface instead of just a []interface{} array. This allows sequences to also use the existing optimized implementations of Array that wrap more specific array types for bytes, chars, and CodePoints.

This was relatively straightforward but also involved adding a few more methods to the Array interface that weren't necessary to support Dafny array operations: arrayGetRange1, arraySetRange1, arrayCopy and arrayEqualUpTo.

@fabiomadge fabiomadge marked this pull request as ready for review August 31, 2025 04:44
Copy link
Member

@robin-aws robin-aws left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks like a good and well-formed optimization to me.

In case you weren't already aware, we already have similar specializations for the implementations of Dafny arrays in this runtime: https://github.com/dafny-lang/dafny/blob/master/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny.go#L1063. The Array interface and the dafnyRuntime.dfy changes went in at the same time and as a result the latter doesn't use the former abstraction even though it should - that is, the NativeArray and Array interfaces should actually be one combined interface. Since this version is working and a significant improvement I'm definitely cool with it, but I think we should merge the types before going any further down this path.

I don't have high confidence existing tests provide quite enough coverage, given you're making a sequence of bytes a separate case. I'm not even sure it's possible to execute the // Generic fallback from Dafny code in fact. I'd strongly recommend a few extra unit tests as well. You can add more to dafny_test.go in both copies of the runtime.

Comment on lines 849 to 851
contents := make([]interface{}, other.Length())
for i := uint32(0); i < other.Length(); i++ {
contents[i] = other.Select(i)
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think we'd better implement this using copy as in the original, just with two different versions. Otherwise the loop will be a performance regression over the original.

Comment on lines 869 to 871
for j := uint32(0); j < other.Length(); j++ {
array.contents[i+j] = other.Select(j)
}
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Same as above.

@robin-aws robin-aws changed the title feat: Stop boxing byte sequences in Go feat: Stop boxing byte/char/CodePoint sequences in Go Sep 4, 2025
@robin-aws robin-aws closed this Sep 4, 2025
@robin-aws robin-aws reopened this Sep 4, 2025
@robin-aws robin-aws closed this Sep 4, 2025
@robin-aws robin-aws reopened this Sep 5, 2025
@robin-aws robin-aws dismissed their stale review September 5, 2025 00:35

Addressed my own feedback and took over the PR while Fabio is out

@robin-aws robin-aws merged commit 22cbb20 into dafny-lang:master Sep 5, 2025
45 of 47 checks passed
robin-aws added a commit that referenced this pull request Sep 10, 2025
#6361)

### 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 new `Array`s created to hold the result are
also optimized for those types. This required modifying the
`Sequence<T>` implementation to expose a `PrototypeArray()` to indicate
the array type at runtime. The overall solution mirrors the solution in
`DafnyRuntimeJava` quite 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 the `--quick` scenario (a payload of 50 MB), the peak memory usage
before was 5822mb, and after the optimization was 595mb. The average
latency also improved from 3652 ms to 2047 ms.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants