Anatomy of a run-time: your contract with the kernel
summary
Argues that the kernel interface constrains what a language runtime can offload and what “write once, run anywhere” actually buys, demonstrates a two-function Rust TCP file server that runs unchanged on Linux, Windows, macOS and FreeBSD, and describes building upward from bare metal to a minimal OS: seL4 microkernel with formal verification, an initial-thread C runtime that becomes a memory manager, a serial server, filesystem and process-launcher, and a custom seL4 runtime used at Trustworthy Systems — a practical stack that proves which runtime assumptions break portability.
AI-written summary · about
chapters (21)
- 0:00Intro
- 0:38Anatomy of a run-time
- 1:04Overview
- 1:39Programming language run-time
- 2:10Features of run-times & standard libraries
- 3:42How a runtime provides features
- 4:50Rust on Linux
- 5:33A simple file server
- 8:47Freestanding C18 Embedded applications
- 10:14What is a microkernel? Developing with a microkernel
- 11:36What features does sel4 provide? Developing with a microkernel
- 13:22The initial thread in an sel4 system
- 14:42Crun-time for seL4 initial thread
- 16:09Useful application in the initial thread?
- 17:17Bootstrapping an OS on sel4
- 18:53C runtime for initial OS
- 20:24Full system support Building operating system components
- 22:49Operating system personalities Building operating system components
- 23:30An operating system personality Building operating system components
- 24:06C runtime for our OS personality
- 25:18Requirements of 'portable' run-times
related talks
22mWriting a Container Runtime in Go
44mCompiling the Linux Kernel with gccrs
09mRustc: How I Learned to Respect the Compiler
40mKeynote: Kernel Developer Roundtable
19mRex: Closing the language-verifier gap with safe and usable kernel extensions
11mLightning Talk: What If the Runtime Was Portable Too? Self-Hosted Runtime Capabilitie...
51mRust in the Linux kernel
41mStatus of Embedded Linux