Skip to content

Commit 9976346

Browse files
Sunrisepeakmcpplibs
Sunrisepeak
and
mcpplibs
authored
openkal-linux 0.5.0: implement on the kernel, so that a C library can sit above (#1)
* openkal-linux 0.5.0: implement on the kernel, so that a C library can sit above Version 0.4 was written upon the C library of the host. That is a correct implementation of openkal and it fails for the program openkal exists to support. A C library ported onto openkal defines write, malloc and open; so does the host's; one program cannot reach both definitions, so this implementation's calls resolved to the ported library, which called openkal, which called this implementation again. Neither side reads as though anything is wrong. Every interface is now implemented on the kernel's own system-call interface for x86_64 and aarch64, and the objects reference no C library symbol - which CI asserts against the objects rather than the source, and which a probe confirms the check can detect the absence of. The kernel's structure layouts are declared here rather than taken from a header, because the same-named structure differs between C libraries and an implementation compiled against one and linked with another would read the wrong fields. A "freestanding" feature supplies what a C library's first object ordinarily supplies, for a program that is a C library: the program entry, a thread-local storage block per execution context built from the program's own PT_TLS segment, and execution contexts created with clone. Without it, contexts come from the C library the program is linked against, which is the ordinary configuration and remains the default. kal_fs_preopen(0) now reports the working directory's absolute path rather than ".", because a C library above openkal must report a working directory and could not have done so. The four operations and one property openkal 0.5 adds are implemented, and a sixth conformance suite observes each of them by its effect. * openkal-linux: state the arrangement in openkal's terms The feature is renamed from 'freestanding' to 'standalone' and restated: what it selects is whether this implementation is the whole of the program's environment, which is a property of the program. The finding that produced it is unchanged and is now stated generally --- an implementation must not depend upon a runtime the program may itself supply --- with a C library as the instance rather than as the subject. * ci: two compiler families, the shared suite, and the feature under its own name The workflow named a feature this package renamed --- `freestanding' became `standalone', because the arrangement is a statement about the program and not about how much of a C library is present --- so the two steps that assert this version's central property were building the default configuration and asserting nothing about the one they name. It also ran only this package's own tests. The specification now carries the behavioural half of clause 9 as a suite every implementation runs, so that is run first and this package's own tests, which examine the operations version 0.5 added, follow it. Both are now run under two compiler families. An implementation is a contract's evidence, and a contract that holds only under the compiler its author used is a description of that compiler. * openkal-linux: set a file's modification time, and name the fixed widths openkal names * docs: the feature under its own name, and where the shared suite is --------- Co-authored-by: mcpplibs <noreply@mcpplibs.org>
1 parent 6ef1dbb commit 9976346

19 files changed

Lines changed: 1850 additions & 532 deletions

‎.github/workflows/ci.yml‎

Lines changed: 133 additions & 74 deletions
Original file line numberDiff line numberDiff line change
@@ -1,27 +1,60 @@
11
name: CI
22

3+
# What this workflow asserts.
4+
#
5+
# conformance the suite in the specification package runs against this
6+
# implementation and every observation holds
7+
# additions this package's own tests, which examine the operations
8+
# version 0.5 added
9+
# surface the exported names are exactly the fifty-one the
10+
# specification lists, in both forms
11+
# independence the objects reference no C library symbol
12+
#
13+
# The last is the property version 0.5 exists for, and it is asserted against
14+
# the objects rather than against the source, because a source can reach a C
15+
# library through a macro.
16+
#
17+
# Two compiler families, because an implementation is a contract's evidence and
18+
# a contract that holds only under the compiler its author used is a description
19+
# of that compiler.
20+
321
on:
422
push:
523
branches: [main]
624
pull_request:
725
workflow_dispatch:
826

27+
env:
28+
MCPP_VERSION: 2026.8.19.4
29+
XLINGS_VERSION: v2026.8.17.2
30+
XLINGS_NON_INTERACTIVE: '1'
31+
932
jobs:
10-
build:
11-
name: conformance
33+
conformance:
34+
name: conformance, surface, and independence (${{ matrix.toolchain }})
1235
runs-on: ubuntu-24.04
13-
timeout-minutes: 30
14-
env:
15-
# A version verified to build this package, not a measured minimum. The
16-
# package uses modules, exported extern "C" declarations and ordinary
17-
# dependencies, none of which is recent; the pin exists for reproducibility
18-
# rather than because an older mcpp is known to fail.
19-
MCPP_VERSION: 2026.8.19.4
20-
XLINGS_VERSION: v2026.8.17.2
21-
XLINGS_NON_INTERACTIVE: '1'
36+
timeout-minutes: 60
37+
strategy:
38+
fail-fast: false
39+
matrix:
40+
toolchain: ['gcc@16.1.0', 'llvm@22.1.8']
2241
steps:
2342
- uses: actions/checkout@v4
2443

44+
# The specification is checked out at the branch under test where it has
45+
# one, so that this run asserts what it is for: that the specification as
46+
# written there and this implementation as written here agree today.
47+
- name: The specification
48+
run: |
49+
git clone --quiet https://github.com/mcpplibs/openkal.git .spec
50+
branch='${{ github.head_ref || github.ref_name }}'
51+
if git -C .spec rev-parse --verify --quiet "origin/$branch" > /dev/null; then
52+
git -C .spec checkout --quiet "origin/$branch"
53+
echo "the specification is at $branch"
54+
else
55+
echo "the specification has no $branch; its default branch is used"
56+
fi
57+
2558
- name: Install xlings
2659
run: |
2760
curl -fsSL https://raw.githubusercontent.com/openxlings/xlings/main/tools/other/quick_install.sh \
@@ -35,82 +68,108 @@ jobs:
3568
mcpp --version
3669
mcpp self config --mirror GLOBAL
3770
38-
# The version of the specification this implementation is written against
39-
# is stated once, in the manifest, and read from there. Stating it a second
40-
# time in this file is what allowed the two to drift: the manifest moved to
41-
# 0.3.0 and this file compared against the 0.2.0 surface, so four names
42-
# this implementation is required to export were reported as unspecified.
43-
- name: Read the specification version from the manifest
71+
# The compiler family and version for this row. mcpp keeps its toolchains
72+
# in a sandbox of its own, so this selects rather than installs into the
73+
# system, and `mcpp test' and `mcpp run' have no flag for it --- which is
74+
# why it is set once here rather than passed to each command.
75+
- name: Select the toolchain
76+
run: |
77+
spec='${{ matrix.toolchain }}'
78+
case "$spec" in
79+
msvc*) mcpp toolchain default msvc ;;
80+
*) mcpp toolchain install "${spec%@*}" "${spec#*@}"
81+
mcpp toolchain default "$spec" ;;
82+
esac
83+
mcpp toolchain list
84+
85+
- name: Every interface, every kind of examination
4486
run: |
45-
v="$(sed -n 's/^openkal[[:space:]]*=[[:space:]]*"\([^"]*\)".*/\1/p' mcpp.toml | head -1)"
46-
test -n "$v" || { echo "the manifest does not name openkal" >&2; exit 1; }
47-
echo "OPENKAL_VERSION=$v" >> "$GITHUB_ENV"
48-
echo "written against openkal $v"
87+
bash .spec/tools/run-conformance.sh openkal-linux . full
4988
50-
- name: Conformance
89+
- name: Point at the specification's working tree
5190
run: |
52-
mcpp test 2>&1 | tee conformance.log
91+
# run-conformance.sh has already done this; it is repeated because a
92+
# reader of this file should not have to know that.
93+
sed 's|^openkal = .*$|openkal = { path = ".spec" }|' mcpp.toml > mcpp.toml.next
94+
mv mcpp.toml.next mcpp.toml
5395
96+
- name: This package's own tests
97+
run: |
98+
mcpp test 2>&1 | tee tests.log
5499
# A suite that discovered nothing reports success, so every suite is
55100
# asserted to have run. The list is derived from the files present
56101
# rather than written out here: a hand-written list names the suites
57-
# that existed when it was written, and a suite added afterwards
58-
# escapes the assertion silently. This assertion named two of five.
102+
# that existed when it was written, and one added afterwards escapes
103+
# the assertion silently.
59104
missing=0
60105
for f in tests/*.cpp; do
61106
name="$(basename "$f" .cpp)"
62-
if ! grep -q "^$name \.\.\. ok" conformance.log; then
63-
echo "suite did not run, or did not pass: $name" >&2
64-
missing=1
65-
fi
107+
grep -q "^$name \.\.\. ok" tests.log || { echo "did not run or did not pass: $name" >&2; missing=1; }
66108
done
67109
test "$missing" -eq 0
68110
69-
- name: The specification, at the version the manifest names
70-
uses: actions/checkout@v4
71-
with:
72-
repository: mcpplibs/openkal
73-
ref: ${{ env.OPENKAL_VERSION }}
74-
path: .spec
75-
76-
- name: The exported surface matches the specification
111+
- name: The exported surface is complete and contains nothing else
77112
run: |
78-
# Clause 9.3. The list and the checker come from the specification
79-
# itself rather than from a copy kept here, so that the comparison has
80-
# one source. --complete because this implementation claims every
81-
# interface: a name it fails to export is a failure, not an interface
82-
# it declines to provide.
113+
rm -rf target && mcpp build
83114
bash .spec/tools/check-surface.sh --complete .spec/SURFACE.txt \
84-
$(find target -name '*.o' | tr '\n' ' ')
85-
86-
# The program is taken from the specification rather than copied here. A
87-
# copy in each implementation is a copy that can diverge, and the value of
88-
# the program is precisely that every implementation runs the same one.
89-
#
90-
# The manifest is written here because naming the implementation is the
91-
# manifest's job and not the program's, which is the arrangement the
92-
# program exists to demonstrate.
93-
- name: The portable program runs
115+
$(find target -path '*/obj/*' -name '*.o' ! -name '*.m.o' ! -name 'conformance*' | tr '\n' ' ')
116+
117+
- name: The C++ declarations are complete
94118
run: |
95-
# Not `sed -i`: BSD sed requires a backup suffix after -i and reads
96-
# the next word as one, so the GNU form fails on macOS with
97-
# `invalid command code m`. This form is the same on both.
98-
sed 's|^openkal = ".*"$|openkal = { path = ".spec" }|' mcpp.toml > mcpp.toml.next
99-
mv mcpp.toml.next mcpp.toml
100-
cat > .spec/examples/portable/mcpp.toml <<'TOML'
101-
[package]
102-
name = "portable"
103-
version = "0.1.0"
104-
105-
[dependencies]
106-
openkal = { path = "../.." }
107-
openkal-linux = { path = "../../.." }
108-
TOML
109-
cd .spec/examples/portable
110-
mcpp run 2>&1 | tee run.log
111-
# Both directions: that the program reported, and that nothing it
112-
# observed failed to hold. Asserting only the first would pass for a
113-
# program that printed its failures.
114-
grep -q 'openkal: the portable program, above eight interfaces' run.log
115-
grep -q 'openkal: observations that did not hold: 0' run.log
116-
! grep -q 'NOT HELD' run.log
119+
# The specification's own tool examines the C form. The module form is
120+
# examined here, where a build of the modules exists: the test names
121+
# every entity SURFACE.txt lists, so a name the modules do not export
122+
# fails to compile and the diagnostic names it.
123+
list="$(grep -vE '^[[:space:]]*(#|$)' .spec/SURFACE.txt | sort -u)"
124+
{
125+
for m in types abort stream memory env time fs process task; do
126+
echo "import openkal.$m;"
127+
done
128+
echo 'const void *const surface[] = {'
129+
while read -r n; do [ -n "$n" ] && echo " (const void *)&$n,"; done <<< "$list"
130+
echo '};'
131+
echo 'int main() { return surface[0] == 0; }'
132+
} > tests/conformance_declarations.cpp
133+
mcpp test conformance_declarations 2>&1 | tee decl.log
134+
grep -q '^conformance_declarations \.\.\. ok' decl.log
135+
rm -f tests/conformance_declarations.cpp
136+
137+
# The property this version exists for. An implementation beneath a
138+
# program that supplies its own runtime must not reach for that runtime's
139+
# names, or its calls resolve to the program's and recur without bound.
140+
- name: The objects reference no C library symbol
141+
run: |
142+
rm -rf target && mcpp build --features standalone
143+
objs=$(find target -path '*/obj/*' -name '*.o' ! -name '*.m.o' ! -name 'conformance*')
144+
test -n "$objs" || { echo "no objects were found; the check would pass vacuously" >&2; exit 1; }
145+
146+
# The permitted set. memcpy, memmove, memset and memcmp are the four a
147+
# freestanding translation unit is permitted to require: a compiler
148+
# emits calls to them from ordinary loops, and they compute rather
149+
# than call, so none of them can re-enter this implementation.
150+
# __libc_start_main and main are the hand-over, and are undefined here
151+
# by construction.
152+
permitted='^(memcpy|memmove|memset|memcmp|__libc_start_main|main|_GLOBAL_OFFSET_TABLE_|kal_[a-z_]+|__init_array_start|__init_array_end|__preinit_array_start|__preinit_array_end|_ZN3okl.*)$'
153+
bad=0
154+
for s in $(nm --undefined-only $objs | awk '{print $2}' | sort -u); do
155+
[ -n "$s" ] || continue
156+
if ! printf '%s\n' "$s" | grep -qE "$permitted"; then
157+
echo "the implementation references a symbol it must not: $s" >&2
158+
bad=1
159+
fi
160+
done
161+
test "$bad" -eq 0
162+
echo "the implementation references no C library symbol"
163+
164+
# A checker is only useful if it fails when it should.
165+
- name: The independence check detects a dependence
166+
run: |
167+
printf 'extern "C" int puts(const char*);\nextern "C" void okl_probe(void) { puts("x"); }\n' > src/probe.cpp
168+
rm -rf target && mcpp build --features standalone
169+
objs=$(find target -path '*/obj/*' -name '*.o' ! -name '*.m.o')
170+
if ! nm --undefined-only $objs | awk '{print $2}' | grep -qx puts; then
171+
echo "the probe did not produce the reference it was written to produce" >&2
172+
rm -f src/probe.cpp; exit 1
173+
fi
174+
rm -f src/probe.cpp
175+
echo "a dependence upon a C library is visible to the check"

0 commit comments

Comments
 (0)