- l4-hackers - example.com Site

Sculpt 25.10 with Fiasco.OC kernel
by Alexander Boettcher 03 Nov '25

03 Nov '25

Hello, last week Genode released a new version of its open source OS - Sculpt OS 25.10 [0]. I took the opportunity to craft a PC image that also contains an (unofficial and experimental) Sculpt variant based upon a Fiasco.OC kernel [1] version. The variant reflects to large degree the state I presented live during the Systems Meetup [2] gathering at the TU Dresden in January 2025. In case you are interested, feel free to check out [1]. Cheers, Alex. [0] https://genode.org/download/sculpt [1] https://genodians.org/alex-ab/2025-11-02-sculpt-multi-kernel [2] https://ukvly.org -- Alexander Boettcher Genode Labs https://www.genodians.org - https://www.genode.org

1 0

Assertion ‘state() & Thread_vcpu_user' in kernel vgic interrupt processing
by yy18513676366 14 Oct '25

14 Oct '25

Hi l4-hackers, When running a virtual machine, I encounter an assertion failure after the VM has been up for some time. The kernel crashes in src/kern/arm/thread-arm-hyp.cpp, specifically in the function vcpu_vgic_upcall(unsigned virq): vcpu_vgic_upcall(unsigned virq) { ...... assert(state() & Thread_vcpu_user); ...... } Based on source code inspection and preliminary debugging, the problem seems to be related to the management of the Thread_vcpu_user state. （1）Under normal circumstances, the vcpu_resume path (transitioning from the kernel back to the guest OS) updates the vCPU state to include Thread_vcpu_user. However, if an interrupt is delivered during this transition while the receiving side is not yet ready, the vCPU frequently return to the kernel (via vcpu_return_to_kernel) and subsequently process the interrupt through guest_irq in vcpu_entries. In this situation, the expected update of Thread_vcpu_user may not yet have taken place, which seems result in the assert being triggered when a VGIC interrupt is involved. （2）A similar condition seems to occur in the vcpu_async_ipc path. At the end of IPC handling, this function explicitly clears the Thread_vcpu_user flag. If a VGIC interrupt is delivered during this phase, the absence of the expected Thread_vcpu_user state seems to lead to the same assertion failure. I would like to confirm if the two points above are correct, and what steps I should take next to further debug this issue. In addition, I have some assumptions I would like to confirm: First, for IPC between non-vcpu threads, the L4 microkernel handles message delivery and scheduling (wake/schedule) directly, without requiring any forwarding through uvmm. Similarly, interrupts bound via the interrupt controller (ICU) to a non-vcpu thread or handler are also managed by the kernel and scheduler, and therefore do not necessarily involve uvmm. Second, passthrough interrupts, when not delivered in direct-injection mode, are routed to uvmm for handling if they are bound to a vCPU. Likewise, services provided by uvmm (such as virq) are also bound to a vCPU and therefore require forwarding through uvmm. There seems to have been a similar question in the past, but it does not seem to have been resolved. Re: Assertion failure error in kernel vgic interrupt processing - l4-hackers - OS Site I wonder if my questions are related to that post, and if any solutions exist. Thanks!

2 7

Questions regarding L4::Platform_Control
by David Q 13 Oct '25

13 Oct '25

Hello L4 hackers, I would like to thank the community for helping me learn; I am back with more questions. This time it is about L4::Platform_Control 1. It seems IO and UVMM both have this L4::Platform_Control capability, is it correct? 2. I can't seem to create a usable L4::Platform_Control capability in a userland application using the factory from env. Does this mean there is one such platform control capability only? 3. It seems there is a system_suspend() function, and X86 is particularly supported. Does it work right now for ARM? 4. Once system_suspend() is called in an ARM environment, does the kernel communicate with PSCI, which then gets intercepted by Arm trusted firmware? 5. Also, before suspending the entire system, it would seem a good idea to quiesce all threads (except the kernel I assume) and save the CPU/Thread states/contexts. Is there an API that could help with quiescing threads and saving relevant states? I only see the debugger being able to quiesce all threads, but I can't seem to find an API that can save and reload the saved states once we want to exit suspend. These are a lot of question, and I thank anyone who reads them.

1 0

L4 Thread, pthread, comprehension question
by xudino＠gmail.com 23 Sep '25

23 Sep '25

