seL4 RefOS - Multiserver Example OS Personality
RefOS is a sample implementation of a simple multi-server operating system built on seL4.
The aim of RefOS is to:
- Provide a reference design of a simple multi-server operating system built on seL4
- Provide a sample implementation of how seL4 protocols can be used
- Simplify development and porting of userland programs built on seL4
- Serve as an example codebase to start new component-based seL4 projects
Features
- Simple and light-weight operating system
- Multi-server component based design
- Process and thread abstraction
- Dataspace abstraction
- Shared memory support
- Dynamic mmap and sbrk support
- Userland serial and timer drivers
- Sample user programs include:
- Terminal - a simple terminal program
- Tetris - a port of Micro Tetris
- Snake - a snake game
Release Announcement
RefOS is an OS personality that runs on seL4. RefOS stands for “Reference OS”, the aspirational goal of the project, which is to provide a reference OS personality for seL4.
RefOS is a student project built as a case study to explore more dynamic virtual memory (VM) management systems than the typical static systems architected on separation kernels. When compared to statically allocated systems, a key difference (and complexity) of dynamic VM management is relaxing the assumption that virtual memory (and memory objects) are managed by a single task upon the microkernel (or by the microkernel itself).
RefOS has a distributed VM framework inspired by the Sawmill VM framework [1], though differing in the centralisation of some core book-keeping into a single server (mainly fault forwarding and mapping authorisation). An additional goal of the project was to create tension between user-level and kernel-level VM primitives to enable ongoing kernel experimentation in the area of higher-level VM abstractions.
The current functionality of RefOS consists of processes, an in-memory boot-image file server, and console support. Additionally, some games and test applications have been ported to the system.
RefOS is available at https://github.com/seL4/refos-manifest under a “BSD 2-Clause” license.
[1] Mohit Aron, Jochen Liedtke, Kevin Elphinstone, Yoonho Park, Trent Jaeger, and Luke Deller. 2001. The sawmill framework for virtual memory diversity. In Proceedings of the 6th Australasian conference on Computer systems architecture (ACSAC ‘01). IEEE Computer Society, Washington, DC, USA, 3-10.