The process of determining the exact behavior of a system call begins with a careful reading of its documentation, including an inspection of the arguments that are passed to the system call, its return values, and their types. Man pages typically specify valid inputs and expected return values. The latter are divided into values that indicate success and values that indicate failures, or exceptions. Based on this information, an initial mock-up of a CCM can be developed.
Figure 2 shows an example, the modeling of the creat system call as a method of the FileSystem CCM. Let us first describe the visual notation. A class machine is a named rounded box that has several compartments: one for attributes and one for each method. A method has an entry point (hollow circle), several exit points (filled circles) and several exception points (filled diamonds). Exit and exception points may be marked with an expression denoting the return value. The entry point is connected to the exit (and exception) points by transitions and method invocations. A transition (shown as a labeled arrow) is an atomic guarded assignment. A method invocation (shown as a rounded box) has an entry point, an exit point and several exception points. Exit and exception points may be marked with variables to hold the return values. Exceptions propagate by default to the enclosing levels. A method may contain local variable declarations. As in UML, an attribute or method marked with + is public.
The creat method takes as arguments a pathname pn and a mode
m, splits the first into a path 
and a name 
, creates a new
file with path 
, name 
and mode 
and returns its file descriptor
. If a file already exists at 
, creat truncates it to zero
bytes. However, the call only works for regular files, not directories (for
which the user should use mkdir). We reflect this condition in the
CCM as follows: if the file name to be created already exists and the type
of that file is dir, then exit this system call with the error
condition EISDIR; otherwise continue to the next step in the CCM.
In cases where the man pages are insufficiently detailed or known to be inaccurate, we inspect the actual kernel sources at or near the entry point of that given system call into the kernel. For example, the manual page for the creat system call (on Red Hat Linux 7.1) does not specify that it will return an ENOQUOTA (quota exceeded) error code if the user's quota was exceeded when trying to add the new file; or that it will return EIO (I/O error) if a hardware failure occurred while trying to add the new file's entry to the on-disk directory. We found these conditions by inspecting the kernel sources for a running version of Linux. Incorporating this behavior into the CCM above is straightforward, and the result is a more complete accounting of the behavior of creat than is available from its man pages. The description is also much more concise; instead of the several pages of text used to document creat, the diagram fits onto less than half a page.
CCM models have several benefits. In addition to their clarity and conciseness, they are executable, which enables application and OS developers to experiment with system calls on different inputs to see how they behave. CCMs also permit inter-system-call analyses in general, and those involving concurrency in particular, to be rigorously studied. For example, suppose one process tries to read a (shared-mapping) memory-mapped file, while another process tries to write to that same file asynchronously not using the mmap-interface. The OS must carefully coordinate the transfer of (possibly cached) data, lock pages and files, to ensure data coherency. Moreover, this seldom-used combination of Unix features should never result in a kernel crash. Whereas a small file system tool named FSX [8], recently released by Apple, can detect a few such anomalies, such tools have to be written by hand. Our method allows such anomalies to be systematically uncovered using fully automatic techniques that thoroughly search the state space of a CCM.
