Tuesday, October 31, 2017

RISC-V RTEMS port is Upstream


Having the RISC-V's GCC and Binutils upstream, as well as the increasing popularity and support RISC-V is getting pushed us to upstream RTEMS/RISC-V port, and it is gonna be part of the upcoming major RTEMS release.

RTEMS (The Real-Time Executive for Multiprocessor Systems) is a contemporary Real-time embedded OS, started as a project back in 1988. Since then, it has been used in space (e.g. by NASA), military, robotics and many other embedded applications.

This blog post gives a brief status of the porting efforts (that's upstream), as well as a quick how to build/run the port on Spike.


[RTEMS Kernel/OS]

  • Compatible with RISC-V priv-1.10.
  • Has interrupt support.
  • Only tested on Spike.
  • Only timer ISR is handled.
  • Uses HTIF for console IO, and power off.
  • Works entirely in Machine mode, standalone (doesn't rely on bbl).
  • Tier-2 RTEMS Architecture (For info about different RTEMS Tiers see this).
  • BSD-2 License.
  • Some of the code is copied from riscv-pk. 
The port is divided into 2 main parts:
  • CPU Port (riscv32, and riscv64)
    • General CPU port that can be used by different RISC-V-based boards. 
    • Fairly complete (but not optimized) for single core systems.
  • BSP port (Board Support Package).
    • generic_riscv that runs on Spike.
      • Only timer and console drivers are implemented.
    • generic64_riscv 64-bit of generic_riscv.
  • No cache or MMU management.
  • No FPU support.

 [RTEMS Source Builder] Toolchain

RTEMS has, maintains and tests its own toolchain for each CPU architecture (target), which relies on source code upstream from GNU (and others). For example, by using RSB to build RTEMS/RISC-V toolchain, RSB will fetch GCC and Binutils from GNU repos/servers, extract, build and install them for RTEMS. This is an example output after installing the RISC-V/RTEMS toolchain:

Installed riscv*-rtems toolchain (RSB)

We currently use the following revisions/releases for the RISC-V/RTEMS toolchain:

Tools built by RSB for riscv32

Furthermore, Spike/fesvr can be built using RSB (fetched from GitHub).

 [RTEMS Tester]

Scripts have been added to RTEMS Tester in order to be able to run the > 500 RTEMS tests on Spike. Currently, most of the tests pass on Spike.

Final output after running RTEMS Tester on riscv32 port


Binary sizes

With -Os flag:

minimum.exe (simplest RTEMS app that does nothing)

➜  build riscv32-rtems4.12-size riscv32-rtems4.12/c/riscv_generic/testsuites/samples/minimum/minimum.exe
   text    data     bss     dec     hex filename
  33944    8433 268393028       268435405       fffffcd riscv32-rtems4.12/c/riscv_generic/testsuites/samples/minimum/minimum.exe

hello.exe (Hello World App - Uses console driver, printf)
➜  build riscv32-rtems4.12-size riscv32-rtems4.12/c/riscv_generic/testsuites/samples/hello/hello.exe   
   text    data     bss     dec     hex filename
  75612    7768 268352004       268435384       fffffb8 riscv32-rtems4.12/c/riscv_generic/testsuites/samples/hello/hello.exe

ticker.exe (Uses clock driver and console driver, printf)
➜  build riscv32-rtems4.12-size riscv32-rtems4.12/c/riscv_generic/testsuites/samples/ticker/ticker.exe 
   text    data     bss     dec     hex filename
  66480    8744 268360196       268435420       fffffdc riscv32-rtems4.12/c/riscv_generic/testsuites/samples/ticker/ticker.exe



Final output after running RTEMS Tester on riscv32 port


Final output after running RTEMS Tester on riscv64 port


Hardware Platforms: We need to test on actual hardware in order to level up RISC-V/RTEMS port to a Tier-1 architecture (the highest, on par with ARM and x86). Issues with current RISC-V HW platforms (that I know):
  • HiFive1: We had a student working on HiFive1 port this summer part of Google Summer of Code. The main challenge was the memory size limitation.
  • FPGAs: Currently, I'm aware of the Rocket Chip as an FPGA/HW target. It relies on bbl as a bootloader. Furthermore, it changes to S-Mode before jumping to the payload entry. That's not the case for RTEMS as it works in M-Mode.
  • Do you have a RISC-V HW implementation: Please get it touch, we need more RISC-V/HW BSPs (with reasonably big enough memory for RTEMS e.g. > 128KiB). Only M-Mode is needed (for CPU) and console/timer (for BSPs). It would be also great if it can be remotely powered off/reset (for RTEMS Tester).

SMP support: Adding SMP support is easy for OSes working in S-Mode (just calling sbi_xxx functions). However, I've not investigated yet how feasible it is to implement SMP support for M-Mode-based implementations.

QEMU: Hasn't been updated for a while (and not upstream), and the latest privileged mode is 1.9. Tried to run the port on it though, but didn't work.

GDB: Would be great if it's gonna be upstream soon (with target sim?). RSB tries to build GDB for all targets/architectures, which is used part of RTEMS Tester as well (and to run basic sample apps).

Bugs: Will try to go over failed tests from RTEMS Tester and try to fix the bugs, unless someone beats me to it.

Quick HowTo

 To build the tools from source, RTEMS Source Builder is needed.

$ git clone git://git.rtems.org/rtems-source-builder.git
$ cd 

Setup development directories and export PATH:

$ mkdir -p ~/development/rtems
$ export PATH=$HOME/development/rtems/4.12/bin:$PATH
$ export RTEMS_DEV=$HOME/development/

[Build Toolchain]


rtems-source-builder git:(master) ✗ cd rtems/
$ ../source-builder/sb-set-builder --log=l-riscv32.txt --prefix=$RTEMS_DEV/rtems/4.12 4.12/rtems-riscv32


$ ../source-builder/sb-set-builder --log=l-riscv64.txt --prefix=$RTEMS_DEV/rtems/4.12 4.12/rtems-riscv64

[Build Spike]

rtems-source-builder git:(master) ✗ cd  bare
$ ../source-builder/sb-set-builder --log=spike --prefix=$RTEMS_DEV/rtems/4.12 devel/spike

[Build RTEMS]

Clone RTEMS:

 $ git clone git://git.rtems.org/rtems.git
 $ cd rtems && ./bootstrap -p && ./bootstrap 

To build generic_riscv BSP (32-bit)

$ cd .. && mkdir build && cd build
$ ../rtems/configure --target=riscv32-rtems4.12  --enable-rtemsbsp=riscv_generic --enable-tests=samples

To build generic64_riscv BSP (64-bit)

$ cd .. && mkdir build64 && cd build64
$ ../rtems/configure --target=riscv64-rtems4.12  --enable-rtemsbsp=riscv64_generic --enable-tests=samples



➜  build spike --isa=RV32IMAFDC -m0x10000000:0x10000000 riscv32-rtems4.12/c/riscv_generic/testsuites/samples/hello/hello.exe


hello.exe (Hello World App - Uses console driver, printf)

➜ build64 spike -m0x10000000:0x10000000 riscv64-rtems4.12/c/riscv64_generic/testsuites/samples/hello/hello.exe
Hello World
LD ***


(Uses clock driver and console driver in a multithreading test)

➜ build64 spike -m0x10000000:0x10000000 riscv64 rtems4.12/c/riscv64_generic/testsuites/samples/ticker/ticker.exe
TA1 - rtems_clock_get_tod - 09:00:00 12/31/1988
TA2 - rtems_clock_get_tod - 09:00:00 12/31/1988
TA3 - rtems_clock_get_tod - 09:00:00 12/31/1988
TA1 - rtems_clock_get_tod - 09:00:05 12/31/1988
TA1 - rtems_clock_get_tod - 09:00:10 12/31/1988
TA2 - rtems_clock_get_tod - 09:00:10 12/31/1988
TA1 - rtems_clock_get_tod - 09:00:15 12/31/1988
TA3 - rtems_clock_get_tod - 09:00:15 12/31/1988
TA1 - rtems_clock_get_tod - 09:00:20 12/31/1988
TA2 - rtems_clock_get_tod - 09:00:20 12/31/1988
TA1 - rtems_clock_get_tod - 09:00:25 12/31/1988
TA3 - rtems_clock_get_tod - 09:00:30 12/31/1988
TA1 - rtems_clock_get_tod - 09:00:30 12/31/1988
TA2 - rtems_clock_get_tod - 09:00:30 12/31/1988

[Run RTEMS Tester]



➜  build $RTEMS_DEV/rtems/rtems-tools/tester/rtems-test --log=riscv_generic.txt --rtems-bsp=riscv_generic --rtems-tools=$RTEMS_DEV/rtems/4.12 --timeout=40 riscv32-rtems4.12/c/riscv_generic/testsuites

➜  build $RTEMS_DEV/rtems/rtems-tools/tester/rtems-test --log=riscv64_generic.txt --rtems-bsp=riscv64_generic --rtems-tools=$RTEMS_DEV/rtems/4.12 --timeout=40 riscv64-rtems4.12/c/riscv64_generic/testsuites

Saturday, June 24, 2017

[Update] seL4/RISC-V SMP support | seL4/RISC-V Tutorials Release

Updates (since 03062017)


A new unofficial 24062017 release of seL4, libraries and seL4 Tutorials.

  • SMP support, tested on Spike with 2 - 9 cores:
    • seL4 is using a big kernel lock.
    • Only reschedule IPI (set affinity) is provided.
    • Relying on SBI to do other remote operations.
    • SBI doesn't provide VADDR-> ASID -> HART operation.
    • Using tp register to hold per-core IPC buffer addresses.
  • Ported seL4-tutorias to RISC-V. This means:
    • People can learn more about both seL4/RISC-V doing the tutorials.
    • Lack of RISC-V/Spike user-level timer (or another S-timer) is an issue. seL4 (being a microkernel) is not supposed to provide a timer API, rather, user-level apps should have their own HW timer and device drivers.
  • More tests are passing on sel4test now after:
    • SMP support.
    • Re-adding a supervisor timer (for seL4 scheduling).
    • [154/154] Tests pass (8 more tests pass after multicore and timer support).
    • All libraries, kernel are rebased to latest seL4's revisions.

seL4 Tutorials 


sel4-tutorials [1] is the first recommended entry point for people who want to learn and get hands-on experience on seL4 and its libraries.  This repo [1] contains slides, docs and code tutorials with commented instructions and tasks that take you from writing a seL4 hello world application to doing IPC in a multithreading environment, now on RISC-V.

hello-3 exercise showing 2 threads doing IPC communication

 [1] https://github.com/heshamelmatary/sel4-tutorials/tree/RISCVUnofficialRelease-24062017



seL4test is a comprehensive unit and functional testing suite for seL4 and can be useful when porting to new platforms or adding new features.

It can be used as a reference how to develop a big project on seL4. A new riscv_smp_defconfig config file for RISC-V is added to test SMP support. Instructions how to run it are provided in this blog post.

For this release that contains SMP, use:

$repo init -u git@github.com:heshamelmatary/sel4riscv-manifest.git -m sel4test-24062017.xml



This work is my personal/independent effort (during spare time) and it's not related to Data61/CSIRO/TS Group (that maintains seL4), until it gets upstream.

Saturday, June 3, 2017

sel4test/RISC-V unofficial release - priv-1.10 - spec-2.3

Major updates since 2015

  • - It's now based on seL4's master (rather than experimental) branch, which means it makes use of architecture-independent verified code.
  • - Instead of earlier 32-bit support, it's now based on 64-bit RISC-V.
  • - Compatible with latest RISC-V priv-1.10 and user-2.2/3 specs.
  • - sel4test and libraries are ported and passing 146/146 tests.
  • - Tested on Spike and Rocket Chip on FPGA soft-float (also previous version worked with QEMU 1.9.1).
  • - Implements seL4's fastpath support.
  • - 3 page mappings are supported (Sv39: 4KiB, 2MiB and 1GiB).
  • - Relies on SBI from unmodified riscv-pk/bbl to emulate M-mode (same as riscv-linux).

Work in progress

  • - Upstreaming seL4/RISC-V port.
  • - Multicore support.
  • - Research-wise, I've been working on adding CHERI support to RISC-V (Spike) as an extension, and aiming to experiment seL4 on it.

TODO list

  • - Upstream the kernel (and libraries).
  • - Add debug and benchmark support.
  • - Release sel4bench.
  • - Port sel4-tutorial to RISC-V (Start Guide for new comers/learners).
  • - External interrupt handling and work with PLIC.

Quick How to

  1. Install riscv64 tools (priv-1.10)
  2. Get sel4test/RISC-V (using repo, for more info see [1])
  3. $repo init -u git@github.com:heshamelmatary/sel4riscv-manifest.git -m sel4test-03062017.xml
    $repo sync
  4. $make riscv_defconfig && $make 
  5. build riscv-pk/bbl with path to images/sel4test-driver-image-riscv-spike (from 4)
  6.  run spike with bbl image generated from 5.
sel4test/RISC-V running on Spike


This work is of my personal/independent effort (during spare-time) and it's not related to Data61/CSIRO/TS Group (that maintains seL4), until it gets upstreamed.


[1]  https://wiki.sel4.systems/Getting started

Tuesday, December 15, 2015

RTEMS port for RISC-V, with/without seL4 support

This is a brief update about RTEMS port progress to RISC-V.

RTEMS port for RISC-V architecture (currently riscv32) runs Hello World and Ticker (with sim timer), on both Spike simulator and seL4 microkernel (two cores). The github repo of the port is here [1].

There are two BSPs currently:

1) riscv_generic: This BSP is intended to run in Machine mode, and has been tested on Spike.

To run it configure and build RTEMS with:

$ ../rtems/configure --target=riscv32-rtems4.12 --disable-posix --disable-networking --disable-itron --enable-rtemsbsp=riscv_generic

$ make

Command to run on Spike:

$ spike --isa=RV32 riscv32-rtems4.11/c/riscv_generic/testsuites/samples/ticker/ticker.exe

2) riscv_seL4: This BSP assumes it runs with support of seL4 microkernel, and it runs in Supervisor mode (on another core). seL4 application would allocate and map memory for it from its untyped memory (userspace), before off-loading it to another core.

