A Mathematical Model of the Mach Kernel: Entities and Relations

William R. Bevier and Lawrence M. Smith

Technical Report 88 April 23, 1993

Computational Logic, Inc. 1717 West Sixth Street, Suite 290 Austin, Texas 78703-4776

TEL: +1 512 322 9951 FAX: +1 512 322 0656

EMAIL: bevier@cli.com, lsmith@cli.com.

Not Releaseable to the Defense Technical Information Center per DoD Instruction 3200.12. DISTRIBUTION LIMITED TO U.S. GOVERNMENT AGENCIES ONLY, THIS DOCUMENT CONTAINS NSA INFORMATION (April 23, 1993 14:51). REQUEST FOR THIS DOCUMENT MUST BE RE-FERRED TO THE DIRECTOR, NSA. The views and conclusions contained in this document are those of the author(s) and should not be interpreted as representing the official policies, either expressed or implied, of Computational Logic, Inc.

Copyright \begin{matrix}c \\ ◯ \end{matrix} 1993 Computational Logic, Inc.

Contents

1 Introduction 1

2 Notation 2 2.1 Symbols . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 2.2 Operator Precedence . . . . . . . . . . . . . . . . . . . . . . . 3 2.3 Declarations . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3

3 Primitive Entities 5

4 Threads and Tasks 8

5 Ports and Port Sets 9 5.1 Port Rights . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 5.2 Port Sets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 5.3 Dead Rights . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 5.4 Local Names . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15

6 Virtual Memory 15 6.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 6.2 Abstract Memories . . . . . . . . . . . . . . . . . . . . . . . . 17 6.3 Address Spaces . . . . . . . . . . . . . . . . . . . . . . . . . . 23 6.4 Pages . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25

7 Message Queues and Messages 29 7.1 Message Queues . . . . . . . . . . . . . . . . . . . . . . . . . . 29 7.2 Reply Ports . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 7.3 Messages . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31

8 Physical Resources 35 8.1 Processor Sets and Processors . . . . . . . . . . . . . . . . . . 35 8.2 Devices . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 8.3 Hosts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39

9 Special Purpose Ports 39 9.1 Task Special Ports . . . . . . . . . . . . . . . . . . . . . . . . 39 9.2 Thread Special Ports . . . . . . . . . . . . . . . . . . . . . . . 41 9.3 Processor Special Ports . . . . . . . . . . . . . . . . . . . . . . 42 9.4 Processor Set Special Ports . . . . . . . . . . . . . . . . . . . . 42 9.5 Device Special Ports . . . . . . . . . . . . . . . . . . . . . . . 43 9.6 Host Special Ports . . . . . . . . . . . . . . . . . . . . . . . . 44 9.7 Uniqueness of Special Port Roles . . . . . . . . . . . . . . . . 45 9.8 Notification Ports . . . . . . . . . . . . . . . . . . . . . . . . . 46

10 Consistency of the Specification 47

11 Conclusion 48

1 Introduction

Mach [Ras86] is an operating system kernel that has been under development for a number of years, primarily at Carnegie-Mellon University. It is not a fully functional operating system. It implements a few basic abstractions like task, thread, message and port. Usable operating systems are built on top of the Mach kernel in terms of these abstractions.

This is the first in a series of reports that give a mathematical model of the functional behavior of the Mach kernel version 3.0. We have several goals in doing this work. The first is simply to provide mathematically precise documentation. As documentation, this report supplements existing sources [Loe91b], [Loe91a]. In them, Keith Loepere writes:

Although it is a goal of the Mach kernel to minimize abstractions provided by the kernel, it is not a goal to be minimal in the semantics associated with those abstractions. As such, each of the abstractions provided has a rich set of semantics associated with it, and a complex set of interactions with other abstractions.

— [Loe91b], pg 2.

This is an accurate characterization of the microkernel architecture. We believe that our mathematical formulation clarifies the essential features of Mach by precisely defining required behavior of the kernel interface, and ignoring implementation issues. Of course, by leaving out implementation issues we leave out much of what is interesting about Mach.

Our second goal is to begin the process of defining a contract between Mach users and implementors. It would be a benefit to the Mach community if an unambiguous statement of the required features of a Mach implementation were available. Programs which use only these features would be completely portable. This would make possible program portability at a high level of abstraction.

A benefit of having a mathematically precise contract is that it can be used to resolve disputes about what is compatible with Mach. Is a new feature purely an extension of Mach — or does it modify existing functionality? Such questions can be addressed by proof, not only by testing. This contrasts with programming language based efforts at standardization like [IEE90].

Our third and final goal is to begin research on the formal specification and proof of correctness of applications programs which run on Mach, and of programs and hardware which implement Mach. Ultimately, we would like to have a Mach kernel specification in a form which can be used by a mechanical proof checker. This report provides a first step in that direction.

This report describes the primitive entities and properties of those entities in a Mach kernel state. It states axioms about a “legal” Mach state. Subsequent reports will deal with transitions on a Mach state, ultimately leading to formal specifications for kernel calls.

This report can be viewed as an introduction to Mach, but it assumes at least a familiarity with the overall design goals of the Mach project. We have not attempted to provide complete explanations for every concept introduced. We rely heavily on the existing literature, and make frequent references to [Loe91b] for corroboration.

This report is derived from an annoted “script” of events submitted to Nqthm, the Boyer-Moore theorem prover [BM88]. A script is a file containing function definitions, axioms and theorems in the Nqthm logic. We have arranged for Nqthm to process this script as follows. It checks that all applications of function symbols are syntactically correct, all suggested theorems are in fact true, and all definitions are well-formed. We have used the theorem prover to demonstrate the consistency of the axioms introduced in this report (see Section 10). This report can be thought of as a guide to the Nqthm script, which contains all of the details of our formalization of a Mach kernel state. We have suppressed some of the details in this report for the sake of readability.

Implementation Note. To help motivate and explain our formalization, we refer to the existing Mach implementation in C. These implementation notes are set off from the rest of the text, and may be ignored by the reader who is unfamiliar with, or uninterested in, the Mach implementation.

2 Notation

2.1 Symbols

N the set of natural numbers = equality ≃ set equality ⊆ subset ∩ set intersection ∈ set membershiip ¬ negation ∧ conjunction ∨ disjunction → implication ↔ bi-implication ∃ existential quantification ∀ universal quantification +, −, ∗, ÷ arithmetic operations on natural numbers

E.g., 5 − 2 = 3, but 2 − 5 = 0. Also, 7 ÷ 2 = 3

<, ≤, >, ≥ inequalities on natural numbers ⟨a, b⟩ an ordered pair

2.2 Operator Precedence

We use infix notation for many mathematical expressions. When parentheses are omitted, this can result in ambiguities. Does a ∗ b + c mean (a ∗ b) + c or a ∗ (b + c)? To resolve such ambiguities, we resort to a convention of operator precedence. In the absence of parentheses, one associates arguments to operators according to the following rules.

Minus (−) has the highest precedence. Therefore −a + b means (−a) + b. Next comes integer quotient (÷), remainder (mod) and multiplication (∗), followed by the group consisting of addition (+) and subtraction (−), which is followed by the group =, <, ≤, >, ≥, and ∈. Negation (¬) comes next, followed by conjunction (∧), followed by disjunction (∨). The quantifiers ∀ and ∃ are in the next group. Finally, the group consisting of implication (→) and bi-implication (↔) has the lowest precedence.

As a result of these rules, a ∗ b + c means (a∗b)+c. The logical expression p ∧ q → r means (p ∧ q) → r, and ¬ a ∨ b ∧ c means (¬a) ∨ (b ∧ c).

2.3 Declarations

We specify Mach by introducing functions and predicates that represent Mach concepts, and by stating axioms about them. We introduce a new function symbol in a number of ways. A defined function is introduced as follows.

Definition 2.1 f (x, y) ≡ g (x, y)

Here, f is a new function symbol and g is an expression on f’s arguments involving only previously defined functions.

When we intend only to partially specify a new function symbol, we introduce it with a sequence of declarations. The following form declares a new function symbol and the names of its formal parameters. This information determines the function’s arity, that is, the number of its parameters.

Function 2.2 f (x, y)

Subsequent axioms state assumptions about a function symbol, as in the following example.

Axiom 2.3 p (x, y, z) → f (x, y) = z

In the special case where we intend for a partially specified function to be a predicate, i.e, a function whose range is the set of boolean values {true, false}, we use the following declaration.

Predicate 2.4 p (x, y) where q (x, y)

This declaration introduces a new function symbol p along with the following axioms.

p(x, y) = false ∨ p(x, y) = true
¬ q(x, y) → ¬ p(x, y)

The boolean expression following “WHERE” can be read as implication. It can also be thought of as a guard. The guard defines conditions which must hold for the new predicate to hold. While the guard can be an arbitrary predicate on the parameters to p, we typically write only elementary requirements. In our usage the guard looks like a signature, an expression which states the types of the parameters.

In the Mach specification, certain predicates have particular prominence. A relation is a predicate on one or more Mach entity classes, optional additional parameters from other data types, and a state variable σ. We declare such a predicate in the following way.

Relation 2.5 p (\underline{x}, y, σ) where q (x, y, σ)

The underlined parameters in a relation indicate keys. As in database terminology, a key determines the other parameters of any instance of a relation. The state variable is a part of every key. We refrain from underlining it. For the above example, the following axiom is introduced.

p(x, y_{1}, σ) ∧ p(x, y_{2}, σ) → y_{1} = y_{2}

A relation may have more than one key. When there are two keys, we indicate the second key with overlining. The Mach specification currently has no relation with more than two keys. The following notation indicates that in a given state, a p relation is 1-1 on any x and y.

Relation 2.6 p (\underline{x}, \overline{y}, σ) where q (x, y, σ)

3 Primitive Entities

