Parallelism and Fault Tolerance

The intensional nature of Lucid and eduction has two important practical consequences: (i) Lucid programs possess massive amounts of implicit parallelism and (ii) their evaluation can automatically tolerate faults. This chapter is devoted to explaining these two consequences. We start with massive implicit parallelism in Lucid programs. There are three forms of parallelism that arise in problem solving [13, 6]. The simplest form of parallelism, functional parallelism, is in the simultaneous execution of independent functions (or operators). This is sometimes referred to as structural parallelism or static parallelism.

Intensionality

The intensional programming language, Lucid, described in Chapter 1 is based directly on intensional logic, a family of mathematical formal systems that permit expressions whose value depends on hidden contexts or indices. Our use of intensional logic is one in which the hidden contexts or indices are integers or tuples of integers. Intensional logic, as used to give semantics to natural language, uses a much more general notion of context or index. Of course, intensional logic is hardly the first example of a formal system of interest to both logicians and computer scientists. The language LISP (invented by McCarthy and others in the early sixties [34]) was originally intended to be an adaptation of the lambda calculus, although it diverged in its treatment of variable-binding and higher-order functions. Shortly after, however, Landin produced ISWIM, the first true functional language [30]. These “logical” programming languages such as ISWIM are in many respects vastly superior to the more conventional ones. They are much simpler and better defined and yet at the same time more regular and more powerful. These languages are notationally closer to ordinary mathematics and are much more problem-oriented. Finally, programs are still expressions in a formal system, and are still subject to the rules of the formal system. It is therefore much easier to reason formally about their correctness, or to apply meaningpreserving transformations. With these languages, programming really is a respectable branch of applied mathematical logic. These logic-based (or declarative) languages at first proved difficult to implement efficiently, and interest in declarative languages declined soon after the promising initial work of McCarthy and Landin. Fortunately, the advent of large scale integration and new compiling technology reawakened interest in declarative languages, and brought about a series of new “second generation” declarative languages, such as Prolog [12] and Miranda [44]. Lucid itself was one of these second generation declarative languages. Lucid is based not so much on classical logical systems as on the possible worlds approach to intensional logic—itself a relatively new branch of logic [43] which reached maturity during the period (1965-75) in which declarative programming languages were in eclipse.

Introduction

This book, obviously, is about multidimensional declarative programming. Many different languages and paradigms may be claimed to result in multidimensional declarative programming. We are most concerned with a programming paradigm where the existence of different dimensions (even temporary dimensions) enables algorithms to be expressed naturally. The latest version of the language Lucid uses dimensions in this way and we will use Lucid throughout most of this book. We will emphasize that Lucid is a language that embodies a particular style or paradigm of programming that we call intensional programming. Toward the end of the book there will be a chapter that indicates how other language features and capabilities could fit into this same paradigm. Therefore this book is about multidimensional, declarative, intensional programming, with examples given mostly in the latest version of Lucid. Lucid has been around since the mid-seventies [7]. Nevertheless, with its new poly dimensionality capabilities it provides a fresh approach to programming and, we hope, introduces declarative programming to a whole new audience. In addition, we often find it is useful to think of Lucid programs as manipulating geometrical entities, even though programs are actually implemented very simply i.e., without any data structures corresponding to those geometrical entities. Thinking of programs as manipulating geometrical entities adds a visual aspect to programs, while the fact that there are no actual structures in the implementation emphasizes that Lucid programs can be thought of in several different ways. We tend to think of programs, and variables in programs, at a very high level when writing programs and ignore the implementation details. Yet for a very high level language, those implementation details are surprisingly simple. Programs are written while thinking of large, multidimensional entities, and yet the implementation deals only with small fragments. In fact, we might modify an environmental movement slogan and say “program globally and implement locally.” By the end of the book the appropriateness and meaning of this slogan should be apparent. This introductory chapter begins by illustrating some of the novelty of the new Lucid with a very simple program for transposing a matrix.

Syntax and Semantics

In this chapter, the syntax of Lucid will be formally specified. Also, the denotational semantics of Lucid will be outlined. The example programs in Chapter 1, surprisingly perhaps, informally introduced all the syntax of Lucid. There, we saw where clauses, definitions, terms, dimension names variables, functions, constants, and operations. Now, we will see how these syntactic entities are formalized, and the examples in the previous chapter will be looked at again, this time to see which of the syntactic entities are being used, and how. Lucid is an expression-based language: every Lucid program is a term, which might be a where clause of size 1. A where clause of size n is an n-tuple of terms together with declarations of new dimensions and subsidiary definitions (that follow the keyword where). The definitions in a where clause have right-hand sides that may be where clauses. Thus, Lucid programs are naturally recursively structured, to arbitrary depth. We will say that Lucid is where clause structured, where we intend that expression to convey all that the expression block structured conveys about scoping in, say, Algol, Pascal, or Ada. After that very cursory top-down view of Lucid, we now immediately look at the basic entities from which terms are formed: variables, functions, constants, and operations. These four basic types of entities we will call atoms. Syntactically, variables and functions are represented by identifiers, which are alphanumeric strings that start with a letter. Constants and operations, on the other hand, are usually represented by characters other than letters, such as + and 3 and #. Some operations and constants are represented by alphanumeric strings, such as fby, true, and div. (Also, the ternary conditional operation is represented by four such strings: if, then, else, and fi.) We will say that these strings are not identifiers—they are special reserved keywords—and we will not allow them to be used to represent variables or functions. (This is standard practice for many languages.) All atoms have two arities, which we will call the Roman and the Greek arities.

