#356 overall
15-410 Operating System Design and Implementation
Carnegie Mellon University
1 recommender · 2 threads · recommended in 2 years, 2018–2021 · score 1.4
15-410 is Carnegie Mellon's operating systems course in which students build a preemptive multitasking kernel from scratch. Commenters also point to course materials that include a lecture on using the SPIN model checker, which is linked from the course site.
Commenters call it a great course, with one saying anyone at CMU should take it if they have a high pain tolerance, and describe the hands-on kernel project as an intense but valuable experience.
CS Fundamentals & Systemsadvancedproject-based#operating systems#kernel#preemptive multitasking#spin#model checking
Recommendations by year
20062026
Anyone who really wants to dig into this, and is willing to be a bit scared, should review the materials for the 15-410 operating systems course at Carnegie Mellon University. The fall edition of the page isn't up yet but there are probably some older versions kicking around.
If you are at CMU you should definitely take this course, as long as your pain tolerance is high.
This course teaches students to write a preemptive operating systems kernel from scratch. It is quite an experience (I TA'd it after finishing my PhD while trying to figure out what to do next).
The kernels the students wrote used to be able to boot on standard (but old) PC hardware. Sadly the modern USB stack is so complex that a conformant thing to talk to a USB keyboard is pretty much as complex as the student's whole project (but less educational). So non-legacy hardware that lacks a PS/2 keyboard no longer has this nice easy path to read/write stuff to console without a lot of setup.
A perennial complaint; Rob Pike had a trollier but similar version years back. I'm not nearly as optimistic that we have the resources to cope with the monstrous complexity of hardware now.
An anecdote I like to share is that while I was TA'ing CMU's 15-410 operating systems course (a great course - build a preemptive multitasking operating system from scratch) was that the student projects could run on real - if old - hardware. There was a PC that could boot your stuff if you put it on a disk.
This PC had to have PS/2 interface to the keyboard, though. A newer PC would be all USB. Apparently, the complexity of the codebase to talk to the USB device was around the similar level of complexity to the entire preemptive multitasking operating system the students were building (and, of course, considerably less educational). I mean, this wasn't a full-functioned OS, but it allowed multitasking and preemption of kernel calls, so seriously non-trivial.
Multiply this story by all the devices a reasonable OS would be expected to talk to and it's a scary prospect for the OS researcher... and if you don't have those devices up and running, good luck supporting most workloads anyone cares about.
When I was a TA for my undergrad operating systems class, I gave a lecture once on using SPIN for basic verification of a handful of mutex implementations, and proving a handful of properties about them. If you want a basic conceptual primer for Spin, I recommend checking it out -- here's a PDF of the slide deck:
http://www.cs.cmu.edu/~410-s11/lectures/L38_SPIN.pdf
And here's a set of resources:
http://www.cs.cmu.edu/~410-s09/lectures/L40_SPIN/spinfiles/
Linked to from the above is another good resource from people who have used Spin -- a formal verification of Linux's RCU design, using Spin:
http://lwn.net/Articles/243851/