Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
32 commits
Select commit Hold shift + click to select a range
cbb1a07
the c-abi probe measures the target it verifies, and a capability is …
speak-agent Sep 20, 2026
0f870c6
the [c-abi.absent] parser gets its own function, and the docs index i…
speak-agent Sep 20, 2026
88dfb74
the [c-abi.absent] parser is an internal helper, in the plainest form…
speak-agent Sep 20, 2026
68bb737
docs/22: which of the two new keys an older engine ignores, and which…
speak-agent Sep 20, 2026
10fa191
the execution record: what the measurement settled, and the three def…
speak-agent Sep 20, 2026
9d337bd
the wave's sandbox verification, and the reading from each of its two…
speak-agent Sep 20, 2026
a4993b0
Merge remote-tracking branch 'origin/main' into cenv-probe-target-and…
speak-agent Sep 20, 2026
14b28ed
two defects found reviewing this branch: the wrong provider, and a na…
speak-agent Sep 20, 2026
9aa57be
the record: what this wave did not do, and the first two implementati…
speak-agent Sep 20, 2026
f0573e0
the resolved provider is matched by name, not by substring
speak-agent Sep 20, 2026
9cfa9ee
the wave's self-review: five defects, and the one place this landing …
speak-agent Sep 20, 2026
790b303
the design under-estimated L3, and the two sentences that cannot both…
speak-agent Sep 20, 2026
3eb6ea2
the absent-facility advice reaches both channels a failed build repor…
speak-agent Sep 20, 2026
9af26c6
the design points at the record of what landed and what did not
speak-agent Sep 20, 2026
71ee489
the two probe tests that never ran anywhere now run
speak-agent Sep 20, 2026
fec98c1
the #674 Path C design is marked superseded, with a pointer to what r…
speak-agent Sep 20, 2026
9fca8e7
the probe fix, read from the probe's own cache rather than from a log
speak-agent Sep 20, 2026
4f2d2d2
the refusal carries its code, because something reads it
speak-agent Sep 20, 2026
f7d0fbf
the refusal-token table gains the four it was missing
speak-agent Sep 20, 2026
061c3fa
the zh note is placed beside the token table, not in the page's own p…
speak-agent Sep 20, 2026
ba09a01
the end-to-end reading: one requirement, two implementations, two ans…
speak-agent Sep 20, 2026
3907cc0
the release notes name the reason token, as this file's own conventio…
speak-agent Sep 20, 2026
854b99d
the assembler asked PATH first, and every other tool in this engine d…
speak-agent Sep 20, 2026
9fd2f8a
the absence table is top-level, because the nested spelling refuses t…
speak-agent Sep 20, 2026
c2fbe08
the host-surface table was written from one sweep, and three were mis…
speak-agent Sep 20, 2026
5381db9
the self-review gains the two findings that neither the diff nor CI c…
speak-agent Sep 20, 2026
d4921f1
one predicate, named once, because both tables gate on it
speak-agent Sep 20, 2026
48973cf
the recorded readings are the ones the top-level table actually produces
speak-agent Sep 20, 2026
de49198
the note about a declared absence was missing a closing parenthesis
speak-agent Sep 20, 2026
4d1748a
the label under a missing interface read as the claim the refusal denies
speak-agent Sep 20, 2026
4b6252b
e2e 744 depended on the host having a C runtime, and on a key mcpp ig…
speak-agent Sep 20, 2026
42a8f8f
the reason-token table and the engine no longer agree by being read
speak-agent Sep 20, 2026
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
359 changes: 359 additions & 0 deletions .agents/docs/2026-09-19-issue-674-cenv-posix-preinclude-design.md

Large diffs are not rendered by default.