Hello L4 hackers, I hope you are all doing well today. I am hoping to discuss the topic of threads to better my understanding of it, as it seems to be a major building block in L4Re. I have the following questions (using the c++ based libraries.): 1. Is Pthread the official way to create threads in an L4Re application? 2. I have made a L4 thread (to understand how threads work in L4) without the help of pthreads by setting up the Attr, which involved in setting the exception handlers(using rm()), pager (using rm()), instruction pointers, stack pointers, binding, ex_reg() and finally running. All seems well until I try printing a message. It seems seems I am unable to use the printf() function in the instruction pointer function of said thread. The error I get is : ttest | l4re_itas[rm]: unhandled read page fault at 0x141 pc=0x100f8a0 ttest | l4re_itas: rom/thread_test: Unhandled exception: PC=0x100f8a0 PFA=0x140 LdrFlgs=0x0 However, if I use printf in a pthread, none of these errors pop up. 2a. Am I using the wrong exception handler and pager (I got both from rm)? 2b. Also, the "l4_vcon_send(L4_BASE_LOG_CAP,..,...) function seems to work fine in either case, shouldn't printf() eventually call this function as after a series of indirections? 2c. What exc_handler and pager do pthreads use? Why are they able to handle the pager faults and exceptions from printf? Can I appropriate them for the L4 threads I started? 3. It seems the Virtual Machines (VMs) that are on the hypervisor are also closely related with threads. I assume these are Vcpu threads and not pthreads. 3a. Am I correct in this assumption? 3b. How are the exception handlers and pagers set up for these Vcpus? Thank you so much for your time, David

3 3

Re: L4 Thread, pthread, comprehension question
by Marcus Haehnel 23 Sep '25

23 Sep '25

Hi David, On 2025-09-22 05:37, xudino(a)gmail.com wrote: > Hello L4 hackers, I hope you are all doing well today. > > I am hoping to discuss the topic of threads to better my understanding > of it, as it seems to be a major building block in L4Re. I have the > following questions (using the c++ based libraries.): > > 1. Is Pthread the official way to create threads in an L4Re > application? That is at least the high level primitive that you should use if you have no good reason to use the low level L4 primitives and want to use any of the POSIX / libc functionality inside your thread. > > 2. I have made a L4 thread (to understand how threads work in L4) > without the help of pthreads by setting up the Attr, which involved in > setting the exception handlers(using rm()), pager (using rm()), > instruction pointers, stack pointers, binding, ex_reg() and finally > running. All seems well until I try printing a message. > It seems seems I am unable to use the printf() function in the > instruction pointer function of said thread. The error I get is : > ttest | l4re_itas[rm]: unhandled read page fault at 0x141 > pc=0x100f8a0 > ttest | l4re_itas: rom/thread_test: Unhandled exception: > PC=0x100f8a0 PFA=0x140 LdrFlgs=0x0 > However, if I use printf in a pthread, none of these errors pop up. > 2a. Am I using the wrong exception handler and pager (I got both > from rm)? > 2b. Also, the "l4_vcon_send(L4_BASE_LOG_CAP,..,...) function seems > to work fine in either case, shouldn't printf() eventually call this > function as > after a series of indirections? > 2c. What exc_handler and pager do pthreads use? Why are they able > to handle the pager faults and exceptions from printf? Can I > appropriate > them for the L4 threads I started? What you are seeing is a side-effect of libpthread being quite tightly integrated with the libc. While it is true that printf will call l4_vcon_send somewhen down the line it will use some (potentially thread-local) internal buffers to print its output. While you can mix libpthread threads with native L4 threads you must take care to call no function from the libc that would make any use of TLS storage, unless you set this up yourself. If you want to write normal applications std::thread and pthread threads are the way to go. > > 3. It seems the Virtual Machines (VMs) that are on the hypervisor are > also closely related with threads. I assume these are Vcpu threads and > not pthreads. > 3a. Am I correct in this assumption? > 3b. How are the exception handlers and pagers set up for these > Vcpus? Yes, a vCPU is in the end only a thread with some extended state. A thread in vcpu mode provides an additional exception execution context. When a trap from avcpu occurs the kernel will switch the vCPU to the exception entry point. See entry_ip and entry_sp here https://l4re.org/doc/structl4__vcpu__state__t.html#a1f45174954aa47bb2f21b7b… These must be set as part of the vcpu state before starting the vcpu. The exception handler must take care of handling page-faults generated by threads user code. I hope this helps :) Best regards, - Marcus > > Thank you so much for your time, > David > _______________________________________________ > l4-hackers mailing list -- l4-hackers(a)os.inf.tu-dresden.de > To unsubscribe send an email to l4-hackers-leave(a)os.inf.tu-dresden.de

2 1

Help: interactive REPL I/O for user program on L4Re/Fiasco.OC (amd64-plain) — Vcon/cons nearly working; canonical approach?
by Robert A. James 07 Sep '25

07 Sep '25

