On Concurrent Programming

Frontmatter

Chapter 1. Introduction

Abstract

A concurrent program consists of processes and shared objects. A process is a sequential program executing on some processor; the shared objects are built using shared memory or a computer-communication network.

Fred B. Schneider

Chapter 2. Formal Logic

Abstract

The methods in this textbook for reasoning about programs are based on using formal logic to characterize program execution. Here, we review some rudiments of logic and show how logic can be used to formalize safety and liveness. Our study of logic is done from the programmer’s viewpoint, not the logician’s. For us, logic is simply a tool. However, as with most tools, it must be understood to be used effectively.

Fred B. Schneider

Chapter 3. Temporal Logic

Abstract

Predicate Logic allows sets of states to be specified; Temporal Logic allows sets of anchored sequences to be specified. Because properties are modeled by sets of anchored sequences, Temporal Logic is well suited for specifying properties and reasoning about programs. In this chapter, we give an axiomatization for Temporal Logic and explore how the logic relates to other modal logics.

Fred B. Schneider

Chapter 4. Notation and Logic for Sequential Programming

Abstract

In order to reason about concurrent programs, one must first be able to reason about their component sequential programs. In this chapter, we describe a sequential programming notation and a logic for reasoning about programs written in the notation. The logic is obtained by extending Predicate Logic with a new type of formula, the proof outline. We also present a calculus to aid in deriving a proof outline along with a program.

Fred B. Schneider

Chapter 5. Concurrency and Interference

Abstract

We now add statements for concurrency and synchronization to the sequential programming notation of Chapter 4. We also extend Proof Outline Logic, using interference freedom to characterize when a valid proof outline for a concurrent program can be derived from valid proof outlines for its component processes. Synchronization statements are then viewed as mechanisms to prevent interference.

Fred B. Schneider

Chapter 6. Safety Properties: Invariance

Abstract

A safety property asserts that some “bad thing” does not happen during execution. In this chapter, we consider invariance properties, an important class of safety properties. We discuss methods for proving that a program satisfies an invariance property and show how these methods can guide in the development of programs.

Fred B. Schneider

Chapter 7. Safety Properties with Past Terms

Abstract

For some safety properties, whether a state is considered a “bad thing” depends on the preceding states. We discuss in this chapter how to specify and reason about such safety properties. We show that by extending Predicate Logic, the techniques of Chapter 6 can be used for reasoning about arbitrary safety properties. The chapter also discusses the design of programs satisfying arbitrary safety properties and the role of auxiliary variables in reasoning about programs.

Fred B. Schneider

Chapter 8. Verifying Arbitrary Temporal Logic Properties

Abstract

Additional axioms and rules are needed for us to go beyond safety properties and be able to reason about properties specified by arbitrary Temporal Logic formulas. These axioms and inference rules of S-Temporal Logic are given in this chapter. We also discuss fairness assumptions for cobegin implementations, because satisfying a liveness property often requires making assumptions that specific processes will have opportunities to execute. Finally, we describe helpful actions and other techniques for proving eventualities.

Fred B. Schneider

Chapter 9. Programming with Fine-Grained Atomic Actions

Abstract

Real computer hardware does not implement as atomic actions all the assignment statements, guard evaluation actions, and atomic statements of our programming notation. A typical computer can execute only a small, fixed set of unconditional atomic actions; an operating system might add to this a few conditional atomic actions. Thus, there is a gap between the programming model we have been assuming and what is available on an actual computer system.

Fred B. Schneider

Chapter 10. Semaphores, Locks, and Conditional Critical Regions

Abstract

Looping by a process to wait for a condition consumes processor cycles without helping the awaited condition to become true. Other processes must be executed if we want the condition truthified. Since it is the operating system that multiplexes a processor among processes, wasted processor cycles are avoided if the operating system implements primitives to await and signal conditions. These primitives implement conditional atomic actions because they can block, but their execution also changes which processes the operating systems considers eligible for execution.

Fred B. Schneider

Chapter 11. Message Passing and Distributed Programming

Abstract

Absence of shared memory is the defining characteristic of a distributed system. Processes in such a system coordinate by reading and writing shared objects called communications channels. Thus, concurrent programs for distributed systems, or distributed programs, are fundamentally no different from other concurrent programs: all use shared objects of one sort or another for synchronization and communication.

Fred B. Schneider

Chapter 12. Putting It Together

Abstract

Around 1885, French painters Georges Seurat (1859–1891) and Paul Signac (1863–1935) developed a style of painting variously known as pointillism, divisionism, or neo-impressionism. Instead of brush strokes, small dots of pure color are placed on the canvas. The dots fuse at normal viewing distance and create the illusion of regions having color and texture. Seurat’s A Sunday on La Grande Jatte —1884 is among the best-known examples of pointillist painting; it is reproduced on the cover of this text.

Fred B. Schneider

Backmatter