230 changes: 230 additions & 0 deletions .agents/docs/2026-09-20-cenv-interfaces-verify.sh
Original file line number Diff line number Diff line change
@@ -0,0 +1,230 @@
#!/usr/bin/env bash
# Ecosystem verification for the 2026.9.20.1 wave against the PUBLISHED mcpp
# and index, run inside a SubOS sandbox with CN mirrors for xlings and mcpp.
#
# B64=$(base64 -w0 .agents/docs/2026-09-20-cenv-interfaces-verify.sh)
# xlings subos new v920
# xlings subos use v920 --sandbox --cmd \
# "echo $B64 | base64 -d > /tmp/v.sh && MCPP_VERIFY_VERSION=2026.9.20.1 bash /tmp/v.sh"
#
# Run it once against the PREVIOUS release first
# (MCPP_VERIFY_VERSION=2026.9.18.3): every section marked CHANGE must fail there
# and pass here; every section marked GUARD must pass on both. A section that
# passes on both releases in a CHANGE section measured nothing.
#
# The sandbox's $HOME persists between runs of one SubOS, so each section clears
# its own directory. A section that cannot run says so and is listed again at
# the end, because a run that reports only failures cannot be told from one that
# examined nothing.
# TWO RUNS, AND THE READING FROM EACH (host dry run, 2026-09-20, against the
# genuine published archive of the older release rather than a local build):
#
# mcpp 2026.9.18.3 (published) fails=2
# B a requirement the implementation does not provide must be refused
# C an absence with an unknown shape must be refused
# mcpp 2026.9.20.1 fails=0
#
# ONE PASSING LEG IN EACH CHANGE SECTION IS THE EVIDENCE, NOT A HOLE. Both new
# tables are top-level, and an older engine IGNORES an unknown top-level table:
# so B's first leg (a graph that satisfies its requirements) and C's first leg
# (an absence with a known shape) build on both releases, and that is exactly
# the backward compatibility this wave claims. What distinguishes the releases
# is the REFUSAL in each: an older engine cannot refuse what it never read.
#
# An earlier revision of this file recorded three failures against 2026.9.17.1,
# one of them `[c-abi] has no member 'absent'`. That reading was taken while
# the absence table was nested inside `[c-abi]`, where an unrecognised member
# is a parse error and the whole manifest was refused. Moving the table to the
# top level is what turned that failure into the passing first leg above --
# see docs/22 and the design's §5.7.5.
set -u

VER="${MCPP_VERIFY_VERSION:?set MCPP_VERIFY_VERSION}"
STORE="${MCPP_VERIFY_BIN:-$HOME/.xlings/data/xpkgs/xim-x-mcpp/$VER/bin/mcpp}"

fails=0
skipped=""
fail() { printf 'ASSERT-FAIL: %s\n' "$1"; fails=$((fails + 1)); }
ok() { printf 'ok: %s\n' "$1"; }
section() { printf '\n== %s ==\n' "$1"; }
skip() { printf 'NOT RUN: %s\n' "$1"; skipped="$skipped
- $1"; }
unset XLINGS_ACTIVE_SUBOS

root="$HOME/verify-920"
rm -rf "$root"; mkdir -p "$root"

section "A. identity and mirror"
if [ ! -x "$STORE" ]; then
skip "mcpp $VER is not in the store at $STORE"
printf '\n-- summary --\nfails=%d\nnot run:%s\n' "$fails" "${skipped:- (none)}"
exit 1
fi
got="$("$STORE" --version 2>&1 | head -1)"
case "$got" in
*"$VER"*) ok "mcpp $VER from $STORE" ;;
*) fail "the binary at $STORE reports '$got'" ;;
esac
"$STORE" self config --mirror CN >/dev/null 2>&1 \
&& ok "mcpp mirror set to CN" || fail "mcpp self config --mirror CN"

# ── CHANGE 1. A package states which interfaces of the layer it requires ─────
#
# The engine knows no interface name: it compares two sets and refuses before
# anything is compiled. Both legs are here because only the second says the
# comparison happened -- a build that succeeds proves nothing about a check
# that never ran.
section "B. requires-interfaces is answered at resolution (CHANGE)"
b="$root/b"; rm -rf "$b"; mkdir -p "$b/impl/src" "$b/src"
printf 'int fake_kernel_marker(void){return 0;}\n' > "$b/impl/src/lib.c"
printf 'int main(void){return 0;}\n' > "$b/src/main.c"
cat > "$b/impl/mcpp.toml" <<'EOF'
[package]
name = "fakekernel"
version = "0.1.0"
provides = ["mcpp:kernel-abi=openkal"]

[targets.fakekernel]
kind = "lib"
sources = ["src/*.c"]

[kernel-abi]
provides-interfaces = ["openkal.abort", "openkal.stream", "openkal.memory"]
EOF
mk_root() { # $1 = requires-interfaces body
cat > "$b/mcpp.toml" <<EOF
[package]
name = "iface-probe"
version = "0.1.0"

[dependencies]
fakekernel = { path = "impl" }

[build]
allow_host_libs = true

[kernel-abi]
requires-interfaces = [$1]
EOF
}
mk_root '"openkal.stream"'
rm -rf "$b/target"
if (cd "$b" && "$STORE" build >/dev/null 2>&1); then
ok "a requirement the implementation provides builds"
else
fail "a requirement the implementation provides must build"
fi
mk_root '"openkal.stream", "openkal.net"'
rm -rf "$b/target"
out="$(cd "$b" && "$STORE" build 2>&1)"
if [ $? -eq 0 ]; then
fail "a requirement the implementation does not provide must be refused"
else
case "$out" in
*openkal.net*iface-probe*|*iface-probe*openkal.net*)
ok "the refusal names the interface and the package" ;;
*) fail "the refusal does not name both: $(printf '%s' "$out" | head -3 | tr '\n' ' ')" ;;
esac
if [ -d "$b/target" ] && find "$b/target" -name '*.o' -print -quit 2>/dev/null | grep -q .; then
fail "the refusal arrived after something was compiled"
else
ok "nothing was compiled before the refusal"
fi
fi