Hello l4-hackers, My name is Robert (Bob) A. James I'm VERY new to the L4Re world. This is also my first foray into systems programming having come from the Medical Device and Enterprise areas during my career. I am now retired and developing a full Operating System based on L4Re/Fiasco.OC. I’m looking for guidance on the /canonical/ way to wire an interactive text console (stdin/stdout) for a user program under L4Re/Fiasco.OC on amd64-plain. Context * I have a small, headless FORTH VM (“StarForth”) running under L4Re/Fiasco.OC; its self-tests pass. What’s missing is an *interactive REPL*. * Target outcomes: a) Run via |make qemu E=starforth O=build-x86_64| b) Build GRUB2 ISO via |make grub2iso E=starforth O=build-x86_64| c) ISO runs in QEMU and VirtualBox d) Same ISO boots on commodity x86_64 hardware What I’ve tried (and where I’m stuck) 1. *Vcon + cons* (almost there) * My mental model: Vcon as a frontend; |cons| providing the console service; StarForth as the “backend” client/subscriber. * Behavior I see: • The “terminal” prints what the *logger* prints rather than the process’s normal *stdout*. • Output sometimes *flushes only on newline*; interactive prompts without |\n| don’t appear reliably. * Aside from those two issues, this was close to a working REPL. * *Questions:* Is |cons| effectively write-only (log)? If so, what’s the supported input-capable console frontend to bind both stdin and stdout for a user process? Is there a minimal example showing correct capability wiring so user stdout/stderr don’t get mixed with the system log? 2. *GOOS/Framebuffer route* * I attempted a tiny terminal server that maps the GOOS framebuffer and renders an 8×16 CP437 font. I did not get this path working end-to-end, so I’m fine dropping it if there’s a simpler, recommended console approach. What would help * The *recommended minimal pattern* (modules/services + boot script) to give a user task a real interactive stdin/stdout: o works with |make qemu …| and |make grub2iso …| o also works on typical PCs without a full graphics stack. * A *small reference* that: (1) prints text, and (2) reads keystrokes from the user, with a snippet of |modules.list| and the Lua loader snippet. Environment / details * L4Re/Fiasco.OC on amd64-plain, built with the L4Re toolchain. * Intended entry points: |make qemu E=starforth O=build-x86_64|, |make grub2iso E=starforth O=build-x86_64|. One of my simple boot variants (for reference): |modules.list| (simplified) entry starforth kernel fiasco -serial_esc roottask moe rom/quark.cfg module l4re module ned module cons module quark.cfg module starforth |quark.cfg| --> I think this is about what I had. -- rom/quark.cfg local L4 =require("L4") local ld =L4.default_loader -- Start cons; feed it to the real serial logger (fe =L4.Env.log) local cons_ctl =ld:new_channel() ld:start({ caps = { cons = cons_ctl:svr(), -- server gate for cons' factory fe = L4.Env.log, -- cons frontend goes to serial/log }, }, "rom/cons -m l4re -f fe -a -t -c StarForth") -- ← added -c StarForth -- Ask cons to create a Vcon client for StarForth and pass it in as 'tty' -- (Capabilities are first-class in Ned; calling 'create' on caps is supported.) local tty =cons_ctl:create(L4.Proto.Log, "StarForth", "show", "key=1", "bufsz=65536") -- Start StarForth with that Vcon as its TTY ld:start({ caps = { tty = tty, -- the Vcon client for StarForth }, }, "rom/starforth") I can share a minimal reproducible case (sources, build logs, QEMU output) off-list if that helps. Thanks in advance for any pointers to the “right way,” or to a maintained example I can follow. Best regards, R. A. “Bob” James (rajames440(a)gmail.com) Kubuntu 25.04 • amd64-plain • QEMU/VirtualBox • GRUB2 boot targets

2 1

Question about SMC filtering in smc_user.cpp on ARM64
by Gravel Yuan 25 Jul '25

25 Jul '25

Hello all, I'm currently working on integrating OP-TEE support on the ARM64 architecture within the L4Re framework, specifically focusing on cryptographic operations such as encryption and decryption. While reviewing the implementation, I noticed that in fiasco/src/kern/arm/smc_user.cpp, non-fast SMC calls are explicitly filtered out with the following check: // only allow fast callsif (!(r0 & 0x80000000)) return commit_result(-L4_err::ENosys); I'm trying to understand the rationale behind this design decision. Was it primarily driven by real-time performance requirements, or are there other considerations？ Additionally, as OP-TEE often uses *yielding calls* for certain operations, do you think it would be appropriate for us to consider extending the kernel to support such calls? We would appreciate any insights or recommendations you can provide. Best regards,

2 1

L4Re: MIPS SMP cache initialisation may be broken for some CPUs
by Paul Boddie 20 Jul '25

20 Jul '25