The definition of each Mach concept involves a state variable σ. One thinks of a Mach property as holding in a given state. A Mach kernel state contains entities from the following disjoint classes: tasks, threads, ports, messages, memories, pages, processors, processor sets, and devices.

A task is the unit of resource allocation. A task holds access to message ports and to memory. A task may contain one or more threads.

A thread represents a flow of control within a task. One thinks of a thread as a program counter together with local register state. All threads share the resources allocated to the task in which they are contained.

A port is container of messages. A task may hold the right to send a message to a port, and/or to receive a message from a port.

A message is a unit of information which can be passed between two tasks. Messages can be used to pass data, and to pass rights to ports.

An abstract memory, or just memory, is a unit of data. An abstract memory has roughly the semantics of a Unix file: it is a mapping from offsets to words. A task cannot access a memory directly—i.e., via a machine instruction. It can only directly access the contents of a page.

A page is the unit of physical memory. A page is a fixed-size sequence of words. A task accesses a page via a virtual address. The primary purpose of a page is to hold a snapshot of some segment of an abstract memory.

A processor is a hardware instruction interpreter.

A processor set is a collection of processors.

A device is one of a number of types of peripheral hardware.

We write taskp (x, σ) to say that x is a task in state σ. We call taskp a recognizer because it recognizes an element of one of the distinguished classes. The names of the other recognizers are threadp, portp, messagep, memoryp, pagep, procp, procsetp, and devicep. Here is the axiom that taskp may not recognize a member of any of the other entity classes. A analogous constraint applies to the other recognizers.

Axiom 3.1

taskp (x, σ) → ¬ threadp (x, σ)

∧ ¬ portp (x, σ)

∧ ¬ messagep (x, σ)

∧ ¬ memoryp (x, σ)

∧ ¬ pagep (x, σ)

∧ ¬ procp (x, σ)

∧ ¬ procsetp (x, σ)

∧ ¬ devicep (x, σ)

In Mach, the kernel is viewed as a task. We introduce the constant kernel to represent the kernel task.

Axiom 3.2 taskp (kernel, σ)

The following is a useful definition. x satisfies entityp in state σ if it is a member of one of the entity classes.

Definition 3.3

entityp (x, σ) ≡ taskp (x, σ)

∨ threadp (x, σ)

∨ portp (x, σ)

∨ messagep (x, σ)

∨ memoryp (x, σ)

∨ pagep (x, σ)

∨ procp (x, σ)

∨ procsetp (x, σ)

∨ devicep (x, σ)

We assume the existence of the constant null-ptr that identifies no entity.

Axiom 3.4 ¬ entityp (null-ptr, σ)

One possible interpretation of the formula taskp (x, σ) is to think of σ as an association list of names and entities. The predicate taskp holds on x when it is a name bound in σ to an entity of type task. One should think of the first argument to a recognizer as a reference to a unique entity, and not as an entity itself.

Implementation Note. The C implementation of Mach suggests an interpretation of the formula taskp (x, σ) which is similar to the association list interpretation. Think of σ as the memory occupied by the kernel, and x as the address of a task structure as defined by the C code. taskp (x,

s) is implemented by a pointer to a task structure. The C structures which implement the other entity classes are thread, ipc port, ipc kmsg (a message), vm object (an abstract memory),

 vm page, processor, processor set, and device.

Webster [Web87] offers the following as a definition of the word entity.

… the existence of a thing as contrasted with its attributes.

This reflects our attitude about Mach entities. At the level of abstraction of this specification, a Mach entity has no contents. It is an element of an abstract data type and may engage in axiomatized relationships with other entities, and with elements of other sets, e.g., integers. The entity classes are only a subset of the elementary data types axiomatized in this paper. We introduce the others, for example port names, as needed in the presentation.

Implementation Note. A relation is typically implemented in the Mach code with pointers and flags. A field within a C structure which is used as a pointer to another implements a relation between instances of the structures. See Section 4 for a particularly simple example.

4 Threads and Tasks

A task contains zero or more threads. The relation task-thread-rel associates a thread with a task.

Relation 4.1 task-thread-rel (t, \underline{th}, σ) where taskp (t, σ) ∧ threadp (th, σ)

A thread belongs to at most one task ^{1}. The identity of a thread’s owning task is a function of a thread and a state σ. The function owning-task is defined to be the unique task to which a thread is assigned, when such an assignment exists.

Axiom 4.2 task-thread-rel (t, th, σ) → owning-task (th, σ) = t

The function threads is the set of threads associated with a task.

Axiom 4.3 task-thread-rel (t, th, σ) → th ∈ threads (t, σ)

Axiom 4.4 taskp (t, σ) ∧ ¬ task-thread-rel (t, th, σ) → th ∉ threads (t, σ)

1cf. [Loe91b], pg. 8

As a result of these axioms, we can conclude that any element of the value of the function threads must be a thread.

Theorem 4.5 taskp (t, σ) ∧ th ∈ threads (t, σ) → threadp (th, σ)

Implementation Note. Taskp is implemented by a pointer to a task structure, and threadp is implemented by a pointer to a thread structure. Task-thread-rel is implemented by the task field of a thread structure. This is a pointer from a thread to a task. A task contains a header to a linked list of threads owned by the task. This suggests the implementation invariant that the task field of a thread th must point to the task in whose thread list th is linked.

5 Ports and Port Sets

5.1 Port Rights

Let N be a set. N is a set of names used to identify capabilities on ports. A task has access to a port only via a name in N. We assume the existence of two distinguished names nullname ∈N, and deadname ∈N.

There are three access rights which a task can have on a port.^{2} R is the set of port access rights.

Definition 5.1

R ≡ {send, receive, send-once}

A port right identifies a task’s name for a port, and what by rights the task may access the port. In port-right-rel, t is a task, p is a port, n is a name and R is a non-empty subset of R. The port right parameter i is a natural number which can be thought of as representing the number of times a given port right has been granted to a task. This value is called the reference count of the port right. In any sequence of states, the value of i is the number of times the right has been granted minus the number of times the right has been revoked.

2cf. [Loe91b], pg. 28

Relation 5.2 port-right-rel (\underline{t}, p, \underline{n}, R, i, σ) where taskp (t, σ) ∧ portp (p, σ) ∧ (n ∈ N) ∧ (R ⊆ R) ∧ (i ∈ N)

Neither nullname nor deadname may serve as the name for a port right. The set of rights in a port right may not be empty. The reference count of a port right is non-zero.

Axiom 5.3 n = nullname ∨ n = deadname → ¬ port-right-rel (t, p, n, R, i, σ)

Axiom 5.4 ¬ port-right-rel (t, p, n, ∅, i, σ)

Axiom 5.5 ¬ port-right-rel (t, p, n, R, 0, σ)

A task and name determine the port in a port right relation, the set of rights held to it, and the reference count of the right. The function namedport identifies the port to which task t holds a right by name n. The function port-rights identifies the set of rights that task t holds to a port by name n. The function port-right-refcount is the reference count of a port right. The reference count of a receive or send-once port right is exactly 1. A send right can have multiple references.

Axiom 5.6

port-right-rel (t, p, n, R, i, σ) → named-port (t, n, σ) = p

∧ (port-rights (t, n, σ) ≃ R)

∧ port-right-refcount (t, n, σ) = i

Axiom 5.7 port-right-rel (t, p, n, {receive}, i, σ) → i = 1

Axiom 5.8 port-right-rel (t, p, n, {send-once}, i, σ) → i = 1

Axiom 5.9 port-right-rel (t, p, n, R, i, σ) ∧ (R ≃ {send, receive}) → 2 ≤ i

The predicate s-right holds on a task and a name in state σ if and only if the name represents a send right in the task. The predicates r-right and so-right recognize names which represent receive and send-once rights, respectively, for a given task.

Definition 5.10

s-right (t, n, σ) ≡ (∃ p, R, i: port-right-rel (t, p, n, R, i, σ)) ∧ send ∈ port-rights (t, n, σ)

Definition 5.11

r-right (t, n, σ) ≡ (∃ p, R, i: port-right-rel (t, p, n, R, i, σ))

∧ receive ∈ port-rights (t, n, σ)

Definition 5.12

so-right (t, n, σ) ≡ (∃ p, R, i: port-right-rel (t, p, n, R, i, σ))

∧ send-once ∈ port-rights (t, n, σ)

A task has only one name for a send or receive right to a given port.^{3} This is called name coalescing.

Axiom 5.13

s-right (t, n_{1}, σ) ∧ s-right (t, n_{2}, σ) ∧ named-port (t, n_{1}, σ) = named-port (t, n_{2}, σ)

→n_{1} = n_{2}

Axiom 5.14

s-right (t, n_{1}, σ) ∧ r-right (t, n_{2}, σ) ∧ named-port (t, n_{1}, σ) = named-port (t, n_{2}, σ)

→n_{1} = n_{2}

Axiom 5.15

r-right (t, n_{1}, σ) ∧ r-right (t, n_{2}, σ) ∧ named-port (t, n_{1}, σ) = named-port (t, n_{2}, σ)

→n_{1} = n_{2}

3cf. [Loe91b], pg. 30

While send and receive rights to a port coalesce in a single name, a sendonce right does not combine with others.^{4} A task holding multiple send-once rights to a given port must hold them with distinct names.

Axiom 5.16 so-right (t, n, σ) → ¬ r-right (t, n, σ) ∧ ¬ s-right (t, n, σ)

At most one task can have a receive right on a port.^{5}

Axiom 5.17

r-right (t_{1}, n_{1}, σ) ∧ r-right (t_{2}, n_{2}, σ) ∧ named-port (t_{1}, n_{1}, σ) = named-port (t_{2}, n_{2}, σ)

→t_{1} = t_{2}

From the name coalescing property of receive rights, one can prove that n_{1} = n_{2} in the constraint above.

The identity of a port’s receiver is a function of a port and a state σ. We call this partial function receiver.

