A Discipline of Multiprogramming

The main software challenge in developing application programs during the 1960s and the 1970s was that the programs had to operate within limited resources, i.e., slow processors, small memories, and limited disk capacities. Application programming became far more widespread during the 1980s because of the falling prices of hardware (which meant that more processing power and storage were available for the same cost) and a better understanding of the application programming process. However, most applications still ran on mainframes or over a cluster of machines in a local-area network; truly distributed applications that ran over wide-area networks were few because of the latency and bandwidth limitations of long-haul communication. The 1990s saw great strides in broad-band communication, and the World Wide Web provides a giant repository of information. This combination promises development of a new generation of distributed applications, ranging from mundane office tasks —e.g., planning a meeting by reading the calendars of the participants— to real-time distributed control and coordination of hundreds of machines —e.g., as would be required in a recovery effort from an earthquake.

In chapter 1 we suggested that a program be structured as a set of objects. Each object consists of actions and/or methods, where the actions are executed autonomously (following a specific execution rule) and the methods are executed when they are called. In this chapter, we consider a simpler version of this model; we eliminate the methods altogether, retaining only actions. The immediate consequence of this decision is that the objects can no longer communicate through procedure calls; we require the objects to communicate via shared variables. Actions from different objects can read/write into these variables. However, at most one action is executed at any time, so there is no possibility of concurrent write into a variable.

Action systems are used in chapter 2 to represent a message communicating process (Merge), a fragment of an operating system (mutual exclusion), a process controller (odometer), and even solutions to combinatorial problems (gcd, shortest path). The syntax and semantics of action systems are sparse, yet we developed succinct programs for several well-known problems. This chapter extends the programming model of chapter 2 to make it easier to describe process interactions. Additionally, we address the issue of program composition in some detail.

A number of small examples are treated in this chapter. The goal is to show that typical multiprogramming examples from the literature have succinct representations in Seuss. Additionally, the small number of features of Seuss is adequate for solving many well-known problems: communications over bounded and unbounded channels, maintaining a database, implementing a caching strategy, mutual exclusions and synchronizations, and resource allocation. We show a number of variations of some of these examples, implementing different progress guarantees, for instance.

The most fundamental attribute of any program is “correctness”. Correctness has many interpretations, ranging from the narrow technical ones —the kind advocated in this book— to esoteric science-fiction notions that require a machine to mimic human behavior. In this book, we develop the theory for two major classes of program properties: safety and progress. We study safety properties in this chapter, and progress in the next chapter, for the programming model of chapter 2. A new class of properties, called maximality, is introduced in chapter 7. Logics for program composition are developed in chapters 8 and 9. In chapter 12, we extend the logic for the full programming model of chapter 3. In each chapter, we develop the theory —which is typically quite small— and apply the theory to a variety of examples to show its effectiveness.

Traditionally, a program specification is given by safety and progress properties, as explained in chapters 5 and 6. A safety property —e.g., no two neighbors eat simultaneously in a dining philosophers solution— is used to exclude certain undesirable execution sequences. A specification with safety properties alone can be implemented by a program that does nothing; that is, the safety constraints are implemented by excluding all nontrivial executions. Therefore, it is necessary to specify progress properties —e.g., some hungry philosopher eats eventually— which guarantee that some execution sequence will be included. Safety and progress requirements are sufficient for specifying nontrivial sequential programming tasks, but they are not sufficient for concurrent program design because, for instance, the dining philosophers solution may allow only one philosopher to eat at a time, thus eliminating all concurrency. We propose a new class of properties, called maximality, to permit inclusion of all executions that satisfy a specification. Thus, the sequential solution to the dining philosophers problem can be excluded by requiring that the solution be maximal for the appropriate specification.

The goal of a program composition theory is to answer questions of the following form:

The union theorem, introduced in section 8.2.3, is the main tool for the study of asynchronous compositions of programs. The major virtue of this theorem is that it provides a simple rule for deducing the co-properties and transient predicates of a system from those of its component boxes. The major shortcoming is that it does not provide a simple rule for deducing the leads-to properties of a system from those of its components. The only way we can use a progress property of a component, p→ q in F, to deduce a similar property of the system is to either (1) apply the union theorem for progress (see section 8.2.6), which requires introduction of a well-founded order over the values of the shared variables, or (2) exhibit the proof of p→ q in F and show that the other components do not falsify the proof steps. The first strategy is cumbersome, and the second defeats the whole purpose of modular program construction.

The operational semantics of the programming model —action systems in chapter 2 and object-oriented systems in chapter 3— is based on tight executions, where each action execution is completed before another one is started. This is a convenient model for understanding a program and reasoning about its properties, because an action represents an indivisible unit whose execution cannot be preempted by another. We applied induction on the number of actions in a tight execution to deduce invariant properties in chapter 5, for instance. We developed a logic to reason about tight executions in chapters 5, 6, 8, and 9, and we extend the logic for the general programming model in chapter 12.

In this chapter, we develop algorithms for implementing Seuss programs on multiprocessor architectures in which the processors communicate using messages. The implementation strategy is to partition the boxes over a set of processors and have a scheduler that instructs each processor which action to execute next. The scheduler can be centralized or distributed among the processors. In the next section, we describe the scheduler in abstract terms that permits either type of implementation; specific implementations are described in section 11.5.

The logic of action systems, developed in chapters 5 and 6, allowed us to specify safety and progress properties of a single box; the logic is extended in chapters 8 and 9 for specifications of ensembles of boxes. Properties such as co and leads-to specify the collective effect of the executions of the actions of a box or a set of boxes; the individual actions are not identified in a specification. Therefore, it is not possible to deduce from earlier specifications how a specific action affects the program state.