Prof. Dr. Frank Bellosa

Thorsten Gröninger

Abstract
Optimizing time performance of interprocess communication (IPC) facilities on microkernels (μkernels), kernels with minimal functionality, is essential to ensuring competitiveness with monolithic kernels like Linux. With the emergence of recent work like SkyBridge, modern processor features have become key research subjects to develop new IPC libraries with that surpass native implementations and therefore improve μkernels. seL4 is a modern representative of μkernels, which we use as a design and implementation platform for user interrupt (UINTR) support, Intel’s recently-introduced extension to send and receive (inter-processor) interrupts directly from user-space. In addition to UINTR we also implement support for the new user-wait extension, e.g. timed pause TPAUSE, and design an IPC library to make use of both of these new features on seL4. We find that our new IPC library—uIntercom (uIcom)—provides 1.1−5.5× better time performance than either existing seL4 IPC facilities in the cross-core case, while potentially indicating better power efficiency in some metrics.

BibTex:

@bachelorthesis{Gurres25ProcessorFeaturesL4Microkernels,
  author = {Martin Ludwig Gurres},
  title = {Applying Modern Processor Features to L4 Microkernels},
  type = {Bachelor Thesis},
  year = 2025,
  month = oct# "17",
  school = {Operating Systems Group, Karlsruhe Institute of Technology (KIT), Germany}
  }