Synchronization primitives for a multiprocessor: a formal specification
Andrew D. Birrell, John V. Guttag, J. J. Horning, Roman Victorovich Levin · ACM SIGOPS Operating Systems Review · 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.