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 (mpj@pdx.edu), Department of Computer Science, Maseeh College of Engineering & Computer Science, 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.

Course Description

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:

1. 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 abstractions.

2. 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 enforcement."

3. 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.

Context: The CEMLaBS project:

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 applications.

Prerequisites:

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 other institutions);

• 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.

Course Objectives:

Upon the successful completion of this course, students will be able to:

1. Write simple programs that can run in a bare-metal environment using low-level programming languages.
2. Discuss common challenges in low-level systems software development, including debugging in a bare-metal environment.
3. Explain how conventional operating system features (multiple address spaces, context switching, protection, etc.) motivate the desire for (and benefit from) hardware support.
4. Develop code to configure and use programmable hardware components such as a memory management unit (MMU), interrupt controller (PIC), and interval timer (PIT).
5. Describe the key steps in a typical boot process, including the role of a bootloader.
6. Describe the motivation, implementation, and application of microkernel abstractions for managing address spaces, threads, and interprocess communication (IPC).
7. Explain the use and implementation of capabilities in access control and resource management.
8. Develop programs using a capability abstraction, like the one provided by the seL4 microkernel.
9. Illustrate the use of a range of domain specific languages in the development of systems software.
10. Use practical case studies to evaluate and compare language design proposals.
11. 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.
12. Explain how the requirements of low-level systems programming motivate the desire for (and benefit from) language-based support.

Course Schedule:

The class meets over ten weeks with the following schedule of lectures and labs:

Supporting software:

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.

Reference Materials:

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 2B).

  • 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 https://sourceware.org/binutils/docs-2.25/as/index.html.

• 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: http://www.sco.com/developers/devspecs/abi386-4.pdf. (Details related to function calling conventions are described in Section 3-9.) (local copy)

• The Multiboot Specification version 0.6.96. Available online from: http://www.gnu.org/software/grub/manual/multiboot/multiboot.pdf. (local copy)

• The GNU Grub manual: The GRand Unified Bootloader, version 2.02.: Available online from: https://www.gnu.org/software/grub/manual/grub/grub.pdf. (local copy)

• Executable and Linkable Format (ELF). Available online from: http://www.skyfree.org/linux/references/ELF_Format.pdf. (local copy)

• Using ld, the GNU Linker. The current version of the ld manual is available in html format for online viewing at: https://sourceware.org/binutils/docs-2.29/ld/index.html. (local copy)

• Datasheet for the 8259A Programmable Interrupt Controller (PIC). (local copy)

• Datasheet for the 8253 Programmable Interval Timer (PIT). (local copy)

• Datasheet for the 8250 Universal Asynchronous Receiver/Transmitter (UART). (local copy)

• Datasheet for the 8255 Programmable Peripheral Interface. (local copy)

• Datasheet for the 8237 Programmable DMA (Direct Memory Access) Controller. (local copy)

• Reference manual for the NICTA N1 L4 API (rev 2). Available online from http://l4hq.org/docs/manuals/refman-n1.pdf. (local copy)

• 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.