# ── CHANGE 2. A C library states what it does not supply ────────────────────
section "C. [c-abi-absent] is read, and a bad shape is refused (CHANGE)"
c="$root/c"; rm -rf "$c"; mkdir -p "$c/libc/src" "$c/src"
printf 'int fake_libc_marker(void){return 0;}\n' > "$c/libc/src/lib.c"
printf 'int main(void){return 0;}\n' > "$c/src/main.c"
cat > "$c/mcpp.toml" <<'EOF'
[package]
name = "absent-probe"
version = "0.1.0"

[dependencies]
fakelibc = { path = "libc" }

[build]
allow_host_libs = true
EOF
mk_libc() { # $1 = the form value
cat > "$c/libc/mcpp.toml" <<EOF
[package]
name = "fakelibc"
version = "0.1.0"
provides = ["mcpp:c-abi=musl"]

[targets.fakelibc]
kind = "lib"
sources = ["src/*.c"]

[c-abi]
presents = "posix"
data-model = "arch-default"
wchar = 32

[c-abi-absent]
fork = { form = "$1", note = "no process image duplication" }
EOF
}
mk_libc link
rm -rf "$c/target"
if (cd "$c" && "$STORE" build >/dev/null 2>&1); then
ok "a declared absence with a known shape is accepted"
else
fail "a declared absence with a known shape must be accepted"
fi
mk_libc sometimes
rm -rf "$c/target"
out="$(cd "$c" && "$STORE" build 2>&1)"
if [ $? -eq 0 ]; then
fail "an absence with an unknown shape must be refused"
else
case "$out" in
*accepted-no-effect*) ok "the refusal names the shapes that exist" ;;
*) fail "the refusal does not name the shapes: $(printf '%s' "$out" | head -2 | tr '\n' ' ')" ;;
esac
fi

# ── GUARD. A package that declares neither key is untouched ─────────────────
section "D. a package declaring neither key is unchanged (GUARD)"
d="$root/d"; rm -rf "$d"; mkdir -p "$d/src"
printf '#include <cstdio>\nint main(){std::puts("plain");return 0;}\n' > "$d/src/main.cpp"
cat > "$d/mcpp.toml" <<'EOF'
[package]
name = "plain"
version = "0.1.0"
EOF
if (cd "$d" && "$STORE" build >/dev/null 2>&1) \
&& "$d"/target/*/*/bin/plain 2>/dev/null | grep -q plain; then
ok "a package declaring nothing builds and runs"
else
fail "a package declaring nothing must build and run unchanged"
fi

# ── GUARD. openkal from the published index ─────────────────────────────────
section "E. an openkal program from the published index (GUARD)"
e="$root/e"; rm -rf "$e"; mkdir -p "$e/src"
printf '#include <cstdio>\nint main(){std::puts("openkal ok");return 0;}\n' > "$e/src/main.cpp"
cat > "$e/mcpp.toml" <<'EOF'
[package]
name = "openkal-hello"
version = "0.1.0"

[dependencies]
openkal-llvm-runtime = "0.12.0"
EOF
if (cd "$e" && "$STORE" build >/dev/null 2>&1); then
if "$e"/target/*/*/bin/openkal-hello 2>/dev/null | grep -q "openkal ok"; then
ok "an openkal program builds and runs from the published index"
else
fail "the openkal program built and did not run"
fi
else
skip "openkal-llvm-runtime 0.12.0 did not resolve from the index"
fi

printf '\n-- summary --\nfails=%d\nnot run:%s\n' "$fails" "${skipped:-
(none)}"
[ "$fails" -eq 0 ]
119 changes: 119 additions & 0 deletions .agents/docs/2026-09-20-cxa-thread-atexit-finding.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,119 @@
---
subject: review
status: active
---

# `__cxa_thread_atexit` 在 openkal-Windows 上:定位到一层,第二层未定位

- 日期:2026-09-20
- 来源:mcpp-index 的 30-member 重测,doctest 与 spdlog 两个成员停在
`ld.lld: error: undefined symbol: __cxa_thread_atexit`
- 结论:**不要只修第一层。** 只修它会把一个构建期的响亮失败换成一个运行期的静默失败。

