ERTOS Summer Projects 12/2009 – 2/2010
These project are available to holders of the UNSW/NICTA Summer Research Scholarships. We may also provide some additional scholarships for good students with the a strong OS background who miss out in the official process. Talk to us if you are interested.
Contents
Projects marked 
are not on the official list but are available nevertheless.
Linux Projects
These projects involve work on the Linux kernel or userspace. They will be supervised by Peter Chubb.
- PC90: Interrupt handling for realtime systems
The standard Unix/Linux interrupt handler runs at a very high priority and steals time from the currently running process. As such, under heavy interrupt loads, real time processes can miss their deadlines. There is currently a patch available for Linux, called PREEMPT:RT, that moves interrupt handling to threads that can be given a lower priority than real time processes. However, it seems from the preliminary results that we have as if the advantages possible from using a thread per interrupt are not being fully utilised, and there is a significant performance hit. This project is to evaluate the current, and PREEMPT:RT interrupt handling styles, and to devise more efficient ways to handle interrupts.
more info - PC91: Linux as a Boot Loader
Linux has a feature called `KEXEC' that allows a linux kernel to replace itself with another kernel. Therefore, it should be possible to use a small Linux instance as a boot loader, to boot over NFS or TFTP, without some of the problems that other boot loaders (e.g., U-boot) have. In fact this is done in a small way for the Sharp Zaurus Angstrom distribution. However, it would be really nice to be able to boot systems other than Linux. This project is to develop a root filesystem that in the first case can be used to boot another Linux instance on the BeagleBoard, and when successful, to be able to boot SeL4 plus other components as required.
more info - LR90: Event-Based Device Drivers
The Dingo device driver architecture, developed at ERTOS, helps driver writers produce better code, free of many types of errors found in conventional drivers, including concurrency and protocol errors. The initial version of Dingo was successful in demonstrating the effectiveness of the approach. In order to facilitate wider adoption of the Dingo architecture, we are currently building an open source version of the Dingo framework for Linux. This project is to develop several sample drivers for Dingo. These drivers will be used to test and benchmark the framework and will also serve as examples demonstrating advantages of the Dingo architectures to the Linux kernel community.
more info
Componentisation Projects
These projects deal with the building of componentised operating systems on top of L4 (OKL4 or seL4), and CAmkES the component architecture that supports this. They are supervised by Ihor Kuz and various PhD students.
- IK70: Audio Framework for Embedded OS
Multimedia and audio devices are a popular class of embedded systems. As part of our research into modularised, microkernel-based operating systems for embedded devices, we wish to look at the design and implementation of an audio framework. This involves designing and developing a reusable software framework for audio applications and devices. The framework must be built using the component architecture we have developed for microkernel-based operating systems. Building a demonstrator showing the framework in use will also be part of the work.
more info - IK71: Embedded File System
One of the key services that an OS provides is a file system. We are in the midst of designing and building a modular (L4) microkernel-based operating system for embedded devices. While there are many file-systems available, we do not yet have a suitable file system service for our OS. Furthermore, not much work has been done on the design of a file system service in a componentised environment. This project involves designing and implementing an existing file system to work in a componentised operating system. Besides providing a functioning and reusable system component, it is necessary that the resulting file system also exhibits good performance.
more info - IK80: Linux as a Component
The ERTOS group has done (and commercialised) much work in virtualising Linux to run on the L4 microkernel. We have also done work developing a componentised microkernel-based OS. However the two essentially live in separate worlds. The goal of this project is to integrate virtualised Linux (and its applications) into the componentised OS. One way to do this is to treat Linux as a large component and develop appropriate interfaces and an appropriate framework for this. The project will investigate the best way to do this and implement a prototype system.
more info - IK81: Video phone
A great way to demonstrate the flaws of a componentised operating system is to run a multimedia application on it (which may explain why there are so few of them). Two-way video conferencing is a particularly good demonstration because it uses a large number of operating system components (such as an IP stack and video, camera, and network drivers) and requires careful co-ordination between the scheduler and all threads in the system to manage the large amount of data flow. This project aims to produce a video conferencing application on a componentised operating system. It will involve some implementation work and design and testing of a complete system.
more info
L4 and Embedded Systems Projects
These projects cover a wide range of operating systems and embedded systems research, mostly dealing with L4 and seL4. They are supervised by Kevin Elphinstone, Gernot Heiser, and various PhD students and research engineers.
- KE90: Lottery Scheduling for Embedded Systems
A flexible CPU scheduling mechanism should be able to accommodate many application domains with only configuration of the scheduler being required. One such scheduler that might fufil the role is a lottery scheduler. A lottery scheduler randomly draws a winner to determine which task runs next. The distribution of tickets to tasks is used to affect the scheduling behaviour. This project aims to develop an efficient lottery scheduler and an API for managing the ticket distribution.
more info - KE91: Optimising memory management in a high-performance
secure microkernel
The seL4 microkernel is designed to give unprecedented reliability and security via a formal proof of correctness. However, up until now, seL4's design has focused on correctness, amenability to proof, and security. Limited attention has been given to optimising memory management. This project involves identifying, proposing, and exploring solutions to memory management issues in a modern microkernel. It will give the opportunity for a clever student to have real impact on the evolution of leading-edge operating system technology.
more info - KE92: Covert Channels - building infrastructure to steal secrets
Many operating systems are explicitly designed to keep secrets exactly that - secret. They actively seek to prevent data from leaking from one data clasification (e.g. top secret) to another lower clasification - even if the user actively attempts to violate system security. Your mission, should you choose to accept it, is to develop software to bypass system security to leak secrets using covert channels. The project would be fairly open for the student to survey communications techniques includling signal processing and error correction to develop tools capable of sending secret messages to a collaborator.
more info - GHs80: seL4 vs Singularity
Singularity (using language-based protection) and OKL4/seL4 (using hardware-based protection) are the leading examples of two alternative approaches to OS kernels for high security. This project is to do a quantitative comparison of the two approaches, focussing on the size of the trusted computing base and the performance of systems buillt on top (starting with assessing the basic communication performance).
more info - GHs81: Locking tradeoffs for multiprocessor kernels
Multi-threaded (SMT) processors are characterised by shared caches and very low (single-cycle) communication latencies between execution contexts. Consequently, treads on such a system are scheduled from a single scheduling queue, and other kernel data structures are also shared. This makes fine-grained locking hard and potentially expensive. For a kernel where average latencies of kernel operations are very short, a global kernel lock (i.e., single-threaded kernel) could be an appropriate approach.
This project is to investigate global vs fine-grained kernel locking on the OKL4 microkernel running on a highly (>4) multi-threaded processor core. This is likely to lead to publishable results.
more info - GHs83: NoTA prototype on OKL4
The Network on Terminal Architecture (NoTA) is an emerging approach for structuring software on a mobile phone handset, turning it logically into a distributed system. OKL4 should be the ideal platform for supporting NoTA with low overhead. This project is to demonstrate this by building a prototype NoTA-based system, and evaluate its performance.
more info - GHs90: Performance limits of IPC fastpath implemented in C
High-performance L4 microkernels use traditionally an assembler OfastpathO to overcome the performance problems resulting from C code in the critical IPC system call path. Relying on assembler code has a high engineering and maintenance cost, and makes formal verification harder. Eliminating the need for assembler code, or, at least, reducing the amount needed, would have significant practical benefits. This project is to analyse the IPC path in order to understand why C compilers do not do a better job on it. It will analyse possible (semantically-invariant) modifications of the C code, in order to investigate how far C performance can be pushed, and whether it can be made competitive with the assembler implementation. This study is to be done on at least the ARM architecture (x86 optional) and using several compilers (gcc, RVCT, maybe Green Hills).
more info - IK52: Web Server for L4-based Devices
Any computer system worth its salt must be able to run a web server these days. At ERTOS we are building a research OS based on a component architecture and a microkernel. We already have a (simple) network stack, but we still don't have a web-server! What this project will accomplish is to design and build a componentised web server and OS. But, it doesn't end there. The system must be fast. Therefore a significant amount of effort will also be spent analysing and optimising the resulting system.
more info - GK94: User interface for a high-performance, retargetable
architecture simulator
The aim of this project is to develop a user interface for debugging system-level code in our locally-developed retargetable architectural simulator. You will evaluate the available options (Eclipse plugin, www.eclipse.org vs. Custom-built GUI), take into account usability requirements, and then deliver a frontend module to integrate with the existing (Python based) runtime framework.
more info
Static Analysis and Verification Projects
The following summer projects are strongly related to the verification of seL4 and systems built on top of it. Details can be found on the L4.verified page. They are supervised by Gerwin Klein, June Andronick, and various PhD students and research engineers.
- GK90: A Pragmatic, Formal Verification Framework for ARM
Assembly Code in Isabelle/HOL
Modern operating system kernels such as seL4 are implemented mostly in C and, where performance or hardware access are critical, in assembly. The L4.verified project has created a formal verification framework for low-level C code. This project is about creating a similar framework for the practical formal verification of ARM assembly code in the interactive theorem prover Isabelle/HOL.
more info - GK91: A Formal Verification Framework for Functional
Correctness of User-Level Components in Microkernel Systems
The L4.verified project has produced a formal proof of correctness of the seL4 microkernel. This project fits in the aim of formally verifying, in the theorem prover Isabelle/HOL, the functional correctness of user-level components running on top of a microkernel. This requires turning our existing internal model of seL4 functionality into an external, user-level view of microkernel primitives and integrating this model with an existing verification framework for C programs.
more info - GK92: Processor Modelling for Kernel Verification
The L4.verified project has produced a formal proof of correctness of the seL4 microkernel. The aim of this project is to extend our locally developed model of the ARM architecture to include privileged and system-management behaviour (processor modes, banked registers, memory management). This model underpins the bare-metal correctness proofs for the seL4 microkernel. Project may involve: simulator/HDL-compiler development, model validation on real hardware, formal model development in Isabelle/HOL.
more info - GK93: The Top 100 Theorems
Of the top 100 most famous and interesting mathematical theorems in the world, 80 have now been verified in an automated proof assistant, but only 69 in one theorem prover. Will we be able to get the full 100? This summer project consists of picking a small number of the easier and smaller ones of these famous theorems and prove them in the interactive, industrial grade theorem prover Isabelle. Although this is a fun project, it has the more serious background of driving interactive theorem proving technology and to make this technology more accessible to not-yet-experts. You will learn state of the art theorem proving technology that is also applied to program verification.
more info