To run it with seL4, you need to get seL4-rtems project first, configure it, but before building seL4 two shell variables have to be exported so that seL4 can know about where/which RTEMS image to load.

$ export RTEMS_IMAGE="Absolute path to the RTEMS .exe image"
$ export RTEMS_IMG_NAME="Name of the RTEMS image you would use, i.e hello.exe, ticker.exe"

For how to build/run seL4-rtems project follow the exact same instructions here [2] with the only difference replacing:

repo init -u https://github.com/heshamelmatary/sel4riscv-manifest.git


repo init -u https://github.com/heshamelmatary/sel4riscv-rtems-manifest.git

Which fetches the seL4-rtems project.

And finally run both seL4 and RTEMS on Spike:

$ spike --isa=RV32 -p2 images/sos-image-riscv-spike 


Monday, October 12, 2015

A talk about my GSoC project with lowRISC - ORCONF Conference 2015

It was great to give a talk about my Google Summer of Code project with lowRISC at the fourth instance of ORCONF conference held this year in CERN, Geneva, Switzerland. ORCONF is concerned with open-source digital design hardware and embedded systems, motivated by the great success of open-source software. lowRISC, my GSoC organization, which aims to produce a fully open hardware system, was one of the participant organizations over there.

During my talk at ORCONF 2015
The conference was of great success, having about 30 talks ranging from physics, up to software. There was also an interesting discussion about how to adapt open-source software licenses to hardware designs.