Axiom 5.18 port-right-rel (t, p, n, R, i, σ) ∧ receive ∈ R → receiver (p, σ) = t

Implementation Note. The data type mach port t implements N. The constant mach port null is the implementation of nullname, and mach port dead is the implementation of deadname. The set of port rights granted to a task is maintained in an ipc space structure—each task owns one and only one ipc space. A computation on a mach port t and an ipc space (done by the routine ipc entry lookup) identifies an ipc entry, where a port capability is recorded. The ie bits field of an ipc entry encodes the right and reference count of a port right. The field ie object contains a pointer to the port (an active ipc port structure) involved in the right. If the port is inactive, the ipc entry is interpreted as a dead right (see Section 5.3).

4cf. [Loe91b], pg. 30

5cf. [Loe91b], pg. 25

5.2 Port Sets

A port set is a named aggregation of port right names. The purpose of collecting these names is to permit a task to receive a message from any one of a number of ports.

Relation 5.19 port-set-rel (\underline{t}, \underline{n}, N, σ) where taskp (t, σ) ∧ (n ∈ N) ∧ (N ⊆ N)

Neither nullname nor deadname may serve as the name of a port set.

Axiom 5.20 n = nullname ∨ n = deadname → ¬ port-set-rel (t, n, N, σ)

A port set is uniquely determined by its name in a task. The function port-set identifies the set of receive right names associated with task t and name n.

Axiom 5.21 port-set-rel (t, n, N, σ) → (port-set (t, n, σ) ≃ N)

Port sets are mutually disjoint. In [Loe91b], page 31, this fact is stated by saying that a receive right can belong to only one port set.

Axiom 5.22

port-set-rel (t, n_{1}, N_{1}, σ) ∧ port-set-rel (t, n_{2}, N_{2}, σ) ∧ n_{1} ≠ n_{2} →disjoint (N_{1}, N_{2})

The set of names involved in a port set relation must be a set of receive rights.^{6}

Axiom 5.23 port-set-rel (t, n, N, σ) ∧ n_{1} ∈ N → r-right (t, n_{1}, σ)

Implementation Note. The Mach port set implementation is similar to the port right implementation. A mach port t identifies an ipc entry contained in an ipc space. The ie bits field of an ipc entry indicates whether or not the entry represents a port or port set. If so, the ie object field points to an ipc pset structure, which represents the port set.

6cf. [Loe91b], pg. 31

5.3 Dead Rights

A task may hold a name which represents neither a port nor a port set. This is called a dead right. A dead right usually is created when a port involved in some port right is terminated. The name associated with that right becomes a dead name. As with a send right, a task can have multiple references to a dead right.

Relation 5.24 dead-right-rel (\underline{t}, \underline{n}, i, σ) where taskp (t, σ) ∧ (n ∈ N) ∧ (i ∈ N)

Neither nullname nor deadname may serve as the name of a dead right. The reference count of a dead right is non-zero.

Axiom 5.25 n = nullname ∨ n = deadname → ¬ dead-right-rel (t, n, i, σ)

Axiom 5.26 ¬ dead-right-rel (t, n, 0, σ)

A dead right’s reference count is unique. Therefore, we define dead-right-refcount to be a function on a task and a name.

Axiom 5.27 dead-right-rel (t, n, i, σ) → dead-right-refcount (t, n, σ) = i

Implementation Note. A dead right is implemented by an ipc entry in which (a) the ie bits field signals a dead name and the ie object field equals ip null, or (b) the ie bits field signals a send or sendonce right and the ie object field points to an inactive ipc port structure. Case (b) is lazily converted to (a) when discovered (in the routine ipc right check), so that an inactive port can eventually be reclaimed.

5.4 Local Names

For a given task, a name may be at most one of a port right name, a port set name or a dead name.

Axiom 5.28 (∃ N: port-set-rel (t, n, N, σ)) → ¬ (∃ p, R, i: port-right-rel (t, p, n, R, i, σ))

Axiom 5.29

(∃ i: dead-right-rel (t, n, i, σ)) → ¬ (∃ p, R, i: port-right-rel (t, p, n, R, i, σ))

∧ ¬ (∃ N: port-set-rel (t, n, N, σ))

A local name for a task is either a port right name, a port set name, or a dead name.

Definition 5.30

local-namep (t, n, σ) ≡ (∃ p, R, i: port-right-rel (t, p, n, R, i, σ))

∨ (∃ N: port-set-rel (t, n, N, σ))

∨ (∃ i: dead-right-rel (t, n, i, σ))

6 Virtual Memory

6.1 Introduction

Virtual memory is perhaps Mach’s most subtle subsystem. Its implementation, using copy-on-write techniques to optimize the performance of copying and sharing memory, is complex. We address here not the implementation of virtual memory, but only the abstract view of memories, address spaces, and resident pages.

A Mach address space is a “sparsely populated indexed set of memory pages” ([Loe91b], page 36) associated with a task. To explain our formalization of Mach virtual memory, let us first take a look at the more familiar Unix view. In a Unix system, the entity which is “real” is a single virtual memory M large enough to hold all address spaces. M is, abstractly, a sequence of pages but it is usually implemented by a combination of RAM and backing store.

A virtual address va in task t is conceptually associated with a logical address la in M. Let’s call this mapping vl, for virtual-to-logical translation.

vl : t, va → la ∨ ⊥  (1)

⊥ represents failure. vl failure is caused only by the implementation error that there is not enough RAM and backing store to hold all of M. Abstractly, vl is a total function from virtual to logical addresses, i.e., there are no “address holes” in a task’s address space.

In understanding Unix virtual address translation, we do not usually think about vl. Rather, we think about the mapping vp from virtual addresses to physical addresses that is part of the implementation of vl.

vp : t, va → pa ∨ ⊥

vp maps a task’s virtual address either to a physical address pa or to ⊥, representing a page fault. vp together with page fault handlers implement the more abstract mapping vl.

Now let us look at Mach. Mach generalizes the Unix view to permit multiple memories M_{1}, M_{2}, etc. A virtual address in a task is conceptually associated with a logical address in one of the memories. The virtual-to-logical address translation therefore has the following signature.

vl : t, va → m, la ∨ ⊥  (2)

where m is a memory and la is a logical address in that memory.

The virtual addresses in a Mach address space need not be associated with logical addresses in a single memory. Rather, different virtual addresses in a task can be associated with different memories. A virtual address may be associated with no memory and logical address, i.e., there can be holes in an address space. This is the sparseness referred to above. A page-aligned virtual address always maps to a page-aligned logical address in formula (1) above. This need not be the case in (2).

(2) suffices to characterize the most abstract view of Mach virtual memory. This view does not coincide, however, with the Mach kernel interface. Much of the responsibility for memory management lies outside the kernel, in so-called external memory managers. Each memory is associated with a memory manager that is responsible for maintaining the integrity of the memory’s contents. When a page fault occurs, the kernel enters into a dialog with a memory manager to initialize the necessary resident pages. This dialog is part of the Mach 3.0 kernel interface. We have included in our model of Mach the idea of a resident page, and the notion that a resident page represents a segment of an abstract memory.

In the remainder of this section we present our model Mach virtual memory. Section 6.2 explains properties of abstract memories. We define relations that model a memory’s contents, its control ports, and issues pertaining to its management — shadows and temporary bits. Section 6.3 explains how an abstract memory is mapped into a task’s address space. Finally, Section 6.4 explains how a physical page may represent a region of an abstract memory, i.e., when the memory region is mapped in.

6.2 Abstract Memories

Memory Contents

Let W be a finite set of words. In this document a word is an undefined concept, but we assume that a representation of the number 0 occurs in W. W is implemented by hardware bytes or words.

The relation memoryp recognizes an abstract memory known to the kernel. (We consider a file that exists in a Mach system but is not open to some process not to be an abstract memory in the current state. It becomes an abstract memory when it is made known to the kernel.)

The content of an abstract memory is defined by the store relation. Store is a mapping from natural numbers to words. A natural number in the domain of a memory is called an offset.

Relation 6.1 store-rel (\underline{m}, \underline{o}, w, σ) where memoryp (m, σ) ∧ (o ∈ N) ∧ (w ∈ W)

It is either the case that a memory m and an offset o determine a word w, or else there is no word associated with m and o. We do not axiomatize a memory as a sequence of words, where every offset in some range is guaranteed to be associated with a word. If we did so, then store-rel would give the semantics of a Unix file. This constraint allows us to think of a memory as a partial function from natural numbers (offsets) to words. We use the notation m_{σ}[o] to denote the word associated with offset o in memory m and state σ. For m_{σ}[o] to be defined, o must be in the domain of the memory.

Axiom 6.2 store-rel (m, o, w, σ) → m_{σ}[o] = w

In general, the contents of abstract memories are not implemented by the Mach kernel. They are implemented, rather, by user processes called external memory managers, or just memory managers. The kernel enters into a dialog with a memory manager to handle various aspects of memory management such as page faults, memory creation, and memory termination. Part of the purpose of a dialog is to maintain consistency between a memory and the kernel’s cache.

We place no further constraints on a store-rel relation, since it is beyond the scope of this document to specify any processes above the level of the kernel. It is useful in specifying the kernel to have store-rel declared so that the dialog with an external memory manager can be described. In some cases, the kernel is responsible for initializing all or part of a memory’s store. This occurs, for instance, when a range of zero-filled pages is allocated by the kernel call vm allocate.

Control Ports

Managed memory is paged by some memory manager. It is associated with some special ports: an object port, a control port and a name port. These ports are important in the kernel/memory manager dialog. A memory manager holds a receive right on a memory’s object port, and a send right on a memory’s control port.^{7}. The kernel holds a send right on the object port and a receive right on the control and name ports.

Relation 6.3 object-port-rel (\underline{m}, \overline{p}, σ) where memoryp (m, σ) ∧ portp (p, σ)

