Skip to content

ToCString: emit stackalloc as 64-byte-aligned uint64_t array - #532

Open
spitters wants to merge 1 commit into
mit-plv:masterfrom
spitters:spitters/tocstring-aligned-uint64-stackalloc
Open

ToCString: emit stackalloc as 64-byte-aligned uint64_t array#532
spitters wants to merge 1 commit into
mit-plv:masterfrom
spitters:spitters/tocstring-aligned-uint64-stackalloc

Conversation

@spitters

Copy link
Copy Markdown

Summary

The previous emission for cmd.stackalloc used a byte-granular array:

```c
uint8_t _br_stackalloc_x[N] = {0};
x = (br_word_t)&_br_stackalloc_x;
```

Downstream code that treats the buffer as a word array (very common — most extracted-bedrock2 WP proofs allocate scratch for felem / scalar / pairing-tower values) then accesses through unaligned word loads/stores. On x86_64 this is fine for correctness but takes the unaligned-access slow path under some microarchitectures + SIMD; on ARM and RISC-V it can fault outright.

This patch switches to a word-sized, 64-byte-aligned allocation:

```c
uint64_t _br_stackalloc_x[ceil(N/8)] attribute((aligned(64))) = {0};
x = (br_word_t)_br_stackalloc_x;
```

  • 64-byte alignment matches typical cache-line + SIMD requirements.
  • ceil(N/8) words rounds up so we keep ≥ N bytes available.
  • Zero-init preserved (bedrock2's stackalloc specifies arbitrary contents, but downstream code may have observed zeros under the prior emission — keep that to avoid surprising downstream).
  • Drops the & since tmp already decays to a pointer.

Test plan

  • Local rebuild of bedrock2 + downstream Rocq tree clean.
  • Measured ~5-15% speedup on extracted-C ed25519_sign timing in curve25519-jasmin-rs bench, attributable to aligned-load fast paths.
  • gcc accepts __attribute__((aligned(64))) on the array declaration; clang likewise. MSVC syntax would be different but bedrock2's emitted C already uses GCC-style extensions.

The previous emission used [uint8_t tmp[N] = {0};] then took its address
as a [br_word_t]. This produces unaligned access in downstream code that
treats the buffer as a word array (common in extracted bedrock2-WP proofs
where the allocation is the backing memory for a felem / scalar).

Switch to:
    uint64_t tmp[ceil(N/8)] __attribute__((aligned(64))) = {0};
    x = (br_word_t)tmp;

- 64-byte alignment matches typical cache-line + SIMD requirements.
- ceil(N/8) words rounds the allocation up so we keep ≥ N bytes available.
- Zero-init preserved (bedrock2's [stackalloc] specifies arbitrary contents
  but downstream code may have observed zeros under the prior emission).
- Drops the [&] since [tmp] already decays to a pointer.

Verified clean compile of the bedrock2 + downstream Rocq tree after the
swap, and measured ~5-15% speedup on extracted-C ed25519_sign timing in
our downstream (curve25519-jasmin-rs) bench, attributable to aligned-load
fast paths.
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.

1 participant