lowRISC, based in the University of Cambridge, has first participated in GSoC this year as an umbrella organization to include open-source projects like: RISC-V, seL4, Rump Kernels, jor1k and YosysJS. I was fortunate enough to be one of the three students who have been accepted to work with lowRISC out of 52 GSoC applicants there. This gave me the chance to have a great rewarding experience working on Porting seL4 to RISC-V/lowRISC.

During GSoC’15 program, I had the chance to work on the world's first formally verified operating system kernel—seL4, which is also open-source, to port it to run on lowRISC/RISC-V that are open hardware architectures. The project also implied some coding with the open-source muslc C library. I even worked on some digital design tasks out of curiosity. My mentor, Stefan Wallentowitz, and the lowRISC organizers: Alex Bradbury and Robert Mullins have been of great help even after GSoC has ended.

The outcome of the project was good enough to present about at ORCONF. After my talk (see the slides), I got some positive feedbacks and future ideas, had interesting discussions, and spoke with people who want to build on, and make use of, my project.

Right after I returned back to York, I received my GSoC T-Shirt and certificate.

GSoC'15 T-Shirt and certificate 
I’d like to take this opportunity to thank GSoC, lowRISC and ORCONF organizers, and I am looking forward to continuing to work/participate with them.

Saturday, July 25, 2015