7It may be the case that the actual EMM is on a different host. In this case the net message server is the receiver of the object port. The kernel does not treat this case specially – as far as the kernel is concerned, the net message server is the EMM for this memory entity.

Relation 6.4 control-port-rel (\underline{m}, \overline{p}, σ) where memoryp (m, σ) ∧ portp (p, σ)

Relation 6.5 name-port-rel (\underline{m}, \overline{p}, σ) where memoryp (m, σ) ∧ portp (p, σ)

A managed memory determines its object port, and vice versa. Similar constraints hold for control and name ports. We introduce object-port, control-port and name-port to be functions on a memory and a state that give a memory management port.

Axiom 6.6 object-port-rel (m, p, σ) → object-port (m, σ) = p

Axiom 6.7 control-port-rel (m, p, σ) → control-port (m, σ) = p

Axiom 6.8 name-port-rel (m, p, σ) → name-port (m, σ) = p

The functions object-memory, control-memory, and name-memory give the memory associated with a port.

Axiom 6.9 object-port-rel (m, p, σ) → object-memory (p, σ) = m

Axiom 6.10 control-port-rel (m, p, σ) → control-memory (p, σ) = m

Axiom 6.11 name-port-rel (m, p, σ) → name-memory (p, σ) = m

A memory is managed if and only if it has an object port.

Definition 6.12 managed (m, σ) ≡ object-port-rel (m, object-port (m, σ), σ)

No task other than the kernel task may hold a receive right on a control or name port.

Axiom 6.13

control-port-rel (m, p, σ) ∧ (∃ t, n: r-right (t, n, σ) ∧ named-port (t, n, σ) = p)

→receiver (p, σ) = kernel

Axiom 6.14

name-port-rel (m, p, σ) ∧ (∃ t, n: r-right (t, n, σ) ∧ named-port (t, n, σ) = p)

→receiver (p, σ) = kernel

Implementation Note. Memoryp is implemented by a pointer to a

 vm object structure. The pager, pager request and pager name fields

of a vm object name the object, control and name ports, respectively, of an abstract memory. The ipc kobject field of one of these ports contains a back pointer to a vm object. (The back pointer from a name port was added to the Mach 3.0 implementation in 1992.)

Temporary Memories

A memory may be temporary. This affects the behavior of the kernel, for example, when flushing dirty pages. A temporary memory may or may not be managed. A persistent memory is not temporary.

Relation 6.15 temporary-rel (\underline{m}, σ) where memoryp (m, σ)

We’ve presented two orthogonal properties of abstract memories. A memory may or may not be managed and may or may not be temporary. A memory therefore falls into one of the following four categories.

1. Unmanaged, Temporary. A temporary memory is typically unmanaged. The kernel provides the initial represented values in physical memory. The kernel can cause an unmanaged temporary memory to become managed when there is a shortage of physical memory^{8}.

8This is done in the routine vm pageout scan.

2. Managed, Temporary. A managed temporary memory is usually managed by the default memory manager, but the identity of the default memory manager may change. Regardless of the identity of the manager of a managed, temporary memory, the kernel assumes that the pages representing such a memory need not be flushed back to the manager when the memory is deallocated.

3. Managed, Persistent. A persistent memory in always initially managed. The initial represented values for a persistent memory are provided through a dialog between the kernel and an external memory manager.

4. Unmanaged, Persistent. A persistent memory becomes unmanaged when its object port is terminated. Anomalous behavior of an external memory manager can cause this situation, for example, if the memory manager terminates or destroys its object port before the memory it manages is deallocated.

Implementation Note. A temporary memory can be created in the kernel, for example, by vm allocate. A temporary memory is indicated by the logical Or of the internal and temporary bits of a vm object structure. The temporary bit indicates that the object contents are of no interest after the object is unmapped, and can be discarded at that time instead of being returned to the manager. The internal bit indicates that the kernel created the object as opposed to it being mapped in from an external manager. Internal and temporary are currently duplicates (always have the same value).

Shadow Memories

When a memory m_{1} backs a memory m_{2}, the kernel will ask m_{1}’s manager for a page if m_{2}’s manager fails to supply it. This supports Mach’s copy-on-write mechanism. Memory m_{1} backs m_{2} at an offset within m_{1}. We say that m_{2} shadows m_{1}.

Relation 6.16 backing-rel (bm, \underline{sm}, o, σ) where memoryp (bm, σ) ∧ memoryp (sm, σ) ∧ (o ∈ N)

A memory may shadow at most one memory. Thus, backing-rel is a one-to-many relation on memories. The function backing-memory gives a memory’s backing memory if one exists. The function backing-offset gives a memory’s backing offset.

Axiom 6.17

backing-rel (bm, sm, o, σ) →backing-memory (sm, σ) = bm ∧ backing-offset (sm, σ) = o

The function shadow-memories gives the set of memories backed by a given memory.

Axiom 6.18 backing-rel (bm, sm, o, σ) → sm ∈ shadow-memories (bm, σ)

Axiom 6.19 memoryp (sm, σ) ∧ ¬ backing-rel (bm, sm, o, σ) → sm ∉ shadow-memories (bm, σ)

The backing chain of a memory m is the finite sequence of memories transitively related to m via backing-rel. When m shadows no memory, then the sequence is empty. Mach requires that there are no cycles in a backing chain. In other words, a memory is not in its own backing chain.

Axiom 6.20

(0 ≤ i < (length (backing-chain (m, σ)) − 1)) →∃ o: backing-rel (backing-chain (m, σ)_{i+1}, backing-chain (m, σ)_{i}, o, σ)

Axiom 6.21 m ∉ backing-chain (m, σ)

Implementation Note. The shadow field of a vm object points to a memory’s backing object. The shadow offset field of a vm object contains the offset into the backing object. The shadowed bit indicates that this memory is a backing object for some other memory. The Mach implementation guarantees that whenever a page must be copied from a backing memory m to its shadow memories, m has only one shadow memory. (See Section 4.4.5 of [You89] for a discussion of virtual memory copying.) The function shadow-memories is implemented by the copy field of a vm object, which points to the vm object which is its only shadow-memory.

6.3 Address Spaces

The map relation associates a virtual page address (that is, a page-aligned virtual address) vpa in task t with a number of attributes:

1. the contents of a memory m at offset o,

2. an inheritance value, and

3. a current and maximum protection.

The association with a memory and offset formalizes the virtual-to-logical mapping described in Section 6.1. The inheritance attribute is used to determine which regions of a parent task are mapped into a child task upon creation. The protection attributes enforce access control on regions of a virtual address space.

Relation 6.22 map-rel (\underline{t}, m, \underline{vpa}, o, inh, CP, MP, σ) where

taskp (t, σ) ∧ memoryp (m, σ) ∧ (vpa ∈ N) ∧ (o ∈ N) ∧ inh ∈ I ∧ (CP ⊆ P) ∧ (MP ⊆ P)

The set I defines the various inheritance options.

Definition 6.23

I ≡ {share, copy, none}

The set P defines the protection attributes.^{9}

Definition 6.24

P ≡ {read, write, execute}

9The same set is used to define locks on physical pages. See Section 6.4.

The task and virtual address of a map relation determine the other values in a map-rel. The function mapped-memory is the memory associated with task t at virtual address vpa. The function mapped-offset is the memory offset associated with task t at virtual address vpa.

Axiom 6.25 map-rel (t, m, vpa, o, inh, CP, MP, σ) → mapped-memory (t, vpa, σ) = m

Axiom 6.26 map-rel (t, m, vpa, o, inh, CP, MP, σ) → mapped-offset (t, vpa, σ) = o

The function inheritance gives the inheritance attribute of an instance of a map relation.

Axiom 6.27 map-rel (t, m, vpa, o, inh, CP, MP, σ) → inheritance (t, vpa, σ) = inh

We define protection and max-protection to be the set of current and maximum protection attributes, respectively, for a virtual address in a task. The current protection on a virtual address must not exceed its maximum protection.

Axiom 6.28 map-rel (t, m, vpa, o, inh, CP, MP, σ) → (protection (t, vpa, σ) ≃ CP)

Axiom 6.29 map-rel (t, m, vpa, o, inh, CP, MP, σ) → (max-protection (t, vpa, σ) ≃ MP)

Axiom 6.30 map-rel (t, m, vpa, o, inh, CP, MP, σ) → (CP ⊆ MP)

We say that a virtual address va is allocated within a task if the virtual address computed by truncating va to a page boundary occurs in a map relation.

Definition 6.31 trunc-page (va) ≡ va ÷ pagesize ∗ pagesize Definition 6.32

allocated (t, va, σ) ≡ (∃ m, o, inh, CP, MP: map-rel (t, m, trunc-page (va), o, inh, CP, MP, σ))

A memory is mapped if some offset o is mapped to an address within some task.

Axiom 6.33 map-rel (t, m, vpa, o, inh, CP, MP, σ) → mapped (m, σ)

Implementation Note. A task’s address space is represented by a collection of data structures. The map field of a task structure is a pointer to a vm map, which contains the topmost description of an address space. Conceptually, each page index is associated with a vm object (the kernel’s representation of an abstract memory). In fact, the information concerning consecutive indices that share the same vm object, and protection and inheritance attributes (see subsequent sections of this paper), is coalesced into a single data structure called a vm map entry. The object field of vm map entry contains a pointer to a vm object. The offset field is an offset into the abstract memory. The ⟨m, o⟩ pair of a map relation is determined by these two fields. The inheritance attribute of a virtual page index is contained in the inheritance field of a vm map entry. The protection attributes of a page index are contained in the protection and

m protection fields of a vm map entry.

6.4 Pages

A page is a finite sequence of words. The primitive relation that associates a page, offset and word is page-word-rel. All pages have the same size, a constant pagesize, where 0 < pagesize. We use the notation pg_{σ}[i] to denote the ith word of page pg in state σ, where 0 ≤ i < pagesize.

