Using Spin to Help Teach Concurrent Programming

This document accepts as a given that the goal of an undergraduate operating systems course is to teach the principles of concurrent programming, as well as the design and implementation of real operating systems. I will argue that the former is very difficult to teach well, and that it can be taught better with the help of a system that can be used to model and prove properties about concurrent programs