Proof of a mutual exclusion algorithm. A 'class'ic example

Abstract

In this note, the author presents a proof of the n-processors protocol invented by Peterson. An important part of the proof is the unending effort to make the naturally descriptive language we use to state temporal relationships and the behavior of software sufficiently precise to provide what the students will recognize to be a valid mathematical proof. In particular, no new reasoning tools are presented beyond what the students had presumably encountered in basic mathematics courses, and in particular - induction over the integers.