Synchronization Primitives for a Multiprocessor: a Formal Specification
- Andrew Birrell ,
- J. V. Guttag ,
- J. J. Horning ,
- Roy Levin
Proceedings of the 11th ACM Symposium on Operating System Principles |
A preliminary version appeared as SRC Research Report 20. A revised version appeared in Systems Programming with Modula-3, Prentice Hall, 1991
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.