Relation 6.34 page-word-rel (\underline{pg}, \underline{i}, w, σ) where pagep (pg, σ) ∧ (i ∈ N) ∧ (w ∈ W)

A page may represent a portion of length pagesize of a memory at a given offset.

Relation 6.35 represents-rel (\underline{pg}, \overline{m}, \overline{o}, σ) where pagep (pg, σ) ∧ memoryp (m, σ) ∧ (o ∈ N)

The page occuring in a represents relation uniquely determines a memory and an offset. The converse holds as well. A given offset within a memory may be represented by at most one page. Because of these uniqueness axioms, we can introduce the functions represented-memory, represented-offset and representing-page.

Axiom 6.36

represents-rel (pg, m, o, σ) →represented-memory (pg, σ) = m ∧ represented-offset (pg, σ) = o

Axiom 6.37 represents-rel (pg, m, o, σ) → representing-page (m, o, σ) = pg

We say that a page represents memory if and only if it occurs in a represents relation with some memory and offset. A memory and offset are represented if they occur in a represents relation with some page.

Definition 6.38 represents-memory (pg, σ) ≡ (∃ m, o: represents-rel (pg, m, o, σ))

Definition 6.39 represented (m, o, σ) ≡ (∃ pg: represents-rel (pg, m, o, σ))

Implementation Note. We consider an entity that satisfies pagep to be a resident page. A pagep is implemented by a pointer to a vm page structure. A vm page contains the address of a physical page. The fields object and offset of a vm page implement the ⟨m, o⟩ pair of a represents relation. The pages which represent segments of a given abstract memory are linked together. The header of this linked list is the memq field of a vm object. This arrangement suggests two implementation invariants. First, the object field of a vm page must point to the vm object in which the vm page is linked. Second, the offset field of a vm page must be distinct from the offset of each other linked page. Failure to satisfy these invariants would imply violation of the constraints on the represents relation.

A page may be dirty, precious or wired. These attributes affect the dialog between the kernel and the external memory manager.

The dirty attribute characterizes the situation in which a value has been written to a page by a task, but the page is not yet flushed back to a memory manager. If space is short, pages that are not dirty can be deallocated at the whim of the kernel. The kernel assumes that the external memory manager has a copy of the unaltered page on its backing store. Dirty pages must be passed back to the external memory manager before they can be deallocated, so the external memory manager can update its store.

Relation 6.40 dirty-rel (\underline{pg}, σ) where pagep (pg, σ)

In practice, the external memory manager might not retain a copy of information which is represented in a page. The external memory manager can mark a page as precious, which instructs the kernel that it must pass the page back to the external memory manager whether it is dirty or not.

Relation 6.41 precious-rel (\underline{pg}, σ) where pagep (pg, σ)

A page which is wired cannot be evicted from memory under any circumstances. Only privileged tasks, for example device handlers and the default memory manager, can wire pages. A page can be wired multiple times.

Relation 6.42 wired-rel (\underline{pg}, i, σ) where pagep (pg, σ) ∧ (i ∈ N)

A page’s wire count is unique. Therefore, we define wire-count to be a partial function on a page.

Axiom 6.43 wired-rel (pg, i, σ) → wire-count (pg, σ) = i Implementation Note. A dirty page is identified by the dirty bit of a vm page structure. The precious attribute is implemented by a precious bit, and the wired attribute is implemented by the wired count field.

The Mach kernel provides a locking mechanism on pages. A lock associated with a page prevents access of the indicated type. Page locks are applied on request of an external memory manager. The set P defines the locking attributes which can be associated with a physical page.^{10}

Relation 6.44 page-lock-rel (\underline{pg}, P R, σ) where pagep (pg, σ) ∧ (P R ⊆ P)

The set P defines the locking attributes which can be associated with a physical page.^{11}

Definition 6.45

P ≡ {read, write, execute}

The function page-locks gives the unique, non-empty set of locks applied to a page.

Axiom 6.46 page-lock-rel (pg, P R, σ) → (page-locks (pg, σ) ≃ P R)

Implementation Note. The protection attributes of a page index are

 contained in the protection and m protection fields of a vm map entry.

The page lock field of a vm page records a page’s lock attribute.

In the remainder of this section we define the notions of a zero page, and of page equality.

A zero segment is a range of addresses within a page, each of which contains 0. The segment is identified by an offset o and length l.

10The same set is used to define protection attributes on virtual addresses. See Section 6.3.

11The same set is used to define protection attributes on virtual addresses. See Section 6.3.

Definition 6.47

zero-segment (pg, o, l, σ) ≡ pagep (pg, σ)

∧ (o ∈ N)

∧ (l ∈ N)

∧ o + l ≤ pagesize

∧ (∀ i: ((o ≤ i < (o + l)) → pg_{σ}[i] = number-to-word (0)))

A zero page is one in which every location contains 0.

Definition 6.48 zero-page (pg, σ) ≡ zero-segment (pg, 0, pagesize, σ)

Two pages are equal in the range of offsets [o … o+l) if pg-read is identical for both pages in that range. We call this notion page-segment-equal.

Definition 6.49

page-segment-equal (pg_{1}, pg_{2}, o, l, σ) ≡ pagep (pg_{1}, σ)

∧ pagep (pg_{2}, σ)

∧ (o ∈ N)

∧ (l ∈ N)

∧ o + l ≤ pagesize

∧ (∀ j : ((o ≤ j < (o + l)) → pg_{1}_{σ}[j ] = pg_{2}_{σ}[j ]))

Two pages are equal of they are page-segment-equal in the segments ranging from 0 to pagesize.

Definition 6.50 page-equal (pg_{1}, pg_{2}, σ) ≡ page-segment-equal (pg_{1}, pg_{2}, 0, pagesize, σ)

7 Message Queues and Messages

7.1 Message Queues

A port contains a queue of messages. The relation message-in-port-rel asserts that mg is “in” a port p. The parameter i is a member of a totally ordered set — for convenience, we pick the natural numbers. We call i the order number of the message in the queue. It can be thought of as a timestamp, or as an index into a port’s message queue. The function order-ub is an upper bound on the order numbers of messages in a port. We use the notation p_{σ}[i] to denote the message with order number i in port p in state σ.

Relation 7.1 message-in-port-rel (mg, \underline{p}, \underline{i}, σ) where messagep (mg, σ) ∧ portp (p, σ) ∧ (i ∈ N)

Axiom 7.2 message-in-port-rel (mg, p, i, σ) → i < order-ub (p, σ)

The messages in a port are distinct.

Axiom 7.3

message-in-port-rel (mg_{1}, p, i, σ) ∧ message-in-port-rel (mg_{2}, p, j , σ) ∧ i ≠ j

→mg_{1} ≠ mg_{2}

A message occurs in at most one port. The function containing-port is a function on a message that gives its containing port if such a port exists.

Axiom 7.4 message-in-port-rel (mg, p, i, σ) → containing-port (mg, σ) = p

Implementation Note. When a message is sent, the kernel creates a copy of the caller’s data^{a} in an ipc kmsg data structure. We consider this internal representation of a message to be the implementation of messagep. The ipc mqueue field of an ipc port is a message queue. This field’s data type is a structure that contains a header for a linked list of ipc kmsgs.

acf. [Loe91b], pg. 32

7.2 Reply Ports

A message may be associated with a reply port. A reply port is the port to which the receiver of a message may send a reply. To do so, of course, the receiver must have a send right to the reply port. The relation indicates the transferred right.

Relation 7.5 reply-port-rel (\underline{mg}, p, r, σ) where messagep (mg, σ) ∧ portp (p, σ) ∧ r ∈ {send, send-once}

A message may be associated with at most one reply port. As a result, the functions reply-port and reply-right can be defined.

Axiom 7.6

reply-port-rel (mg, p, r, σ) →reply-port (mg, σ) = p ∧ reply-right (mg, σ) = r

Implementation Note. A pointer to the reply port of a message is carried in the msgh local port field of a message header.

7.3 Messages

A message is used to transmit port rights and data. A message is thought of as a finite sequence of data types induced by the relations discussed below.

A transit right is a relation on a message and a port. An assertion of a transit right means that message mg contains an access right r to port p (at index i of the message).

Relation 7.7 transit-right-rel (\underline{mg}, p, r, \underline{i}, σ) where messagep (mg, σ) ∧ portp (p, σ) ∧ r ∈ R ∧ (i ∈ N)

A message and index determine a transit right.

Axiom 7.8 transit-right-rel (mg, p, r, i, σ) → transit-right (mg, i, σ) = ⟨p, r⟩

No task may hold a receive right on a port whose receive right is being transmitted.

Axiom 7.9

transit-right-rel (mg, p, receive, i, σ) →¬ (∃ t, n: r-right (t, n, σ) ∧ named-port (t, n, σ) = p)

Data can be transmitted in two ways: in line and out of line. In line transmission means that the data is placed in the destination task’s message buffer and is copied in word by word. Out of line transmission means that pages containing the data are mapped somewhere into the destination task’s address space.

Data is copied at the time a message is sent. In fact, data that is in transit conceptually is copied into a temporary abstract memory. An abstract memory that is in transit may not be mapped into any address space. (We state this constraint below.)

A transit memory is a relation on a message and a memory. An assertion of a transit memory means that message mg contains an abstract memory m to be inserted in-line or out-of-line in the receiving task. The offset and length parameters indicate a region of the memory which is “of interest” to the receiver. For out of line transmission the entire memory is mapped into the receiver’s address space, but the receiver is informed that the data at offset o for length l is what was sent. The transit memory is the ith element of the message.

Relation 7.10 transit-memory-rel (\underline{mg}, m, a, o, l, \underline{i}, σ) where

messagep (mg, σ) ∧ memoryp (m, σ)

∧ a ∈ {in-line, out-of-line}

∧ (o ∈ N) ∧ (l ∈ N) ∧ (i ∈ N)

