Pre-RFC: Specify a fixed kernel ABI for each architecture

RFC discussion
19

So an idea that came to mind is:

  • libseL4 is the only stable entry point for calling into seL4. Its API and ABI will be backwards-compatible. libseL4 is built as part of the kernel build process, and ideally will be formally verified at some point.

    There are two cases where the API and ABI may change in a backwards-incompatible way:

    1. If the major version number of seL4 is bumped, compatibility of the libseL4 API and ABI is not guaranteed. Such bumps are expected to be very rare (~once per decade or less).
    2. If a feature is marked as experimental, its API and ABI may change in minor releases. Experimental features are not enabled by default.

  • libseL4 is complete: every feature compiled into the kernel is exposed in the libseL4 API. It is possible that a feature (such as virtualization) is built into the kernel, but is found to be unsupported by the hardware the kernel runs on. In such cases, the corresponding libseL4 calls will return an error at run-time.

  • The system call ABI is not stable, with one exception: there is an seL4_Version syscall that returns information about the kernel configuration. This syscall has two purposes:

    1. It is used by libseL4 to check that it is running on a matching build of seL4. If it is not, all calls to libseL4 will fail.
    2. If we decide to allow libseL4 to be been embedded into the kernel image, seL4_Version would be used to load it.