Synchronization Primitives for a Multiprocessor: a Formal Specification

  • Andrew Birrell ,
  • J. V. Guttag ,
  • J. J. Horning ,

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.