A message and index determine a transit memory.

Axiom 7.11

transit-memory-rel (mg, m, a, o, l, i, σ) →transit-memory (mg, i, σ) = ⟨m, a, o, l⟩

No abstract memory occuring in a transit memory may be mapped into an address space. Furthermore, such a memory is temporary.

Axiom 7.12 transit-memory-rel (mg, m, a, o, l, i, σ) → ¬ mapped (m, σ) ∧ temporary-rel (m, σ)

There are several flavors of null message elements. Because a message is used to transmit arguments to a remote procedure, there is a need at times to provide a null port right or null data as an argument. Additionally, a transit right may turn into a dead transit right if the port is killed while the message is queued. We define M to be the set of null message element types.

Definition 7.13

M ≡ {null-right, null-memory, dead-right}

The null message element relation identifies a component of a message that is null, and what flavor of null element the component is.

Relation 7.14 null-message-element-rel (\underline{mg}, tag, \underline{i}, σ) where messagep (mg, σ) ∧ tag ∈ M ∧ (i ∈ N)

The function null-msg-tag gives the tag associated with a null message element.

Axiom 7.15 null-message-element-rel (mg, tag, i, σ) → null-msg-tag (mg, i, σ) = tag

A message is a finite sequence of transit rights, transit memories and null message elements. Since a message is a finite sequence, we use the notation mg_{σ}[i] to denote the ith element of message mg in state σ. mg_{σ}[i] is either a pair ⟨p, r⟩ indicating a transit right, a quadruple ⟨m, a, o, l⟩ indicating a transit memory, or a tag from M indicating a null message element. We write p_{σ}[i][j ] to denote the jth element of the ith message in port p. The function message-size (mg, σ) gives number of elements in a message.

Implementation Note. When a message is sent, the kernel creates a copy of the caller’s data^{a} in an ipc kmsg data structure. We consider this internal representation of a message to be the implementation of messagep. Each element of a message is represented by a type descriptor, either the

data structure mach msg type t or the structure mach msg type long t.

A type descriptor contains fields which determine the type of the element. The msgt name field indicates whether an element is a port right or is data. If a port right, then msgt name indicates which right is being trasferred. If the element is data, then the msgt inline bit indicates whether it is in line or out of line data.

acf. [Loe91b], pg. 32

We say that a port p_{1} transmits a receive right for port p_{2} if p_{1} contains a message m that contains the transit right ⟨p_{2}, receive⟩. The transmission set of a port p is the set of ports closed under transmission of a receive right.

Definition 7.16

transmits-r-right (p_{1}, p_{2}, σ) ≡ ∃ mg, i, j :

message-in-port-rel (mg, p_{1}, i, σ) ∧ transit-right-rel (mg, p_{2}, receive, j , σ)

Axiom 7.17

p_{1} ∈ transmission-set (p, σ) ↔ transmits-r-right (p, p_{1}, σ)

∨ (∃ p_{2}: p_{2} ∈ transmission-set (p, σ) ∧ transmits-r-right (p_{2}, p_{1}))

One can think of a port’s transmission set as identifying a subgraph on the ports in a Mach state. Mach requires that there be no cycles in such a subgraph. In other words, a port is not in its own transmission set.

Axiom 7.18 p ∉ transmission-set (p, σ)

Implementation Note. Mach detects cycles in a transmission graph at the time a receive right is transmitted. All ports involved in the cycle are destroyed, since once a cycle is created no task can gain a right to any port in the cycle.

8 Physical Resources

8.1 Processor Sets and Processors

A processor set is a collection of processors. A processor set is a first class entity because of its relationships with other entities. For example, a processor set has a self port (see Section 9.4). Tasks and threads are also assigned to processor sets for scheduling purposes.

Relation 8.1 procset-proc-rel (procset, \underline{proc}, σ) where procsetp (procset, σ) ∧ procp (proc, σ)

The identity of a processor’s processor set is a function of a processor and a state σ. The function proc-assigned-procset is defined to be the unique processor set to which a processor is assigned, when such an assignment exists.

Axiom 8.2

procset-proc-rel (procset, proc, σ) →proc-assigned-procset (proc, σ) = procset

The function processors is the set of processors associated with a processor set.

Axiom 8.3 procset-proc-rel (procset, proc, σ) → proc ∈ processors (procset, σ)

Axiom 8.4

procsetp (procset, σ) ∧ ¬ procset-proc-rel (procset, proc, σ) →proc ∉ processors (procset, σ)

As a result of these axioms, we can conclude that any element of the value of the function processors must be a processor.

Theorem 8.5 procsetp (procset, σ) ∧ proc ∈ processors (procset, σ) → procp (proc, σ)

Implementation Note. A procset entity is implemented by a pointer to a processor set structure, and procp is implemented by a pointer to a processor structure. We consider procp to be implemented by the kernel data structure, not the actual hardware. procset-proc-rel is implemented

by the processor set field of a processor structure. A processor set

contains the header of a linked list of processors assigned to this processor set. This suggests the implementation invariant that the processor set field of a processor proc must point to the processor set in whose processor list proc is linked.

A processor set is assigned zero or more threads. The relation procsetthread-rel associates a thread with a processor set.

Relation 8.6 procset-thread-rel (procset, \underline{th}, σ) where procsetp (procset, σ) ∧ threadp (th, σ)

A thread belongs to at most one processor set. The identity of a thread’s assigned processor set is a function of a thread and a state σ. The function thread-assigned-procset is defined to be the unique processor set to which a thread is assigned, when such an assignment exists. The function procsetthreads is the set of threads associated with a processor set.

Axiom 8.7

procset-thread-rel (procset, th, σ) →thread-assigned-procset (th, σ) = procset

Axiom 8.8 procset-thread-rel (procset, th, σ) → th ∈ procset-threads (procset, σ)

Implementation Note. procset-thread-rel is implemented by the processor set field of a thread structure. This is a pointer from a thread to a processor set. A processor set contains a header to a linked list of threads owned by the processor set. This suggests the implementation invariant that the processor set field of a thread th must point to the processor set in whose thread list th is linked.

A processor set is also assigned zero or more tasks. This is used only for the default assignment for newly created threads in the task. The relation procset-task-rel and the derived functions task-assigned-procset and processorset-tasks are developed in an analogous manner to the threads’ relations.

Relation 8.9 procset-task-rel (procset, \underline{t}, σ) where procsetp (procset, σ) ∧ taskp (t, σ)

Axiom 8.10 procset-task-rel (procset, t, σ) → task-assigned-procset (t, σ) = procset

Axiom 8.11 procset-task-rel (procset, t, σ) → t ∈ procset-tasks (procset, σ)

Axiom 8.12

procsetp (procset, σ) ∧ ¬ procset-task-rel (procset, t, σ) →t ∉ procset-tasks (procset, σ)

Implementation Note. The relation procset-task-rel is implemented by the processor set field of a task structure. This is a pointer from a task to a processor set. A processor set contains a header to a linked list of tasks owned by the processor set. This suggests the implementation invariant that the processor set field of a task tk must point to the processor set in whose task list tk is linked.

One processor set is known as the default processor set. It cannot be destroyed. The function default-procset is defined to return the default processor set, when one is set.

Relation 8.13 default-procset-rel (procset, σ) where procsetp (procset, σ)

Axiom 8.14 default-procset-rel (procset, σ) → default-procset (σ) = procset

Implementation Note. The default processor set is initialized at bootstrap time in the global variable default pset and is never changed.

One processor is known as the master processor. It is responsible for keeping time on a host. It may not be reassigned to a different processor set. The function master-proc is defined to return the master processor, when one is set.

Relation 8.15 master-proc-rel (proc, σ) where procp (proc, σ)

Axiom 8.16 master-proc-rel (proc, σ) → master-proc (σ) = proc

Implementation Note. The master processor is initialized at bootstrap time in the global variable master processor and is never changed.

8.2 Devices

The kernel interface to devices is very generic. A task gets access to a device port via a device master port. Thereafter, access to the port is via the device port in a device-specific protocol. We display the relation on devices and their special ports in Section 9.5.

Relation 8.17 master-device-port-rel (p, σ) where portp (p, σ)

Axiom 8.18 master-device-port-rel (p, σ) → master-device-port (σ) = p

Only the kernel task may hold a receive right to the master device port.

Axiom 8.19

master-device-port-rel (p, σ) ∧ (∃ t, n: r-right (t, n, σ) ∧ named-port (t, n, σ) = p)

→receiver (p, σ) = kernel

Implementation Note. A pointer to a device structure is the implementation of devicep. The master device port is initialized at bootstrap time in the global variable master device port and is never changed.

8.3 Hosts

We consider a state σ to be the configuration of a given host. We may define functions on a state for obtaining information about a given host. For now, we are content merely to identify the function host-time that gives the global time kept by a host.

Axiom 8.20 host-time (σ) ∈ N

Implementation Note. A host data structure contains only pointers to the two host special ports (Section 9.6). The remainder of the data relevant to a host is distributed in global variables in the kernel task’s address space.

9 Special Purpose Ports

The kernel assigns special meaning to some of its ports. Many of the special ports described in this section are used to make service requests on the kernel. The kernel holds the receive right in these ports. In other cases, the kernel holds a send right on a port, allowing it to asynchronously provide information to a user task. There are other special ports to which the kernel has no rights. These port relations are maintained by the kernel in support of higher-level protocols.

We have already seen three special purpose ports: the memory management ports described in Section 6.2.

9.1 Task Special Ports

A task may be associated with four special ports^{12}. A task self port (also called a task kernel port) identifies a task to the kernel and is used to perform actions in behalf of a task. The task exception port is used by the kernel to convey information about exceptions. The task bootstrap port is typically used for locating services. An task’s sself port typically is identical to its self port. When task A’s sself port differs from its self port, a debugging task holds a receive right on the sself port. The debugging task is said to interpose between the kernel and task A.

