The Win32 Threads API Specification

Last modified 14 May 1996
This is a work in progress: a TLA specification of the kernel threads procedures from the Windows Win32 Application Programming Interface (API). If you want to be informed when there are significant changes to this specification, send e-mail to me at

This is a complete draft, but it still has lots of minor errors, and possibly some major ones. There are a number of small details missing from the specification, mostly concerning error conditions. Those details are apparently known only within Microsoft. I hope to talk to engineers there to learn these details and correct any inaccuracies in the specification.

The current specification provides a fairly simple model of the API, in which kernel calls and returns are atomic actions. The specification thus does not describe the details of how kernel calls are made. This seems to me to be the appropriate interface for application programmers (and for the implementers), who already understand how procedure calls are coded. I intend eventually to provide a lower-level specification that does model some of the details of kernel calls. I will do this by using an interface refinement that relates the higher-level and lower-level models of procedure calls, and is independent of the particular kernel calls being specified.

The specification is written in an "object oriented" style, which is discussed in the introduction.

The specification is:

Postscript - DVI - LaTeX

To run the document through LaTeX (version 2e required), you will need the following files:
tla.sty - tlaspec92.sty