Skip to content

openkal-linux 0.5.0: implement on the kernel, so that a C library can sit above #1

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
Sunrisepeak merged 5 commits into from
Aug 20, 2026
Merged

openkal-linux 0.5.0: implement on the kernel, so that a C library can sit above #1

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
df86108
openkal-linux 0.5.0: implement on the kernel, so that a C library can…
Aug 19, 2026
a07d26d
openkal-linux: state the arrangement in openkal's terms
Aug 20, 2026
4930339
ci: two compiler families, the shared suite, and the feature under it…
Sunrisepeak Aug 20, 2026
32817e4
openkal-linux: set a file's modification time, and name the fixed wid…
Sunrisepeak Aug 20, 2026
41b0840
docs: the feature under its own name, and where the shared suite is
Sunrisepeak Aug 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
207 changes: 133 additions & 74 deletions .github/workflows/ci.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,27 +1,60 @@
name: CI

# What this workflow asserts.
#
# conformance the suite in the specification package runs against this
# implementation and every observation holds
# additions this package's own tests, which examine the operations
# version 0.5 added
# surface the exported names are exactly the fifty-one the
# specification lists, in both forms
# independence the objects reference no C library symbol
#
# The last is the property version 0.5 exists for, and it is asserted against
# the objects rather than against the source, because a source can reach a C
# library through a macro.
#
# Two compiler families, because 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.

on:
push:
branches: [main]
pull_request:
workflow_dispatch:

env:
MCPP_VERSION: 2026.8.19.4
XLINGS_VERSION: v2026.8.17.2
XLINGS_NON_INTERACTIVE: '1'

jobs:
build:
name: conformance
conformance:
name: conformance, surface, and independence (${{ matrix.toolchain }})
runs-on: ubuntu-24.04
timeout-minutes: 30
env:
# A version verified to build this package, not a measured minimum. The
# package uses modules, exported extern "C" declarations and ordinary
# dependencies, none of which is recent; the pin exists for reproducibility
# rather than because an older mcpp is known to fail.
MCPP_VERSION: 2026.8.19.4
XLINGS_VERSION: v2026.8.17.2
XLINGS_NON_INTERACTIVE: '1'
timeout-minutes: 60
strategy:
fail-fast: false
matrix:
toolchain: ['gcc@16.1.0', 'llvm@22.1.8']
steps:
- uses: actions/checkout@v4

# The specification is checked out at the branch under test where it has
# one, so that this run asserts what it is for: that the specification as
# written there and this implementation as written here agree today.
- name: The specification
run: |
git clone --quiet https://github.com/mcpplibs/openkal.git .spec
branch='${{ github.head_ref || github.ref_name }}'
if git -C .spec rev-parse --verify --quiet "origin/$branch" > /dev/null; then
git -C .spec checkout --quiet "origin/$branch"
echo "the specification is at $branch"
else
echo "the specification has no $branch; its default branch is used"
fi

- name: Install xlings
run: |
curl -fsSL https://raw.githubusercontent.com/openxlings/xlings/main/tools/other/quick_install.sh \
Expand All @@ -35,82 +68,108 @@ jobs:
mcpp --version
mcpp self config --mirror GLOBAL

# The version of the specification this implementation is written against
# is stated once, in the manifest, and read from there. Stating it a second
# time in this file is what allowed the two to drift: the manifest moved to
# 0.3.0 and this file compared against the 0.2.0 surface, so four names
# this implementation is required to export were reported as unspecified.
- name: Read the specification version from the manifest
# The compiler family and version for this row. mcpp keeps its toolchains
# in a sandbox of its own, so this selects rather than installs into the
# system, and `mcpp test' and `mcpp run' have no flag for it --- which is
# why it is set once here rather than passed to each command.
- name: Select the toolchain
run: |
spec='${{ matrix.toolchain }}'
case "$spec" in
msvc*) mcpp toolchain default msvc ;;
*) mcpp toolchain install "${spec%@*}" "${spec#*@}"
mcpp toolchain default "$spec" ;;
esac
mcpp toolchain list

