Semantics of Sequential and Parallel Programs

Stephen Brookes
Carnegie Mellon University
Department of Computer Science

15-812
Fall 2000
MW 10:30-11:50
Starts on Wednesday, 13 September
Wean 4615A

This course can be taken as a ``starred course'' to fulfil the Programming Languages core requirement of the CMU CS Ph.D. program.

Course Outline

This course introduces foundational concepts and techniques of programming language semantics, and demonstrates their application in program analysis and synthesis, and their relevance in language design and implementation. We bring out the key concepts and techniques, building in the necessary mathematics and logic as we go. We aim to demonstrate the utility of a scientific approach to programming languages in answering questions about the pro's and con's of various languages, about compiler correctness, and for other practical purposes.

Syllabus

A tentative syllabus for the course, subject to change, includes:
    Introduction
      Static and dynamic semantics
      Denotational and operational semantics
      Notions of semantic equivalence
      Levels of abstraction

    Sequential imperative programming

      Stores, environments, and state transformations
      Hoare's Logic for partial and total correctness
      Jumps and continuations
      Correctness of compiler optimizations

    Functional programming

      Types and polymorphism
      Call-by-name, call-by-value, and lazy evaluation
      Direct and continuation-style semantics

    Parallel imperative programming

      Shared-variable programs
      Communicating processes and dataflow networks
      Safety and liveness properties, fairness

    Combining functional and imperative programming

    Logic programming (if time permits)

Texts

Lecture notes will be handed out on a regular basis. The following texts are suggested for background reading:

  1. Reynolds, Theories of Programming Languages, Cambridge University Press, ISBN 0-521-59414-6.

  2. Winskel, The Formal Semantics of Programming Languages: An Introduction, MIT Press, ISBN 0-262-23169-7.

Pre-requisites

This course should be accessible to graduate students, masters-level students, and advanced undergraduates in CS, Math, or Philosophy. Some mathematical maturity will be expected. Undergraduates wishing to take this course should contact the instructor for permission.

Introduction

There is a wide variety of programming languages, ranging from low-level machine code and assembler to high-level languages such as C, Java, and Standard ML. A few major paradigms have been identified (e.g. ``functional'', ``imperative'', ``object-oriented'') and a particular language may belong to one or more of these. This type of classification can be useful to a limited extent, but it is much more important to understand the relationship between program syntax (what we write) and algorithms (what happens, in abstract terms, when a program runs). This is one of the purposes of programming language semantics. A semantics for a programming language is a mathematical model that reflects the intended computational behavior of programs. In addition to its role in validating program correctness, semantics can provide a firm foundation for many activities related to programming and the design and implementation of programming languages.

  1. Semantics can allow us to make rigorous statements about properties of programs and the interactions between program constructs.

  2. Lessons learned in semantics of programming languages can guide the design of new languages, including special-purpose languages for scripting or hypertext.

  3. Many code optimization tricks used in compilers (e.g. loop unrolling, code motion, goto-chasing) rely for their soundness on laws of semantic equivalence. Semantics can be used to develop more efficient compilers.

  4. The theory of programming languages provides foundations for the ``formal methods'' advocated by software engineers.

To be useful, a semantics needs to be:
    tractable: as simple as possible without losing the ability to express behavior accurately;
    abstract: uncluttered by irrelevant detail;
    computational: an accurate abstraction from runtime behavior.
To support syntax-directed, or modular, program development and analysis a semantics needs to be compositional.

We will focus on two of the most successful styles of semantic description: denotational and operational semantics. These two styles offer complementary approaches to understanding languages and programs. A denotational semantics is automatically compositional, whereas operational models may lack this property but might compensate by being intuitively easier to understand.

Following tradition, we focus on small ``core'' languages with an idealized syntax, chosen to illustrate a specific paradigm with a minimum of syntactic distraction. We will begin with a sequential imperative programming language, since it requires little semantic sophistication and allows us to introduce the major concepts, notation, and techniques painlessly. We then apply and generalize these ideas and techniques to a series of more complex languages. The approach is incremental, studying each feature in as simple a setting as possible to minimize the potential for confusion and bring out the key issues caused by the feature itself, rather than having to deal with a grab-bag language containing many disparate features.

Requirements

The course will have a strong mathematical flavor, with additional emphasis on writing and analyzing programs. Grading will be based on homeworks, a midterm examination, and a final examination. Homework will include both written assignments and programming problems. The midterm and final will be open-book.

The course will be graded (for CS graduate students) on a pass/fail basis. Undergraduates will be assigned a letter grade.

Students are encouraged to form study groups to discuss homework problems and course material, but any work turned in for a grade must be solely the work of the individual.

Lecture Notes

Lecture notes handed out in class may also be obtained here (in ps format).

Lecture Notes vol. 1

Homework

Look here for homework assignments.

Some macros useful for type-setting homeworks in LaTeX, designed by John Reynolds, can be found in:

diagmac.tex

catmac.tex

Some documentation on these macros:

diagmac.doc