Other Uses of Intensionality

In Chapter 2 we presented what is essentially a creation myth of intensional programming—that far-sighted researchers studied intensional logic and then applied this knowledge by designing a language that embodied intensional principles. In fact, the whole project grew out of a more modest attempt to make fairly conventional Pascal-style programming mathematically acceptable. Indexed sequences were originally added so that programs which, in Pascal, used for-loops and reassignment, could be rewritten as equations involving temporal operators.

High-Performance Implementation

In Chapter 1, we saw how Lucid could be used to express solutions to standard problems such as sorting and matrix multiplication. One of the unique characteristics of Lucid is not only that it can be used as a programming language but it can also be used as a “composition” language. That is, instead of using Lucid to specify computations, it can be used to express how computation components (expressed in some other language) can be “glued” together to form a coherent application. By doing so, the resulting application can enjoy some of the practical benefits attributable to Lucid such as high performance through exploitation of implicit parallelism and robustness through software fault tolerance. In this chapter, we discuss one such use of Lucid—as part of a hybrid language to construct parallel applications to be executed on conventional parallel computers. A conventional parallel computer either consists of a number of processors each with local memory interconnected by a network (as in distributed memory architectures) or a number of processors that share memory possibly using an interconnection network (as in shared memory architectures). The past decade has seen the advent of conventional parallel computers starting with the Denelcor HEP evolving to the CM-2 and Intel Hypercube and further evolving to the CM-5, Intel Paragon, Cray T3D, and IBM SP-2. Even networks of workstations (or workstation clusters) are seen as low-cost (“poor man’s”) parallel computers. Programming of conventional parallel computers has proven to be far more challenging than had been expected. Part of the reason is the continued use of low-level, explicitly parallel programming models such as PVM [42], Linda [10]. Two factors have fueled the continuing use of such languages despite their limited success. 1. The need to reuse existing sequential code because the cost of rewriting legacy applications from scratch is considered prohibitive both in economic and technical terms. 2. The need to run on conventional parallel computers that view a “parallel program” at a low level—as consisting of sequential processes that frequently synchronize and communicate with each other using some form of message passing.

Eduction

We know what a Lucid program means mathematically (see Chapter 3), yet that in itself does not suggest a particular model of computation for deriving the same meaning operationally. The purpose of this chapter is to consider the various ways that Lucid programs can be evaluated and to describe in detail the most appropriate model of computation, namely, eduction. Previously, we have seen that Lucid programs can be viewed globally in geometrical terms or locally in elemental terms. Both these views are equally valid as mental devices to enable the programmer to conceive and understand Lucid programs. And each view suggests its own family of computing models—extensional models that embody the global geometrical view and intensional models that embody the local elemental view. Before we compare these two approaches to evaluating Lucid programs, it is worth relating the operational semantics given by a model of computation to the mathematical semantics. Since Lucid is purely declarative, the correct meaning of a Lucid program is that which is given mathematically. This is done without appealing to any operational notions [8]. Thus, the mathematical semantics of a Lucid program has primacy over the many operational semantics that can be given to the Lucid program using different models of computations. Consequently, the correctness of a model of computation is determined by its ability to operationally give semantics to Lucid programs that coincide with their mathematical semantics. Let us consider an extensional model of computation called reduction [37]. It is the standard model for evaluating declarative programs, and more specifically, functional programs. In reduction, programs are considered to be expressions, and a program is evaluated by repeatedly transforming, or reducing, the expression into a possibly simpler expression. The original expression must include any data that the program is to work on, so that at every stage we are manipulating both program and data, and the two become intimately entwined. The process stops when no further transformation can be applied. At each stage, several transformations may be possible, but it doesn’t matter which we apply. If we get an answer, we always get the same answer, but it is possible to make choices so that we do not arrive at the answer.

Transformation and Verification

The ability to verify and reason about programs was one of the main goals behind the design and development of Lucid. In fact, from its very inception Lucid was intended to be not just a programming language, but also a formal system in which program specifications and correctness proofs could be expressed as well. Our goal was a formal programming system in which programs for “realistically” complicated problems could be proved correct with only a realistic amount of effort. The nonprocedural nature of Lucid and its mathematical semantics led naturally to a reasoning technique where properties proved of variables and functions (assertions) are true throughout the where clauses in which the variables and functions are defined, and are not just thought of as being true at particular points where they are “attached” (as would be the case in the usual verification technique for procedural programs). In that respect, Lucid verification is like verification of functional programs. The assertions proved for Lucid, however, have the basic simplicity of the assertions proved in the procedural case, and the proofs are very similar. We will illustrate the differences by using a very simple program for computing integer square roots. We will express it in an imperative language, in a functional language, and in Lucid and show how verification would be performed for each language using the different techniques. In all three techniques, we will use the following terminology from the procedural approach, namely that the precondition is a restriction on the inputs of a program and the postcondition is a desired property of the outputs of the program, assuming that the inputs satisfied the precondition.