[HOWTO] Build and run seL4 on RISC-V targets

This post gives instructions how to build seL4 to run on RISC-V targets (currently Spike simulator and Rocket Chip/FPGA). The default, and currently only, application is SOS [1] which is a simple operating system running on top of seL4. This means other simple applications can be developed based on this seL4/RISC-V port.


The development environment is Linux, you need the following tools installed before pursuing with the build/run process:
  • riscv32-unknown-elf- [2]
  • Spike  [3]
  • fesvr [4]
  • Python
  • git
  • gpg
Optional (If you want to build/run seL4 on Rocket Chip/FPGA):
  • Xilinx/Vivado 
  • Scala
  • Chisel

Build/Run seL4/RISC-V

Assuming all the previous packages are installed, the build system (and steps) are exactly the same as of other seL4 projects here [5], but it uses my own repos because the port is not upstream (yet).

1- Get repo
mkdir -p ~/bin
export PATH=~/bin:$PATH
curl https://storage.googleapis.com/git-repo-downloads/repo > ~/bin/repo
chmod a+x ~/bin/repo
2- Fetch seL4/RISC-V project
The following commands fetche seL4 microkernel, SOS, tools, and all the libraries required to build a complete seL4/RISC-V system (currently SOS project):

mkdir seL4riscv
cd seL4riscv
repo init -u https://github.com/heshamelmatary/sel4riscv-manifest.git
repo sync 
3- Build seL4/RISC-V project
The default project is SOS that runs on Spike, RV32 mode, SV32 memory system. First type:
make riscv_defconfig
Make sure ROCKET_CHIP option is  UNCHECKED:

make menuconfig
seL4 kernel > seL4 System
You should find the sos image under images directory.

SOS binary images

 4- Run seL4/RISC-V (SV32) on Spike (and jor1k):

Running SOS on spike is easy, just type the following command and you should see some interesting output (for more details about SOS see [6]):

make simulate-spike

SOS running on seL4 on RISC-V 

seL4/RV32/SV39 (the same image output from the previous steps) can run on jor1k [8], however jor1k for RISC-V is still under development, and may not work properly.

* Build and run seL4/RISC-V (SV39) on Spike/Rocket

Building seL4 for RV64 follows almost the same previous steps, the differences are followed:

1- Assuming you got all the required repos (see steps 1 and 2 above), change the kernel branch to point to sel4Rocket:

cd kernel/
git checkout sel4Rocket
cd ..

2- This time make sure ROCKET_CHIP is CHECKED

make riscv_defconfig
make menuconfig

ROCKET_CHIP config option checked
Save and exit.

3- build and run seL4/RV64/SV39

make simulate-spike64

The same seL4/SV39 image can run on Rocket Chip on FPGA. Just follow the instructions how to build the Rocket Chip on FPGAs [7]. Note that you have to build all the FPGA-related components along with the software tools (zynq-fesvr)  from scratch to get the latest privileged-spec compliant tools (the prebuilt images are not updated).

If you've followed the previous steps and found any issues, just let me know. Your feedback, bug reports, feature-addition requests are welcomed.