12We are currently ignoring the registered ports.

Relation 9.1 task-self-rel (\underline{t}, \overline{p}, σ) where taskp (t, σ) ∧ portp (p, σ)

Relation 9.2 task-eport-rel (\underline{t}, p, σ) where taskp (t, σ) ∧ portp (p, σ)

Relation 9.3 task-bport-rel (\underline{t}, p, σ) where taskp (t, σ) ∧ portp (p, σ)

Relation 9.4 task-sself-rel (\underline{t}, p, σ) where taskp (t, σ) ∧ portp (p, σ)

The special ports of a task are unique. Additionally, a task’s self port is related to only one task. We introduce the function task-self to be the self port associated with a task, and the function self-task to be the task with which a self port is associated.

The other kinds of task special ports need not be related to only one task. The functions task-eport, task-bport, and task-sself have axioms analogous to task-self.

Axiom 9.5 task-self-rel (t, p, σ) → task-self (t, σ) = p

Only the kernel task may hold a receive right to a task self port.

Axiom 9.6

task-self-rel (t, p, σ) ∧ (∃ t, n: r-right (t, n, σ) ∧ named-port (t, n, σ) = p)

→receiver (p, σ) = kernel Implementation Note. Pointers to a task’s special ports exist in a task structure. The ip kobject field of an ipc port is a back pointer from a special port to the entity that it represents. The ip kotype of a port gives a scalar value indicating what the type of special port. A port may play at most one special port role as defined by ip kotype. Section 9.7 discusses this further.

9.2 Thread Special Ports

A thread has a self port, a sself port and an exception port.

Relation 9.7 thread-self-rel (\underline{th}, \overline{p}, σ) where threadp (th, σ) ∧ portp (p, σ)

Relation 9.8 thread-sself-rel (\underline{th}, p, σ) where threadp (th, σ) ∧ portp (p, σ)

Relation 9.9 thread-eport-rel (\underline{th}, p, σ) where threadp (th, σ) ∧ portp (p, σ)

The special ports of a thread are unique, and, additionally a self port is related to at most one thread. Therefore, we introduce the function threadself to be the self port associated with a thread, and the function self-thread to be the thread with which a self port is associated. The functions thread-eport and thread-sself have axioms analogous to thread-self.

Axiom 9.10 thread-self-rel (th, p, σ) → thread-self (th, σ) = p

Only the kernel task may hold a receive right to a thread self port.

Axiom 9.11

thread-self-rel (th1 , p, σ) ∧ (∃ t, n: r-right (t, n, σ) ∧ named-port (t, n, σ) = p)

→receiver (p, σ) = kernel

9.3 Processor Special Ports

A processor has one special port - its self port.

Relation 9.12 proc-self-rel (\underline{proc}, \overline{p}, σ) where procp (proc, σ) ∧ portp (p, σ)

The self port of a processor is unique. Conversely, a self port is related to at most one processor. We introduce the function proc-self to be the self port associated with a processor, and the function self-proc to be the processor with which a self port is associated.

Axiom 9.13 proc-self-rel (proc, p, σ) → proc-self (proc, σ) = p

Axiom 9.14 proc-self-rel (proc, p, σ) → self-proc (p, σ) = proc

Only the kernel task may hold a receive right to a processor self port.

Axiom 9.15

proc-self-rel (th1 , p, σ) ∧ (∃ t, n: r-right (t, n, σ) ∧ named-port (t, n, σ) = p)

→receiver (p, σ) = kernel

9.4 Processor Set Special Ports

A processor set has two special ports, a self port and a name port. A send right to the former gives a task the ability to change the processor set, but the latter may be used only to get information about the processor set.

Relation 9.16 procset-self-rel (\underline{procset}, \overline{p}, σ) where procsetp (procset, σ) ∧ portp (p, σ)

Relation 9.17 procset-name-port-rel (\underline{procset}, \overline{p}, σ) where procsetp (procset, σ) ∧ portp (p, σ)

The special ports of a processor set are unique. Conversely, a special port is related to at most one processor set. We introduce the function procsetself to be the self port associated with a processor-set, and the function self-procset to be the processor-set with which a self port is associated. The pair of functions procset-name-port and name-port-procset have analogous axioms.

Axiom 9.18 procset-self-rel (procset, p, σ) → procset-self (procset, σ) = p

Axiom 9.19 procset-self-rel (procset, p, σ) → self-procset (p, σ) = procset

Only the kernel task may hold a receive right to a processor set’s service ports.

Axiom 9.20

procset-self-rel (procset, p, σ) ∧ (∃ t, n: r-right (t, n, σ) ∧ named-port (t, n, σ) = p)

→receiver (p, σ) = kernel

Axiom 9.21

procset-name-port-rel (procset, p, σ) ∧ (∃ t, n: r-right (t, n, σ) ∧ named-port (t, n, σ) = p)

→receiver (p, σ) = kernel

9.5 Device Special Ports

A device has a special port called the device port.

Relation 9.22 device-port-rel (\underline{dev}, \overline{p}, σ) where devicep (dev, σ) ∧ portp (p, σ)

The device port of a device is unique. Conversely, a device port is related to at most one device. We introduce the function device-port to be the device port associated with a device, and the function port-device to be the device with which a device port is associated.

Axiom 9.23 device-port-rel (dev, p, σ) → device-port (dev, σ) = p

Axiom 9.24 device-port-rel (dev, p, σ) → port-device (p, σ) = dev

Only the kernel task may hold a receive right to a device’s device port.

Axiom 9.25

device-port-rel (th, p, σ) ∧ (∃ t, n: r-right (t, n, σ) ∧ named-port (t, n, σ) = p)

→receiver (p, σ) = kernel

A task gets access to a device port by making a kernel request via the master device port.

9.6 Host Special Ports

For hosts, the terms host name port and host self port are synomyms referring to the information port. The terms host control port or privileged host port refer to the port with which changes can be affected. We define the relations host-name-port-rel and host-control-port-rel, and the functions host-name-port and host-control-port. The relations are between a port and a state, and the functions have only a state argument.

Relation 9.26 host-control-port-rel (p, σ) where portp (p, σ)

Relation 9.27 host-name-port-rel (p, σ) where portp (p, σ)

Axiom 9.28 host-control-port-rel (p, σ) → host-control-port (σ) = p

Axiom 9.29 host-name-port-rel (p, σ) → host-name-port (σ) = p

Only the kernel task may hold a receive right to host service ports.

Axiom 9.30

host-control-port-rel (p, σ) ∧ (∃ t, n: r-right (t, n, σ) ∧ named-port (t, n, σ) = p)

→receiver (p, σ) = kernel

Axiom 9.31

host-name-port-rel (p, σ) ∧ (∃ t, n: r-right (t, n, σ) ∧ named-port (t, n, σ) = p)

→receiver (p, σ) = kernel

9.7 Uniqueness of Special Port Roles

We have identified a number of special roles to which a port can be assigned. There is a subset of these roles for which the kernel guarantees a port’s assignment is unique - the kernel service ports plus memory control ports. For example, a port that is some task’s self port may not also be the device master port. We state this axiom for the task self port as follows. Analogous axioms hold for the other relations.

Axiom 9.32

task-self-rel (t, p, σ) → ¬ thread-self-rel (x, p, σ)

∧ ¬ proc-self-rel (x, p, σ) ∧ ¬ procset-self-rel (x, p, σ) ∧ ¬ procset-name-port-rel (x, p, σ) ∧ ¬ master-device-port-rel (p, σ) ∧ ¬ device-port-rel (x, p, σ) ∧ ¬ host-control-port-rel (p, σ) ∧ ¬ host-name-port-rel (p, σ) ∧ ¬ object-port-rel (x, p, σ) ∧ ¬ control-port-rel (x, p, σ) ∧ ¬ name-port-rel (x, p, σ)

9.8 Notification Ports

A notification port is used for queueing notifications for certain classes of events. The kernel holds a send-once right on the notification port. Mach currently implements the following notification classes.

Port-Destroyed. A port-destroyed notification prevents a port from being destroyed. When an operation attempts to destroy the port, it is instead queued as a transit receive right in the notification message.

Dead-Name. A task is notified when a port is destroyed to which a task has a send right. The local name of the right is included in the notification.

No-Senders. A task is notified when a port to which it has a receive right has no send rights.

Message-Accepted. A task is notified when a message that it wishes to be sent to a port is finally delivered to the message queue.

Port-destroyed and message-accepted notifications will be deleted in subsequent versions of Mach. Therefore, we do not model them here.

Dead-Name Notifications

A dead-name notification is modeled by a relation on a port, a task, and a name. In dn-notification-rel, destruction of the port denoted by name n in task t causes a message containing n to be sent to port p. When the name of a task’s capability on a port is changed (via mach port rename), the dead-name notification relation is modified to reflect the new name.

Relation 9.33 dn-notification-rel (p, \underline{t}, \underline{n}, σ) where portp (p, σ) ∧ taskp (t, σ) ∧ (n ∈ N)

At most one dead-name notification port is associated with a ⟨task, name⟩ pair. The function dn-notification-port gives this port.

Axiom 9.34 dn-notification-rel (p, t, n, σ) → dn-notification-port (t, n, σ) = p Implementation Note. The ip dnrequests field of an ipc port is an array of ⟨port, name⟩ pairs. Each element of the array identifies a port to which a dead-name notification is to be sent when the port denoted by the containing ipc port is destroyed. The notification contains the given name. An ipc entry that represents a name for which there is a dead-name notification request contains an index into the ip dnrequests field of the port denoted by the ipc entry. When a task’s name for a port is changed via the kernel call mach port rename the corresponding entry in ip dnrequests is updated to contain the new name.

No-Senders Notifications

A no-senders notification is a relation on two ports. The first is the notification port. The second is the port for which notification of no senders is to be made.

Relation 9.35 ns-notification-rel (np, \underline{p}, σ) where portp (np, σ) ∧ portp (p, σ)

