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

RFC discussion
1

Note: This discussion is continued from this thread.

Currently, the seL4 kernel ABI – the enumerations, structures, types, system calls, and object invocations needed to communicate between the kernel and user space – changes depending on the selected kernel build configuration and is not documented.

This has the following disadvantages:

  • seL4 software and the seL4 library (libsel4) must be aware of, and are tightly coupled to, the kernel build configuration. This complicates the build process and prevents the creation of software that is binary compatible with multiple configurations of a seL4 kernel.

  • It is difficult to create and maintain a new seL4 library (for example, to target seL4 in another programming language)

  • It is difficult to create dynamic systems on seL4

This RFC would propose specifying a fixed kernel ABI for each seL4 architecture in order to address those issues.

If implemented this would:

  • Remove the dependency on kernel configuration from libsel4. All enumerations, structures, types, system calls, and object invocations used to communicate with the kernel would have the same definition and binary representation for all kernel configurations on a specific architecture.

  • Increase the amount of information the kernel shares about its configuration with the root task at boot so the root tasks knows what functionality is available.

  • Make it easier to improve and expand the scripts and IDL used to generate libsel4 in the future

Questions on what to include in the RFC:

  • Should the ABI be defined in the RFC itself?

    • I think it would be a good excersize to do when writing the RFC to understand the issues involved; Would it be useful for reviewers of the RFC as well to see and review a concrete ABI and not just a description of how it will be created?

    • Since the ABI will be updated in the future without going through the RFC process maybe defining it in the RFC would set a bad expectation?

  • What level of backwards and forwards compatibility should the ABI provide?

  • How to introduce this without worsening the experience for developers of static systems who want to keep a tight coupling with their kernel configuration?

    • Keep constants in libsel4 that depend on the kernel configuration, while also providing them in the bootinfo to the root task? Would this be too confusing?

  • Should the ABI be provided in a machine-readable format?

  • What should the procedure be for updating the ABI?

2

I think doing this in the RFC might also constrain the implementation too much.

3

There are a number of constants that vary greatly as seL4 configuration changes such as the size of untyped required for a TCB. Whenever this structure is modified the values for these constants need to be re-determined for each configuration.

If we remove these constants from libsel4 and only provide them via the boot mechanism then we should be able to rely on the compiler to determine the exact number of bits for each structure (they can be determined when the structures are visible to the compilation unit which happens for the kernel but not libsel4). This would make maintaining these constants much easier but may effect verification.

4

Note that I’m not a verification engineer and may get some of the verification specifics slightly wrong.

A fixed kernel ABI for all configurations on a particular architecture is not something that is possible for seL4 at the moment. Providing an interface that works across multiple hardware/platform configurations would require a single kernel configuration to support them and this is not how the verification is currently approached. Each of seL4’s verified configurations target a single hardware/platform configuration. This specificity drasticially simplifies the proofs and also allows them to refer to a more accurate model of the platform/hardware.

The tradeoff is that changes to the hardware/platform configuration also require changes to the proofs and, because of correspondence requirements, also to the C source implementation of the kernel. As the kernel ABI is described by the C implementation of the kernel, the ABI can only target a single hardware/platform configuration at a time. There is tooling to make it easier to switch hardware/platform configurations across different kernel configurations, but this must all happen before the kernel is compiled; this is why there are lots of C preprocessor macros used in all the definitions.

This isn’t something that is impossible to change, but would require a very large investment into the verification to support it. We currently don’t prioritise this for the following reasons:

  • As the goal of seL4 is to provide low level access to system resources, it is not a goal of the ABI to abstract over them in all cases. This means that configuration options that affect what hardware features are available change the kernels ABI . The kernel typically only provides abstracted access to something if it is not possible to correctly delegate access to user-level while maintaining isolation properties, or if implementing something at user-level would lead to worse performance outcomes.
  • the seL4 ABI boundary also isn’t considered to be an interface that provides portability, or backwards compatiblitly. Any system that gets built on top of seL4 is going to have its own system environment of which seL4 is only a part of. If the goal of said system is to provide an application interface that is portable and forwards/backwards compatible across versions, then it should be implementing these features itself.
  • Making it possible to reuse existing binaries on different kernel configurations can be achieved by using user-level libraries that abstract over different configurations and versions.

As for trying to engineer the ABI definitions to coincidentally not conflict with each other across different hardware/platform configurations, this may be easier in some cases but harder in others. One example is that many of the enumerations, such as the invocation labels, intentionally have continuous values as this makes it a lot easier when doing conversions as a lot of checks can get generated automatically. Moving to a global name space would require a more complicated structure for mapping between labels and values and therefore more burden for proof maintenance.

