Proving Operating Systems Correct:#8

One of the longstanding problems with operating systems is that there is no way to validate their correctness in the same way that engineers can calculate the ability of a beam to carry a weight or a wire to carry a current. Well, the problem is worse than that, because we don’t even have a precise way of stating exactly what we want the OS to do. We have APIs, a good thing, but suppose that you want to show that an implementation of pthread_create is correct. The first question is correct according to what specification and then you start trying to figure out a precise way to state the requirements implied by the man page. Not easy. At least for me. This paper is a start.