{"id":"28032b77-b85c-4481-98b7-dd903c7dcf91","arxiv_id":"2501.06234","paper_version":2,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"LionsOS, a highly modular seL4-based OS using simple single-purpose components and use-case-specific policies, outperforms Linux on network echo and storage benchmarks despite many more context switches.","lead":"LionsOS is a new operating system for embedded devices built on the formally verified seL4 microkernel, using tiny isolated components and special-purpose policies. In benchmarks, it handles network traffic with far less CPU than Linux and similar or better throughput, challenging the idea that modular microkernels must be slow.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The central outperformance claim depends on a stock, possibly untuned Linux baseline; a tuned Linux could match or beat LionsOS on the UDP echo workload, weakening the headline claim.","rationale":"The reader's weakest assumption identifies exactly the risk that the Linux baseline may be underperforming due to configuration choices, making the headline superiority claim an artifact of an unfair comparison. My stress-test pass found no internal contradiction in the design or the reported measurements; the concern is about external validity and the strength of the comparative claim. The paper's own text signals that Linux was run with defaults, and no tuning effort is documented, while the novelty hinges on beating a representative monolithic OS. Therefore the conditionality expressed in the reader's verdict is appropriate. I recommend no change to the reader's verdict: the claim should not be accepted unconditionally until the Linux baseline is shown to be reasonably tuned or the conclusion is weakened to 'at par.'","tokens_in":20125,"tokens_out":7562,"duration_ms":82099,"concrete_test":"Re-run the i.MX8MQ unicore UDP echo experiment (Figure 4a) with Linux tuned: enable FEC interrupt coalescing via ethtool, pin the FEC IRQ and the echo process to the same core, increase socket buffers, and optionally use a single-threaded echo program built on recvmmsg/sendmmsg. Also run a comparable x86 test with tuned NIC parameters (e.g., IXGBE interrupt coalescing and IRQ affinity). Repeat each configuration at least 10 times and report the mean and variance. If tuned Linux sustains the full 1 Gb/s while keeping one core below 100% utilization, the claim that LionsOS outperforms Linux on this context-switch-intensive workload is not robust to baseline configuration.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The strongest claim—that LionsOS outperforms all compared systems on context-switch-intensive loads—rests primarily on the UDP echo comparison against Linux in Section 6.3.1. The paper reports that LionsOS 'does not need to configure a Rx IRQ hold-off value' and that Linux 'switches to polling under high load,' but it does not state that equivalent tuning was attempted on the Linux side. On the i.MX8MQ, the stock FEC driver's interrupt default settings can severely limit throughput; the x86 comparison likewise uses a default Debian kernel without reported tuning (e.g., interrupt coalescing, IRQ affinity, socket buffer sizes). If Linux were tuned to reach line rate at acceptably low CPU usage, the conclusion that LionsOS outperforms monolithic designs on this workload would be reduced to 'at par,' which is a materially weaker form of the central claim. The absence of error bars and the reliance on a single network workload make this baseline-fairness concern load-bearing; the Genode and CEOS comparisons do not mitigate it because the claim is specifically framed against 'traditional monolithic designs.'","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper presents LionsOS, an operating system for safety- and security-critical embedded systems built on the formally verified seL4 microkernel. The design is deliberately static and highly modular, with strict separation of concerns, least privilege, and use-case-specific policies. The authors report an implementation of Ethernet and storage subsystems using device drivers, virtualisers, and shared-memory SPSC queues, plus mechanisms for reusing Linux drivers in virtual machines. The evaluation compares LionsOS against Linux, Genode, and a commercial microkernel-based OS (CEOS) on UDP echo and block I/O workloads. The headline results are that LionsOS sustains line-rate UDP echo with substantially lower CPU utilisation and lower round-trip times than Linux on both Arm and x86, and that storage throughput is comparable to Linux while using less CPU at small block sizes. The paper also reports code-size comparisons, a dynamic policy-swap experiment, and a simulated analysis of IPC cost. The central claim is that LionsOS is the first highly modular microkernel-based OS whose performance is at par with or better than traditional monolithic designs on system-call intensive workloads.","tokens_in":20365,"tokens_out":4792,"duration_ms":50802,"significance":"If the performance claims hold, this is a significant result for the microkernel and verified-OS communities: it would show that fine-grained modularity, with many inter-component context switches, need not impose a prohibitive performance penalty. The paper is also useful as a systems design study, with concrete mechanisms (SPSC queues, virtualisers, location transparency, driver VMs) and an openly available implementation. The authors are explicit about the verification-friendly intent and provide code-size data and a reproducible benchmark methodology. The main empirical contribution, however, rests on the fairness of the Linux baseline and on the absence of run-to-run variance reporting, so the strength of the headline claim is currently not fully established.","major_comments":[{"comment":"The central claim that LionsOS outperforms traditional monolithic designs is supported almost entirely by the UDP echo comparison against Linux, but the Linux baseline is not shown to be reasonably tuned. Section 6.1 states only that the Arm Linux runs a Buildroot system with kernel 6.1.0 and that the x86 Linux uses a Debian kernel 6.6.15-2 with the performance frequency governor. The paper mentions that Linux requires an Rx IRQ hold-off configuration and switches to polling under high load, but it does not report what tuning was attempted on the Linux side (e.g., interrupt coalescing, IRQ affinity, receive-side scaling, socket buffer sizes, or kernel configuration options). On the i.MX8MQ FEC controller, stock interrupt defaults can severely limit throughput, so the observed Linux plateau of about 500 Mb/s may not represent a well-configured monolithic baseline. Please repeat the comparison with a Linux configuration that has been explicitly tuned for this NIC and workload, report the specific settings, and state whether the qualitative conclusion (LionsOS uses less than half the CPU and has lower RTT) survives. Without this, the headline claim is vulnerable to the objection that an untuned baseline, rather than modularity, explains the result.","section":"Section 6.3.1, Figures 4 and 5"},{"comment":"No error bars or run-to-run variance are reported anywhere in the networking evaluation. The curves in Figures 4, 5, and 6 appear to be single measurements, and the text reports precise-looking ratios (e.g., 'less than half the CPU', RTTs 'three to ten times less') without any indication of measurement spread or repeat count. Because the deltas are used to assert a large performance advantage, the paper should report at least the number of repetitions and the min/median/max (or confidence intervals) for the key curves, and should state how the load generator handles packet loss and measurement error. This is particularly important near saturation, where CPU utilisation and achieved throughput can be sensitive to timing artifacts.","section":"Section 6.3.1, Figures 4-6"},{"comment":"The 'free IPC' simulation is explicitly acknowledged as imprecise ('We do not claim that this is in any way precise'), yet Section 7 uses it to conclude that IPC cost has only minor impact and to contradict prior claims that IPC cost is still a bottleneck. Adding fixed delays to seL4 system calls, or subtracting 493 cycles for 'free' IPC, is a coarse approximation of what would happen on Fiasco, Zircon, or a hypothetical zero-cost IPC system; it does not model differences in cache behaviour, scheduling, queue batching, or notification mechanisms. This experiment is useful as a sensitivity analysis, but the conclusion in Section 7 should be hedged accordingly, or the paper should provide a more direct comparison against at least one of the actual kernels. As written, the strength of the 'IPC cost matters little' conclusion exceeds what the methodology can support.","section":"Section 6.3.1, Figure 5d and Section 7"}],"minor_comments":[{"comment":"The caption states that 'the left axis and solid lines are throughput except where stated otherwise', but Figure 4a shows CPU utilisation on the left axis and does not appear to follow this rule. Please clarify the axis assignment for each subfigure, or standardise the captions.","section":"Section 6.3.1, Figure 4 caption"},{"comment":"The term 'unicore' is used repeatedly; 'single-core' or 'uniprocessor' is the conventional term and would read more naturally.","section":"Section 6.1 and Section 6.3.1"},{"comment":"The text says the benchmark reads 4 files, while the figure shows 4 file positions, but then states that LionsOS 'is slower when reading more than five files'. This is internally inconsistent; please reconcile the number of files in the benchmark with the reported cross-over point.","section":"Section 6.3.2, Figure 7e"},{"comment":"The methodology for the simulated Fiasco, Zircon, and 'free IPC' curves is described only in the text; adding a concise explanation in the figure caption would improve readability.","section":"Section 6.3.1, Figure 5d"},{"comment":"The Genode comparison uses the 'hw' base configuration, which runs bare metal without a microkernel underneath, so it is not directly comparable to a microkernel-based design. The text acknowledges this, but the figure legend simply lists 'Genode'; please make the configuration difference explicit in the figure and in the corresponding discussion.","section":"Section 6.3.1, 'Other OSes' paragraph"},{"comment":"The driver-VM experiments report memory footprints and development effort, but not the latency overhead of the VM-based driver path. Since the text states that this path 'is unlikely to be an option for performance-critical devices', a quantitative latency or throughput comparison for at least one driver class would strengthen the claim.","section":"Section 5.4 and Section 6.2.3"}],"recommendation":"major_revision","confidential_remarks":"The paper is authored by the developers of the evaluated system, and the central claim depends on the Linux baseline being a fair, representative comparison point. The lack of detailed Linux tuning and the absence of variance reporting are the main risks. If the authors can supply a well-tuned Linux comparison and repeat counts, the result would be much more convincing. The 'free IPC' simulation should be retained only as a sensitivity analysis, not as a standalone refutation of prior IPC-cost claims."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Quick take: this is a serious systems paper, not vaporware. The authors built LionsOS on seL4 Microkit, shipped it open source, and run a real web server on it. The design principles—strict separation of concerns, least privilege, use-case-specific policies—are coherent, and the evaluation is much more than a toy: UDP echo against Linux, Genode, and CEOS on Arm and x86, plus storage and file benchmarks. The code-size comparison (LionsOS NIC drivers 400-670 SLOC vs Linux 3,000-10,000) is a concrete, reproducible point. The 'free IPC' simulation is explicitly rough, and they say so, which is good practice.\n\nThe two real soft spots. First, the Linux baseline may not be tuned. On Arm they use a stock Buildroot 6.1 kernel; on x86, a stock Debian 6.6 kernel with the performance governor. They don't report trying interrupt coalescing, IRQ affinity, socket buffer tuning, or the specific FEC driver settings. The stress-test note is right that a tuned Linux could close part of the gap. That said, the gap is large (LionsOS uses less than half the CPU at line rate, RTTs 3-10x lower), and Linux is given two threads on x86 without matching LionsOS. So I would not call the comparison invalid, but the claim 'outperforms all systems' is stronger than what the paper proves. It proves it against the configurations tested. That is a fixable weakness, not a fatal one.\n\nSecond, no error bars or run-to-run variance anywhere in Section 6. For a performance paper, that's a standard referee request. The graphs show single curves; we don't know if the SLOC ratios or the throughput gaps are stable across runs. This is minor to fix but should be in the revised version.\n\nThe benchmark coverage is narrow—UDP echo and block I/O—but the paper's claim is about system-call intensive workloads, and UDP echo is exactly that. I won't penalize it heavily.\n\nBottom line: the central argument holds up: a highly modular microkernel OS can be fast if the components are simple and the policies are tailored. The paper deserves a serious referee. I'd send it to review, and ask for tuned Linux baselines, error bars, and a statement about configuration details. It's a useful paper for anyone in embedded systems, seL4, or microkernel performance.","headline":"LionsOS is a real, open-source microkernel OS with surprisingly strong UDP echo and storage numbers; the headline claim is probably right, but the Linux baseline fairness and missing variance are the soft spots a referee should push on.","tokens_in":20913,"tokens_out":2792,"would_cite":true,"duration_ms":27193,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"This paper claims the performance penalty of highly modular microkernel-based OSes is not inevitable: LionsOS, built on the formally verified seL4 microkernel, matches or beats Linux on UDP echo and storage workloads while using far less…","keywords":["LionsOS","seL4","microkernel","modular operating systems","embedded systems","separation of concerns","IPC performance","device drivers"],"falsifier":"Run the identical UDP echo benchmark with a carefully tuned Linux on the same board — minimal initramfs userspace, IRQ coalescing and busy-polling tuned to the offered load, the echo process pinned, and preemption configured for throughput — and compare throughput per core and round-trip latency. If tuned Linux matches or beats LionsOS on throughput and latency at equal CPU cost, the claim that modularity costs nothing would be falsified; the same test can be rerun with hardware offload features (Tx IRQ coalescing, checksum offload) re-enabled for the CEOS comparison to check that the disabled-features choice is not the source of the gap.","tokens_in":19971,"feed_emoji":"🧩","tokens_out":13075,"duration_ms":101557,"temperature":0.7,"pith_summary":"The paper sets out to overturn the long-held assumption that fine-grained modularity in microkernel-based operating systems inevitably carries a prohibitive performance cost. It presents LionsOS, an operating system for safety- and security-critical embedded systems that sits on the formally verified seL4 microkernel and is built from many small, single-purpose, address-space-isolated components communicating through simple lock-free queues. The paper claims this is the first such highly modular system to perform at par with or better than monolithic designs, and demonstrates it on system-call-intensive workloads: UDP echo networking, where LionsOS sustains full line rate with a large fraction of CPU to spare while Linux saturates at roughly half the throughput, and storage benchmarks with similar bandwidth at a fraction of Linux's CPU cost. LionsOS itself is not yet formally verified; the claim is that the extreme simplicity of its components makes verification achievable, and the paper already cites a verified NIC driver in the same style.","feed_headline":"LionsOS beats Linux on UDP echo using a fraction of the CPU","feed_subtitle":"A microkernel built from many small isolated modules reaches full 1 Gb/s line rate where Linux tops out around 500 Mb/s.","key_machinery":"The mechanism that makes the performance claim work is the combination of a static system architecture with single-producer-single-consumer (SPSC) shared-memory queues synchronised by semaphores. The seL4 Microkit fixes the system at configuration time as a set of single-threaded protection domains (PDs) with declared communication channels; LionsOS components then communicate only through bounded, lock-free SPSC queues, signalling a peer only when a queue changes between empty and non-empty (or full and non-full). All policy-independent state lives in shared memory, so a failed component can be restarted or even swapped for a different executable (a demonstrated 17 µs policy switch) without disturbing the rest of the system. Because no component ever blocks on another's internal state, components are location-transparent: a component cannot tell whether its peer runs on the same core or a remote one, so multicore scaling comes from distributing the small components across cores rather than from threading, and device drivers are reduced to pure hardware translation, with data buffers deliberately unmapped from the driver's address space.","core_discovery":"The paper's central claim is that LionsOS is the first highly modular microkernel-based OS to achieve performance at par with or better than traditional monolithic designs, and that on context-switch intensive workloads — where modularity-imposed overheads should be greatest — it outperforms all systems compared against, including Linux, Genode, and a commercial microkernel OS (CEOS). The paper attributes this result to \"radical simplicity\": strict separation of concerns, least privilege, narrow interfaces, and use-case-specific policies produce components so small that their frequent context switches cost less than the interface layers and generality of monolithic designs. The evidence is quantitative: on an Arm i.MX8MQ platform LionsOS sustains the full 1 Gb/s NIC capacity with roughly one third of the CPU left unused, whereas Linux plateaus at about 500 Mb/s with its core saturated and round-trip times three to ten times higher; on x86 with a 10 Gb/s NIC, LionsOS keeps up with about 20% CPU spare while Linux saturates at 4 Gb/s. Simulated IPC costs from zero (free IPC) to Zircon-like prices change LionsOS's CPU utilisation only slightly, which the paper takes as evidence that context-switch cost is not the bottleneck the literature has assumed.","pith_inferences":["If the performance advantage is really about simplicity rather than kernel speed, then porting the same protection-domain structure to a microkernel with deliberately inflated IPC latency should reproduce the same throughput, isolating the design principle from the processor's context-switch cost; the paper's simulated-IPC experiments suggest this test is cheap to run.","The use-case-specific policy principle implies the performance story may not transfer to general-purpose workloads: static resource allocation works because embedded systems do not over-commit, so on dynamic, unpredictable workloads the advantage over adaptive monolithic schedulers could shrink or even reverse.","The 17 µs policy swap suggests a broader design pattern for adaptive behaviour in critical systems: keep a small library of specialised policy modules and hot-swap them in response to events, rather than building one general policy with configuration knobs — a pattern that could also be applied to schedulers, cache partitioning, and power management."],"forward_implications":["If modularity no longer costs performance, isolation-heavy OS architectures become the natural choice for mixed-criticality embedded systems, since the security and safety benefits come without the traditional performance tax.","The simplicity of the small components makes formal verification tractable: a high-performance NIC driver written in the LionsOS style has already been verified with automated proof techniques, and the paper expects the rest of the small trusted computing base to follow.","Linux driver reuse inside small virtual machines (a few MiB of RAM for optimised configurations, weeks of effort per device class) gives LionsOS broad hardware coverage without sacrificing the isolation model, so device availability is not a barrier to adoption.","Runtime policy swapping (demonstrated at 17 µs for network traffic shaping) lets a static-architecture system change behaviour on the fly, so use-case-specific policies do not mean inflexible systems."],"supporting_citations":[{"why":"The HongMeng microkernel paper that claims IPC cost still forces co-locating services and a 90 kSLOC kernel; it is the \"IPC is still a bottleneck\" position LionsOS must beat.","marker":"[Chen et al., 2024]"},{"why":"The comprehensive formal verification of seL4 (correctness, integrity, confidentiality, binary-level semantics) that supplies the isolation guarantees LionsOS builds on.","marker":"[Klein et al., 2014]"},{"why":"The seL4 Microkit, whose protection-domain abstraction, event-driven model and system description file are the foundation of the LionsOS architecture.","marker":"[seL4 Foundation, 2023]"},{"why":"The measured round-trip IPC latencies for seL4, Fiasco.OC and Zircon that the paper uses to simulate the effect of higher or zero IPC cost on LionsOS performance.","marker":"[Mi et al., 2019]"},{"why":"The Genode OS documentation; Genode 24.11 is the comparison highly-modular system in the UDP echo evaluation.","marker":"[Feske, 2015]"},{"why":"The original driver-virtualisation approach that LionsOS adapts for reusing unmodified Linux drivers in per-driver VMs.","marker":"[LeVasseur et al., 2004]"},{"why":"The classic source cited for the traditional view that IPC performance is the Achilles heel of microkernels, the assumption this paper challenges.","marker":"[Bershad, 1992]"},{"why":"The verification of a high-performance NIC driver with automated proof techniques, cited as evidence that the simple LionsOS driver style is verifiable.","marker":"[Zhao et al., 2025]"}],"fun_headline_variants":["LionsOS outruns Linux on UDP echo with CPU to spare","Modular microkernel hits 1 Gb/s where Linux caps at 500 Mb/s","Radical simplicity: LionsOS beats Linux on network speed","seL4-based OS outpaces Linux on UDP echo workloads","Tiny isolated modules, top speed: LionsOS surpasses Linux"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The central performance claim rests on the fairness of the comparison: Linux, Genode, and CEOS must be reasonably well-tuned representatives of their designs, so that LionsOS's win reflects its architecture rather than under-configured rivals.","fun_headline_variants_meta":{"raw":{"variants":["LionsOS outruns Linux on UDP echo with CPU to spare","Modular microkernel hits 1 Gb/s where Linux caps at 500 Mb/s","Radical simplicity: LionsOS beats Linux on network speed","seL4-based OS outpaces Linux on UDP echo workloads","Tiny isolated modules, top speed: LionsOS surpasses Linux"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000427,"raw_usage":{"total_tokens":2144,"prompt_tokens":863,"completion_tokens":1281,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":479,"completion_tokens_details":{"reasoning_tokens":1197}},"tokens_in":479,"tokens_out":1281,"duration_ms":10879,"temperature":1.0,"reasoning_tokens":1197,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-10T21:36:20.493755+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Run the identical UDP echo benchmark with a carefully tuned Linux on the same board — minimal initramfs userspace, IRQ coalescing and busy-polling tuned to the offered load, the echo process pinned, and preemption configured for throughput — and compare throughput per core and round-trip latency. If tuned Linux matches or beats LionsOS on throughput and latency at equal CPU cost, the claim that modularity costs nothing would be falsified; the same test can be rerun with hardware offload features (Tx IRQ coalescing, checksum offload) re-enabled for the CEOS comparison to check that the disabled-features choice is not the source of the gap.","supporting_citations":[],"review_version":1}