Quick update - I had to build the toolchain with the "--with-arch=rv32gc --with-abi=ilp32" flags. seL4test now runs and passes all but the FPU tests. -----Original Message----- From: Ortiz, Baltazar Sent: Wednesday, July 31, 2019 2:01 PM To: 'Zhuang, Siwei (Data61, Kensington NSW)' ; devel@sel4.systems Subject: RE: [seL4] SeL4 on 32 bit RISC-V Thanks for the response! I tried using the latest sel4test and got the same assertion failure. I once again had to remove the two CONST labels from thread.h to fix the below error.

[196/214] Building C object kernel/CMakeFiles/kernel.elf.dir/kernel_all.i.obj FAILED: kernel/CMakeFiles/kernel.elf.dir/kernel_all.i.obj ccache /home/baltazar/riscv/bin/riscv32-unknown-linux-gnu-gcc --sysroot=/host/sel4test-upstream-riscv/build32 -I../kernel/include -I../kernel/include/32 -I../kernel/include/arch/riscv -I../kernel/include/arch/riscv/arch/32 -I../kernel/include/plat/spike -I../kernel/include/plat/spike/plat/32 -Ikernel/gen_config -Ikernel/autoconf -Ikernel/gen_headers -Ikernel/generated -march=rv32ima -mabi=ilp32 -D__KERNEL_32__ -nostdinc -nostdlib -O2 -DHAVE_AUTOCONF -DDEBUG -g -ggdb -mcmodel=medany -fno-pic -fno-pie -fno-stack-protector -fno-asynchronous-unwind-tables -std=c99 -Wall -Werror -Wstrict-prototypes -> Wmissing-prototypes -Wnested-externs -Wmissing-declarations -Wundef -Wpointer-arith -Wno-nonnull -ffreestanding -MD -MT kernel/CMakeFiles/kernel.elf.dir/kernel_all.i.obj -MF kernel/CMakeFiles/kernel.elf.dir/kernel_all.i.obj.d -o kernel/CMakeFiles/kernel.elf.dir/kernel_all.i.obj -c kernel/kernel_all.i In file included from /host/sel4test-upstream-riscv/kernel/src/api/faults.c:18: ../kernel/include/arch/riscv/arch/kernel/thread.h:27:1: error: 'const' attribute on function returning 'void' [-Werror=attributes] void CONST Arch_activateIdleThread(tcb_t *tcb); ^~~~

I'm going to build the 64 bit version of the toolchain and see if that works any better than the 32 bit. Worst case, I'll give the obsolete version of the toolchain another shot, though I had trouble getting it set up in the past. Thanks, Baltazar -----Original Message----- From: Devel On Behalf Of Zhuang, Siwei (Data61, Kensington NSW) Sent: Monday, July 29, 2019 10:28 PM To: devel@sel4.systems Subject: Re: [seL4] SeL4 on 32 bit RISC-V Hi Baltazar, To get that version of seL4 working, you should use an obsolete version of the RISC-V toolchain. Follow the instructions here, https://docs.sel4.systems/Hardware/RISCV.html If you prefer to use the upstream riscv-gnu-toolchain, you need to checkout the latest sel4test-manifest. In either case, modifying the seL4 source code shouldn't be required. Regards, Siwei On Mon, 2019-07-29 at 21:36 +0000, Ortiz, Baltazar wrote:

Hi all,

I'm looking into getting seL4 booting on 32 bit RISC-V. Currently working with seL4test 10.1.1, QEMU 4.0.0, and an upstream copy of riscv-gnu- toolchain (is there a specific release I should try?).

I'm able to get seL4 to build after deleting a few CONST labels that the compiler was complaining about, but when I try to run the simulation script, I get the following output:

...

./simulate -b /home/baltazar/qemu/build/riscv32-softmmu/qemu-system- riscv32 /home/baltazar/qemu/build/riscv32-softmmu/qemu-system-riscv32 -machine spike_v1.10 -nographic -s -serial mon:stdio -m size=2000M -kernel images/sel4test-driver-image-riscv-spike bbl loader /host/sel4test-upstream-riscv/tools/riscv-pk/machine/minit.c:74: assertion failed: !(read_csr(misa) & fd_mask) Power off

Are there any tricks for getting this working right now?

Thanks,

Baltazar ________________________________ Notice: This email and any attachments may contain proprietary (Draper non- public) and/or export-controlled information of Draper. If you are not the intended recipient of this email, please immediately notify the sender by replying to this email and immediately destroy all copies of this email. ________________________________ _______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel ________________________________ Notice: This email and any attachments may contain proprietary (Draper non-public) and/or export-controlled information of Draper. If you are not the intended recipient of this email, please immediately notify the sender by replying to this email and immediately destroy all copies of this email. ________________________________

Thanks! -----Original Message----- From: Hesham Almatary Sent: Friday, August 9, 2019 5:30 AM To: Ortiz, Baltazar ; seL4 Subject: Re: [seL4] SeL4 on 32 bit RISC-V On Fri, 2 Aug 2019 at 17:07, Ortiz, Baltazar wrote:

Quick update - I had to build the toolchain with the "--with-arch=rv32gc --with-abi=ilp32" flags. seL4test now runs and passes all but the FPU tests.

