Synchronization Primitives for a Multiprocessor: a Formal Specification - Birrell, Andrew; Guttag, J. V.; Horning, J. J.; Levin, Roy (Proceedings of the 11th ACM Symposium on Operating System Principles, 1987)
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, give a formal specification of the synchronization primitives, briefly discuss the implementation, and conclude with a discussion of what we have learned from using the specification for more than a year.
A preliminary version appeared as SRC Research Report 20. A revised version appeared in Systems Programming with Modula-3, Prentice Hall, 1991