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.
-
Recent
- The UNIX file system as a recursive function
- Apple’s A5 chip made in Austin
- Richard Stallman speaks
- Dennis Ritchie
- Droning on about computer security
- The multics file system
- Fukushima Robot Blog
- Sinking in too many layers
- Computer architecture, power, and PHP
- VCs bailing on signed term sheets
- American corporate management
- Apple’s Patents possibly covering android
- Computer Science 101
- Why computers are more and more devices for generating heat from electricity
- Dutch masters