[1] seL4 on RISC-V is running SOS (Simple Operating System)
[2] https://github.com/riscv/riscv-gnu-toolchain/
[3] https://github.com/riscv/riscv-isa-sim
[4] https://github.com/riscv/riscv-fesvr
[5] http://sel4.systems/Download/
[6] http://www.cse.unsw.edu.au/~cs9242/14/project/framework.shtml
[7] https://github.com/ucb-bar/fpga-zynq
[8] http://jor1k.com/jor1k/demos/riscv.html

Friday, July 17, 2015

seL4 runs on Rocket Chip (RISCV/FPGA)


After running on Spike simulator, seL4 can now run on the latest up-to-date version of Rocket Chip code on FPGA, the first hardware platform that seL4/RISC-V port can run on. Moreover, seL4 runs on the online jor1k emulator [1]. This can be considered as a starting point for both RISC-V and seL4 to experiment some new security-related and/or scalability solutions based on the flexibility to easily modify the hardware according to seL4 requirements (or vice versa), given that both are open-source, and under research development.


Previously seL4/RISC-V was only running on RV32 (RISC-V 32-bit mode) which assumes SV32 (Page-Based 32-bit Virtual-Memory Systems) to work on. SV32 was only supported by Spike simulator, and that's why seL4 could, previously, only run there. The 32-bit seL4 has been progressing till the point that it is able to run, not only a hello world application, but it can run another simple operating system above it [2] that can fork other applications. That seems to be a good progress, but it would be better to have it running on a real hardware.

The issue was that the only open-source RISC-V hardware is currently Rocket Chip, which doesn't support 32-bit (SV32) mode, only RV64 (SV39 and SV48 virtual memory systems that run only on RISC-V 64-bit mode), and since there's no 64-bit support on seL4 (yet), it would have been hard and time-consuming to re-factor the entire seL4 code to run 64-bit code (including pointers, variables, data structures, scripts, etc).

How does 32-bit seL4 run on RV64/SV39?

The workaround was to keep running 32-bit seL4, but with modifications to the RISC-V low-level target-dependent MMU handling code to run on RV64/SV39 memory system without touching the target-independent seL4 code. This was possible because both RV32 and RV64 execute 32-bit fixed instructions. So basically, only the memory configuration was required (apart from HTIF code) to be modified to make this step possible, including initialization and page-tables layout. This means that seL4 is still being built and compiled using riscv32-* toolchain.

The seL4 components that had to be changed are:
  • vspace.c
  • elfloader
vspace.c is an architecture-dependent core file (for all seL4 ports) for MMU handling in seL4 microkernel. A new file, vspace64.c was added to run on RV64 mode. The difference between the 32-bit version is that the 4KiB pages should now follow 3 levels page-tables implementation instead of just 2 levels (SV32).

elfloader is just statically mapping the seL4 microkernel image at 2-level page-table, 2MiB pages granularity, while it maps seL4 at 4MiB granularity (just one level page-table) on SV32
RV32/SV32 implementation of seL4 can cover 4GiB address space, while RV64/SV39 extends this to 2^9 GiB. seL4 port only uses 256 MiB, so this amount of SV39 memory wasn't needed. This made it simpler by using only two entries in the first-level page-table: one for the first GiB (reserved for applications use), and the second one for the kernel page-tables. The first-level page-table (AKA page-directory) is then shared between all applications, but write accesses is only  exclusive to seL4 microkernel. New applications (address spaces) are just allocating/filling 2nd-level (and if necessary 3rd-level to provide 4KiB pages) page-tables without worrying about the first level. During context switches, address space change is done by writing the address of the second-level page table (allocated by applications) into the first entry of the page-directory rather than updating the sptbr register. This solution has a limitation of restricting application address space mapping to the first GiB virtual address range, but it has the benefit of optimizing both memory and time. Memory optimization is achieved by the fact that there is no need to allocate 3-level page-tables when creating a new task, only two (or even one) as with SV32. From timing perspective, seL4 is copying the kernel mapping for each created task, this is no longer needed since this kernel mapping lies on a separate 2nd entry, covering the 256 MiB of the second GiB virtual memory of the page directory. The SV39 mapping of seL4 is shown in the next figure.

seL4 mapping on RV64/SV39

Next, I will be working on cleaning up the code, writing some tutorials how to build and run seL4 on different RISC-V platforms, fixing bugs and adding more features.