WasmEdge on seL4

    In this article, we demonstrate how to run WasmEdge on the seL4 RTOS, there are two parts:

    1. Guest Linux OS on seL4: This is the controller of WasmEdge runtime, which will send wasm program to WasmEdge runner that is a agent on seL4 to execute.
    2. WasmEdge runner on seL4: This is the wasm program runtime, which will execute the given wasm program from Guest Linux OS.

    The figure below illustrates the architecture of the system.

    This demo is based on the seL4 simulator on Linux.

    Hardware:

    • at least 4GB of RAM
    • at least 20GB of disk storage (the wasmedge_sel4 directory will contain over 11 GB of data after the following installation completes)

    Software: Ubuntu 20.04 with dev tools packages (ep. Python) installed. We recommend the (See a list of installed apt packages). Or, you could use our Docker image (see the ).

    And this will clone and build our wasmedge on seL4 to an image.

    After finishing the build script, you will have a folder sel4_wasmedge.

    If this automatic installation completed successfully, skip over the manual installation information and proceed to boot wasmedge-sel4

    The above all-in-one script will work in most cases. However, if your system resources were stressed and you encountered an error such as ninja: build stopped: subcommand failed please note that you can decrease the parallelization of the install by explicitly passing in a -j parameter to the ninja command (on the last line of the build.sh file). You see, Ninja runs the most amount of parallel processes by default and so the following procedure is a way to explicitly set/reduce parallelization.

    Manually fetch the `wasmedge-sel4 repository.

    1. cd ~
    2. git clone https://github.com/second-state/wasmedge-seL4.git
    3. cd wasmedge-seL4

    Manually edit the build.sh file.

    1. vi build.sh

    Add the following -j parameter to the last line of the file i.e.

    1. ninja -j 2

    Run the edited `build.sh file.

    1. ./build.sh

    Once this manual installation is complete, follow along with the following steps; boot wasmedge-sel4

    Boot wasmedge-seL4

    1. cd sel4_wasmedge/build
    2. ./simulate

    Expected output:

    1. $ ./simulate: qemu-system-aarch64 -machine virt,virtualization=on,highmem=off,secure=off -cpu cortex-a53 -nographic  -m size=2048  -kernel images/capdl-loader-image-arm-qemu-arm-virt
    2.   paddr=[6abd8000..750cf0af]
    3. No DTB passed in from boot loader.
    4. Looking for DTB in CPIO archive...found at 6ad18f58.
    5. Loaded DTB from 6ad18f58.
    7. ELF-loading image 'kernel' to 60000000
    8.   paddr=[60000000..60242fff]
    9.   vaddr=[ff8060000000..ff8060242fff]
    10.   virt_entry=ff8060000000
    11. ELF-loading image 'capdl-loader' to 60245000
    12.   paddr=[60245000..6a7ddfff]
    13.   vaddr=[400000..a998fff]
    14.   virt_entry=408f38
    15. Enabling hypervisor MMU and paging
    16. Jumping to kernel-image entry point...
    18. Bootstrapping kernel
    19. Warning: Could not infer GIC interrupt target ID, assuming 0.
    20. Booting all finished, dropped to user space
    21. <<seL4(CPU 0) [decodeUntypedInvocation/205 T0xff80bf85d400 "rootserver" @4006f8]: Untyped Retype: Insufficient memory (1 * 2097152 bytes needed, 0 bytes available).>>
    22. Loading Linux: 'linux' dtb: 'linux-dtb'
    24. ...(omitted)...
    25. Starting syslogd: OK
    26. Starting klogd: OK
    27. Running sysctl: OK
    29. done.
    30. Starting network: OK
    31. [    4.086059] connection: loading out-of-tree module taints kernel.
    32. [    4.114686] Event Bar (dev-0) initalised
    33. [    4.123771] 2 Dataports (dev-0) initalised
    34. [    4.130626] Event Bar (dev-1) initalised
    35. [    4.136096] 2 Dataports (dev-1) initalised
    37. Welcome to Buildroot
    38. buildroot login:

    Enter root to login

    1. buildroot login: root

    Expected output:

    Execute wasm examples

    Example A: nbody-c.wasm

    Run nbody simulation.

    1. wasmedge_emit /usr/bin/nbody-c.wasm 10

    Expected output:

    1. [1900-01-00 00:00:00.000] [info] executing wasm file
    2. -0.169075164
    3. -0.169073022
    4. [1900-01-00 00:00:00.000] [info] execution success, exit code:0

    Example B: hello.wasm

    1. wasmedge_emit /usr/bin/hello.wasm

    Expected output:

    1. [1900-01-00 00:00:00.000] [info] executing wasm file
    2. hello, sel4