AOS Design Guide


The AOS project is a very large and complex system. Often the system is built in an ad-hoc manner with little or no design beforehand, frequently with the attitude that it will be cleaned up later.

This design methodology typically produces a system with only partial functionality. This also involves a lot of writing and re-writing the same code. It is usually also the case that "I'll do it later" never eventuates.

This page lists some of the design choices involved when building SOS to allow you to better understand the difficulties before they occur. You are free borrow or ignore as much or as little of this information as you like. This is only a guide, and any SOS project you want to produce is fine.

Data Structures and Subsystems

While designing SOS you will need to consider a number of different subsystems and data structures, and how they inter-relate.

Some systems you will need to consider include:

Some systems you probably don't need to implement, but still might like to consider are:

Inter-process communication

In Milestone 0 you are required to pass data from an application to the OS in the form of text data for printing. This is an example of passing parameters and data between seL4 address spaces.

There are many ways to pass data between applications, not limited to the following:

Which model you use is up to you, however some mechanisms are more appropriate for some systems and not others (eg. copyin/copyout will not work well with a multi-server OS, and tricky to implement as a recovery-on-fault approach). A poorly designed IPC primitive is a common problem and leads to an inefficient system. You must ensure it is capable of providing fast communication (eg. simple system calls) and also efficient when dealing with large amount of data (eg. file access). You must also ensure your IPC mechanism is free of denial of service (DOS).


Debugging your SOS project can often be a very difficult task. For more information on debugging in seL4 have a look at this page.

L4 Server Thread Management

Regardless of what kind of OS personality you choose to write, you will need to deal with multiple asynchronous requests to your seL4 server(s). There are a number of ways this can be achieved. Once again, this list is neither exhaustive nor truly distinct.

All the above techniques are valid for use in SOS. Each has their own advantages that make them easier/nicer/faster/better/whatever. They also have their own problems with implementation and testing. Make sure your solution is deadlock free, DOS free, thread safe, efficient and easy to debug.

Advanced Work

In AOS you are encouraged to do extra work that you are specifically interested in. This can be in the form of additions to the SOS project, or entirely different OS related projects. Some suggested SOS enhancements for extra marks are listed below. Feel free to come up with your own ideas. If you would like to do one of these (or your own suggestion), talk to us about what is to be done and how marks will be awarded.

Disclaimer: None of these advanced features is easy or trivial. You should avoid making your project dependent on any of these as there is a good chance you will not complete it. You should try to make sure you at least one to two milestones ahead of the marking schedule before you attempt one of these. The motto is "make it work, then make it fancy".

Alternate System Models

There are a number of different general system structures you can use when building an OS personality on top of seL4. A few major categories are listed here. Be aware that this is in no way an exhaustive list, and you are encouraged to come up with or design your own. These categories are also very rough, and in no way well defined.

Monolithic System

Most operating systems, eg. Windows, Linux and any BSD (Net, Free, Open, ...) use a monolithic system model, with most, if not all, of the system implemented in a monolithic kernel.

By placing all system components in the same address space communication is done trivially with shared memory and function calls. Of course, this means that all code in that address space is trusted and can bring down the whole system.

Example of how a typical monolithic (UNIX) address-space layout

This model is the most commonly used for SOS as it is the easiest to implement and debug. Within this model there is plenty of scope for creativity and ample work for two people. Other models are presented here so you can incorporate ideas and abstractions. Students with a keen caffeine dependence are welcome to try them for a system model. There are very few systems to source examples from and many have problems which are as yet unsolved. If you choose a system model other than monolithic, you have been warned.

Single Address Space (SAS)

Single-address-space systems are designed to make sharing between applications easier. By placing all applications and the kernel in the same address space (translation) pointers can be passed around while maintaining their meaning. To preserve security the system needs to implement protection as an orthogonal abstraction.

While a SAS is not necessarily an entirely different model (it could be monolithic or multi-server), it does offer some interesting design decisions. Instead of the typical SOS filesystem you could create a persistent system. A SAS also helps in making a distributed shared memory system.

Example single address space operating systems include Mungi, Nemesis and Sombrero.


A multi-server OS is the holy-grail of microkernel systems. By decomposing the system into components (eg. VFS, file systems, memory management, naming), each in their own address space, the system can be constructed in a more flexible way. Multi-server OSes have a strong tendency to move more work into application libraries rather than the OS modules, but still preserving security. An example Multi-Server OS is Minix 3.

Example multi-server structure on seL4


L4 is a flexible and fast microkernel, however there are other designs for microkernel (and micro-kernel-like) systems including L3, EROS, Mach, Exokernel and K42.

You may choose to pick an existing microkernel (or come up with your own abstractions) and implement this on top of seL4. You will also need to implement elements of SOS on this system to demonstrate its usefulness.

OS161 on seL4

Many students are probably familiar with OS161 used in the introductory operating systems course. OS161 is a specific example of a (simple) monolithic kernel written for the MIPS32 architecture.

One option for the project is to port OS161 to seL4 by adding a new 'seL4' architecture. Because OS161 is already quite complete, it will also be necessary to add extensions and features to make this project in-line with writing SOS from scratch.