- name: Every interface, every kind of examination
run: |
v="$(sed -n 's/^openkal[[:space:]]*=[[:space:]]*"\([^"]*\)".*/\1/p' mcpp.toml | head -1)"
test -n "$v" || { echo "the manifest does not name openkal" >&2; exit 1; }
echo "OPENKAL_VERSION=$v" >> "$GITHUB_ENV"
echo "written against openkal $v"
bash .spec/tools/run-conformance.sh openkal-linux . full

- name: Conformance
- name: Point at the specification's working tree
run: |
mcpp test 2>&1 | tee conformance.log
# run-conformance.sh has already done this; it is repeated because a
# reader of this file should not have to know that.
sed 's|^openkal = .*$|openkal = { path = ".spec" }|' mcpp.toml > mcpp.toml.next
mv mcpp.toml.next mcpp.toml

- name: This package's own tests
run: |
mcpp test 2>&1 | tee tests.log
# A suite that discovered nothing reports success, so every suite is
# asserted to have run. The list is derived from the files present
# rather than written out here: a hand-written list names the suites
# that existed when it was written, and a suite added afterwards
# escapes the assertion silently. This assertion named two of five.
# that existed when it was written, and one added afterwards escapes
# the assertion silently.
missing=0
for f in tests/*.cpp; do
name="$(basename "$f" .cpp)"
if ! grep -q "^$name \.\.\. ok" conformance.log; then
echo "suite did not run, or did not pass: $name" >&2
missing=1
fi
grep -q "^$name \.\.\. ok" tests.log || { echo "did not run or did not pass: $name" >&2; missing=1; }
done
test "$missing" -eq 0

- name: The specification, at the version the manifest names
uses: actions/checkout@v4
with:
repository: mcpplibs/openkal
ref: ${{ env.OPENKAL_VERSION }}
path: .spec

- name: The exported surface matches the specification
- name: The exported surface is complete and contains nothing else
run: |
# Clause 9.3. The list and the checker come from the specification
# itself rather than from a copy kept here, so that the comparison has
# one source. --complete because this implementation claims every
# interface: a name it fails to export is a failure, not an interface
# it declines to provide.
rm -rf target && mcpp build
bash .spec/tools/check-surface.sh --complete .spec/SURFACE.txt \
$(find target -name '*.o' | tr '\n' ' ')

# The program is taken from the specification rather than copied here. A
# copy in each implementation is a copy that can diverge, and the value of
# the program is precisely that every implementation runs the same one.
#
# The manifest is written here because naming the implementation is the
# manifest's job and not the program's, which is the arrangement the
# program exists to demonstrate.
- name: The portable program runs
$(find target -path '*/obj/*' -name '*.o' ! -name '*.m.o' ! -name 'conformance*' | tr '\n' ' ')

- name: The C++ declarations are complete
run: |
# Not `sed -i`: BSD sed requires a backup suffix after -i and reads
# the next word as one, so the GNU form fails on macOS with
# `invalid command code m`. This form is the same on both.
sed 's|^openkal = ".*"$|openkal = { path = ".spec" }|' mcpp.toml > mcpp.toml.next
mv mcpp.toml.next mcpp.toml
cat > .spec/examples/portable/mcpp.toml <<'TOML'
[package]
name = "portable"
version = "0.1.0"

[dependencies]
openkal = { path = "../.." }
openkal-linux = { path = "../../.." }
TOML
cd .spec/examples/portable
mcpp run 2>&1 | tee run.log
# Both directions: that the program reported, and that nothing it
# observed failed to hold. Asserting only the first would pass for a
# program that printed its failures.
grep -q 'openkal: the portable program, above eight interfaces' run.log
grep -q 'openkal: observations that did not hold: 0' run.log
! grep -q 'NOT HELD' run.log
# The specification's own tool examines the C form. The module form is
# examined here, where a build of the modules exists: the test names
# every entity SURFACE.txt lists, so a name the modules do not export
# fails to compile and the diagnostic names it.
list="$(grep -vE '^[[:space:]]*(#|$)' .spec/SURFACE.txt | sort -u)"
{
for m in types abort stream memory env time fs process task; do
echo "import openkal.$m;"
done
echo 'const void *const surface[] = {'
while read -r n; do [ -n "$n" ] && echo " (const void *)&$n,"; done <<< "$list"
echo '};'
echo 'int main() { return surface[0] == 0; }'
} > tests/conformance_declarations.cpp
mcpp test conformance_declarations 2>&1 | tee decl.log
grep -q '^conformance_declarations \.\.\. ok' decl.log
rm -f tests/conformance_declarations.cpp

# The property this version exists for. An implementation beneath a
# program that supplies its own runtime must not reach for that runtime's
# names, or its calls resolve to the program's and recur without bound.
- name: The objects reference no C library symbol
run: |
rm -rf target && mcpp build --features standalone
objs=$(find target -path '*/obj/*' -name '*.o' ! -name '*.m.o' ! -name 'conformance*')
test -n "$objs" || { echo "no objects were found; the check would pass vacuously" >&2; exit 1; }

# The permitted set. memcpy, memmove, memset and memcmp are the four a
# freestanding translation unit is permitted to require: a compiler
# emits calls to them from ordinary loops, and they compute rather
# than call, so none of them can re-enter this implementation.
# __libc_start_main and main are the hand-over, and are undefined here
# by construction.
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.*)$'
bad=0
for s in $(nm --undefined-only $objs | awk '{print $2}' | sort -u); do
[ -n "$s" ] || continue
if ! printf '%s\n' "$s" | grep -qE "$permitted"; then
echo "the implementation references a symbol it must not: $s" >&2
bad=1
fi
done
test "$bad" -eq 0
echo "the implementation references no C library symbol"

# A checker is only useful if it fails when it should.
- name: The independence check detects a dependence
run: |
printf 'extern "C" int puts(const char*);\nextern "C" void okl_probe(void) { puts("x"); }\n' > src/probe.cpp
rm -rf target && mcpp build --features standalone
objs=$(find target -path '*/obj/*' -name '*.o' ! -name '*.m.o')
if ! nm --undefined-only $objs | awk '{print $2}' | grep -qx puts; then
echo "the probe did not produce the reference it was written to produce" >&2
rm -f src/probe.cpp; exit 1
fi
rm -f src/probe.cpp
echo "a dependence upon a C library is visible to the check"
Loading
Loading