Hello, Pushing on with my efforts to port L4Re to another MIPS-based SoC, I have been attempting to activate more than one CPU core. Although there is some support in Fiasco for the MIPS Coherence Manager (CM) and Cluster Power Controller (CPC), these technologies are not supported in this particular SoC, which is related to the JZ4780 used in the MIPS Creator CI20. However, the Platform_control abstraction (in src/kern/mips/platform_control- mips.cpp) does seem to provide some flexibility in the way secondary CPUs or cores may be started. It seems that even in situations where the CM is not available, the alloc_secondary_boot_code method will assemble a bootstrap routine from snippets including one, _tramp_mp_cache, that initialises the caches. Unfortunately, it appears that this cache initialisation code does not work on this particular SoC. The method used by_tramp_mp_cache is the familiar one where the cache tags are invalidated for all cache index entries using the Index_Store_Tag operation for each cache type. This is supposed to work on any MIPS CPU, but through some tedious troubleshooting, I discovered that it does not work for the data cache. If the data cache variant of the Index_Store_Tag operation is performed for a range of addresses starting from the base of KSEG0, I found that some kind of side-effect would occur, possibly affecting the rather critical addresses in that range. This would prevent Fiasco from continuing to start up, and things like timers and the UART would not function, although the processor was not halted and would still run code, illuminating LEDs as a last-resort debugging tool. There is some preliminary support for this SoC, as well as the JZ4780, in Linux and it seems that instead of using Index_Store_Tag, the tag records are explicitly invalidated and updated. However, it also seems to be the case that caches can be invalidated using Hit_Invalidate. Changing the cache operations in _tramp_mp_cache to use this invalidation operation in its two variants appears to work, avoiding the problems described above. Does anyone have any thoughts or recollections about this cache initialisation routine? On the topic of actually starting secondary cores, this SoC has its own set of registers for resetting cores, interrupt control, mailboxes, and so on. I have developed a fairly simple abstraction that performs similar core bootstrapping work to that of the Cm abstraction (in src/kern/mips/cm.cpp). I then extend the Platform_control abstraction so that it will call the alloc_secondary_boot_code method, followed by the appropriate method to start the secondary cores. Is there any documentation for the SMP architecture in Fiasco and L4Re? I note that interprocessor interrupts (IPI) are one element that I might need to support, probably using the mailboxes. Thanks in advance for any advice or feedback that may be given! Paul

2 2

Subject: Introduction – StarshipOS: A gForth/JVM Hybrid on L4Re
by Robert James 12 Jul '25

12 Jul '25

Hello everyone, My name is Rob James, and I wanted to introduce myself and an OS I’ve been developing called **StarshipOS**. StarshipOS is a unique hybrid operating system built on top of the L4Re microkernel framework. It combines: - A Forth-based core powered by **gForth** - A lightweight persistent **object memory model** that completely replaces the traditional filesystem - Embedded **OpenJDK 21** services for high-level logic and tooling The system is non-POSIX by design. Instead of files, everything lives in a dynamic memory graph of interactive objects. You interact with your system through a Forth-based REPL that evolves and mutates this object universe in real time. No shell scripts, no /etc, no /usr — just memory objects and messaging. The ultimate goal is to make the **REPL the new shell**, and the **memory graph the new filesystem**. Here’s what’s already in place: - A full Maven-driven build system that compiles Fiasco.OC, L4Re, OpenJDK, and gForth from source - A `starship-maven-plugin` that automates ROMFS image generation and ISO boot layout coming soon: - A sandboxed REPL environment that boots directly into gForth and supports mounting JVM modules as interactive bundles - Early support for memory graph ACLs, entropy-based object lifespan, and “bubbles” — user-defined isolated memory regions Right now, I’m focused on integration, getting the system to boot into the gForth REPL with full JVM runtime support, and beginning to layer in userland services via custom dictionary words. Source is available (in-progress) here: 👉 **https://github.com/rajames440/StarshipOS** I’ve been programming since the 1970s, mostly in userland, and I’m diving deep into kernel space and L4 internals for the first time. I’d love to hear from others doing low-level work on L4Re, especially anyone who's extended the build system or tackled non-POSIX boot flows. Thanks again to everyone who’s contributed to L4Re and Fiasco.OC — it’s a hell of a foundation to build a new kind of OS on. All the best, Rob James

2 1

L4Re: Why was EXTERN_C_BEGIN/END replaced?
by Paul Boddie 23 Jun '25

23 Jun '25

Hello, Taking the opportunity to use a newer snapshot of L4Re, I notice that EXTERN_C_BEGIN and EXTERN_C_END now cause errors like this: error: unknown type name ‘DO_NOT_USE_EXTERN_C_END_ANY_MORE__USE__END_DECLS’ The commit introducing this behaviour seems to be this one: https://github.com/kernkonzept/l4re-core/commit/ e04b50e0e4f7c7a3316a2d8b658db6d81bd3e88d It would appear that throughout L4Re, a mass renaming has occurred from these symbols to __BEGIN_DECLS and __END_DECLS. Was there a particular reason for what might seem like an arbitrary change? Paul

3 2