seL4 in GLAS ============ This document desribe the procedure to run seL4 in GLAS on Morello FVP. Prerequisite ------------ Setup the Kirsch toolchain container - see :ref:`toolchain-setup`. Prepare the workspace --------------------- Multiple repos are required for this project. Prepare a folder as your workspace. This folder will be shared with the Kirsch Docker container later. 1. Clone `seL4 (our version) `_ as ``sel4``. .. note:: To boot the second kernel in the low memory (staring ``0x80000000``), we need to mark the later part of the region invisible to seL4. In this case, use branch ``limited-ram-for-sel4``, where seL4 sees RAM size ``0x40000000``. 2. Clone `seL4 Microkit (our version) `_ as ``sel4-microkit``. 3. Clone `the main repo `_ as ``sel4-in-glas``. Compile the seL4 Microkit ------------------------- Enter the toolchain container with the workspace mapped to ``\src``: .. code-block:: shell docker run --mount type=bind,source=$(pwd),target=/src --rm -ti registry.ethz.ch/project-opensockeye/kirsch-toolchain /bin/bash Inside the container shell: .. code-block:: shell cd /src/sel4-microkit python3 -m venv pyenv ./pyenv/bin/pip install --upgrade pip setuptools wheel ./pyenv/bin/pip install -r requirements.txt The following command build the Microkit for Morello FVP platform: .. code-block:: shell PATH="/tools/arm-gnu-toolchain/bin:$PATH" ./pyenv/bin/python3 build_sdk.py --sel4="../sel4" --filter-boards morello_fvp --no-doc --no-archive --tool-rebuild .. note:: To build more boards such as ``qemu_arm_virt``, supply more options to ``--filter-boards``. See ``build_sdk.py`` for available boards. Not all boards can be built or work. For example, the RISC-V ones currently cannot be built without the RISC-V toolchain. .. note:: If only seL4 is modified, removing ``--tool-rebuild`` can save some build time. However, if Microkit script is modified, ``--tool-rebuild`` is needed. The built SDK is in ``/src/sel4-microkit/release/microkit-sdk-1.2.6``. Target: wordle_part3 -------------------- This target launches seL4 with Wordle programs (``wordle_part3.system``) as well as booting ``helloworld/helloword.c`` on a second core. Inside the container, in ``/src/sel4-in-glas``, run ``make run_wordle_part3``. Alternatively, outside the container, at your workspace: .. code-block:: shell docker run --mount type=bind,source=$(pwd),target=/src --rm -ti registry.ethz.ch/project-opensockeye/kirsch-toolchain make -C /src/sel4-in-glas run_wordle_part3 .. note:: The ATF build assets are left inside the container. To save time building it, consider using a persistent contaienr. In the output, you should see the following: .. code-block:: shell # ATF NOTICE: Booting Trusted Firmware ... # seL4 loader LDR|INFO: Flags: 0x0000000000000001 seL4 configured as hypervisor LDR|INFO: Kernel: entry: 0x0000008080000000 ... LDR|INFO: region: 0x00000008 addr: 0x0000000080269000 size: 0x0000000000001070 offset: 0x000000000026c2f0 type: 0x0000000000000001 LDR|INFO: region: 0x00000009 addr: 0x00000000f0000000 size: 0x0000000000000349 offset: 0x000000000026d360 type: 0x0000000000000001 # This last region is the binary for the second kernel ... LDR|INFO: Boot CPU ID (0x00000000) LDR|INFO: PSCI version 0x00010001 LDR|INFO: Boot the secondary kernel (entry 0x00000000f0000000) on CPU ID (0x00000100) LDR|INFO: enabling MMU **************************************** Hello world from CPU 0x00000100 at EL2 **************************************** LDR|INFO: jumping to kernel # seL4 kernel Bootstrapping kernel ... # User programs SERIAL SERVER: starting WORDLE SERVER: starting CLIENT: starting Welcome to the Wordle client! [ ] [ ] [ ] [ ] [ ] ... # The answer is "hello" The console is connected to telnet. To exit, use ``Ctrl + ] quit``. Target: virtio_blk ------------------ This target generates a random 5K file as ``bin/virtio_blk.load.bin``, runs the virtio-blk server and a demo client to read and print all its content (``virtio_blk.system``). .. code-block:: shell docker run --mount type=bind,source=$(pwd),target=/src --rm -ti registry.ethz.ch/project-opensockeye/kirsch-toolchain make -C /src/sel4-in-glas run_virtio_blk Target: vmm_minimal ------------------- This target launches a minimal VM on Morello FVP (``vmm_minimal.system``). .. code-block:: shell docker run --mount type=bind,source=$(pwd),target=/src --rm -ti registry.ethz.ch/project-opensockeye/kirsch-toolchain make -C /src/sel4-in-glas run_vmm_minimal .. note:: The VM images (kernel, DTB, initrd) are loaded through virtio-blk becuase ATF FIP cannot handle large BL33 that has images embedded. So far we haven't found a way to load data directly into the Morello FVP main memory (``--data`` does not work, possibly due to the tagged memory?). The loading can take several minutes. Target: demo --------------- This demo launch ``demo.c`` (``demo.system``) as well as booting ``cheriette_morello_loader.bin`` on a second core. .. note:: ``cheriette_morello_loader.bin`` is not part of ``sel4-in-glas`` repo. You need to add it manually. If using ``.bin`` instead of ``.elf``, the kernel entry address need to be specified in the Makefile. To build Cheriette for the seL4 GLAS demo, generate the build script with ``python3 generators/build.py --demo-enable True > build/build.ninja``, and build the Morello target ``ninja -C build morello_all``. Then, copy ``build/loader_morello.bin`` to the ``sel4-in-glas`` directory as ``cheriette_morello_loader.bin``. Inside the container, in ``/src/sel4-in-glas``, run ``make demo``. Alternatively, outside the container, at your workspace: .. code-block:: shell docker run --mount type=bind,source=$(pwd),target=/src --rm -ti registry.ethz.ch/project-opensockeye/kirsch-toolchain make -C /src/sel4-in-glas run_demo Target: clean ------------- .. code-block:: shell docker run --mount type=bind,source=$(pwd),target=/src --rm -ti registry.ethz.ch/project-opensockeye/kirsch-toolchain make -C /src/sel4-in-glas clean Tracing ------- To enable tracing on target ``wordle_part3``, use target ``trace_wordle_part3``. The same applies to other targets. In the code, trace starts after ``asm volatile ("hlt 0x1" ::: "memory");``. Insert this code to the desirable place. Note that executing this instruction without tracing enabled results in an error. The trace is stored in ``logs/trace.log``. It can be very long, you may want to use command like ``cat logs/trace.log | tail -n +200000 | head -n 100000 > trace_part.log`` to skip the first 200000 lines and take 100000 lines, before you open the whole file. Note that tracing will significantly slow down execution!