- Devel - lists.sel4.systems

Announcing release v0.2 of Neptune OS: a Windows NT personality for the seL4 microkernel
by Dr. Chang Liu, PhD. 12 May '24

12 May '24

Dear seL4 community, I'm announcing the release of v0.2 of Neptune OS, an operating system that I have been developing that aims to create a Windows NT personality on top of the seL4 microkernel, by implementing the upper layer of the Windows kernel called the NT Executive, as well as Windows kernel drivers, as userspace processes under seL4. For those that remember the release of v0.1 two years ago and have been wondering, yes, the project is still alive. I have been a bit busy with postdoc work (academia is hard!!) last year but finally got a bit of free time lately to get enough work done that I think is interesting enough to warrant a v0.2 release. The project can be found on github (https://github.com/cl91/NeptuneOS) The biggest feature of the v0.2 release is a (I hope) reasonably complete file system stack supporting read-ahead and write-back caching, that includes a FAT12/16/32 file system driver and a floppy controller driver, both of which are ported over from ReactOS (but running in userspace instead of kernel space). I'll explain the technical points below but you can watch a short video (https://www.youtube.com/watch?v=o3FLRnkh0ic) that demonstrates the basic file system commands, including cd, dir, copy, move, del, md, and mount/umount. Arguably the biggest challenge for a userspace file system stack is minimizing the performance penalties of the additional context switches. There are radical solutions to this problem along the lines of Unikernels that require linking the FS code with the applications. These solutions are not very practical for everyday desktop or server OSes. On traditional OSes there is FUSE on Linux/Unix which is often regarded as having inferior performance compared to equivalent kernel-mode drivers. To some extent this problem is inevitable, as context switches are always more expensive than function calls, no matter how much you optimize the former. However, that doesn't mean we can't optimize our OS design so that the performance penalties of running file systems in userspace are small enough that the benefit of userspace file systems outweighs their performance cons. The key to this performance goal I believe is an efficient cache design. Indeed, for FUSE it is possible to tune the cache parameters to drastically increase its performance (see [1] and the citation therein). On Neptune OS we cache aggressively: not only do we cache the underlying block device pages, we also maintain the relationship between file regions and their underlying disk regions. In other words, the primary role of the file system driver is to translate an offset of a file object into an offset of the underlying storage device, and this relationship is cached since they are not expected to change, at least for currently open files. Furthermore, we cache file attributes as well as the file hierarchy itself, so that if a process opened a file and the file system driver returned a valid handle, we do not need to query the FS driver again (at least not before the first process closes the handle) when another process opens the same file with the same attributes (because we know it exists and know about its attributes). Of course, we need to be careful when things get closed/deleted/moved, etc, so we need a mechanism to synchronize information with the file system driver process. This is done by sending messages using the seL4 IPC. What is amazing is the fact that despite these changes to the inner workings of the NT cache manager, not to mention the fact that all drivers are now running in userspace, the Windows kernel driver API remains largely unchanged, so that it is indeed possible to port the relevant ReactOS drivers to our architecture without doing too much work (I believe I spent three to four man-weeks worth of work porting the FAT file system itself). The vast majority of work is in fact removing code rather than writing new code, because of the simplifications of locking and other synchronization issues that simply disappear when drivers run in userspace. For those who are interested in knowing more about our architecture and are perhaps interested in porting drivers from ReactOS, I am in the process of writing a book (found under the docs of the github repo) called "Neptune OS Developer Guide" that explains all these things. Note this is very much a work-in-progress. In addition to the cache manager work, in order for the file system stack to function, several other system components must be implemented, most notably DMA and Win32 SEH (structured exception handling). Our DMA architecture supports both PCI bus mastering and the weird ISA DMA that must go through the ISA DMA controller. The latter requires managing the so-called "map registers" that must be shared across different ISA devices. Again we find that the Windows kernel API can be adapted to a seL4-based userspace driver model almost straightforwardly. This is perhaps not so surprising, because NT was allegedly originally designed as a microkernel OS (this is inevitably an urban legend, but early NT design documents refer to the code beneath the NT Executive as the "microkernel", so there is reason to believe). To summarize, what I hope is that with the design outlined above, we can in fact have a practical, reasonably performant userspace file system stack without resorting to radical departures from traditional desktop/server computing paradigms. Of course, it's ridiculous to talk about performance for floppy disk controllers, so the primary goal of the next release is to port the ATA/AHCI hard disk drivers from ReactOS to Neptune OS, in order to produce a valid benchmark against equivalent kernel mode designs. Anyway, if you read so far, I hope you find the work interesting (I personally do!). If you have any comments, or even better if you ran the code and found bugs/issues, please do open an issue in the github repo. Thank you! [1] https://medium.com/@xiaolongjiang/linux-fuse-file-system-performance-learni… --- Dr. Chang Liu, PhD. github.com/cl91/NeptuneOS

2 1

seL4 multicore boot failed on arm64
by Leonid Meyerovich 10 May '24

10 May '24

Hello, I run my seL4 application on 4 core ARMv8. Recently I have developed some more application code (I mention it because file system size is increased an I believe it may change boot time) and from time to time I observed that boot process failed (stuck after the following print) calling schedule calling activate thread kernel boot done.. CPU=1 calling schedule calling activate thread kernel boot done.. CPU=2 calling schedule calling activate thread kernel boot done.. CPU=3 Booting all finished, dropped to user space calling schedule calling activate thread kernel boot done.. CPU=0 Some time I see that only 2 CPU have been booted (like CPU1 and CPU3, or CPU2 and CPU3) Last print is the last one in init_kernel() function Thanks you, Leonid

2 3

Building seL4test 12.1.0 fails on Ubuntu 22.04 (WSL2)
by Ben McCart 09 May '24

09 May '24

I have run into the following build error when running ninja to build seL4test (following instructions at: https://docs.sel4.systems/GettingStarted#setting-up-your-machine) Here is what I get for output. Any suggestions on a work-around? (Do I have the wrong version of a python tool or library?) -- [65/263] Generating circular_includes_valid FAILED: kernel/circular_includes_valid /home/dev/seL4test/build-x86/kernel/circular_includes_valid cd /home/dev/seL4test/build-x86/kernel && /home/dev/seL4test/kernel/tools/circular_includes.py --ignore kernel_all_copy.c < kernel_all.i && touch circular_includes_valid Traceback (most recent call last): File "/home/dev/seL4test/kernel/tools/circular_includes.py", line 74, in <module> sys.exit(main(args)) File "/home/dev/seL4test/kernel/tools/circular_includes.py", line 61, in main while file_stack[-1] != header: IndexError: list index out of range [66/263] Invoking muslc build system /home/dev/seL4test/projects/musllibc/src/prng/seed48.c:6:40: warning: argument 1 of type ‘short unsigned int *’ declared as a pointer [-Warray-parameter=] 6 | unsigned short *seed48(unsigned short *s) | ~~~~~~~~~~~~~~~~^ In file included from /home/dev/seL4test/projects/musllibc/src/prng/seed48.c:1: /home/dev/seL4test/projects/musllibc/include/stdlib.h:133:25: note: previously declared as an array ‘short unsigned int[3]’ 133 | unsigned short *seed48 (unsigned short [3]); | ^~~~~~~~~~~~~~~~~~ /home/dev/seL4test/projects/musllibc/src/unistd/getcwd.c: In function ‘getcwd’: cc1: warning: function may return address of local variable [-Wreturn-local-addr] /home/dev/seL4test/projects/musllibc/src/unistd/getcwd.c:9:14: note: declared here 9 | char tmp[PATH_MAX]; | ^~~ ninja: build stopped: subcommand failed.

2 2

seL4 developer hangout reminder
by Birgit Brecknell 28 Apr '24

28 Apr '24

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Wed 1 May, 8:00 UTC. For your local date and time please see https://sel4.systems/contact/. Zoom link: https://unsw.zoom.us/j/82640784431 Birgit Brecknell seL4 Foundation Project Coordinator birgit(a)sel4.systems <mailto:birgit@sel4.systems> bbrcknl(a)gmail.com <mailto:bbrcknl@gmail.com>

1 0

seL4 summit: deadline extension to 29 April 2024
by Birgit Brecknell 22 Apr '24

22 Apr '24

The deadline to submit a presentation to the seL4 summit 2024 [0] has been extended by 1 week. You now have until 29 April 2024 to propose a talk [1], by uploading an abstract of one page or less to the submission portal [2]. Looking forward to receiving your proposals. We want to hear about your cool seL4 work! And spread the word! If you want to hear about specific seL4 work, ping people around you or let us know at summit(a)sel4.systems. [0] https://sel4.systems/Foundation/Summit/2024/ [1] https://sel4.systems/Foundation/Summit/2024/cfp [2] https://sel4.systems/Foundation/Summit/2024/submit Birgit Brecknell seL4 Foundation Project Coordinator birgit(a)sel4.systems <mailto:birgit@sel4.systems> bbrcknl(a)gmail.com <mailto:bbrcknl@gmail.com>

1 0

Question about LionsOS
by Isaac Beckett 20 Apr '24

20 Apr '24

Hello! Looking at the LionsOS website and documentation you posted, it seems like Lions is an operating system built using Microkit out of components/drivers that use the sDDF? Do I have the right shape of things in my head? Also, would sDDF drivers for a static OS like Lions (or other OS built in Microkit, since that’s what’s it’s built for) be potentially portable to other operating systems using the seL4 kernel and sDDF? Like, if I design a non-static operating system that uses sDDF drivers, could I use existing code from Lions or would I face issues with code assuming that the system’s components can’t change at runtime? Thanks, Isaac

11 26

seL4 vs QNX and Linux benchmarks
by Andrew Warkentin 19 Apr '24

19 Apr '24

Somebody in the Zoom call the other day (IIRC it was Gernot) said that seL4 IPC is considerably faster than QNX IPC, but it seems that QNX is somehow faster in a simple benchmarking experiment in which a client repeatedly sends messages to a bit-bucket server, using the TSC to determine timing. I'm running both QNX and seL4 under identical VirtualBox configurations with a single core. I'm using a QNX 6.3.1 x86-32 image i have in my collection (x86-64 support was only added in 7.0; this is the most recent image I have with dev tools installed). The seL4 version I'm using is from February 2022 and is built for x86-64 with MCS enabled (the priority of the threads is 255, and both the timeslice and budget are the initial thread default of 5 ms). My benchmark times a loop of 10000 RPCs; for QNX it's just using the regular read() function on /dev/null or a custom server that also acts like /dev/null but forces a copy of the message into a server-provided buffer, and for seL4 I'm directly calling Send()/Recv()/Reply(). I've also tested Linux's /dev/null, and QNX's implementation actually seems somewhat faster than it (for the system /dev/null; the custom server's best case seems only slightly worse than under Linux). Under QNX and Linux I'm running a C implementation of the benchmark and under seL4 I tried both C and Rust implementations (which have very similar performance). The messages on QNX and Linux are 100 bytes, and on seL4 they are 2 words, which should be hitting the fast path. Here are the best and worst cases I got: seL4: 0.114-0.136s QNX, custom null server: 0.006-0.063s QNX, system null server: 0.002-0.022s Linux: 0.004-0.005s Has anyone else benchmarked seL4 IPC against that of QNX and gotten better (or comparable) results for seL4, unlike what I got? Is synchronous IPC just less optimized under seL4 than QNX?

5 12

Release 0.1.0 of LionsOS
by Ivan Velickovic 16 Apr '24

16 Apr '24

Hello all This is a message to let people know that version 0.1.0 of LionsOS has been released. LionsOS is aimed at embedded, IoT and cyberphysical systems and is designed to be formally verifiable, adaptable to a wide class of use cases in the target domain, while at the same time setting the benchmark for performance of microkernel-based operating systems. We expect to achieve all three aims by a highly modular yet ruthlessly performance-oriented design and strict adherence to the time-honoured KISS principle. LionsOS is still in its early stages but we are at the point where we have a non-trivial example system and initial documentation. You can find the website here: https://lionsos.org/ and the source code here: https://github.com/au-ts/lionsos Thanks, Ivan

1 0

One week to go to submit a talk for seL4 summit 2024
by Birgit Brecknell 15 Apr '24

15 Apr '24

One week to go to submit a talk [0] for seL4 summit 2024 [1]! If you’d like to submit a talk, please upload an abstract of one page or less to the submission portal [2]. The seL4 Summit 2024 will be held 15-17 October 2024 at the Holiday Inn Potts Point, Sydney, Australia. The summit will be an in-person event. Registration details to follow soon. We’re looking forward to many exciting proposals! [0] https://sel4.systems/Foundation/Summit/2024/cfp [1] https://sel4.systems/Foundation/Summit/2024/ [2] https://sel4.systems/Foundation/Summit/2024/submit Birgit Brecknell seL4 Foundation Project Coordinator birgit(a)sel4.systems <mailto:birgit@sel4.systems> bbrcknl(a)gmail.com <mailto:bbrcknl@gmail.com>

1 0

question about the seL4/camkes-vm-examples
by PX 15 Apr '24

15 Apr '24

Hi,All I am trying to build the seL4 VMM example for the qemu-arm-virt platform from seL4/camkes-vm-exmaples. I can build the vmm image successfully, but I cannot run the image. Here are what I did: 1. I use the "../init-build.sh -DCAMKES_VM_APP=vm_minimal -DPLATFORM=qemu-arm-virt" command. 2. ninja After these two steps, the vmm image, capdl-loader-image-arm-qemu-arm-virt is successfully built. But when I run the generated scripts, ./simulate, to run the VMM on qemu, the vmm fails to boot up. The error message is attached below. I use Ubuntu 20.04 and QEMU emulator version 4.2.1. Do I miss something here? Do I use the correct version of the building environment? Any help would be appreciated! ./simulate ./simulate: QEMU command: qemu-system-arm -machine virt,virtualization=on,highmem=off,secure=off -cpu cortex-a15 -nographic -m size=2048 -kernel images/capdl-loader-image-arm-qemu-arm-virt ELF-loader started on CPU: ARM Ltd. Cortex-A15 r2p1 paddr=[61805000..62c02ebf] No DTB passed in from boot loader. Looking for DTB in CPIO archive...found at 6192264c. Loaded DTB from 6192264c. paddr=[60042000..60043fff] ELF-loading image 'kernel' to 60000000 paddr=[60000000..60041fff] vaddr=[e0000000..e0041fff] virt_entry=e0000000 ELF-loading image 'capdl-loader' to 60044000 paddr=[60044000..6140cfff] vaddr=[10000..13d8fff] virt_entry=1880c Enabling hypervisor MMU and paging Jumping to kernel-image entry point... Bootstrapping kernel Warning: Could not infer GIC interrupt target ID, assuming 0. available phys memory regions: 1 [60000000..c0000000] reserved virt address space regions: 4 [e0000000..e0042000] [e0042000..e0043da9] [e0044000..e140d000] [ff000000..ff200000] Booting all finished, dropped to user space *<<*seL4(CPU 0)* [decodeUntypedInvocation/205 T0xffc13400 "rootserver" @1070c]: Untyped Retype: Insufficient memory (1 * 33554432 bytes needed, 0 bytes available).>>* *<<*seL4(CPU 0)* [decodeUntypedInvocation/205 T0xffc13400 "rootserver" @1070c]: Untyped Retype: Insufficient memory (1 * 16777216 bytes needed, 0 bytes available).>>* *<<*seL4(CPU 0)* [decodeUntypedInvocation/205 T0xffc13400 "rootserver" @1070c]: Untyped Retype: Insufficient memory (1 * 16777216 bytes needed, 0 bytes available).>>* *<<*seL4(CPU 0)* [decodeUntypedInvocation/205 T0xffc13400 "rootserver" @1070c]: Untyped Retype: Insufficient memory (1 * 2097152 bytes needed, 0 bytes available).>>* *<<*seL4(CPU 0)* [decodeUntypedInvocation/205 T0xffc13400 "rootserver" @1070c]: Untyped Retype: Insufficient memory (1 * 65536 bytes needed, 0 bytes available).>>* run@main.c:1332 Invalid 'num_vcpus' attribute setting: Exceeds maximum number of supported nodes. Capping value to CONFIG_MAX_NUM_NODES (1) install_vm_devices@main.c:704 module name: map_frame_hack install_vm_devices@main.c:704 module name: init_ram Loading Kernel: 'linux' Loading Initrd: 'linux-initrd' Loading Generated DTB -------- *Pagefault from [vm0]: read prefetch fault @ PC: 0x4 IPA: 0x4, FSR: 0x6* *Context:* *r0: 0x0* *r1: 0xffffffff* *r2: 0x4f000000* *r3: 0x0* *r4: 0x0* *r5: 0x0* *r6: 0x0* *r7: 0x0* *r8: 0x0* *r9: 0x0* *r10: 0x0* *r11: 0x0* *r12: 0x0* *pc: 0x4* *r14: 0x0* *sp: 0x0* *cpsr: 0x9b* m-------- main_continued@main.c:1310 Failed to run VM Halting...

3 4