test(verify): prove the arm64 lse atomics through the link-parity kernel
Assisted-by: GLM 5.3 Flash
This commit is contained in:
1 parent
8e3b7f1caa
commit
d1030a1788
2 files changed
+119
No files matched your search
@@ -0,0 +1,60 @@
|
||||
// Copyright (c) 2026 Petr Balvín <opensource@petrbalvin.org> (https://petrbalvin.org)
|
||||
// SPDX-License-Identifier: BSD-3-Clause
|
||||
|
||||
package verify
|
||||
|
||||
import (
|
||||
"os"
|
||||
"os/exec"
|
||||
"testing"
|
||||
)
|
||||
|
||||
// goobjAtomicMainSrc is the Go side of the LSE regression. The kernel
|
||||
// drives a counter with LDADDALD and mixes the accumulated total; main
|
||||
// derives the same value in Go and panics on any divergence before
|
||||
// printing the deterministic line the baseline and the gasm-linked
|
||||
// binaries must agree on.
|
||||
const goobjAtomicMainSrc = `package main
|
||||
|
||||
func caller(p *int64, addv int64, times int64) int64
|
||||
|
||||
func main() {
|
||||
addv, times := int64(3), int64(5)
|
||||
v := int64(0)
|
||||
got := caller(&v, addv, times)
|
||||
oldsum, cur := int64(0), int64(0)
|
||||
for i := int64(0); i < times; i++ {
|
||||
oldsum += cur
|
||||
cur += addv
|
||||
}
|
||||
k := uint64(0x9e3779b97f4a7c15)
|
||||
want := int64(uint64(oldsum+cur) * k)
|
||||
if got != want {
|
||||
panic("atomic")
|
||||
}
|
||||
println("ok", caller(&v, addv, times))
|
||||
}
|
||||
`
|
||||
|
||||
// TestGOOBJLinkAtomicKernel proves the arm64 LSE atomic families are proven
|
||||
// end to end: the kernel assembles by gasm into a GOOBJ object, substitutes
|
||||
// byte-wise into a real go build archive, relinks with cmd/link and the
|
||||
// linked binary computes the same atomic total as the toolchain-built one
|
||||
// under qemu-user, with the documented degradation on emulators without
|
||||
// LSE (the baseline run fails first and the claim drops to link-only).
|
||||
func TestGOOBJLinkAtomicKernel(t *testing.T) {
|
||||
if testing.Short() {
|
||||
t.Skip("builds the gasm binary and links Go programs")
|
||||
}
|
||||
if os.Getenv("GASM_LINK_PARITY") == "" {
|
||||
t.Skip("deliberate verification: set GASM_LINK_PARITY=1 (just link-parity)")
|
||||
}
|
||||
goBin, err := exec.LookPath("go")
|
||||
if err != nil {
|
||||
t.Skip("no Go toolchain available")
|
||||
}
|
||||
gasmBin := buildLinkParityGasm(t, goBin)
|
||||
t.Run("arm64", func(t *testing.T) {
|
||||
goobjLinkKernel(t, goBin, gasmBin, "arm64", "linkatomic_arm64.s", goobjAtomicMainSrc)
|
||||
})
|
||||
}
|
||||
Vendored
+59
@@ -0,0 +1,59 @@
|
||||
// Copyright (c) 2026 Petr Balvín <opensource@petrbalvin.org> (https://petrbalvin.org)
|
||||
// SPDX-License-Identifier: BSD-3-Clause
|
||||
|
||||
#include "textflag.h"
|
||||
|
||||
// The link-regression kernel for the arm64 LSE atomics: atomicsum adds a
|
||||
// value to a counter with LDADDALD in a loop, accumulating every old value
|
||||
// the atomic returns, and finishes with the counter's final contents, so
|
||||
// the result is addv times times times times plus one under any schedule.
|
||||
// caller passes the pointer and the two scalars to atomicsum and mixes the
|
||||
// total through the intra-file mixa call over the ABI0 stack slots. mixa
|
||||
// multiplies by the odd golden-ratio constant, the same arithmetic the Go
|
||||
// side of the regression mirrors bit for bit. The run claim follows the
|
||||
// documented degradation: a qemu-user without LSE fails the baseline and
|
||||
// the claim degrades to link-only.
|
||||
|
||||
// func atomicsum(p *int64, addv int64, times int64) int64
|
||||
TEXT ·atomicsum(SB), NOSPLIT, $0-32
|
||||
MOVD p+0(FP), R3
|
||||
MOVD addv+8(FP), R4
|
||||
MOVD times+16(FP), R5
|
||||
MOVD $0, R6
|
||||
|
||||
loop:
|
||||
CBZ R5, done
|
||||
LDADDALD R4, (R3), R7
|
||||
ADD R7, R6, R6
|
||||
SUB $1, R5, R5
|
||||
JMP loop
|
||||
|
||||
done:
|
||||
MOVD (R3), R8
|
||||
ADD R8, R6, R6
|
||||
MOVD R6, ret+24(FP)
|
||||
RET
|
||||
|
||||
// func mixa(x int64) int64
|
||||
TEXT ·mixa(SB), NOSPLIT, $0-16
|
||||
MOVD x+0(FP), R0
|
||||
MOVD $0x9e3779b97f4a7c15, R1
|
||||
MUL R1, R0, R0
|
||||
MOVD R0, ret+8(FP)
|
||||
RET
|
||||
|
||||
// func caller(p *int64, addv int64, times int64) int64
|
||||
TEXT ·caller(SB), NOSPLIT, $32-32
|
||||
MOVD p+0(FP), R3
|
||||
MOVD addv+8(FP), R4
|
||||
MOVD times+16(FP), R5
|
||||
MOVD R3, 8(RSP)
|
||||
MOVD R4, 16(RSP)
|
||||
MOVD R5, 24(RSP)
|
||||
BL ·atomicsum(SB)
|
||||
MOVD 32(RSP), R0
|
||||
MOVD R0, 8(RSP)
|
||||
BL ·mixa(SB)
|
||||
MOVD 16(RSP), R0
|
||||
MOVD R0, ret+24(FP)
|
||||
RET
|
||||
Reference in new issue
Block a user