A Mathematical Specification for the Mach Kernel

William R. Bevier Lawrence M. Smith

Computational Logic, Incorporated 1717 West Sixth Street, Suite 290

Austin, Texas 78703-4776 Email: bevier@cli.com, lsmith@cli.com.

Motivation

• Mach-like kernels will likely be a part of some trusted distributed systems.

• It is important to understand their behavior at a level of abstraction above the code.

• Some standardization of Mach features is desirable.

• To this end, we have constructed a detailed specification for the Mach kernel.

What is Mach?

• A kernel on which to build operating systems (e.g., Unix)

• Typical OS functions are out of the kernel:

– Memory Management

– Network Service

– File Systems

• Despite this, Mach is large and complex.

– Multiprocessor implementation.

• Developed at CMU.

• TMach designed at TIS.

• DTMach designed at SCC.

• OSF is doing a kernel re-implementation.