This is the home page for CS410/510 LLP (Languages and
Low-level Programming), which was taught in Spring 2015, Spring
2016 and, most recently, in Fall 2017 at Portland State
University. This page provides ongoing access to the materials
that were developed for the course, including lecture slides,
demonstration programs, sample code, and lab exercises.
Please feel free to contact the primary author/instructor
with any questions, bug reports, or suggestions related to the
the materials provided here:
Mark P Jones
Department of Computer Science,
Maseeh College of Engineering &
Portland State University.
Licensing: All of the lecture slides are distributed
under the Creative Commons Attribution 3.0 License and almost all
of the source files (i.e., except those that are subject to
licenses by other parties) are distributed under the terms of the
GNU General Public License, Version 3.0. Please see individual
files and folders for further/more specific details.
Acknowledgements: The development of the materials for
this course was supported in part by funding from the National
Science Foundation, Award No. CNS-1422979.
This course is about the development of low-level, bare-metal
systems—with particular focus on microkernels—and
about the role and design of programming languages in this
application domain—from low-level assembly, to high-level
functional and domain specific languages. The course material is
organized in to three parts:
An overview of conventional, low-level programming
techniques. This will include an introduction to some of the
programmable hardware components of a typical PC system (such as
the memory management unit, interrupt controller, and timer) and
their use in the implementation of fundamental operating system
Case studies of practical microkernel
implementations. These case studies will be used to develop a
more detailed understanding of the requirements for the
programming languages that are used in their construction. The
two specific microkernels that we plan to study are "pork", which
is an implementation of L4 developed at PSU, and "seL4", which is
a "security-enhanced" version of L4, developed by a team in
Australia, that uses a capability abstraction for access control
and resource management. The seL4
system, in particular, has gained some fame in recent years as
"the world's first operating system kernel with an end-to-end
proof of implementation correctness and security
Reflections on the design of programming languages for
use in this application domain. This part of the course will
build on and be informed by the examples that we have seen in
earlier sections. In particular, we will look at some of the
distinguishing features of Habit, a functional programming
language with some specific language features and a broad adoption
of abstract datatypes, that has been specifically designed to
target the development of low-level systems.
This course was developed and taught as a component of
"CEMLaBS", which was an NSF-supported research project that ran
from 2014-2018. (The "CEMLaBS" name is a long acronym for an even
longer formal title: "Using a Capability-Enhanced Microkernel as a
Testbed for Language-based Security".) Three versions of the
course described here were offered over a period of three years as
the CEMLaBS project evolved.
The following text provides some brief context for the CEMLaBS
project and a summary of its research goals:
The work on seL4 is rightly celebrated as a landmark for formal
verification, and provides a strong foundation for building
trustworthy systems. The costs of its development and
maintenance, however, are quite high. Moreover, many of the
security properties established in the seL4 verification
(including the absence of code injection attacks, buffer
overflows, and null pointer dereferences) could have been
guaranteed automatically by writing the microkernel in a language
that incorporates language-based security mechanisms such as an
enhanced type system. Motivated by such insights, the specific
goals of the CEMLaBS project are to evaluate: whether it is
actually feasible to write software of this kind in a language
with meaningful, language-based security guarantees; what
practical impact this might have, particularly in reducing
verification costs; and whether it is possible to meet the
performance goals that are typically required in such
There were no formal prerequisites for this class, but students
were expected to have:
Some background in operating systems (as a result of taking
a class like CS333 at the undergraduate level or CS533 at the
graduate level at Portland State University, or similar courses at
Some experience with programming languages (as a result of
taking classes like CS320/421/422 at the undergraduate level or
CS558 at the graduate level);
Prior experience with the Linux command line and standard
toolset, together with significant programming experience. This
is an important practical consideration for the course, which does
involve substantial programming exercises using C and assembly
language in a IA32 Linux environment.
Upon the successful completion of this course, students will be able to:
- Write simple programs that can run in a bare-metal environment using low-level programming languages.
- Discuss common challenges in low-level systems software development, including debugging in a bare-metal environment.
- Explain how conventional operating system features (multiple address spaces, context switching, protection, etc.) motivate the desire for (and benefit from) hardware support.
- Develop code to configure and use programmable hardware components such as a memory management unit (MMU), interrupt controller (PIC), and interval timer (PIT).
- Describe the key steps in a typical boot process, including the role of a bootloader.
- Describe the motivation, implementation, and application of microkernel abstractions for managing address spaces, threads, and interprocess communication (IPC).
- Explain the use and implementation of capabilities in access control and resource management.
- Develop programs using a capability abstraction, like the one provided by the seL4 microkernel.
- Illustrate the use of a range of domain specific languages in the development of systems software.
- Use practical case studies to evaluate and compare language design proposals.
- Describe features of modern, high-level programming languages---including abstract datatypes and higher-order functions---and show how they can be leveraged in the construction of low-level software.
- Explain how the requirements of low-level systems programming motivate the desire for (and benefit from) language-based support.
The class meets over ten weeks with the following schedule of
lectures and labs:
The primary working environment for this class will be a Linux
virtual machine, which can be hosted on Linux, Windows, and Mac OS X
computers using VirtualBox.
Use of the Unix command line, as well as assembly language and C
programming tools is expected.
A detailed set of instructions for building a suitable virtual
machine are available by clicking here.
In addition to being packaged with the corrsponding laboratory
files via the links in the course schedule, the source code for
the sample/demonstration programs and laboratory exercises is
also available on GitHub at: https://github.com/zipwith/llp-labs.
There is no required textbook for this course, but there are
many useful resources available on the web that can be used for
further reading and more detailed documentation. (Students are
not expected to study these materials in depth.) The
following list includes some items that are likely to be
particularly useful. Most of these are available elsewhere on the
public Internet; we provide links to original copies where
possible, but use local copies in some cases. All rights, of
course, remain with the original authors.
Intel® 64 and IA-32 Architectures Software Developer Manuals:
Extensive documentation for the IA-32 architecture is available online from
the Intel website. Among the thousands of pages of information provided there, the
parts that are likely to be of most use for this course are:
Volumes 2A and 2B, which provide reference pages for specific
instructions (with initial letter A-M in Volume 2A and N-Z in
Volume 3A, which covers essential parts of the "operating-system
support environment" of the IA32 architecture.
Note that the pdf files for these manuals include a table of contents
section that you can access directly in standard pdf viewers to navigate
the documents and find the sections that you need more quickly than by
going through them one page at a time.
Using as, the GNU assembler. Available online from
The OSDev Wiki (http://wiki.osdev.org/Main_Page).
A wiki with lots of useful information for people who are interested in operating systems development.
System V Application Binary Interface, 386 Supplement, Fourth Edition.
Available online from:
(Details related to function calling conventions are described in Section 3-9.)
The Multiboot Specification version 0.6.96.
Available online from:
The GNU Grub manual: The GRand Unified Bootloader, version 2.02.:
Available online from:
Executable and Linkable Format (ELF).
Available online from:
Using ld, the GNU Linker.
The current version of the ld manual is available in html format for online viewing at:
Datasheet for the 8259A Programmable Interrupt Controller (PIC).
Datasheet for the 8253 Programmable Interval Timer (PIT).
Datasheet for the 8250 Universal Asynchronous Receiver/Transmitter (UART).
Datasheet for the 8255 Programmable Peripheral Interface.
Datasheet for the 8237 Programmable DMA (Direct Memory Access) Controller.
Reference manual for the NICTA N1 L4 API (rev 2).
Available online from http://l4hq.org/docs/manuals/refman-n1.pdf.
Improving IPC by kernel design (Liedtke, 1993).
Available online from https://www.cse.unsw.edu.au/~cs9242/18/papers/Liedtke_93.pdf.
On µ-kernel construction (Liedtke, 1995).
Available online from https://os.itec.kit.edu/downloads/publ_1995_liedtke_ukernel-construction.pdf.
The performance of µ-kernel-based systems (Härtig et al., 1997).
Available online from https://os.inf.tu-dresden.de/papers_ps/sosp97.pdf.