Mach-Based Channel Library Citation Manohar, Rajit (1994) Mach-Based Channel Library. Master's thesis, California Institute of Technology. doi:10.7907/q2v9-sq59. https://resolver.caltech.edu/CaltechTHESIS:04122012-094328813 Abstract No abstract. Item Type: Thesis (Master's thesis) Subject Keywords: Computer Science Degree Grantor: California Institute of Technology Division: Engineering and Applied Science Major Option: Computer Science Thesis Availability: Public (worldwide access) Research Advisor(s): Chandy, K. Mani Thesis Committee: Unknown, Unknown Defense Date: 7 July 1994 Record Number: CaltechTHESIS:04122012-094328813 Persistent URL: https://resolver.caltech.edu/CaltechTHESIS:04122012-094328813 DOI: 10.7907/q2v9-sq59 Default Usage Policy: No commercial reproduction, distribution, display or performance rights in this work are provided. ID Code: 6911 Collection: CaltechTHESIS Deposited By: Benjamin Perez Deposited On: 12 Apr 2012 17:48 Last Modified: 09 Nov 2022 19:20 Thesis Files Preview PDF - Final Version See Usage Policy. 1MB Repository Staff Only: item control page

Mach-Based Channel Library 12 123 12 1 2 12 12 1 12 12 123 12 12 123 1 12 12 Rajit Manohar Advisor: K. Mani Chandy Department of Computer Science California Institute of Technology Pasadena, CA 91125. July 7, 1994 In partial Fulllment of the Requirements for the degree of Master of Science Acknowledgments I foremost want to thank my research advisor Prof. K. Mani Chandy for his guidance and support. I would like to thank the members of my research group|Peter Carlin, Peter Hofstee, Svetlana Kryukova, K. Rustan M. Leino, Berna Massingill, Adam Rifkin, Paul Sivilotti, John Thornley|for comments, constructive criticism, and invaluable discussions. This research was supported in part by Air Force Oce of Scientic Research grant number 91-0070. Contents 1 Introduction 1.1 Motivation 1.2 Overview 4 : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 2 Introduction to Mach 4 5 6 2.1 Overview 2.2 Threads and Tasks 2.2.1 Scheduling 2.2.2 Creating Tasks and Threads 2.3 Ports and Messages 2.3.1 Access Rights 2.3.2 Internals 2.4 C-Thread Library 2.4.1 Thread Functions 2.4.2 Mutex Variables 2.4.3 Condition Variables : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 3 Specication 6 7 7 8 8 9 9 10 10 11 11 12 3.1 Preliminaries 3.1.1 Conventions 3.2 Initialization 3.3 Channels 3.4 Communication 3.5 Processes and Threads : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 2 12 13 14 14 15 16 CONTENTS CONTENTS 4 Implementation 18 4.1 Issues 4.1.1 Channels 4.1.2 Threads and Processes 4.1.3 Termination and Channel Close 4.2 Network Channel Server 4.2.1 Channel Table 4.2.2 Log File 4.2.3 Messages 4.2.4 Code Outline 4.3 User Interface 4.3.1 Channel Table 4.3.2 Message Handling 4.3.3 Argument Passing 4.3.4 Code Outline 4.4 Possible Improvements : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 5 Proof Outline 18 18 19 19 19 20 21 22 24 26 26 27 28 29 31 33 5.1 Network Channel Server 5.1.1 Properties 5.2 User Interface 5.2.1 Properties 5.3 Outline of Proof : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 6 Example programs 6.1 Producer-Consumer 6.2 Sorting 33 33 36 36 37 40 : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 7 Conclusion 40 41 44 3 Chapter 1 Introduction 1.1 Motivation We think of a parallel computation to be one that involves a number of tasks cooperating in some fashion. The manner in which the tasks cooperate becomes an important issue. There are two basic paradigms that describe cooperation between tasks: 1. Use of Shared Variables. In this technique the cooperating tasks share certain data structures, which are used to exchange information. 2. Message Passing. The message passing paradigm constrains the parallel computation in two ways: i tasks do not share any data ii the only way that tasks can exchange information is by sending messages to each other. Sometimes, the rst constraint is relaxed, resulting in a computation that uses both shared variables and messages. Mach, an operating system developed at Carnegie Mellon University 1 , provides support for both these paradigms. However, the exibility provided by the operating system makes it dicult to reason about programs. The support provided for message passing focuses the attention of a user on the details of the communication layer provided by the operating system. The goal of this thesis is to write a small message-passing library|using the support provided by Mach|for parallel computation. This library should be easy to use, language independent, and robust. It should focus attention on the message passing abstraction itself, rather than on the details of the underlying operating system. By imposing restrictions on the functions that are available, the library should simplify arguments involving program correctness. The model chosen for the library is the one provided by Mach itself, in which tasks can communicate with one another by sending messages. Communication streams known as channels are provided that allow the user to think about the logical connections between cooperating tasks. Since the concept of channels is central to the library, we call it a channel library. 4 CHAPTER 1. INTRODUCTION 1.2. OVERVIEW Mach provides kernel support for message passing. Since all Mach services are accessed through the message passing mechanism, the message passing mechanism provided is robust. As will be seen in chapter 2, the operating system enforces a system of access rights, which prevent tasks from exchanging messages unless they have permission to do so. In addition, the message passing mechanism provided is reliable, even across machines. Finally, the operating system provides kernel support for fair threads. We chose the Mach operating system as our base because of these features. The functions provided by the channel library can be grouped into four basic categories functions for: 1. Initialization. 2. Creating channels. 3. Sending and receiving messages. 4. Creating new tasks or threads. 1.2 Overview Chapter 2 provides a brief introduction to the relevant concepts of the Mach operating system. Chapter 3 describes the interface provided by the channel library, by specifying each function provided by the library. In chapter 4, the implementation of the library is discussed in detail. Chapter 5 shows some of the major properties and invariants maintained by the library, and indicates how a rigorous proof of the library implementation could be constructed. Chapter 6 provides a few example programs that illustrate how the library is to be used. 5 Chapter 2 Introduction to Mach 2.1 Overview The Mach operating system was developed at Carnegie Mellon University CMU. The goal of the project was to write an operating system with a small kernel that would provide a few powerful primitives that a programmer could use to construct complex programs. With this in mind, the Mach kernel has been written to provide three basic services: Scheduling. Inter-process communication. Virtual memory management. All other features are built on top of these three basic services. As a result, a number of services that are part of the kernel of traditional operating systems, such as UNIX 2 , are user-level applications that run on top of the Mach kernel. The Mach operating system is compatible with 4.3BSD UNIX, and most BSD programs can be executed under the Mach operating system without modi cation after recompilation. Our main concerns when implementing the channel library on top of Mach are the following: Process creation. Thread creation. Communication. We will therefore restrict our attention in this chapter to describing the scheduling and inter-process communication IPC aspects of the Mach kernel. 6 CHAPTER 2. INTRODUCTION TO MACH 2.2. THREADS AND TASKS Two tasks with a partially shared address space. A single thread executing within Each thread has access rights of the task. Threads share a single task. a common address space. Traditional Process Task with many threads Figure 2.1: Tasks and Threads 2.2 Threads and Tasks Under the Mach operating system, the concept of a process has been divided into two parts: the task and the thread. A task is an environment in which execution of a program occurs. The task consists of a virtual address space and access rights which give the task access to certain services and resources provided by the system. The virtual address space of a task cannot be accessed by another task unless explicit permission to do so is granted by the task. A thread is the unit of execution. Threads execute within a task, which provides an environment for execution. Threads within a task share access rights of the task and the virtual address space of the task. Many threads can execute within a single task, and they all share the same address space as shown in g. 2.1. Thus, a traditional process consists of a single thread executing within a single task. 2.2.1 Scheduling Mach provides a exible thread scheduling method. Each thread has associated with it a priority and a policy. The policy indicates the scheduling method to be used for the thread. We will discuss the timesharing policy only, since it is the default, and the only policy we will use. The timesharing scheduling policy ensures that execution of threads is weakly fair: every thread executes eventually. To ensure this, each thread is assigned a priority which decreases with the execution time of the thread. As a result, a thread with a high priority can never starve a low priority thread, thus ensuring that execution is weakly fair. 7 CHAPTER 2. INTRODUCTION TO MACH 2.3. PORTS AND MESSAGES machine2 machine1 remote procedure call proc rsh machine2 "proc" Figure 2.2: Remote Shell Program 2.2.2 Creating Tasks and Threads A thread is dened by specifying the state of the thread, i.e., the state of the processor when the thread is being executed on it. This state typically consists of the program counter, hardware registers, and the execution stack of the thread. As a result, creating a thread also involves the assignment of a valid state to the thread. Tasks can be created in various ways. However, for the purpose of the channel library we are interested in creating tasks on remote processors. As a result, the remote shell execution program rsh can be used Fig. 2.2. This program takes the name of an executable and a machine as arguments, and spawns a new task with a single thread of execution on the remote host. The rsh program comes with the Mach operating system. 2.3 Ports and Messages Under Mach, tasks and threads can communicate with each other by sending messages. This message-passing mechanism is supported through two basic abstractions: messages and ports. A message consists of a xed header|which contains information about the length of the message and its destination|and a list of typed values. Messages are the basic unit of communication. They can be of arbitrary length, and can contain data, pointers, or ports. In Mach, the destination of a message is specied by a port. Any message sent to a port is stored internally by the Mach kernel. Conceptually, a port is like a mailbox: there are a number of tasks that can insert messages into the port threads in at most one task can remove messages from the port. 8 CHAPTER 2. INTRODUCTION TO MACH 2.3. PORTS AND MESSAGES Tasks sending messages to port M. Single task, removing messages from port. Port M, which contains some messages. Figure 2.3: Mach communication ports 2.3.1 Access Rights Each port has two access rights associated with it: send rights, and receive rights. If a task has send rights for a port, it can send messages to that port. If a task has receive rights for a port, it can receive messages that have been sent to the port. Only one task may have receive rights for a port. Multiple tasks can have send rights for a single port. Note that threads within a task have all the access rights of the task. Therefore, there could be multiple threads which have receive rights for a single port. Port rights can be granted to a task by sending them to the task in a message. If a message contains a port, then the port rights the task has for that port are sent to the task that receives the message. If send rights are sent in a message, then send rights are kept by the originator of the message as well as passed to the recipient. Since at most one task can have receive rights for a port, if receive rights are sent in a message, the sender no longer has receive rights for the port. 2.3.2 Internals Internally, a port consists of a nite queue of bounded size which contains the list of messages that have been sent to the port. The size of this queue can be specied for a given port. A task with receive rights can dequeue messages from this internal queue. Sending a message to a port appends the message to the queue associated with the port. Sending a message to a port whose queue is full will result in the suspension of the sender. Ports can refer to tasks on the local machine or tasks across the network. The interface to the ports is exactly the same. The only dierence is that ports over the network are handled transparently by the Mach network server. The network server implements network ports, which represent ports on remote machines. These ports are used by tasks to send messages to remote machines. Mach provides a port server known as the network name server. This server enables a task to associate a port with a name. Other tasks can then look up the port of interest using the name associated with the port. This name server is used to 9 CHAPTER 2. INTRODUCTION TO MACH 2.4. C-THREAD LIBRARY Thread t1 suspends, since the port queue is full. t2 receive t1 send Port queue which can contain at most three messages. Figure 2.4: Mach ports|Internal queue register a service, which then allows other tasks to use the service by looking up the service port from the name server. For instance, if an application programmer decided to write a server that provided access to a remote le system, then the programmer could register this new server with the network name server by giving it a name. Now any application that wants to use this new service can look up the port for the le system server and then send requests for remote les to the server using the port it receives from the name server. 2.4 C-Thread Library The C-thread library consists of functions that are used to manipulate and synchronize threads 3 . This library provides an interface to the Mach kernel services for thread creation and synchronization. The following three main classes of functions are provided by the library: 1. Functions that are used to manipulate threads. 2. Mutex variables, and functions to manipulate them. 3. Condition variables, and functions to manipulate them. Synchronization in the C-thread library is done using condition and mutex variables. 2.4.1 Thread Functions The thread functions can be used to create, terminate, and schedule threads. These functions call existing Mach functions with the appropriate parameters. The main advantage of using the thread functions from the C-thread library rather than the ones provided by Mach is that the C-thread library is portable across architectures. As mentioned earlier, creating a thread in Mach involves setting up the state for the thread. This involves assigning values to hardware registers, which dier from machine to machine. The C-thread library can be used to spawn a thread that starts execution from a function that takes a single argument. All the information required to set up the state can be determined by knowing the C compiler on the system, and the address of the function being spawned. 10 CHAPTER 2. INTRODUCTION TO MACH 2.4. C-THREAD LIBRARY 2.4.2 Mutex Variables Mutex mutual exclusion variables are used to protect access to shared data structures. A mutex variable can be in one of two states: locked or unlocked. A thread attempting to lock a mutex variable will suspend if the mutex is in the locked state. If the mutex variable was unlocked, the mutex will be locked, and execution of the thread will continue. Unlocking a mutex will resume execution of one thread that was suspended due to a lock operation on the mutex. The following functions operate on mutex variables: is used to lock the mutex variable m. mutex_unlockm is used to unlock the mutex variable m. mutex_lockm Initially, the mutex variable is unlocked. Consider the following example: ... mutex_lockm modify data structure mutex_unlockm ... If all access to the data structure are protected with the mutex m as above, then we know that at most one thread can modify the data structure at a time. 2.4.3 Condition Variables Condition variables are used when a thread wants to wait for another thread to complete some action. Every condition variable must be associated with a mutex variable. Two basic operations on condition variables are allowed: signal and wait. A call to function condition_waitc,m does the following actions: 1. The mutex m is unlocked. 2. The thread is suspended waiting for a signal on the condition variable c. 3. On receiving a signal, the mutex m is locked. wakes up a single thread if any waiting on a condition variable. Condition variables can be used to selectively wake up threads that might be suspended waiting for some boolean condition to hold. condition_signalc 11 Chapter 3 Specication 3.1 Preliminaries The channel library provides the following three basic abstractions: Processes. Threads. Channels. A process can be thought of as a virtual address space. A process is similar to a Mach task. The major dierence between Mach tasks and processes is that processes do not share memory. Therefore, two processes cannot interact through shared data structures. The concept of a thread is the same as the one in Mach. Threads run within a process, and they share data with other threads in the same process. The major departure from the Mach model is in the abstraction provided for communication. The channel library provides abstract communication streams known as channels Fig. 3.1 which are used for communication and synchronization. These channels can be thought of as rst-in- rst-out FIFO message buers. Three operations can be performed on a channel: 1. Send message along channel. Sender 1 Channel outport (one of three). Channel inport. Queue of messages. First-in-First-Out. Sender 2 Sender 3 direction of motion. Figure 3.1: Channel 12 Receiver CHAPTER 3. SPECIFICATION 3.1. PRELIMINARIES 2. Receive message from channel. 3. Close channel. Sending a message along a channel is equivalent to inserting the message into the FIFO. Receiving a message from a channel is equivalent to removing the next message from the FIFO. The close channel operation is somewhat dierent in that it inserts a special message into the buer. This message indicates that no more messages will be received along the channel. Furthermore, the sender cannot send a message along the channel after closing the channel. Once a receiver removes the close channel message from a channel, the resources used by the channel can be released. A channel can have any number of senders, but at most one receiver. If a channel has more than one sender, then the channel is closed only when all the senders close the channel. To be able to send receive data along a particular channel, a process must have send receive rights for the channel. These rights are similar to the send and receive rights for Mach ports. However, these rights cannot be passed from one process to another. Once the receiver for a channel is speci ed, the receiver cannot be changed. However, since a channel could have many senders, dierent processes could be given send rights for the same channel. A send operation blocks only when no process has receive rights for the channel. A receive operation blocks only when there is no message in the channel. Once some process has receive rights for a channel, a send operation on that channel never blocks. The inport of a channel is the receiving end of the channel, and the outport is the sending end. The channel library comes with a program known as the network channel server. This program must be running on all the machines in the computation. Chapter 4 describes the purpose of this server in detail. 3.1.1 Conventions The main process in a concurrent computation refers to the rst process that is created in the computation. This process is responsible for creating any additional processes in the computation. The channel library can be speci ed by means of the functions it provides to the user. Note that the speci cation is given only in terms of predicates on state, as is usually done for a sequential program. However, the proof of the speci cation will involve the fact that there could be concurrent access to each function in the library. Each function in the channel library is speci ed by the following: Function is the name of the function, along with its arguments and their types. C syntax is used for the argument list. Precondition, Postcondition. If the function is executed in a state in which the precondition holds, then the function will terminate, and on termination, the postcondition will hold. 13 CHAPTER 3. SPECIFICATION 3.2. INITIALIZATION Wait Condition. This gives the condition under which execution of the function will suspend. If the wait condition is omitted, the function will never suspend. Error Condition is the condition which will cause the function to terminate with an error status. If the error condition is omitted, the function will never terminate with an error status. The channel library functions do not return any values. 3.2 Initialization The initialization functions are used to set up the internal data structures that are used by the channel library. One of these functions should be called once per process before calling the channel library functions. Function: Initialize Main  The current process is the main process. No other function from the channel library has been called. The channel library has been initialized. Duplicate call to Initialize Main. Precondition: Postcondition: Error Condition: Function: Initialize Process  The current process is not the main process. No other function from the channel library has been called from the current process. The channel library has been initialized in this process. Duplicate call to Initialize Process by the same process. Precondition: Postcondition: Error Condition: 3.3 Channels The channel functions are used to create channels, and to manipulate send and receive rights for a channel. Function: New Channel int *chan The channel library has been initialized in the calling process. chan is a non-NULL valid pointer to an integer. *chan contains the logical name of new channel which has no sender and no receiver. The channel library has not been initialized. The following two functions are used by a process to obtain access rights for a particular channel. These functions must be called before actually sending or receiving data along a channel. Precondition: Postcondition: Error Condition: 14 CHAPTER 3. SPECIFICATION Function: 3.4. COMMUNICATION Sending On int chan chan is the logical name of a channel. The calling process does not hold send rights for the channel chan. Send rights for the channel chan have been requested by the calling process. chan is not a valid channel. Initialization has not been done. The calling process already has send rights for channel chan. chan has been closed by some process. Precondition: Postcondition: Error Conditions: Function: Receiving On int chan chan is the logical name of a channel. The calling process does not hold receive rights for the channel chan. Receive rights for the channel chan have been requested by the calling process. chan is not a valid channel. Initialization has not been done. The calling process already has receive rights for channel chan. Another process in the computation has receive rights for channel chan. For instance, the following code in a process would create a new channel, and then declare that the calling process would like to send a message on the newly created channel. Precondition: Postcondition: Error Conditions: int chan ... New_Channel &chan Sending_On chan ... 3.4 Communication The following functions are used to perform the communication actions discussed earlier. They use a format specication|similar to the one used by the C printf function|to specify the type of the message being sent. The format specications that have been implemented are: d for integers and f for oating-point numbers. Spaces are not permitted in the format specication. Function: Send int chan, char *fmt, : : : chan is the logical name of a channel. The calling process has send rights for the channel chan. fmt is a valid format specication. The argument list following fmt matches the format specication. There is no receiver for the channel chan. The specied message has been sent to the receiver for channel chan. The calling process does not have send rights for channel chan. The channel chan has been closed. fmt is not a valid format specication. Precondition: Wait Condition: Postcondition: Error Conditions: 15 CHAPTER 3. SPECIFICATION Function: 3.5. PROCESSES AND THREADS Receive int chan, int *closed, char *fmt, : : : chan is the logical name of a channel. The calling process has receive rights for the channel chan. fmt is a valid format specication. closed is a valid non-NULL pointer. The argument list following fmt are pointers to data structures which match the types specied in the format specication. There is no message in channel chan. The next message from the channel if any has been received, and copied into the pointers in the list. If the channel was closed, then *closed is one otherwise *closed is zero. The calling process does not have receive rights for channel chan. The channel chan has been closed, and an earlier receive operation on the same channel had *closed set to one. fmt is not a valid format specication. The received message length is not the same as the length specied by the format specication. Notice that a receive will allow typecasting of equal length messages. However, this is not recommended since the results are machinedependent. Precondition: Wait Condition: Postcondition: Error Conditions: Notes: Function: Close Channel int chan chan is the logical name of a channel. The calling process has send rights for channel chan. There is no receiver for channel chan. This outport for the channel has been closed. chan is not a valid channel identier. The channel chan was closed. The calling process does not have send rights for channel chan. For instance, a process might send ten messages along a channel, and then close it as follows: Precondition: Wait Condition: Postcondition: Error Conditions: int i, chan ... Sending_On chan ... for i=0 i 10 i++ Send chan, "d", i*i Close_Channel chan ... 3.5 Processes and Threads The following functions are used to create and terminate processes and threads. Function: Spawn Process char *proc, char *host, int n, : : : The channel library has been initialized. proc is a valid non-NULL pointer. host is a valid non-NULL pointer. proc species the pathname Precondition: 16 CHAPTER 3. SPECIFICATION 3.5. PROCESSES AND THREADS of an executable on host. n is the number of arguments following n, which are channel identiers. The process proc has been spawned on host host, with arguments specied by the channel identiers following n in the argument list of Spawn Process. The remote shell program was not found. The host does not allow remote shell access for the user without a password. There are too many processes on the current host. To allow remote shell access without a password, you must have a .rhosts le in your home directory. See the man page for rsh on your system on how to set up this le. Postcondition: Error Conditions: Notes: Spawn Thread void *f, int n, : : : is a valid non-NULL pointer. n is the number of arguments following n, which are channel identiers. n is less than MAXARGS which is Function: Precondition: f dened to be 10. A new thread has been spawned within the current task, starting in the function specied by f. The function was called with arguments specied by the list of arguments after n. The number of arguments exceeded the maximum limit. Postcondition: Error Condition: Function: Finished true. The thread has terminated. This function terminates the main thread of control. This function is called once per task. For instance, the following call would create a new process nproc on machine pete, with two channel arguments ch1 and ch2. Precondition: Postcondition: Notes: ... Spawn_Process "proc", "pete", 2, ch1, ch2 ... 17 Chapter 4 Implementation The implementation has been split into two parts: 1. The network channel server. 2. The user interface. We begin by discussing the issues involved in implementing the channel library. The network channel server is discussed in detail, followed by the user interface. A code outline of the implementation is given for both the channel server and the user interface. 4.1 Issues 4.1.1 Channels Mach provides ports for communication. One possible implementation is to use a single port for each channel. However, ports are system-wide resources that are maintained by the Mach kernel. To conserve ports, the implementation uses a single port for each process which is used to receive messages for all channels connected to that process. We now need a mechanism to distinguish between messages being sent to a process. This is done by tagging each message with an identier which species which channel the message was sent on. For this strategy to succeed, we have to ensure that these message tags are unique across the entire computation. The network channel server is used to provide an identier that is unique to a machine. As a result, the pair hostname, identier is unique across the computation. This pair is used to identify a channel. Since a single Mach port is used for a number of channels, each process must queue messages for a single channel internally. Each process has an internal message handling thread that is used for this purpose. 18 CHAPTER 4. IMPLEMENTATION 4.2. NETWORK CHANNEL SERVER Internal queue of messages for each channel. Mailbox for the process. Chan #1 NULL Chan #2 NULL Chan #3 NULL New message added to appropriate channel queue. Figure 4.1: Implementing Channels 4.1.2 Threads and Processes Threads are implemented on top of the C-thread package. This package allows us to spawn a function with a single argument. Since Spawn_Thread takes a variable number of arguments, we have to implement an argument passing mechanism for newly created threads. The rsh program is used to create processes. However, since this program is UNIX based, it does not give us any mechanism to determine the Mach port of the newly created process. Therefore, argument passing for processes must be handled without using Mach messages. 4.1.3 Termination and Channel Close The C-thread package ensures that when all the threads in the computation terminate, the task itself terminates. However, the implementation uses an extra message handling thread that is always suspended waiting for a message. To be able to terminate gracefully, the channel library keeps track of the number of threads created by the system. Every time a new thread is created, a counter is incremented. When a thread terminates, the counter is decremented. When the number of threads in the system created by the user is zero, the process has terminated. The message handling thread is aborted by means of a function provided by the C-thread library, and the process terminates since all the C-threads have terminated. For a single sender channel, closing a channel is equivalent to sending a special message on the channel. However, the channel close operation becomes complicated once the number of senders is more than one. The receiver of a channel does not know the number of senders that it has. Therefore, some scheme must be used to detect the number of senders, and to close the channel only when all the senders terminate. The network channel server is the only process that knows the number of senders on a channel. This process is used to send a special close-channel message once the channel has been closed. 4.2 Network Channel Server The network channel server has three basic purposes: 19 CHAPTER 4. IMPLEMENTATION 4.2. NETWORK CHANNEL SERVER 1. It provides unique channel identiers to all processes on a single machine. 2. It grants send and receive rights for channels. 3. It is used to close channels once all the senders have closed the channel. A copy of this server must be executing on every machine in the computation. Each channel is created by a specic network channel server. The network channel server maintains a list of channels it has created and their current status. The following user functions interact with the channel server: New_Channel Sending_On Receiving_On Close_Channel New_Channel sends a message to the channel server requesting a new channel identier. The channel server returns an identier it has not used before. Sending_On requests send rights for a particular channel from the server that created it. Receiving_On requests receive rights for a particular channel from the server that created it. Close_Channel sends a message to the channel server indicating that the sender has closed the channel. Note that channel requests are sent to the server that originally created the channel. 4.2.1 Channel Table The network channel server maintains a table that contains the status of all the channels it created. Each channel entry is of type channel_t, which is a structure dened as: typedef struct  int channel_id unsigned int oneclosed:1 unsigned int closed:1 unsigned int nsent unsigned int nout unsigned int in_registered:1 unsigned int in_done:1 unsigned int out_registered:1 unsigned int out_done:1 port_t inport port_t outport mutex_t m condition_t c channel_t 20 CHAPTER 4. IMPLEMENTATION 4.2. NETWORK CHANNEL SERVER is an integer which is unique to this channel server process. It is used to distinguish between channels. The ag oneclosed is true if any sender for the channel has performed a close channel operation. Once any sender closes the channel, the server no longer grants send rights for the channel to any other process. closed is true just when the channel has been closed. To detect the end-of-channel, two elds are used: nout is the number of senders for the channel who have not performed a channel close operation nsent is the number of messages that were sent by the senders that have already closed the channel. in_registered is true when the receiver for the channel is known. The Mach port of the receiver process is stored in inport. out_registered is true when some sender for the channel is known. The Mach port of the rst sender process is stored in outport. in_done is true when receive rights for the channel have been granted to some process. out_done is true when send rights for the channel have been granted to a process. The mutex m and condition variable c are used to control access to the channel elds. channel_id 4.2.2 Log File Each channel server creates and writes information out to a log le. This le records the result of operations for every channel handled by the channel server, and any errors that might be returned by the Mach operating system. The log le can be used to aid debugging, since the status of every channel in the computation is recorded in this le. The following messages are logged by the server: -CTRL-START-CTRL-CLEAR-CTRL-END## Terminated ## These three messages are used to report the status of the server itself. The rst three messages denote the type of the message that was received by the server. The last message is used to denote that the server was terminated normally. These messages can be used to determine the type of requests received by the server. The following messages denote various channel operations that were successful: This message is denotes that fact that the specied channel number was returned by the server to some user process. The log le contains such a message whenever a new channel is created by the user. closed channel #. This message indicates that a close channel request was received for the channel. Note that it does not mean that the channel was actually closed, since the channel could have more than one sender. chan=# registered. 21 CHAPTER 4. IMPLEMENTATION 4.2. NETWORK CHANNEL SERVER This message indicates that some process requested receive rights for the specied channel. Note that the receiver could be a process on the local machine or a remote machine. OUTport chan=# recvd. This message indicates that a process requested send rights for the specied channel. warning:: chan=# multi-send. This message indicates that there is more than one sender for the specied channel. INport chan=# recvd. The messages mentioned above can be used to determine the status of the channels created by the user. Note that the channel identier in the log le is not the same as the channel identier used in each process. However, it is the same as the identier printed out by any error message you may receive. An error message of the form operation chan=# - error message indicates that some server operation failed. The possible error messages that you can get are: duplicate registration of inport multiple requests for an inport multiple requests for an outport specified channel was already closed duplicate registration of channel channel not found 4.2.3 Messages The network channel server interacts with the user interface functions via messages. There are two types of messages exchanged between the user interface and the server: request messages. reply messages. The request messages are sent by the user interface to the channel server. These messages have type request_t, dened below: typedef struct msg_header_t h msg_type_t ct int type msg_type_t t0 int channel_id int chan_type msg_type_t t1 port_t port  request_t 22 CHAPTER 4. IMPLEMENTATION 4.2. NETWORK CHANNEL SERVER The msg_header_t and msg_type_t are elds required by the Mach messaging system. msg_header_t species the length of the message, the destination of the message, and the sender of the message. The msg_type_t elds are used to specify the types of the elds following them in the structure. The type eld is used to indicate what kind of request is being made. The following message types are recognized by the server: CTRL_START is used to restart the channel server. CTRL_END is used to terminate the channel server. CTRL_CLEAR is not used by the user interface. It is used to kill suspended threads. CTRL_REGISTER is used to create a new channel. CTRL_NORM is used to request send or receive rights for a channel. It is also used to close a channel. channel_id is used to specify the particular channel being referred to by the message. Note that since the channel names created by a single channel server are unique, the hostname is not required to identify the channel. chan_type determines whether the message refers to the inport or to the outport for the specied channel. port is used to grant send rights for the receiver port when sending a receive rights request. These send rights can then be granted to any sender for the specied channel. Some of the messages expect a response. These responses by the server are of type reply_t, dened below: typedef struct  msg_header_t h msg_type_t t0 int status int type msg_type_t t1 port_t port msg_type_t t2 char hostname128  reply_t is used to indicate whether the request that triggered this reply message succeeded. type is used to indicate whether the reply refers to an inport or an outport. port is used to grant send rights for the Mach port of a receiver to a process that requested send rights for the channel. hostname is used to identify the channel uniquely. Notice that this eld is required for the reply message since there might be more than one channel server sending messages to a user process. status 23 CHAPTER 4. IMPLEMENTATION 4.2. NETWORK CHANNEL SERVER 4.2.4 Code Outline Note: Underlined functions are potential points at which the executing thread might suspend. Function F4.0: server start initialize data structures do receive request message. ! kill all threads clear all tables request.type = CTRL END ! kill all threads terminate request.type = CTRL REGISTER ! spawn handle register request request.type = CTRL NORM ! spawn handle regular request request.type = CTRL CLEAR ! kill all threads otherwise ! log error if request.type = CTRL START  od Function F4.1: handle register request err = register channel if channel id = -1  ! send reply message with new id otherwise ! skip cthread exit Function F4.2: handle regular request if request = close err = close channel !  request = inport ! err = register inport err = get outport send reply message request = outport ! err = register outport err = get inport send reply message otherwise ! log error cthread exit Function F4.3: register channel mutex lockchan lock channel id := next valid chan++ create new table entry mutex unlockchan lock Function F4.4: find channel mutex lockchan lock ! mutex lockchannel.m mutex unlockchan lock if channel in table 24 CHAPTER 4. IMPLEMENTATION 4.2. NETWORK CHANNEL SERVER return channel otherwise ! mutex unlockchan lock return NULL Function F4.5: close channel chan := nd channel if chan = NULL ! error otherwise ! skip if chan.closed ! error otherwise ! skip chan.nsent += msgs chan.oneclosed := 1 chan.nout  if chan.nout = 0 ! chan.closed := 1 send close channel message condition broadcastchan.c otherwise ! skip mutex unlockchan.m Function F4.6: register inport chan := nd channel if chan = NULL ! error otherwise ! skip if chan.in registered ! error otherwise ! skip chan.in registered := 1 condition signalchan.c mutex unlockchan.m Function F4.7: register outport chan := nd channel if chan = NULL ! error otherwise ! skip chan.nout++ if chan.out registered ! warning otherwise ! skip chan.out registered := 1 condition signalchan.c mutex unlockchan.m Function F4.8: get inport chan := nd channel if chan = NULL ! error otherwise ! skip if chan.oneclosed ! error otherwise ! skip do :chan.in registered ! condition waitchan.c,chan.m if chan.oneclosed ! condition signalchan.c mutex unlockchan.m error otherwise ! skip od condition signal chan.c 25 CHAPTER 4. IMPLEMENTATION 4.3. USER INTERFACE if chan.oneclosed ! error otherwise ! skip  if chan.out done ! error otherwise ! skip  chan.in done := 1 mutex unlockchan.m Function F4.9: get outport chan := nd channel if chan = NULL ! error otherwise ! skip  if chan.oneclosed ! error otherwise ! skip  do :chan.out registered ! condition waitchan.c,chan.m if chan.oneclosed ! condition signalchan.c mutex unlockchan.m error otherwise ! skip  od condition signal chan.c if chan.oneclosed ! error otherwise ! skip  if chan.out done ! warning otherwise ! skip  chan.out done := 1 mutex unlockchan.m 4.3 User Interface The user interface consists of the functions that were specied in chapter 3. These functions use the network channel server to create and close channels, and to request send or receive rights for channels. 4.3.1 Channel Table Each process maintains a table of known channels. This table consists of elements of the following type: typedef struct  int channel_id char *host port_t inport port_t outport unsigned int is_inport:1 unsigned int in_done:1 unsigned int is_outport:1 unsigned int out_done:1 unsigned int closed:1 unsigned int rclosed:1 unsigned int nsent unsigned int nrecv 26 CHAPTER 4. IMPLEMENTATION 4.3. USER INTERFACE list_t *list_of_msgs int nmsgs struct mutex m struct condition c  chan_tab_t and host together uniquely identify the channel name. inport and outport are the Mach ports of the sender and receiver. is_inport indicates whether or not the process has requested receive rights for the channel. in_done is used to indicate whether the process has received receive rights for the channel. is_outport and out_done are similar but used to determine the status of an outport. closed is used to determine if the channel is closed, i.e., if all senders have closed the channel. rclosed is used to determine if at least one sender has closed the channel. nsent and nrecv are used to detect if the channel was closed. list_of_msgs points to a queue of messages in the channel. nmsgs is the number of messages in the queue. m and c are variables used for synchronization. channel_id 4.3.2 Message Handling Each message that is sent along a channel contains the message itself, and the unique channel name. The message structure used is: typedef struct  msg_header_t h msg_type_t t char *msg msg_type_t ht char host128   generic_msg_t points to the data contained in the message. host is used to identify the channel. The msg eld contains all the data that is sent in the message. Each data item specied by the format specication in a Send is copied into a single buer. Note that the virtual memory functions of Mach are used to allocate this buer. As a result, when such a message is sent to a process on the local machine, Mach will not make a second copy of the buer, since Mach uses a copy-on-write scheme for managing virtual memory. The list_of_msgs eld in the channel table is used to store the messages that have been received for a particular channel. Each process has a single thread in it that is responsible for receiving messages for all channels for which the process has receive rights. Each channel has a count nmsgs associated with it, that refers to the msg 27 CHAPTER 4. IMPLEMENTATION 4.3. USER INTERFACE number of messages that were received for the channel. To queue a message for a channel, the following operations are done: 1. The channel mutex m is locked. 2. The received message is appended to the list_of_msgs. 3. A signal action is performed on the condition variable c. 4. nmsgs is incremented. 5. The channel mutex m is unlocked. To remove a message from the channel, the following actions are done: 1. The channel mutex m is locked. 2. A wait is done on the condition variable c until nmsgs is non-zero. 3. The next message is removed from the queue. 4. nmsgs is decremented. 5. The channel mutex m is unlocked. 4.3.3 Argument Passing When a Spawn_Thread or a Spawn_Process call is made, the list of arguments to the thread or process must be converted into a form that can actually be passed to the thread or process, and then reconverted back into the original arguments. Since process and thread creation are very di erent internally, two separate strategies are used to tackle the problem for each of them. Threads The C-thread package allows a thread to be spawned with a single argument. Therefore, we have to convert the list of arguments to Spawn_Thread into one single structure that can then be passed to some function that converts the structure back into the original argument list. The structure used for this purpose is shown below: struct single_argument  void *f int n int *chan_list  is the number of integers in the array chan_list. Together, these specify all the arguments that were passed to the thread. f is a pointer to the function that is to be spawned. n 28 CHAPTER 4. IMPLEMENTATION 4.3. USER INTERFACE does not spawn the function specied in its argument list. Instead, a function known as __generic_unpack is spawned. This function takes a single argument of type struct single_argument*. The purpose of this function is to unpack the arguments and call the function specied by f with the appropriate argument list. Spawn_Thread Processes Argument passing across processes is slightly more complex. The major problem is that the channel identiers that are passed as arguments do not refer to the channel name, but to the location of the channel in the channel table. Therefore, the channels must be entered into the channel table in the remote process, and then converted into a valid channel identier in the remote process. The channel names are passed using the command-line mechanism. This list must then be unpacked by the remote process, and entered into the channel table. The channel library provides a simple tool known as makestub which is used to create the main process for remote processes that are spawned using Spawn_Process. The main program takes the command line arguments, registers them internally, and then calls a specied function an argument to makestub with the actual channel identiers. 4.3.4 Code Outline Note: Underlined functions are potential points at which the executing thread might suspend. Function F4.10: internal msg handler do receive message ! cthread exit otherwise ! skip  chan := nd channel if chan = NULL ! mutex locktable mutex insert new channel into table chan := new channel mutex unlocktable mutex chan 6= NULL ! skip if user interrupt  mutex lockchan.m insert message in message queue condition signalchan.c mutex unlockchan.m od Function F4.11: Sending On if chan.is outport error otherwise ! chan.is outport := 1 chan.out done := 0 29 ! skip  CHAPTER 4. IMPLEMENTATION 4.3. USER INTERFACE send outport request to channel server Function F4.12: Receiving On if chan.is inport error otherwise ! chan.is inport := 1 chan.in done := 0 send inport request to channel server ! skip  Function F4.13: Initialize Main look up channel server initialize all tables Function F4.14: Initialize Process initialize all tables Function F4.15: New Channel request new channel id from server if channel exists ! error otherwise ! skip  mutex locktable mutex  create new table entry mutex unlocktable mutex  Function F4.16: Send if :chan.is outport ! error otherwise ! skip  if :chan.out done ! complete orpc otherwise ! skip  mutex locktable mutex  if chan.closed ! error otherwise ! skip  mutex unlocktable mutex  package message into bu er send message Function F4.17: Receive if :chan.is inport ! error otherwise ! skip  if :chan.in done ! complete irpc otherwise ! skip  mutex lockchan.m  if channel closed ! error otherwise ! skip  do chan.msgs = 0 ! condition waitchan.c,chan.m od take next message out of queue unpack message mutex unlockchan.m  Function F4.18: Spawn Thread pack arguments into one structure mutex lockthread mutex  thread count++ mutex unlockthread mutex  spawn new thread 30 CHAPTER 4. IMPLEMENTATION 4.4. POSSIBLE IMPROVEMENTS Function F4.19: Spawn Process create command line arguments use rsh to spawn new process Function F4.20: Finished mutex lockthread mutex thread count if thread count = 0 ! abort internal msg handler otherwise ! skip mutex unlockthread mutex thread exit Function F4.21: Close Channel if chan.closed error otherwise ! chan.closed := 1 send close channel message to server ! skip Function F4.22: complete irpc mutex lockrpc mutex do :chan.in done ! wait for reply message from server enter message into table set done ag for appropriate channel mutex unlockrpc mutex mutex lockrpc mutex od mutex unlockrpc mutex Function F4.23: complete orpc mutex lockrpc mutex do :chan.out done ! wait for reply message from server enter message into table set done ag for appropriate channel mutex unlockrpc mutex mutex lockrpc mutex od mutex unlockrpc mutex 4.4 Possible Improvements The following modications could be made to the Network Channel Server. These modications, in some cases, incur a cost which a user may or may not be willing to pay.  Each server could have a CTRL SESSION message, which returns a new session id. The channel would then be uniquely identied by the triple hostname, 31 CHAPTER 4. IMPLEMENTATION 4.4. POSSIBLE IMPROVEMENTS session id, channel id. This would allow multiple parallel applications to use the channel server. The network channel server could be simply removed and incorporated into the internal message handling thread in the user interface. However, this presents the additional cost of registering all user processes with the network nameserver. 32 Chapter 5 Proof Outline This chapter contains an informal proof of the channel library. Since there are two basic parts to the channel library, we split the proof into two parts: 1. Proof of the network channel server. 2. Proof of the user interface functions. We shall rst prove some basic properties of the network channel server. These properties, along with the properties of the user interface functions will demonstrate that the user interface functions satisfy their specication. 5.1 Network Channel Server We begin by dening the ghost variable ns. ns is the number of times the channel table is cleared. We dene the interval between two successive values of ns as a session. 5.1.1 Properties P5.1: For every channel , the following pairs are monotonic under lexicographic ordering:  , , , , , .  There are two possible values these channel elds could have: 0 or 1. They are assigned a value of zero just when the channel table is cleared, which increases . All other modications to the channel elds given above only assign them the value 1. c Property ns c:oneclosed ns c:in done ns c:out registered ns c:closed ns c:out done Proof: ns 33 ns c:in registered CHAPTER 5. PROOF OUTLINE Property Proof: 5.1. NETWORK CHANNEL SERVER P5.2: All mutex variables used are created exactly once. The only statements that can modify a mutex variable are the initialization and termination routines. The initialization routine is called exactly once. P5.3: There is exactly one thread in the channel server until the rst receive is done in F4.0 . F4.0 begins the channel server. This function is the only one that spawns new threads. These spawn operations follow a receive operation. Property Proof: P5.4: Only threads from the channel server can modify the data structures in the server. The channel server is created as an independent process. Furthermore, there are no system calls in the server that grant memory access to any other task in the system. Property Proof: Property time. Proof: P5.5: At most one thread can modify or read the channel table at a Initially, there are no threads in the system. From P5.2 we know that the mutex variables themselves do not change in value, but only in state. The only places where the channel table is modi ed or read are in functions F4.4, F4.3, and F4.0. From P5.3, and the fact that the channel table is modi ed in F4.0 before the rst receive operation, the invariant is maintained. The two functions F4.4 and F4.3 lock the mutex variable before accessing the channel table. Therefore, the invariant is maintained. chan lock Property P5.6: The pair ns next valid chan is monotonic under lexicographic ordering. is modi ed in two places: i when the channel table is cleared ii in function F4.3. Clearing the channel table increases . . This increment is done F4.3 increments the value of only when the mutex variable is locked. Therefore, at most one thread can increment at a time. So, F4.3 only performs monotonic changes to the pair. Proof: next valid chan ns next valid chan chan lock next valid chan P5.7: The channel identiers returned by the network channel server in a session are unique. The only place where new channel identi ers are created is in the function F4.3. is used to create new channel identi ers. From P5.6, we know that the modi cations to are monotonic is for a given session. From function F4.3, we see that changed every time a new channel is created. From P5.6, we know that no two values of the variable can be the same. Property Proof: next valid chan next valid chan next valid chan next valid chan 34 CHAPTER 5. PROOF OUTLINE 5.1. NETWORK CHANNEL SERVER P5.8: At most one thread can modify an entry in the channel table at a time. Initially, there are no threads in the computation. Apart from function F4.3, all other functions modify a channel entry only after calling F4.4. This function locks the mutex m associated with the channel. F4.3 creates a new channel entry. From P5.7, we know that these channel entries are identi ed by unique values. Since F4.3 returns a new channel and we know P5.7, no other thread in the computation can access the newly created channel entry. Property Proof: P5.9: For a channel c, c:in registered is 1 just when an inport register request has been received for the channel c. c:in registered is assigned a value 1 only in function F4.6. This function is called only from function F4.1 when the request was an inport request. F4.1 is called just when a register request is received. F4.6 assigns a value 1 to c:in registered. Property Proof: P5.10: For a channel c, c:out registered is 1 just when an outport register request has been received for the channel c. Similar to the proof of P5.9. Property Proof: P5.11: For a channel c, c:oneclosed is 1 just when a close channel request has been received for the channel c. Similar to the proof of P5.11. Property Proof: P5.12: The number of reply messages sent for inport requests without an error status is at most one. A reply message is sent to an inport request only after functions F4.6 and F4.9 have been called. F4.6 returns an error if in registered is 1 for the channel. Since in registered is set to 1 every time F4.6 is called and we know P5.9, we can conclude that an error status is returned if F4.6 is called more than once for the same channel. Since a reply message is sent only after F4.6 is called, we have established P5.12. Property Proof: P5.13: The reply message for an inport request on a channel is sent only after the outport request for the channel has been received. A reply message for an inport request is sent only after the functions F4.7 and F4.8 have been called. Function F4.8 suspends on the condition variable for the channel until in registered has value 1. From P5.9 we can conclude that in registered is 1 just when the outport request for the channel has been received. Property Proof: Property P5.14: The reply message for an outport request on a channel is sent 35 CHAPTER 5. PROOF OUTLINE 5.2. USER INTERFACE only after the inport request for the channel has been received. A reply message for an outport request is sent only after the functions F4.6 and F4.9 have been called. Function F4.8 suspends on the condition variable for the channel until out registered has value 1. From P5.10 we can conclude that out registered is 1 just when the inport request for the channel has been received. Proof: P5.15: A close channel message is sent to the receiver of a channel only after the number of close channel requests is the same as the number of outport requests. Each outport request increases the value of nout for the channel. Each close channel request decreases the value of nout. These modi cations to nout are protected by the channel mutex m. A close channel message is sent to the receiver only when nout is zero. Property Proof: 5.2 User Interface We use the following fact about the channel table: when a new channel table entry is created, all the bit- elds for the newly created channel have value zero. 5.2.1 Properties Property Proof: P5.16: At most one thread can access the channel table at a time. All modi cation to the channel table are protected by the mutex variable table mutex. As a result, at most one thread will succeed in locking the mutex, from which the property follows. P5.17: F4.15 creates new channels with identi ers from the local network channel server. From the code outline of F4.15, we can see that the function satis es the property mentioned above. Since we have P5.16, the channel table update is equivalent to an atomic action. Property Proof: P5.18: For any channel, an outport request from a process is sent at most once to the network channel server. An outport request is sent only from F4.11. This function sets the is outport ag to 1. It returns an error status just when is outport has value 1 when the function is called. Property Proof: 36 CHAPTER 5. PROOF OUTLINE 5.3. OUTLINE OF PROOF P5.19: For any channel, an inport request from a process is sent at most once to the network channel server. An inport request is sent only from F4.12. This function sets the is inport ag to 1. It returns an error status just when is inport has value 1 when the function is called. Property Proof: P5.20: Function F4.11 sends an outport request to the network channel server when it is called for the rst time. Follows from the code outline of F4.11. Property Proof: P5.21: Function F4.12 sends an inport request to the network channel server when it is called for the rst time. Follows from the code outline of F4.12. Property Proof: P5.22: F4.16 succeeds only if the process has called F4.11 for the channel. The is outport eld of a channel is modi ed only by F4.11. Initially, the eld has value 0. From the code of F4.16, it is clear that the function succeeds only when is outport has value 1, i.e. when F4.11 was called for the channel. Property Proof: P5.23: F4.17 succeeds only if the process has called F4.12 for the channel. Similar to the proof of P5.22. Property Proof: P5.24: A process sends a close channel request to the network channel server at most once. A close channel request is sent only by F4.5. The closed eld of the channel is set by F4.5. An error status is returned by F4.5 if it is called for a channel that has the closed eld set to 1. Property Proof: 5.3 Outline of Proof Property Proof: P5.25: Function Initialize Main satis es its speci cation. The program F4.13 for the function is trivial, and the proof is left to the reader. Property P5.26: Function Initialize Process satis es its speci cation. 37 CHAPTER 5. PROOF OUTLINE Proof: The program F4.14 for the function is trivial, and the proof is left to the reader. Property Proof: P5.35: Function Finished satises its specication. Modication of variable thread count is protected by the mutex variable thread mutex. This variable is initially 0. F4.18 increases the value of thread count whenever it is called. F4.20 decreases the value of thread count whenever it is called. Therefore, thread count being zero is equivalent to the condition that there are no user threads in the system. This condition is used to terminate the process. Property Proof: P5.34: Function Spawn Thread satises its specication. Follows from the code outline F4.18, and the fact that modication of thread count is protected by the mutex thread mutex. Property Proof: P5.33: Function Spawn Process satises its specication. Follows from the code outline F4.19. Property Proof: P5.32: Function Close Channel satises its specication. Follows from P5.24 and P5.15. Property Proof: P5.31: Function Receive satises its specication. Follows from P5.23. Property Proof: P5.30: Function Send satises its specication. Follows from P5.22. Property Proof: P5.29: Function Receiving On satises its specication. Follows from P5.21 and P5.19. Property Proof: P5.28: Function Sending On satises its specication. Follows from P5.20 and P5.18. Property Proof: P5.27: Function New Channel satises its specication. Follows from P5.17, and P5.7. Property Proof: 5.3. OUTLINE OF PROOF P5.36: Channel identiers in the system are unique. Follows from P5.7. 38 CHAPTER 5. PROOF OUTLINE 5.3. OUTLINE OF PROOF We now dene send rights and receive rights in terms of the messages exchanged between the channel server. Requesting send rights is equivalent to sending an outport request to the channel server. Requesting receive rights is equivalent to sending an inport request to the channel server. The reply message for an outport request grants send rights to a process. The reply message for an inport request grants receive rights to a process. Now, we have the following properties which needed to be established: P5.37: There is at most one process in the computation that has receive rights for a channel. Follows from P5.12 . Property Proof: P5.38: A send succeeds only if the calling process has send rights for the channel. Follows from P5.22 . Property Proof: P5.39: A receive succeeds only if the calling process has receive rights for the channel. Follows from P5.23 . Property Proof: 39 Chapter 6 Example programs In this chapter we discuss some example programs that were implemented using the channel library. The purpose of these examples is to demonstrate how one might use the channel library to write a parallel program. We have chosen the following two examples: A distributed sorting program. A producer-consumer problem. 6.1 Producer-Consumer In this example, there are two processes in the computation. One of the processes known as the producer sends messages to the other process known as the consumer. The consumer then prints out the messages it received and terminates. The function main creates the channel connecting the producer and consumer, spawns the two processes, and then terminates. void mainvoid  int ch Initialize_Main  Single producer thread, single consumer thread. The dotted thread represents the internal message handler. Producer Consumer Figure 6.1: Producer-Consumer Problem 40 CHAPTER 6. EXAMPLE PROGRAMS 6.2. SORTING New_Channel &ch Spawn_Process "procprod", "chainsaw", 1, ch Spawn_Process "proccons", "pistol", 1, ch Finished The producer requests send rights for the channel that was sent to it as an argument, and then sends messages along it. Finally, the channel is closed, and the producer terminates. void producer int ch int i Sending_On ch for i=0 i  10 i++ Send ch, "d", i*i Close_Channel ch The consumer requests receive rights for the channel that was sent to it as an argument, and then receives messages from the channel until the close channel message is received. void consumer int ch int i, closed FILE *fp Receiving_On ch Receive ch, &closed, "d", &i fp = fopen "log", "w" while !closed fprintf fp, "dn", i Receive ch, &closed, "d", &i fclosefp 6.2 Sorting The program below implements the mergesort algorithm for sorting numbers. This algorithm uses a divide-and-conquer strategy. main is used to create the initial sort process, and to read in the numbers that are to be sorted. void mainvoid 41 CHAPTER 6. EXAMPLE PROGRAMS 6.2. SORTING Figure 6.2: Distributed Mergesort int chan1, chan2 int i, n, val, closed Initialize_Main New_Channel&chan1 New_Channel&chan2 Sending_Onchan1 Receiving_Onchan2 Spawn_Process "mergesort", "pete", 2, chan1, chan2 printf "Enter # of values: " scanf " d", &n Send chan1, " d", n printf "Enter values:n" fori=0 i  n i++ scanf " d", &val Send chan1, " d", val  Close_Channelchan1 fori=0 i  n i++ Receivechan2, &closed, " d", &val printf " dn", val  Finished  Process mergesort checks the problem size. If the base case is reached, then the process sends back the solution and exits. Otherwise, it creates two new processes which are used to solve two sub-problems of the original sorting problem. void mergesortint in, int out int i, n, val int closed int c0, c1, c2, c3 int *left, *right 42 CHAPTER 6. EXAMPLE PROGRAMS Receiving_On in Sending_On out Receivein, &closed, " d", &n if n == 1 Receive in, &closed, " d", &val Send out, " d", val else val = int* mallocsizeofint*n New_Channel&c0 Sending_On c0 New_Channel&c1 Receiving_On c1 New_Channel&c2 Sending_On c2 New_Channel&c3 Receiving_On c3 Send c0, " d", intn2 for i=0 i  n2 i++ Receive in, &closed, " d", &val Send c0, " d", val Send c2, " d", n-intn2 for i=0 i  n-n2 i++ Receive in, &closed, " d", &val Send c2, " d", val Close_Channel c0 Close_Channel c2 left = int*mallocsizeofint*intn2 right = int*mallocsizeofint*n-intn2 for i=0 i  n2 i++ Receive c1, &closed, " d", left+i for i=0 i  n-n2 i++ Receive c3, &closed, " d", right+i mergeleft, right for i=0 i  n2 i++ Send chanout, " d", lefti for i=0 i  n-n2 i++ Send chanout, " d", righti 43 6.2. SORTING Chapter 7 Conclusion We have presented the implementation of a channel library on top of the Mach operating system. From the implementation outline given, it is clear that the channel library implementation was greatly simplied as a result of the support provided by Mach itself. In fact, the entire implementation took 2000 lines of code. Although implementing the library was a simple task, the proof for the channel library was extremely complicated. Presenting a code outline greatly simplied the proof, by hiding details of the implementation and focusing attention on synchronization issues. In spite of using this simplication, the proof outline was complex. The key properties in the proof established that certain variables used in the implementation were monotonic. However, all the monotonic variables could be modied in a non-monotonic manner, but only by a single thread of execution. This leads us to believe that reasoning about correctness of the library using shared data structures that are monotonic will greatly simplify the proof. Reasoning about a concurrent computation in which sharing is restricted to monotonic variables with a single thread of execution that can perform a non-monotonic modication to them can be applied to a large number of existing constructs for instance, channels, monitors, and locks used to restrict the interaction between cooperating tasks. We think that choosing Mach as the base for the channel library was a good decision because of the services provided by the operating system. Proving correctness of the channel library seemed to be a complex task, in spite of the fact that a number of implementation details were hidden. 44 Bibliography 1 Accetta, M., Baron, R., Bolosky, W., Golub, D., Rashid, R., Tevanian, A., Young, M. Mach: A New Kernel Foundation for UNIX Development In Proceedings of Summer Usenix. July, 1986. 2 Bach, M.J. The Design of the UNIX Operating System. Prentice-Hall, 1986. 3 Cooper, E.C., and Draves, R.P. C Threads Technical Report CMU-CS-88-154, School of Computer Science, Carnegie Mellon University. February 1988. 4 Kernighan, B.W., and Ritchie, D.M. The C Programming Language. PrenticeHall, 1988. 5 NeXT Computer Inc. NeXTSTEP Operating System Software. AddisonWesley, 1992. 6 Silberschatz, A., Peterson, J., and Galvin, P. Operating System Concepts. Addison-Wesley, 1991. 45