[seL4] Announcing seL4 9.0.1: with RISC-V support

Matthew.Brecknell at data61.csiro.au Matthew.Brecknell at data61.csiro.au
Thu Apr 19 13:52:59 AEST 2018


Hi Hinnerk,

>From the seL4 9.0.1 release notes:
> 9.0.1 2018-04-18: BINARY COMPATIBLE
>
> ## Changes
>  * On 64-bit architectures, the `label` field of `seL4_MessageInfo` is
>    now 52 bits wide. User-level programs which use any of the following
>    functions may break, if the program relies on these functions to mask
>    the `label` field to the previous width of 20 bits.
>      - `seL4_MessageInfo_new`
>      - `seL4_MessageInfo_get_label`
>      - `seL4_MessageInfo_set_label`

>From Hinnerk van Bruinehsen <n8fear at stackptr.de>:
> I've got a question about the release notes:
> Can it really be called binary compatible if it can introduce breakage
> in userland?
> I think that the required changes to userland are quite minimal but I'd
> understand binary compatible in a way that replacing a 9.0.0 binary by a
> 9.0.1 binary should'nt introduce any troubles at all, which according to
> the patch notes isn't really the case (at least on 64-bit arches.

I can understand the confusion. When I wrote those notes, I was trying
to be concise, but that means I omitted some context.

The label field of seL4_MessageInfo is used in a few ways:
- By the kernel to signal fault and error types to user space.
- By user space to indicate to the kernel which invocation to perform on
  a kernel object.
- By user space fault handlers to indicate to the kernel whether the
  faulting thread should be restarted.
- By user space to pass some information to another thread during IPC.

Since the kernel never tries to use more than 20 bits in the label
field, the first case is not affected by the change.

For the second and third cases, it is possible to construct user-space
programs which behave differently with this change, by setting any of
the most-significant 32 bits of the message info register. Previously,
the kernel would ignore those bits, but now will not. However, our view
is that those programs are already abusing the API, so we don't consider
this an incompatible change. For example, programs which previously
performed invocations with any of those extra bits set will now fail due
to an invalid invocation label.

For IPC, masking the label field only ever occurred in seL4_libs in user
space, so this change really is binary compatible for this case. For
programs recompiled against the new seL4_libs, it is possible to observe
a difference, if the sender attempts to set high bits in the label
field, but the receiver expects them *not* to be set. But again, we
think such programs are far enough outside the range of normal seL4_libs
usage that we don't really consider this a source incompatibility.

Hope that helps!
Matt



More information about the Devel mailing list