Today we announce the release of the RefOS project.  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.