Making it easier to call seL4 from other languages is still something that the libsel4 tooling should better support, but supporting native seL4 bindings in other languages would still require them to have similar tooling that libsel4 has for changing the ABI across different kernel configurations.

1 Like
5

I didn’t mean to suggest that it should do otherwise; the kernel config options would stay the same, but instead of them affecting the ABI, the kernel would return errors at runtime if any functionality that it does not support was requested.

That’s a fair point. I am trying to make the case that this change would benefit anyone using seL4 in another programming language and/or creating a dynamic system.

I didn’t intend to suggest the ABI be changed to abstract anything away. The existing interfaces would be exposed; instead of hiding some depending on the kernel configuration at compile time as you do now, non-supported things would return an error at runtime.

Certainly not today, and if that’s not something that you want to support or include in this RFC that’s fine – providing this is not what this proposal is about, but it is something that needs to have a position defined in the RFC if it gets created.

I do not think this is possible today, can you elaborate on how this might be accomplished?

Even if you hypothetically compiled a version of libsel4 for all possible ABI-affecting kernel configurations and packaged them together into a single library, there would be no way to tell which one to use at runitme.

Additionally, due to the large combination of ABI-affecting kernel configurations, even if this were possible I do not think it would be feasible.

Would it have an ongoing maintenance cost, or would it be a one-time cost to switch methodologies?

To restate my case that changing this is worthwile:

Requiring a seL4 kernel configuration to be known at compile time makes it extremely difficult to create seL4 libraries for another programming language.

There is no feasible way to make this easier that I am aware of without having a fixed ABI, because you can’t get rid of your dependency on the kernel configuration.

This infects all downstream or related libraries offering a seL4 target.

These problems are compounded for those interested in creating dynamic systems (even if they use the official libsel4 in C) or wanting to target lots of hardware, as the number of kernel configurations needed to be supported explodes.

The lack of a fixed ABI is hampering the adoption of seL4 in other progamming language and dynamic systems.

What more information do you need to decide if the tradeoff against the verification effort is worth it?

1 Like
6

Just to clarify this proposal one more (last?) time…

I am not proposing to change any API’s (outside of adding some error return codes where there may not be any today) or introduce any abstraction here.

Nor am I suggesting making any significant changes to the kernel or its verification.

I am absolutely not suggesting that the kernel be forced to expose the same functionality to all architectures or that functionality could not be added to the kernel in the future that is architecture-dependent.

The kernel proper would still be completely dependent on its configuration – the only change would be at the ABI level, where instead of its configuration affecting the ABI it would instead return error codes where functionality was requested that does not exist.

This change would make it feasible to create and maintain higher-level abstraction layers around the kernel behavior. I am arguing that today, without this change, this is not a feasible thing to do.

7

A possible solution that would require no change to the kernel and could even be made to work across a much wider range of kernel versions would be to provide a user-level library that can be linked (either statically or run-time a la VDSO) that provides a consistent C FFI API regardless of the kernel configuration or version.

8

I think the Kent’s reply is quit straight forward.

As far as I’m concerned, the syscall is a number, so two syscall in different platform may share a same number inside kernel. So the kenel couldn’t aware the syscall is belong to another platform, hence it can’t return an error message while it can’t be detected.
As seL4 just a general purpose micro-kernel, mostly use in real-time environment, the cross platform support doesn’t make sense in most of time. For example, PS4 can’t run most PS3’s games, because it decided to change platform to x86.
You still can do the cross platform support by moving these pseudo-syscall into a user-level PROSIX server, unify the call there. The ABI of seL4 can only do a static system without significant amount of work.

9

We could create our own seL4 API that is not configuration dependent, but that doesn’t address the problems which are caused by the kernel ABI being configuration-dependent.

Unless you’re suggesting we create our own seL4 ABI in a root task “shim”. In that case, we still have the same issues, just isolated to that root task. Plus the additional performance overhead of the shim.

10

I’m not proposing to add cross-platform support. The kernel ABI would remain different for each architecture.

11

You could get most of what you want with a library linked into applications which wraps the seL4 ABI. You can make that library API consistent across versions and make its implementation dependent on the kernel configuration but its interface could be made independent of the kernel configuration.

libsel4utils does this to some degree such as its wrappers for the MCS API.

It wouldn’t be too hard to expand this concept to a complete library that would have almost no overhead where the interface can map directly onto the underlying API and that can push dealing with features not supported by the underlying configuration to run-time.

