This is the homepage of the Computer Science for All courses by Professor Christoph Kirsch.
This is an introductory class on systems engineering for bachelor students in computer science. The goal of the class is to introduce basic principles of operating systems for students to understand processor and memory virtualization. Seeing and actually understanding virtualization is the overarching theme of the class, in three sentences: isolation is the semantic problem of systems; virtualization buys performance by introducing self-reference; what a kernel cannot decide, it bounds.
After taking the class, students are able to understand the difference between processes and threads as well as emulation and virtualization, what virtual memory is and how it works, what concurrency is, as opposed to parallelism, how processes and threads synchronize efficiently, and how a memory-safety property of systems code is stated and checked with a model checker.
Week 1 is the talk What is Selfie?. The lectures follow one axis, from the small to the vast to the countable to the uncountable, in six stations: I Size, II Notation, III Meaning, IV Cost, V Machines, VI Intelligence. Each lecture is an HTML deck with a PDF rendering next to it, and ends with a piece of music and, in the introductory class, two things to read. The decks are at selfie.cs.uni-salzburg.at/classes/se.
| week | station | lecture | assignments |
|---|---|---|---|
| 1 | spine | What is Selfie? (pdf) | print-your-name |
| 2 | II | The Machine, Again (pdf) | assembler-parser |
| 3 | III | Emulation (pdf) | self-assembler |
| 4 | III | Virtual Memory (pdf) | |
| 5 | III | Time-Sharing (pdf) | processes |
| 6 | III | Self-Hosting (pdf) | fork-wait |
| 7 | III | Processes (pdf) | fork-wait-exit |
| 8 | III | Concurrency (pdf) | lock, threads |
| 9 | III | Runtime Systems (pdf) | threadsafe-malloc |
| 10 | IV | Verifying Systems Code (pdf) | treiber-stack, rotor-bounds |
| 11 | IV | Cost (pdf) | |
| 12 | III | Universality for Systems (pdf) | |
| 13 | V | Agents as Processes (pdf) | |
| 14 | VI | What is a System? (pdf) |
The class works by explaining the basic principles behind selfie, a software system written in a tiny subset of C called C* that implements a self-compiling compiler targeting a tiny subset of RISC-V machine code called RISC-U, a self-executing RISC-U emulator, and a self-hosting RISC-U hypervisor. Selfie also comes with rotor and bitme, a model generator and a bounded model checker that turn a RISC-U binary into a formula and ask a SAT or SMT solver whether any input reaches a bad state within a bound.
Selfie features an autograder for the systems assignments, one or two per week as listed above, ending with rotor-bounds: state a memory-safety property for a sequential routine of your own systems code, generate its model, and let bitme find the input that violates it, or the bound up to which none does.
The textbook is What is Intelligence? Discovering Unproven Truth; the Computing chapter is this class, and the Meaning and Cost chapters are its theory.
The class is organized as part of a series of Computer Science for All classes.