A port may have at most one no-senders notification port. The function ns-notification-port gives this port.

Axiom 9.36 ns-notification-rel (np, p, σ) → ns-notification-port (p, σ) = np

Implementation Note. The ip nsrequest field of an ipc port contains a pointer to a port’s no-senders notification port.

10 Consistency of the Specification

This formalization of the Mach kernel contains over 400 axioms about some 250 functions. It is important to demonstrate that the axioms are not contradictory, i.e., that they are consistent. One does this by displaying known concepts that satisfy the axioms.

We have used Nqthm ^{13} to demonstrate the consistency of this specification. An Nqthm constrain event permits the introduction of a collection of new function symbols, and axioms which they must satisfy. The Nqthm user must also supply a “witness” to the axioms — that is, a collection of previously defined concepts that provide an interpretation of the new function symbols, and which satisfy the axioms. In this way, consistency of the axioms is proved, since it is demonstrated that there is some collection of concepts that satisfies the axioms.

We have supplied a very simple witness for the Mach state axioms. Interpret each of the relations as a predicate that returns the constant false. The only entity in the state is the kernel task. The axioms follow from this interpretation. This amounts to showing that an (almost) empty state satisfies the axioms. In other work, we hope to demonstrate that a more interesting witness — one that closely models the Mach implementation in C — satisfies tha axioms, as well.

11 Conclusion

This report provides an axiomatic model of the primitive entities in a Mach kernel, and the relations on those entities which a Mach kernel must support. We have partially characterized nine primitive entities: task, thread, port, message, page, memory, processor, processor set, and device. This report represents an axiomatization in the Nqthm logic that contains over 400 axioms on approximately 250 functions. We have proved the consistency of these axioms by giving an interpretation of the new function symbols that satisfies the axioms. If this seems complicated one must remember that even so, it is an abstraction and simplification of the Mach kernel implementation in C.

There are several ways in which the reader may find fault with our mathematical model of Mach. First, we may have omitted some primitive entities which are deemed essential to Mach. Second, we may have omitted some relations on the included entities which are deemed essential. Finally, we may have made an error with respect to the intentions of the Mach designers in describing some relation. We hope that review of this paper will result in elimination of errors and a convergence of opinion on what must be described at the Mach interface.

13The Boyer-Moore theorem prover. See the introduction of this report.

Figures 1 and 2 give a visual representation of the entities and relations in a Mach kernel state. There is a node for each entity class. (Some nodes are duplicated in the two figures. This is done merely to minimize the number of intersecting lines. Three dimensions are required to do justice to the picture.) There is a link between nodes for each relation on two entities. Dangling labeled lines represent a relation involving only members of a single entity class. A Mach state can be thought of as a graph linking nodes (representing instances of the entity classes) via relations. The purpose of the remainder of this report is to specify these relations.

Alternatively, one may think of the axiomatization of a Mach kernel state in terms of a relational database. (See [KS86] for background on relational databases.) Each Mach relation introduced in in this report corresponds to a relation in the database. Each instance of a Mach relation (i.e., an application of a relation predicate to specific arguments) may be thought of as a tuple in the database.

In sum, we may think about the relations in several ways. For example, a task’s ownership of a thread in a kernel state may be thought of as the assertion of some predicate, the existence of a tuple in a relational database, or as a link between two nodes in a state graph.

predicate task-thread(t,th)

tuple [t,th] in a task-thread relation

graph [figure: t; th]

The predicate approach is useful for formal reasoning, and the graph approach for is useful for visualizing a state. As explored in [BS93], the database analogy is useful for addressing atomicity of transitions and concurrency.

We believe that this model of a legal state will make it possible to achieve more thorough analysis of Mach implementations and applications. A companion report [BS93] describes the identification of a collection of fine-grained atomic transitions in terms of which Mach kernel calls can be implemented. We intend to use this model as a basis for studying the correctness of the parallel implementation of Mach kernel calls. As a result of this work we expect the model to evolve somewhat as we fill in omissions, correct mistakes, and respond to design changes in Mach.

The ultimate source of information about Mach, as for many software systems, has been the source code. Description of the system and its underlying design principles exist in a number of published papers and CMU technical reports, e.g., [FR86], [Ras86], [Tev87].

The authors would like to thank the following for their input on this report: Todd Fine, Secure Computing Corporation (SCC), Sue Landauer, Trusted Information Systems (TIS), Spence Minear (SCC), Tim Redmond (TIS), Ed Schneider (SCC), and Matt Wilding (CLI).

[figure: task; thrd; port; mem; msg; page; task-thread; transit-memory; map; represents; backing; self, sself; excpt-port; transit-right; msg-in-port; reply-port; obj-port; ctrl-port; name-port; port-right; self, sself; excpt, bstrap; dn-notify; ns-notify; contents, dirty, lock, precious, wired; null-msg-elem; port-set, dead-right; store, temp]

Figure 1: Mach Entities and Relations

[figure: task; thrd; pset; port; proc; dev; proc-self; procset-thread; procset-task; procset-proc; self-port; name-port; device-port; host-control, host-name; master; master]

Figure 2: Mach Entities and Relations

References

[BM88] Robert S. Boyer and J Strother Moore. A Computational Logic Handbook. Academic Press, Boston, 1988.

[BS93] William R. Bevier and Lawrence M. Smith. A mathematical model of the mach kernel: Atomic actions and locks. Technical Report 89, Computational Logic, Inc., April 1993.

[FR86] R. Fitzgerald and R.F. Rashid. The integration of virtual memory management and interprocess communication. ACM Transactions on Computer Systems, 4(2), May 1986.

[IEE90] IEEE Standard Portable Operating System Interface for Computer Environments. IEEE, New York, NY, 1990.

[KS86] Henry F. Korth and Abraham Silberschatz. Database System Concepts. McGraw-Hill, 1986.

[Loe91a] Keith Loepere. Mach 3 kernel interface. Technical report, Open Software Foundation, May 1991.

[Loe91b] Keith Loepere. Mach 3 kernel principles. Technical report, Open Software Foundation, March 1991.

[Ras86] Richard F. Rashid. Threads of a new system. Unix Review, 4(8), August 1986.

[Tev87] Avadis Tevanian, Jr. Architecture-independent virtual memory management for parallel and distributed environments: The mach approach. Technical Report CMU-CS-88-106, Carnegie Mellon University, December 1987.

[Web87] Webster’s Ninth New Collegiate Dictionary. Merriam-Webster, Inc., 1987.

[You89] Michael Wayne Young. Exporting a user interface to memory management from a communication-oriented operating system. Technical Report CMU-CS-89-202, Carnegie Mellon University, November

Index

I, 23 M, 33 N, 9 P, 23, 28 R, 9 W, 17

allocated, 25

backing-memory, 22 backing-offset, 22 backing-rel, 21

containing-port, 30 control-memory, 19 control-port, 19 control-port-rel, 19

dead-right-refcount, 14 dead-right-rel, 14 deadname, 9 default-procset, 37 default-procset-rel, 37 device-port, 43 device-port-rel, 43 devicep, 6 dirty-rel, 27 dn-notification-port, 46 dn-notification-rel, 46

entityp, 7

host-control-port-rel, 44 host-name-port-rel, 44 host-time, 39 inheritance, 24 iset, 23

kernel, 6

local-namep, 15

managed, 19 map-rel, 23 mapped-memory, 24 mapped-offset, 24 master-device-port-rel, 38 master-proc, 38 master-proc-rel, 38 max-protection, 24 memoryp, 6 message-in-port-rel, 30 message-size, 33 messagep, 6

name-memory, 19 name-port, 19 name-port-rel, 19 named-port, 10 ns-notification-port, 47 ns-notification-rel, 47 null-message-element-rel, 33 null-msg-element-types, 33 null-msg-tag, 33 null-ptr, 7 nullname, 9

object-memory, 19 object-port, 19 object-port-rel, 18 order-ub, 30 owning-task, 8

page-equal, 29 page-lock-rel, 28 page-locks, 28 page-segment-equal, 29 page-word-rel, 25 pagep, 6 port-device, 43 port-right-refcount, 10 port-right-rel, 10 port-rights, 10 port-set, 13 port-set-rel, 13 portp, 6 precious-rel, 27 proc-assigned-procset, 35 proc-self, 42 proc-self-rel, 42 processor-set-tasks, 37 processors, 35 procp, 6 procset-name-port, 43 procset-name-port-rel, 42 procset-proc-rel, 35 procset-self, 43 procset-self-rel, 42 procset-task-rel, 37 procset-thread-rel, 36 procset-threads, 36 procsetp, 6 protection, 24 pset, 23, 28

r-right, 11 receiver, 12 recognizer, 6 reply-port, 31 reply-port-rel, 31 reply-right, 31 represented, 26 represented-memory, 26 represented-offset, 26 representing-page., 26 represents-memory, 26 represents-rel, 26 rset, 9

s-right, 11 self-proc, 42 self-procset, 43 self-task, 40 self-thread, 41 shadow-memories, 22 so-right, 11 store-rel, 17

task-assigned-procset, 37 task-bport, 40 task-bport-rel, 40 task-eport, 40 task-eport-rel, 40 task-self, 40 task-self-rel, 40 task-sself, 40 task-sself-rel, 40 task-thread-rel, 8 taskp, 6 temporary-rel, 20 thread-assigned-procset, 36 thread-eport, 41 thread-eport-rel, 41 thread-self, 41 thread-self-rel, 41 thread-sself, 41 thread-sself-rel, 41 threadp, 6 threads, 8 transit-memory, 32 transit-memory-rel, 32 transit-right, 31 transit-right-rel, 31 transmission-set, 34 transmits-r-right, 34 trunc-page, 24

virtual address, 16 virtual page address, 23

wire-count, 27 wired-rel, 27

zero-page, 29 zero-segment, 29