Advanced Operating Systems
M1: A timer driver
Your first milestone is fairly straightfoward, and should only take you a few hours to complete. However, you should use this as an opportunity to get to used working with your partner, and probably work out exactly how you can work together so you don't end up duplicating work, or worse still not completing essential parts of the project.
Group Work & Version Control
By now you should have got yourself in a group and you should have a group account setup for you. We expect that you are using Git to maintain your source code, and that a repository be setup in your group account with the correct permissions and sticky bits set so that you can both access it. See our git overview page for suggestions.
The aim of this milestone is to design and implement device driver to accurately provide time stamps and trigger activities. You should add a file for the timer implementation and modify the main system call loop to handle timer interrupts.
For many purposes, such as benchmarking, a high clock resolution is desired. The i.MX6 Sabre Lite platform features a clock controller module which contains several high-frequency and low-frequency counters which are used as timers. A high clock resolution timer is desirable for benchmarking, i.e. accurately measuring elapsed time for completion of some unit of work. Using the timer you implement in this milestone, you will be measuring the performance of the file system that you implement in milestone 6. Thus your timer needs to be capable of providing high resolution time stamps.
The Driver Interface
Your driver needs to export the interface specified
The above interface is just an internal function call
interface. You do not need to export this interface to the
users. User programs will indirectly access the clock driver through
NOTE: After registering an interrupt, you must call
The i.MX6Q Sabre Lite
This is a block diagram of the i.MX6Q Sabre Lite. The Sabre Lite is a single chip computer (or system-on a chip, SoC) which has a Quad core ARM9 Cortex A9 processor and lots of integrated hardware. The SoC reference manual can be found here.
Although the Sabre is a complex platform with lots of functionality, we will only be implementing a driver for the Enhanced Periodic Interrupt Timer (EPIT) and/or General Purpose Timer (GPT) modules. If you are interested in device drivers for the other components in the chip, particularly the networking stacks then explore the directory libs/libethdrivers.
General Purpose Timer Modules
Your main job is to learn how to program the Sabre Lite's EPIT and/or GPT timers to generate timer interrupts and how to write a seL4 driver to handle these interrupts.
The Sabre Lite's i.MX6 SoC has many peripherals for various purposes, such as GPU, UART, video, watchdog and so on. For our purposes, we are interested in using the timers EPIT1, EPIT2 and GPT, to set them up as our sources of timer interrupts. The EPIT and GPT timer modules have very similar interfaces.
Implementing a device driver really just a matter of learning about its registers, what values to read and write to those registers, and when to do it. You may choose to start with implementing either the EPIT or the GPT timer. This milestone can be implemented with a single or multiple timers.
The minimal subset of a timer module's functionality that you must understand and use is listed below. You may find the registers for GPT are very similar to EPIT. Refer to Chapter 24, 30 and 18 of the i.MX6 SoC manual for more complete descriptions.
This is only the minimal understanding that you need. You are encouraged to explore other registers for a deeper understanding.
NOTE: This section is deliberately kept short (e.g., we do not dictate which timer to use or in what mode to use it in). The idea is for you to develop your own design and implementation. There are only two conditions that must be satisfied:
For this project you have been supplied with skeleton code to help you along the way. This code is intended as an implementation guide, not as a 'black-box' library.
It is important that you fully understand all provided code that you use. For the purposes of assessment, we treat any supplied code that you call as your code and as such you may be asked to describe how it works.
The seL4/ARM kernel exports specific interrupts to a user level interrupt handler via asynchronous notification.
You will need to perform a series of steps to register to receive interrupts and manage interrupts for the timer device.
Before attempting this, you should read Chapter 5 of the sel4 documentation to gain an understanding of TCBs, and Section 7.1 to understand how interrupts are delivered.
In seL4/ARM, device registers are memory mapped. That is, hardware
registers can be accessed via normal load/store operations to
special addresses. To access device registers, you must first map
the device into the driver's virtual address space with the
appropriate attributes. A function to achieve this has been provided
for you in
You may need to resolve some or all of these issues:
You should be able to show some test code that uses all the functions specified in the driver interface. Specifically set up and demonstrate:
Last modified: 05 Aug 2014.