The seL4 RISC-V port doesn't support FPU yet. You will need "--with-arch=rv32imac --with-abi=ilp32" or --enable-multilib for the FPU tests not to generate FPU instructions.

-----Original Message----- From: Ortiz, Baltazar Sent: Wednesday, July 31, 2019 2:01 PM To: 'Zhuang, Siwei (Data61, Kensington NSW)' ; devel@sel4.systems Subject: RE: [seL4] SeL4 on 32 bit RISC-V

Thanks for the response! I tried using the latest sel4test and got the same assertion failure. I once again had to remove the two CONST labels from thread.h to fix the below error.

...

[196/214] Building C object kernel/CMakeFiles/kernel.elf.dir/kernel_all.i.obj FAILED: kernel/CMakeFiles/kernel.elf.dir/kernel_all.i.obj ccache /home/baltazar/riscv/bin/riscv32-unknown-linux-gnu-gcc --sysroot=/host/sel4test-upstream-riscv/build32 -I../kernel/include -I../kernel/include/32 -I../kernel/include/arch/riscv -I../kernel/include/arch/riscv/arch/32 -I../kernel/include/plat/spike -I../kernel/include/plat/spike/plat/32 -Ikernel/gen_config -Ikernel/autoconf -Ikernel/gen_headers -Ikernel/generated -march=rv32ima -mabi=ilp32 -D__KERNEL_32__ -nostdinc -nostdlib -O2 -DHAVE_AUTOCONF -DDEBUG -g -ggdb -mcmodel=medany -fno-pic -fno-pie -fno-stack-protector -fno-asynchronous-unwind-tables -std=c99 -Wall -Werror -Wstrict-prototypes -> Wmissing-prototypes -Wnested-externs -Wmissing-declarations -Wundef -Wpointer-arith -Wno-nonnull -ffreestanding -MD -MT kernel/CMakeFiles/kernel.elf.dir/kernel_all.i.obj -MF kernel/CMakeFiles/kernel.elf.dir/kernel_all.i.obj.d -o kernel/CMakeFiles/kernel.elf.dir/kernel_all.i.obj -c kernel/kernel_all.i In file included from /host/sel4test-upstream-riscv/kernel/src/api/faults.c:18: ../kernel/include/arch/riscv/arch/kernel/thread.h:27:1: error: 'const' attribute on function returning 'void' [-Werror=attributes] void CONST Arch_activateIdleThread(tcb_t *tcb); ^~~~

I'm going to build the 64 bit version of the toolchain and see if that works any better than the 32 bit. Worst case, I'll give the obsolete version of the toolchain another shot, though I had trouble getting it set up in the past.

Thanks,

Baltazar

-----Original Message----- From: Devel On Behalf Of Zhuang, Siwei (Data61, Kensington NSW) Sent: Monday, July 29, 2019 10:28 PM To: devel@sel4.systems Subject: Re: [seL4] SeL4 on 32 bit RISC-V

Hi Baltazar,

To get that version of seL4 working, you should use an obsolete version of the RISC-V toolchain. Follow the instructions here,

https://docs.sel4.systems/Hardware/RISCV.html

If you prefer to use the upstream riscv-gnu-toolchain, you need to checkout the latest sel4test-manifest.

In either case, modifying the seL4 source code shouldn't be required.

Regards, Siwei

On Mon, 2019-07-29 at 21:36 +0000, Ortiz, Baltazar wrote:

...

Hi all,

I'm looking into getting seL4 booting on 32 bit RISC-V. Currently working with seL4test 10.1.1, QEMU 4.0.0, and an upstream copy of riscv-gnu- toolchain (is there a specific release I should try?).

I'm able to get seL4 to build after deleting a few CONST labels that the compiler was complaining about, but when I try to run the simulation script, I get the following output:

...

./simulate -b /home/baltazar/qemu/build/riscv32-softmmu/qemu-system- riscv32 /home/baltazar/qemu/build/riscv32-softmmu/qemu-system-riscv32 -machine spike_v1.10 -nographic -s -serial mon:stdio -m size=2000M -kernel images/sel4test-driver-image-riscv-spike bbl loader /host/sel4test-upstream-riscv/tools/riscv-pk/machine/minit.c:74: assertion failed: !(read_csr(misa) & fd_mask) Power off

Are there any tricks for getting this working right now?

Thanks,

Baltazar ________________________________ Notice: This email and any attachments may contain proprietary (Draper non- public) and/or export-controlled information of Draper. If you are not the intended recipient of this email, please immediately notify the sender by replying to this email and immediately destroy all copies of this email. ________________________________ _______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

---

Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel ________________________________ Notice: This email and any attachments may contain proprietary (Draper non-public) and/or export-controlled information of Draper. If you are not the intended recipient of this email, please immediately notify the sender by replying to this email and immediately destroy all copies of this email. ________________________________ _______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

-- Hesham ________________________________ Notice: This email and any attachments may contain proprietary (Draper non-public) and/or export-controlled information of Draper. If you are not the intended recipient of this email, please immediately notify the sender by replying to this email and immediately destroy all copies of this email. ________________________________