diff --git a/verify/goobj_link_atomic_test.go b/verify/goobj_link_atomic_test.go new file mode 100644 index 0000000..b838d21 --- /dev/null +++ b/verify/goobj_link_atomic_test.go @@ -0,0 +1,60 @@ +// Copyright (c) 2026 Petr Balvín (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) + }) +} diff --git a/verify/testdata/linkatomic_arm64.s b/verify/testdata/linkatomic_arm64.s new file mode 100644 index 0000000..88a2dfe --- /dev/null +++ b/verify/testdata/linkatomic_arm64.s @@ -0,0 +1,59 @@ +// Copyright (c) 2026 Petr Balvín (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