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

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 : 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