---

## 1. 最小复现(五行)

```cpp
#include <cstdio>
struct D { int v; ~D() { std::printf("dtor %d\n", v); } };
thread_local D t{7};
int main() { std::printf("v=%d\n", t.v); return 0; }
```

依赖 `openkal-llvm-runtime = "0.12.0"`。

| 目标 | 读数 |
| --- | --- |
| `x86_64-linux-gnu` | 构建并运行 |
| `x86_64-windows-gnu` | `ld.lld: error: undefined symbol: __cxa_thread_atexit` |

## 2. 第一层:已定位

`llvm/libcxxabi/src/cxa_thread_atexit.cpp:109`

```cpp
#if defined(__linux__) || defined(__Fuchsia__)
extern "C" {
_LIBCXXABI_FUNC_VIS int __cxa_thread_atexit(Dtor, void*, void*) throw() { ... }
}
#endif
```

**上游只在这两个系统上导出这个符号**,因为在别处别人已经导出了。实测:

```
$ llvm-nm --defined-only .../x86_64-w64-mingw32/lib/libmingw32.a | grep -c __cxa_thread_atexit
1
```

——普通 MinGW 目标由 `libmingw32.a` 提供。openkal 把 C 库连同它的运行时一起换掉,
于是**两边都以为对方会提供**。这与本轮其他几处同形:上游问的是「这是哪个 OS」,
而真正的问题是「这个映像里还有没有第二个 C++ 运行时」。

文件里那段 fallback(`#ifndef HAVE___CXA_THREAD_ATEXIT_IMPL`,把析构挂在一个
`__libcpp_tls_key` 上)是**完整的**,只是被这个守卫挡在导出之外。

## 3. 把守卫放开之后:链接通了,析构不跑

在 `#if` 上加一条本包自己的条件之后:

| | Linux | Windows(wine) |
| --- | --- | --- |
| 链接 | 通过 | **通过**(此前失败) |
| `thread_local` 析构是否运行 | **运行** | **不运行** |

`examples/cxx` 加一条断言(在一个 spawned thread 里构造带析构的 `thread_local`,
join 之后查标志),Linux `ok`、Windows `FAIL`。

## 4. 第二层:两个假设,都被实测否掉

**假设一:PE 上 `thread_local` 走 emutls,它自己的 pthread key 先于 libc++abi 的
key 被析构,于是 `run_dtors` 读到的链表已经空了。**

否。key 析构里读 `thread_local` 在两个目标上都读到正确的值:

```cpp
static thread_local int marker = 0;
static void dtor(void*) { saw = marker; }
// 线程里 marker = 42; pthread_setspecific(k, ...)
```

```
Linux : key destructor read thread_local as 42 (expect 42)
Windows : key destructor read thread_local as 42 (expect 42)
```

**假设二:`__cxa_thread_atexit_impl` 是弱符号,在 PE 上解析成了非空,于是走了
`if (__cxa_thread_atexit_impl)` 那一支而不是 fallback。**

否。两个目标上都是 null:

```
Linux : __cxa_thread_atexit_impl = 0 -> fallback branch
Windows : __cxa_thread_atexit_impl = 0 -> fallback branch
```

另有一条已确认为**正常**的:`pthread_key_create` 的析构在 Windows 上**会**在线程
结束时运行(`pthread tsd dtor ran=1`)。所以不是 TSD 机制本身。

## 5. 为什么本轮不发这个补丁

| | 现状 | 只修第一层 |
| --- | --- | --- |
| 失败在哪 | **链接期** | 运行期 |
| 调用方能否看见 | **能,链接器点名符号** | **不能,注册成功而析构不发生** |

第二种正是 openkal-musl 的 `[c-abi-absent]` 里叫作 `accepted-no-effect` 的那个形状,
也是 SPEC §6.1 把「运行期报告不支持」称为缺陷的理由。**一个响亮的构建期失败,
比一个静默的运行期失败好。**

补丁已撤回。第一层的定位、第二层的两个否定结果,以及最小复现,都在上面——下一个
接手的人不必从 30 个成员的诊断重新走一遍。

## 6. 下一步的判据

1. 在 Windows 上确认 `run_dtors` **是否被调用**(在 fallback 里打一行,重建运行时)。
- 被调用而链表为空 ⇒ 注册那一侧的问题
- 没被调用 ⇒ `__libcpp_tls_create` / key 注册那一侧的问题
2. 无论结论如何,修法必须让「析构会跑」与「链接会过」同时成立,或者两者都不成立。
Loading
Loading