This library could also be made to be entirely accessible via a C FFI from other languages more easily than the seL4 ABI could be directly.

12

I’m currently going through a rust implementation of the AOS project, so the problem domain being discussed here is of interest to me, though it’s unfamiliar and brand new to me as well. Though I’m not so sure what sort of meaningful contribution I can make directly, a more community-engagement oriented idea occurs to me.

I was thinking, perhaps, of adding a channel to mattermost where the more free-flowing thoughts related to this language topic get discussed. I expect that it would start with mostly my questions and me sharing the approaches I’m making, though I hope for it to expand from there. I don’t know if this idea captures the intent of mattermost, though.

If you have any questions about what it’s like for an inexperienced person from the outside to use rust with seL4, don’t hesitate to ask.

13

There exists the exact same problem in the Linux Kernel, which is extensively discussed here.

Although even some Kernel maintainers were open to Rust code, no viable solution fix semantic incompatibility (functionality changing) was found.
What you instead see is ebpf as fixed specification being used to keep the ABI base stable and fragmentation small (also for usage of Rust code inside ebpf).
Since I do expect significant changes until Risc5 and the timing channel issues get resolved for the next 5+ years, I would be skeptical to rely on alot functionality.
Keep in mind that the underlying proof and semantic might also change, which you also need to track.

Finally Rust has very nice in-build proofs for memory safety (soon up to macro level) and parallelization, but sadly kinda poor support for external proof systems due to the young age.
Probably thats why there is no explicit commitment (yet) from Gernot Heiser.

How crazy would it be to fork the minimum ebpf and use that ?

14

Random idea: would it be possible to make at least the architecture-independent syscalls (seL4_Call, seL4_Reply, etc.) have a fixed ABI per architecture, and ideally across kernel versions with warnings in the changelog when the ABI changes?

This feels like it should be doable (maybe it’s even already the case in practice and it’s just not advertised as such), and would already allow all tasks that do not directly interact with the hardware to have a fixed ABI. Tasks that interact directly with the hardware would still have to go through libsel4 or an equivalent of such, but these will probably be more tied to which version of sel4 is running and all the gritty details anyway, so it’s less bad an issue IMO

15

In general, the ABI for system calls (seL4_Send, seL4_Recv, seL4_NBSend, seL4_NBRecv, seL4_Call, seL4_Reply, and seL4_ReplyRecv) and their aliases (seL4_Signal, seL4_Wait, and seL4_Poll) tend to remain relatively stable with most changes being made to invocations on kernel objects. Any changes to these should be documented in the changelog.

One issue is that the versioning of the API reflects the whole kernel API so it is not as easy tell from version number alone when compatibility is maintained across versions.

In addition to the system call ABI, there are two kernel objects with user level APIs that you would want to remain stable: endpoints and notifications, as these form the basis of all communication between threads. As with the syscalls, these remain fairly stable and any change will be documented in the changelog.

Fundamentally, most software should only care about the syscalls, endpoints, and notification objects and shouldn’t interact directly with other objects. There would be a core set of system services that do interact directly with other objects and capabilities that would need to track changes in the kernel.

Having said all of that, there are changes in the works with respect to the Mixed Criticality Systems (MCS) work done by @anna.lyons which resolve a number of issues with the system call API. These include changes to the system call ABI for all platforms, the semantics of different system calls, the introduction of new system calls, and changes to the behavior of notifications and endpoints.

The behavior of notifications and endpoints pre-MCS can be emulated using the new semantics. So if an abstraction over the API were being used rather than the API directly, then the common abstraction could be updated without needing to change every user of the API.

Fundamentally, seL4 is not designed as an abstraction over the system. seL4 is a minimal set of features to provide isolation and integrity between mutually distrusting user-level components. Trying to build on it using the assumption that it behaves like consistent abstraction or treat it in the same way you would treat a kernel that does attempt to abstract a complete operating system is not recommended.

The only way you are going to be able to maintain a consistent user-level API or ABI is to build the abstractions at user level with user-level components, and seL4 provides you all the tools necessary to do that.

1 Like
16

What if instead of a fixed kernel ABI, we provided a C library that provides a stable ABI? From my perspective, it would be much better to have one such library that everyone uses, rather than each user of seL4 having to write their own.

17

That would certainly be much easier to provide and maintain. It sounds like it would make sense to turn libsel4 (and maybe a few other components such as sel4runtime) into that library.

18

Agreed. That would work well with automatic binding generation.

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.
20

As libsel4 is purely a library linked at user level, this only needs to be a symbol provided by the library rather than a syscall. I’m also unsure what you mean by ‘embedded into the kernel image’.