SRC Research Report 20
SRC Research Report 20
Formal specifications of operating system interfaces can be a useful part of their documentation. We illustrate this by documenting the Threads synchronization primitives of the Taos operating system. We start with an informal description, present a way to formally specify interfaces in concurrent systems, and then give a formal specification of the synchronization primitives. We briefly discuss both the implementation and what we have learned from using the specification for more than a year. Our main conclusion is that programmers untrained in reading formal specifications have found this one helpful in getting their work done.