docs(openkal): record the layering correction that produced 0.2 - #462
Merged
Conversation
Version 0.1 let the implementation provide the module a consumer imports, with the specification package providing openkal.decl.<name> for it to re-export. Review identified this as a contradiction of what a specification is for, and the identification was correct. The justification does not survive examination. That arrangement existed solely to make optional operations detectable through argument-dependent lookup, which requires an implementation's declarations to be visible to the consumer — and version 0.1 defined no optional operation. The mechanism served a requirement that did not exist, and it was paid for with a real cost: the name a consumer relies upon sat outside the specification's control. 0.2 restores the intended layering, verified: a backend that exports no module builds and runs, and a missing implementation is reported by the linker naming the undefined functions. This is the third occurrence of one shape in this round. The first was openkal.namespace, which merged two kinds of resource in order to unify naming; the second was extending cfg() with capability predicates, which carried an openarch conclusion into openkal. Each designed a mechanism for a requirement that did not yet exist. A requirement that arrives later can be met by deferring the decision and recording the constraints, which costs far less than implementing the wrong mechanism early.
…mpiler as validation The core set is published; four questions were deferred and each blocks hosting a C library. This plan settles them and derives the interfaces that follow. The method is stated first because it was nearly got wrong. Deriving the interface set from what a compiler calls would have been the third instance of the error the specification already records: POSIX shaped by the C library of its time, WASI preview one shaped by POSIX, openkal shaped by a compiler. Programs validate a derivation; they do not produce one. Two measurements are load-bearing, and they point in opposite directions. GCC creates processes by spawning and calls neither fork nor execve. A specification that had copied the POSIX decomposition would have obliged an implementation on Windows to reproduce fork, which cannot be done faithfully and would have failed the specification's own admission criterion. The resource-derived form and the observed usage agree. GCC also assumes a global namespace of paths, which capability-based kernels do not provide. That is evidence about the program's portability assumptions rather than a reason to admit a global namespace, and it locates the path-resolution work where it belongs: in the C library, performed once. The two validation subjects form a stack rather than a pair. Porting musl is the enabling work; the compiler above it is then an end-to-end check that porting a C library once causes the software above it to run on every implementation. The capability mechanism is settled rather than deferred, by a rule that follows from a distinction the specification already draws: an operation that may be absent becomes an interface of its own, so that its absence is reported by the linker, while a property that varies is reported by a capability word, because a property cannot be called and an operation that is present and always fails is the defect clause 6.4 rejects. Also settles concurrency, ownership, and the interface inventory, and records why openkal.event stays reserved: readiness notification is where environments differ most, and a C library can be hosted without it.
…t the method A program above all eight interfaces was written and run. It exposed two points on which the specification was silent — whether the argument vector supplied to a spawn includes the started program's own name, and how enquiry reports a name that does not exist — and on both, two conforming implementations could have differed. Both were found in under an hour. Neither had been found by reading the text, twice, across two rounds. It exposed three defects in continuous integration alongside them, sharing one shape: a version stated twice and drifted, an assertion naming two of five suites, and a final step that had never executed because the step before it failed first. All four pipelines were green throughout. The document also records what the program had to be redesigned to avoid. Its first version started itself with a marker to distinguish parent from child; the marker did not arrive, because of the very defect the program existed to find, and it started itself without end. A conformance program must not have an unbounded failure mode, and least of all one armed by the defect it looks for.
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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Version 0.1 let the implementation provide the module a consumer imports, with
the specification package providing openkal.decl. for it to re-export.
Review identified this as a contradiction of what a specification is for, and
the identification was correct.
The justification does not survive examination. That arrangement existed solely
to make optional operations detectable through argument-dependent lookup, which
requires an implementation's declarations to be visible to the consumer — and
version 0.1 defined no optional operation. The mechanism served a requirement
that did not exist, and it was paid for with a real cost: the name a consumer
relies upon sat outside the specification's control.
0.2 restores the intended layering, verified: a backend that exports no module
builds and runs, and a missing implementation is reported by the linker naming
the undefined functions.
This is the third occurrence of one shape in this round. The first was
openkal.namespace, which merged two kinds of resource in order to unify naming;
the second was extending cfg() with capability predicates, which carried an
openarch conclusion into openkal. Each designed a mechanism for a requirement
that did not yet exist. A requirement that arrives later can be met by deferring
the decision and recording the constraints, which costs far less than
implementing the wrong mechanism early.