openkal-macos 0.3.0: implement on the kernel, and correct the direction of the suspension primitive #8
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name: CI | |
| # What this workflow asserts. | |
| # | |
| # conformance the suite in the specification package runs against this | |
| # implementation, on both architectures, and every observation | |
| # holds | |
| # surface the exported names are exactly the fifty-one the | |
| # specification lists | |
| # independence the objects reference nothing of a C library but the two names | |
| # no C library defines | |
| # | |
| # The third is the property version 0.3 exists for. A program above openkal may | |
| # supply every name the system's own library supplies; an implementation that | |
| # called one of them would have its calls resolve to the program's, and the | |
| # program's would resolve back here. | |
| 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: | |
| conformance: | |
| name: conformance (${{ matrix.os }}, ${{ matrix.toolchain }}) | |
| runs-on: ${{ matrix.os }} | |
| timeout-minutes: 60 | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| include: | |
| # arm64 and x86_64. The system-call numbers agree; the calling | |
| # convention, the register the current context is reached through and | |
| # one field of a signal context do not, so both are built. | |
| - { os: macos-14, toolchain: 'llvm@20.1.7' } | |
| - { os: macos-13, toolchain: 'llvm@20.1.7' } | |
| 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 \ | |
| | bash -s "$XLINGS_VERSION" | |
| echo "$HOME/.xlings/subos/current/bin" >> "$GITHUB_PATH" | |
| - name: Install mcpp | |
| run: | | |
| xlings update | |
| xlings install "mcpp@$MCPP_VERSION" -y -g | |
| mcpp --version | |
| mcpp self config --mirror GLOBAL | |
| # 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: | | |
| bash .spec/tools/run-conformance.sh openkal-macos . full | |
| - name: The exported surface is complete and contains nothing else | |
| run: | | |
| # Clause 9.3. The list and the checker come from the specification | |
| # 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 | |
| objs="$(find target -path '*/obj/*' -name '*.o' ! -name '*.m.o' | tr '\n' ' ')" | |
| test -n "$objs" || { echo "no objects were found" >&2; exit 1; } | |
| bash .spec/tools/check-surface.sh --complete .spec/SURFACE.txt $objs | |
| # The property version 0.3 exists for. The assertion is made against the | |
| # objects rather than against the source, because a source can reach a C | |
| # library through a macro. | |
| - name: The objects reference nothing of a C library but the two named | |
| run: | | |
| rm -rf target && mcpp build --features standalone | |
| objs="$(find target -path '*/obj/*' -name '*.o' ! -name '*.m.o')" | |
| test -n "$objs" || { echo "no objects were found; the check would pass vacuously" >&2; exit 1; } | |
| # The permitted set, and why each entry is in it. | |
| # | |
| # memcpy, memmove, memset, memcmp a compiler emits calls to these | |
| # from ordinary loops. They compute rather than call, so none of | |
| # them can re-enter this implementation. | |
| # clock_gettime_nsec_np, | |
| # pthread_create_from_mach_thread the two names no C library | |
| # defines, which is why they are reachable from here at all. | |
| # __libc_start_main, main, _main the hand-over, undefined here by | |
| # construction. | |
| # kal_* the interface itself. | |
| # __stack_chk_* emitted by the toolchain around | |
| # a frame it protects; supplied by the program, not called by this | |
| # implementation. | |
| permitted='^_?(memcpy|memmove|memset|memcmp|bzero|clock_gettime_nsec_np|pthread_create_from_mach_thread|pthread_create|pthread_join|__libc_start_main|main|kal_[a-z_]+|__stack_chk_guard|__stack_chk_fail|GCC_except_table.*|_ZN3okm.*|__Unwind_Resume)$' | |
| bad=0 | |
| for s in $(nm -u $objs | sed 's/^ *//' | grep -v ':$' | sort -u); do | |
| [ -n "$s" ] || continue | |
| printf '%s\n' "$s" | grep -qE "$permitted" || { | |
| echo "the implementation references a symbol it must not: $s" >&2 | |
| bad=1 | |
| } | |
| done | |
| test "$bad" -eq 0 | |
| echo "the implementation reaches nothing of a C library but the two names that are named" | |
| # 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 okm_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 -u $objs | sed 's/^ *//' | 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" |