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

Hi Arun, 32-bit RISC-V is not scheduled on our roadmap currently, unless it's required for another project. Code for 32-bit RISC-V is there for the kernel and user-level, and currently compiles. But the kernel doesn't successfully boot and needs investigation. A community contribution is welcome :). Thanks Anna. ________________________________ From: Devel on behalf of Arun Thomas Sent: Thursday, 19 April 2018 1:17 PM To: Mcleod, Kent (Data61, Kensington NSW) Cc: devel@sel4.systems Subject: Re: [seL4] Announcing seL4 9.0.1: with RISC-V support Congrats on the new release! I'm very excited to see upstream support for RISC-V. Out of curiosity, is there a timeline for 32-bit RISC-V support? Thanks, Arun On Wed, Apr 18, 2018 at 12:11 AM mailto:Kent.Mcleod@data61.csiro.au> wrote: We are pleased to announce initial RISC-V support for the UC Berkeley Spike simulator platform. Instructions are available for building and running the seL4 test suite on RISC-V: https://docs.sel4.systems/Hardware/RISCV ?See an online copy of the release notes at: https://docs.sel4.systems/sel4_release/seL4_9.0.1 https://docs.sel4.systems/camkes_release/CAmkES_3.4.0 # seL4 Version 9.0.1 Release Announcing the release of `seL4 9.0.1` with the following changes: 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` * Initial prototype RISC-V architecture port. This port currently only supports running in 64-bit mode without FPU or or multicore support on the Spike simulation platform. There is *no verification* for this platform. ## Upgrade Notes --- # Full changelog Refer to the git log in https://github.com/seL4/seL4 using `git log 9.0.0..9.0.1` # More details See the [9.0.1 manual](http://sel4.systems/Info/Docs/seL4-manual-9.0.1.pdf) included in the release or ask on the mailing list!# CAmkES Version camkes-3.3.0 Release ---- # CAmkES Version camkes-3.4.0 Release Announcing the release of `` with the following changes: camkes-3.4.0 2018-04-18 Using seL4 version 9.0.1 ## Changes ## Upgrade Notes --- # Full changelog Use `git log camkes-3.3.0..camkes-3.4.0` in https://github.com/seL4/camkes-tool # More details See the [documentation](https://github.com/seL4/camkes-tool/blob/camkes-3.4.0/docs/index.md) or ask on the mailing list! _______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

Hi, Congratulations, this is excellent news! It appears that the simulator currently used is riscv-qemu. Is there a version that can run on spike? If not, what would be needed to get it running on spike? --prashanth

On 18:23 Tue 24 Apr, Hesham Almatary wrote:

The same image from the sel4test build that runs on qemu can just run unmodified on Spike.

After you build sel4test (and from the same directory) just run:

"$spike images/sel4test-driver-image-riscv-spike"

Thanks Hesham, this is very good to know. It turns out that with the default build of the spike master version as of today, there's one test that fails: Test FRAMEEXPORTS0001 failed All tests pass in qemu. --prashanth

On 08:49 Wed 25 Apr, Hesham Almatary wrote:

Right, this tests all RISC-V's frame sizes, including Giga pages. Since the default memory given by Spike to sel4test is only 2 GiB, that might not be enough for this test. If you tell Spike to have 4 GiB of memory (similar to QEMU), it should pass.

e.g. "spike -m4096 images/sel4test-driver-image-riscv-spike"

Indeed, that fixes it, thanks! --prashanth