Hi, Here's what I'm doing to run seL4 on an Ariane processor (64 bit) with 16 MB RAM (and some internal BRAM from the FPGA). So far I've only tried the CAmkES adder example. This is the memory layout: 0x80000000: 256K BRAM for OpenSBI 0x80200000: 256K BRAM for ELF-Loader 0x84000000: 16M external RAM for seL4 & servers The BRAM sizes could be reduced to 128kB and 64kB. By default, the final image created by the build system includes the CPIO archive with the DTB and the root server. I modified it to not link the generated archive.o file. Instead, I read the CPIO archive from a memory-mapped flash. This allows me to place the ELF-Loader in a BRAM instead of the SRAM and gives more freedom over the memory layout. https://github.com/seL4-drone-project/seL4_tools/tree/seL4-drone-project There are 4 options in elfloader-tool/CMakeLists.txt * ElfloaderExistingArchive * ElfloaderRelocateArchive * ElfloaderArchiveStart * ElfloaderArchiveEnd Note that there's an option to copy the flash memory to the RAM. This is only there as a workaround for a bug in my FPGA design. shoehorn.py will still complain, but you can disable it by setting IMAGE_START_ADDR. The value doesn't matter because it's not used for RISC-V builds. I set it to 0x80200000. These are the memories in the DTS: memory@80000000 { device_type = "memory"; reg = <0x0 0x80000000 0x0 0x00040000>; }; memory@80200000 { device_type = "memory"; reg = <0x0 0x80200000 0x0 0x00040000>; }; memory@84000000 { device_type = "memory"; reg = <0x0 0x84000000 0x0 0x01000000>; }; hardware_gen.py in the seL4 repository adds an offset for the reserved bootloader section to the first memory, which causes an assertion to fail (start < end) in seL4, so I don't include it in the generated header file: https://github.com/seL4-drone-project/seL4/commit/3a7966ca919157be43e8e1d291... capdl-loader reports 10MB of untyped memory. It probably won't get you to 2MB, but maybe it helps.

The 2MiB large page used for BBL is protected by Physical Memory Protection, preventing any part of that region of physical memory being used by supervisor or user modes. Get Outlook for Androidhttps://aka.ms/ghei36 ________________________________ From: porter.188@osu.edu Sent: Tuesday, January 19, 2021 9:00:49 AM To: devel@sel4.systems Subject: [seL4] Re: Reducing memory footprint - RISC-V I still have some questions regarding this project: I'm still a little confused about the starting point: 0x80200000. I see that I need to add 0x80200000 to the image size/memory usage to get the end point. One of the builds the end point is 0x80396F48. That's about 3.58 MB. Am I understanding correctly that there is 2 MB reserved for the BBL and then another ~1.6 MB for the image/application? Is it possible to move this up in memory? That means give the BBL less than 2 MB and put the payload after that before 0x80200000? I did give this a try and ran into alignment issues. So I don't know if this is possible. I've made some progress on my efforts to reduce the memory footprint (< 2 MB). Here are some items I've found: 1. In shoehorn.py lines 207-209 (https://github.com/seL4/seL4_tools/blob/2f97243012afb42975d29a24752675bf68f0...) add 4 MB for seL4test. These lines can be commented and this immediately reduced the footprint from ~7 MB default, to ~3.5 MB. 2. The items in the archive.o are the kernel.elf, kernel.dtb, and hello.elf (rootserver). The two elf files can be stripped after the build and this reduces the footprint further. Additionally, the elfloader can be stripped before putting this into Berkeley Boot Loader for RISC-V. This again reduces the footprint a little. 3. I've noticed that the memory footprint of hello the rootserver application, takes about 1.18 MB. This lines up exactly with what is in the ELF files PT_LOAD mem_sz fields. _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems

On Tue, 2021-01-19 at 18:32 +0000, porter.188@osu.edu wrote:

Is there any way around that? I can modify BBL to put the payload at a lower address than 0x80200000 still properly page aligned, just not on the mega page size. Also, the elfloader in seL4 relies on this alignment. I suppose that would need to be rewritten as well.

Or is that this is not possible at all?

A few contributing factors to what is going on here: 1) BBL Will always align an integrated payload to a large page (2MiB on rv39 and rv48) with the next boundary after the start of BBL itself being 0x80200000. https://github.com/riscv/riscv-pk/blob/master/bbl/payload.S#L12 2) The elfloader has a hardcoded base to start at 0x80400000, but is actually loaded at 0x80200000, Due to risc-v being generally position independent, this doesn't appear to break anything. https://github.com/seL4/seL4_tools/blob/master/elfloader-tool/src/arch-riscv... 3) The generated memory regions for seL4 skip the first mega page entirely, assuming it is only used for BBL (although the hardware_gen.py script appears to assume that this size is always 2MiB when it is actually 4MiB for rv32...) https://github.com/seL4/seL4/blob/master/tools/hardware/config.py#L45-L51 4) The rv32 seL4 kernel requires that the kernel image falls entirely within a single 2MiB page, for rv64 it must vall within a single 1GiB region with the way that the self-mapping is implemented. 5) The kernel defines a KERNEL_ELF_PADDR_BASE and KERNEL_ELF_BASE which indicate the start of the kernel image in physical and virtual memory respectively. This is placed 64MiB after the start of physical memory (and I am unsure as to why such a large region is left). https://github.com/seL4/seL4/blob/master/include/arch/riscv/arch/32/mode/har... https://github.com/seL4/seL4/blob/master/include/arch/riscv/arch/64/mode/har... 6) The elfloader requires that its own ELF is aligned to 2MiB (even for rv32). https://github.com/seL4/seL4_tools/blob/master/elfloader-tool/src/arch-riscv... 7) The elfloader also requires that it falls within the boundary of a single page table of large pages (i.e. in a single 4GiB region on 32bit or 1GiB region on 64bit). 8) BBL enables PMP protection of its own image excluding its own payload. Given that the BBL itself only use and protect 76KiB at the start of memory, we could be using everything immediately after that. BBL could be modified to place its payload immediately after itself in physical memory and if that payload is position-independent, as elfloader actually appears to be, that would not be an issue. The elfloader would still need to be modified such that when it maps *itself* into virtual memory, it accounts for any misalignment rather than simply throwing an error. This change would not be all that difficult. The kernel ELF then either needs to be placed after the BBL payload *OR* the elfloader needs to be architected such that the kernel location overlapping with its own payload is not an issue. The latter option also removes an apparent upper limit on the size of the initial task image of about 64MiB. Another alternative may be to allow the kernel not to have a statically assigned physical base address. Ultimately it seems that you would at least need to modify BBL to prevent it from putting any payload at the 2MiB boundary. You'd then need to at least modify the mapping routines in the elfloader to deal with finer-grained alignment when remapping itself. To then fit the kernel into that 2MiB region along with the boot loader and the elf loader, you'd then need to modify the static physical address the kernel assumes for itself or enable it to be set dynamically. This former option would be straightforward but would also limit the size of the user image as the entire elfloader payload needs to fit below the base kernel ELF address.

I need to run something in less than 2 MB if possible. If BBL doesn't do it, then what is the alternative? Do I write my own bootloader?

From what I can see, with minimal patching to BBL, some modifications to elfloader, and adjusting the constant definition in seL4, you should be able to fit everything into 2MiB if your initial task is small enough. The most difficult part there would be the elfloader modifications. I'm not certain how much of that would be accepted upstream for any of those repositories however. Hope all of this helps. Cheers, Curtis