diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index fe6c0c3..06238d9 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -31,6 +31,18 @@ on: default: "" env: MCPP_SOURCE_REF: ${{ github.event.inputs.mcpp_ref || vars.MCPP_SOURCE_REF }} + # THE PIN STAYS ON THE RELEASE THAT PREDATES `[c-abi-absent]`, AND THAT IS + # THE POINT. The table is a top-level one, so an engine that does not know + # it ignores it (measured against this published archive on this file); the + # rows are asserted against the OBJECTS by tools/check-absent.sh, which + # reads the manifest itself and needs nothing from the engine. Building this + # package green here is therefore the end-to-end evidence for the claim the + # table's own comment makes: a client below 2026.9.20.1 keeps this package. + # + # An earlier draft of this branch built mcpp from its own pull-request + # branch through MCPP_SOURCE_REF, because the first spelling of the table + # WAS nested and did need the unreleased engine. Moving the table to the top + # level removed that need, and with it this release's dependency on mcpp's. MCPP_VERSION: 2026.9.18.3 XLINGS_VERSION: v2026.8.17.2 XLINGS_NON_INTERACTIVE: '1' @@ -490,7 +502,7 @@ jobs: # accumulates one per configuration, so a search across all of them reads # definitions from a build made before the change --- which is how this # check first reported every withheld symbol as still present. - - name: What is withheld is not defined, and what is not withheld is + - name: Every [c-abi-absent] row agrees with the archive if: runner.os == 'Linux' && matrix.target == '' run: | set -euo pipefail @@ -503,30 +515,42 @@ jobs: echo " examining $n objects in $(ls -d target/*/*/)" [ "$n" -gt 100 ] || { echo "::error::only $n objects; nothing was examined"; exit 1; } - defines() { # symbol -> the number of definitions in these objects - nm $objs 2>/dev/null | grep -cE "^[0-9a-f]+ [TWi] $1\$" || true - } - + # THE LIST LIVES IN THE MANIFEST AND NOT HERE. It used to be written + # out again in this step, which made the manifest's `[c-abi-absent]` + # table and this workflow two copies of one fact --- and a copy goes + # stale the first time only one of them is edited. The script reads + # the table and checks each row against the objects in the direction + # that row's `form` states: a `link` name must not be defined, an + # `enosys` name must be. + bash tools/check-absent.sh mcpp.toml $objs + + # The other half, and a different property: that this package still + # compiles the things it is supposed to. Without it the check above + # would pass for a package that had stopped compiling anything whose + # names happen not to be in the table. `pipe` is here because openkal + # 0.8 made it expressible; `socket` and `fork` because their closures + # reach the password functions and the thread implementation, so they + # are deliberately NOT withheld and the manifest says why. + defines() { nm $objs 2>/dev/null | grep -cE "^[0-9a-f]+ [TWi] $1\$" || true; } fail=0 - for s in epoll_create1 eventfd timerfd_create inotify_init signalfd; do - d=$(defines "$s") - if [ "$d" = 0 ]; then echo " withheld, not defined: $s" - else echo "::error::$s is withheld and yet defined $d time(s)"; fail=1; fi - done - - # The other half. Without it the check above would pass for a package - # that had stopped compiling anything at all. `pipe` is here because - # openkal 0.8 made it expressible; `socket` and `fork` because their - # closures reach the password functions and the thread implementation, - # so they are deliberately NOT withheld and the manifest says why. for s in printf malloc open pipe faccessat chmod socket fork; do d=$(defines "$s") if [ "$d" -ge 1 ]; then echo " defined here: $s" else echo "::error::$s is not withheld and yet is not defined"; fail=1; fi done - [ "$fail" = 0 ] || exit 1 - echo " ok the withheld set is exactly what the manifest names" + + # THE CHECK MUST BE ABLE TO FAIL. A row moved to the other form has + # to turn this step red; without this leg the step above passes + # identically against a script that reads no objects at all. + sed 's/^mprotect = { form = "enosys"/mprotect = { form = "link"/' \ + mcpp.toml > /tmp/absent-flipped.toml + grep -q 'mprotect = { form = "link"' /tmp/absent-flipped.toml || { + echo "::error::the flip that this leg depends on did not apply"; exit 1; } + if bash tools/check-absent.sh /tmp/absent-flipped.toml $objs; then + echo "::error::a row moved to the wrong form was accepted"; exit 1 + fi + echo " ok the table is asserted, and the assertion can fail" - name: What this package is built from is not what it publishes working-directory: examples/cross-hello diff --git a/README.md b/README.md index 835e8ab..8087cd2 100644 --- a/README.md +++ b/README.md @@ -252,6 +252,45 @@ The following are absent, and each is refused rather than quietly accepted, because a facility that reports success and does nothing is the one kind of answer that leaves a program wrong without telling it. +**Since 0.17.0 this table has an executor.** `[c-abi-absent]` in `mcpp.toml` +states each facility and the SHAPE in which its absence reaches a program --- +`link` (the definition is not in the archive), `enosys` (it is, and reports +that it cannot act), `accepted-no-effect` (the call succeeds and part of what +it asked for is not done) --- and `tools/check-absent.sh` asserts every row +against the objects this package builds, in the direction that row states. A +`link` name that turned out to be defined, or an `enosys` name that turned out +to be missing, fails the build. + +Prose alone had no executor, and it was contradicted once: before 0.16.0 +`SIG_IGN` was accepted for every signal and installed for none, so a program +that asked not to be ended by the interrupt keystroke was told it had +succeeded and was ended by it. `accepted-no-effect` is that shape, and it is +named so that "how many of these are there" is a question with an answer. + +`link` is the shape openkal's own capability model requires of an +implementation (SPEC 0.14 clause 6.1, which calls a run-time report of +unsupportedness a defect). The other two are departures from it, and a reader +counting them is reading the cost of presenting POSIX above an interface that +does not carry all of it. + +**Two things this table says and the manifest cannot, stated rather than rounded +off.** + +*A facility narrower than a name.* "A mode given at creation" is about an +ARGUMENT of `open` and `mkdir`, not about those calls: they do what they are +for and the mode is what is not applied. An entry keyed on `open` would say the +call is absent, which is false and worse than no entry. + +*An absence that varies by target.* `fork` is composed here from +`openkal.space`, and the reference to it is weak: a backend that provides the +interface gets a working `fork`, and one that does not gets `ENOSYS`. +openkal-linux provides it; openkal-windows declines it, and its README gives +the reason --- constructing the copy out of `CreateProcessW` would be present, +would look like the operation, and would not produce a copy of the caller. +Every row of `[c-abi-absent]` is unconditional, so `fork` written as `enosys` +would be false on Linux and omitting it is silent on Windows; silence is the +lesser of the two, and the row returns when the schema carries `targets`. + | Absent | What a program observes | Why | | --- | --- | --- | | signal handlers | `sigaction` reports `ENOSYS` for any handler other than the default or ignore. **Since 0.16.0 a disposition is accepted only where it is the one already in effect**: `SIG_DFL` succeeds for every signal but `SIGPIPE`, `SIG_IGN` succeeds for `SIGPIPE` alone, and the enquiry reports `SIG_IGN` for `SIGPIPE` rather than a zeroed record | openkal has no asynchronous delivery. A handler that was accepted and could never run would be silently wrong; masking, which has nothing to mask, succeeds. Until 0.16.0 `SIG_IGN` was accepted for every signal and installed for none, so a program that asked not to be ended by the interrupt keystroke was told it had succeeded and was ended by it. `SIGPIPE` is the one disposition that is not the default, and not by accident: openkal requires a write to a stream whose far end is gone to report the condition rather than end the program, so an implementation beneath has already arranged that the signal does nothing. | diff --git a/mcpp.toml b/mcpp.toml index 65ca208..363f99e 100644 --- a/mcpp.toml +++ b/mcpp.toml @@ -1,7 +1,7 @@ [package] namespace = "mcpplibs" name = "openkal-musl" -version = "0.16.0" +version = "0.17.0" description = "musl 1.2.5 redirected onto openkal: one C library, ported once, above every implementation of the specification rather than above one kernel." license = "Apache-2.0" @@ -38,6 +38,113 @@ data-model = "arch-default" wchar = 32 builtins = "iso" +# WHAT THIS C LIBRARY DOES NOT SUPPLY, AND IN WHAT SHAPE EACH ABSENCE REACHES A +# PROGRAM. +# +# The set of names a C library supplies is not enumerable here --- POSIX has +# about twelve hundred --- and enumerating it is the mistake openkal's own +# specification records withdrawing (SPEC 0.14 clause 3.3, on the name it gave +# to a set of interfaces and then took back). The exceptions are enumerable. +# README's "The following are absent" table has carried them in prose since +# this port began, and nothing executed that prose: it was contradicted once +# already, in the release before this one, where `SIG_IGN` was accepted for +# every signal and installed for none and a program that asked not to be ended +# by the interrupt keystroke was told it had succeeded and was ended by it. +# +# `form` is how the absence reaches the program, and it is the load-bearing +# field: +# +# link the definition is not in the archive; the program +# fails to link, naming the symbol. This is the shape +# openkal's capability model requires of an +# implementation (clause 6.1: a conforming +# implementation shall not provide an interface whose +# operations report a lack of support at run time). +# enosys the definition exists and reports that it cannot act. +# POSIX has a value for this and a caller can read it, +# which is what makes it a bounded answer rather than a +# silent one. +# accepted-no-effect the call succeeds and part of what it asked for is not +# done. This is the shape of the defect the previous +# release repaired, and it is named so that "how many of +# these are there" is a question with an answer. +# +# tools/check-absent.sh asserts every row against the built archive: a `link` +# name that IS defined, or an `enosys` name that is NOT, fails the build. +# +# THIS TABLE ASKS NOTHING OF AN OLDER ENGINE, AND ITS SPELLING IS WHY. mcpp +# ignores a top-level table it does not know and refuses an unknown MEMBER of +# a table it does know, so `[c-abi].absent` --- which reads better, and is +# where the first draft of this file put it --- made every mcpp below +# 2026.9.20.1 refuse THIS WHOLE MANIFEST on every target. Measured against the +# published 2026.9.18.3 archive on exactly this file. Everything the table +# does is diagnostic, so an engine that ignores it reports the same raw link +# error it reports today; an engine that refused it would have taken this +# package away entirely and forced the index floor up, costing every client +# below that floor the whole index for a note they merely would not receive. +# +# The consequence here: 0.17.0 needs no `min_mcpp` move and may be registered +# as soon as it is tagged. An older client builds it and gets the link error +# without the sentence that explains it, which is what it gets today. +[c-abi-absent] + +# Readiness held by the environment. A set is a facility of one kernel rather +# than a capability; `poll` and `select` ask each descriptor in turn, which is +# what an interface without a set permits. These five are not compiled at all +# (see the withheld sources below), so the link names them. +epoll_create = { form = "link", note = "openkal has no readiness set; poll and select ask each descriptor in turn" } +epoll_create1 = { form = "link", note = "as epoll_create" } +epoll_ctl = { form = "link", note = "as epoll_create" } +epoll_wait = { form = "link", note = "as epoll_create" } +epoll_pwait = { form = "link", note = "as epoll_create" } +timerfd_create = { form = "link", note = "a descriptor that is created and never becomes ready is worse than one that cannot be created" } +timerfd_settime = { form = "link", note = "as timerfd_create" } +timerfd_gettime = { form = "link", note = "as timerfd_create" } +eventfd = { form = "link", note = "as timerfd_create" } +eventfd_read = { form = "link", note = "as timerfd_create" } +eventfd_write = { form = "link", note = "as timerfd_create" } +signalfd = { form = "link", note = "as timerfd_create" } +inotify_init = { form = "link", note = "as timerfd_create" } +inotify_init1 = { form = "link", note = "as timerfd_create" } +inotify_add_watch = { form = "link", note = "as timerfd_create" } +inotify_rm_watch = { form = "link", note = "as timerfd_create" } + +# Reported to the caller, which can read the value and act on it. +mprotect = { form = "enosys", note = "openkal has no operation upon a mapping's protection; musl asks for a guard page and proceeds without one when told this" } +sigaction = { form = "enosys", note = "a disposition other than the one already in effect; openkal has no asynchronous delivery, and a handler that was accepted and could never run would be silently wrong" } +chmod = { form = "enosys", note = "a request whose read or write bits differ from what stat already reports; a capability-oriented environment has no principal for a permission to name" } +fchmodat = { form = "enosys", note = "as chmod" } +chown = { form = "enosys", note = "a capability-oriented environment has no principal for an owner to name" } +fchown = { form = "enosys", note = "as chown" } +lchown = { form = "enosys", note = "as chown" } + +# The call succeeds and part of what it asked for is not done. Each of these +# is a place where refusing would be worse than the partial answer, and the +# README row beside it says why. +# +# TWO THINGS THIS TABLE CANNOT SAY TODAY, STATED RATHER THAN ROUNDED OFF. +# +# A FACILITY NARROWER THAN A NAME. "A mode given at creation" is about an +# ARGUMENT of `open` and `mkdir`, not about those calls: they do what they are +# for, and the mode is what is not applied. A row keyed on `open` would say the +# call is absent, which is false and worse than the absence of a row. +# +# AN ABSENCE THAT VARIES BY TARGET. `fork` is composed here from +# `openkal.space` (port/src/okm_fork.c), which the reference to it takes +# WEAKLY: a backend that provides the interface gets a working `fork`, and one +# that does not gets `-ENOSYS`. openkal-linux provides it; openkal-windows +# declines it, for the reason its own README gives --- constructing the copy +# out of `CreateProcessW` would be present, would look like the operation, and +# would not produce a copy of the caller. So `fork` is `enosys` on Windows and +# works on Linux, and every row here is unconditional. Writing it as `enosys` +# would be false on Linux; omitting it is silent on Windows, and silence is the +# lesser of the two. The row returns when the schema carries `targets`. +# +# Both stay in the README until then. A table that answered these two by +# rounding them off would be a table nobody could assert against, which is the +# state this one exists to leave. +tcsetattr = { form = "accepted-no-effect", note = "openkal names three positions of the terminal mode word; a request that alters output post-processing, the line speed, the control characters or VMIN/VTIME is accepted and that part has no effect" } + [dependencies] openkal = "0.14.0" @@ -54,7 +161,7 @@ openkal = "0.14.0" # # The consequence for a program is that it names this package and nothing else. [target.'cfg(os = "linux")'.dependencies] -openkal-linux = { version = "0.14.0", features = ["standalone"] } +openkal-linux = { version = "0.15.0", features = ["standalone"] } [target.'cfg(os = "macos")'.dependencies] openkal-macos = { version = "0.11.0", features = ["standalone"] } @@ -93,7 +200,7 @@ openkal-opensbi = { version = "0.8.0", features = ["standalone"] } defines = ["OKM_HAS_FS=0", "OKM_HAS_PROCESS=0", "OKM_HAS_TASK=0"] [target.'cfg(windows)'.dependencies] -openkal-windows = { version = "0.9.0", features = ["standalone"] } +openkal-windows = { version = "0.10.0", features = ["standalone"] } # The feature macros musl's own build establishes. # diff --git a/tools/check-absent.sh b/tools/check-absent.sh new file mode 100755 index 0000000..66759c6 --- /dev/null +++ b/tools/check-absent.sh @@ -0,0 +1,88 @@ +#!/usr/bin/env bash +# Asserts `[c-abi-absent]` against the archive this package actually builds. +# +# check-absent.sh ... +# +# The table in mcpp.toml states, for each facility this C library does not +# supply, the SHAPE in which the absence reaches a program. Two of the three +# shapes are checkable from the artefact alone, and they are checked in +# opposite directions: +# +# form = "link" the definition must NOT be in the archive. This is the +# shape openkal's capability model requires of an +# implementation (SPEC 0.14 clause 6.1), and a name that +# turned out to be defined would mean a program links and +# then meets the absence somewhere it cannot read it. +# form = "enosys" the definition MUST be in the archive. A name that +# turned out to be missing would fail the link instead, +# which is a different contract from the one stated --- and +# the one a caller prepared to read `ENOSYS` is not +# prepared for. +# +# `accepted-no-effect` is not checkable here: it is a statement about what a +# call does, not about whether it exists, and the conformance suite is where a +# behaviour is examined. It is listed so that "how many of these are there" has +# an answer; this script checks that such a name is defined, which is the most +# an artefact can say about it. +# +# THE DIRECTIONS ARE BOTH CHECKED ON PURPOSE. A script that only verified the +# `link` rows would pass against a manifest that had quietly moved every row to +# `enosys`, which is the change that would matter most. +set -euo pipefail + +manifest="${1:?usage: check-absent.sh ...}" +shift +[ "$#" -gt 0 ] || { echo "no archive or object given" >&2; exit 2; } + +NM="${NM:-nm}" + +defined="$($NM --defined-only "$@" 2>/dev/null \ + | awk '$2=="T"||$2=="W"||$2=="R"||$2=="D"||$2=="B"||$2=="S"{print $3}' \ + | sed 's/^_//' | sort -u || true)" + +# An empty surface is never a conforming one: nothing found means the objects +# were wrong or the symbols were not recognised, and reporting success would +# conceal both. The same rule tools/check-surface.sh states, for the same +# reason. +if [ -z "$defined" ]; then + echo "no defined symbol was found; the objects or the symbol format are wrong" >&2 + exit 1 +fi + +status=0 +rows=0 +in_table=0 +while IFS= read -r line; do + case "$line" in + '[c-abi-absent]'*) in_table=1; continue ;; + '['*) in_table=0; continue ;; + esac + [ "$in_table" -eq 1 ] || continue + case "$line" in ''|'#'*) continue ;; esac + name="${line%%=*}"; name="${name// /}" + [ -n "$name" ] || continue + case "$line" in + *'form = "link"'*) want=absent ;; + *'form = "enosys"'*) want=present ;; + *'form = "accepted-no-effect"'*) want=present ;; + *) echo "row '$name' names no form this script knows" >&2; status=1; continue ;; + esac + rows=$((rows+1)) + if grep -qxF -- "$name" <<< "$defined"; then found=present; else found=absent; fi + if [ "$found" != "$want" ]; then + if [ "$want" = absent ]; then + echo "$name is declared absent at the link and IS defined in the archive" >&2 + else + echo "$name is declared to report its refusal and is NOT defined in the archive" >&2 + fi + status=1 + fi +done < "$manifest" + +if [ "$rows" -eq 0 ]; then + echo "[c-abi-absent] has no rows; this script asserted nothing" >&2 + exit 1 +fi + +[ "$status" -eq 0 ] && echo "every [c-abi-absent] row agrees with the archive: $rows row(s)" +exit "$status"