Stephen Brookes

Professor

Website

Office 9017 Gates and Hillman Centers

Email sb21@andrew.cmu.edu

Phone (412) 268-8820

Department
Computer Science Department

Administrative Support Person
Christina Contreras

Research Interests
Formal Methods
Programming Languages
Pure and Applied Logic

CSD Courses Taught

15812 - Spring, 2024

15314 - Spring, 2024

Biography

Stephen Brookes is well known internationally for his seminal contributions to semantics for concurrent programs and logics for reasoning about program behaviour. He earned both his bachelor’s degree in Mathematics and his Ph. D. in Computer Science at Oxford University, joined Carnegie Mellon University as a research computer scientist in 1981, and has been a full professor there since 2006. His doctoral dissertation, supervised by Tony Hoare, was titled "A Model for Communicating Sequential Processes".

His work with Bill Roscoe led to the development of the failures-divergences model of CSP. Over the years Brookes has developed a trace-based framework for giving semantics to a range of parallel paradigms, including shared-memory, synchronous and asynchronous communication. His work on Parallel Algol shows how these ideas can be extended to deal with a language that combines concurrency with higher-order procedures.

A long-term aim of his research has been to improve the design and analysis of correct concurrent programs. His recent work on Concurrent Separation Logic, in collaboration with Peter O’Hearn, is a major development in this direction. CSL supports correctness proofs for software that involves pointer manipulation and shared-memory concurrency, both notoriously difficult to get right. This work has had significant impact in both theory and in practice. Brookes and O’Hearn were awarded the 2016 Gödel Prize, given jointly by European Association for Theoretical Computer Science (EATCS) and the Association for Computing Machinery Special Interest Group on Algorithms and Computational Theory (ACM SIGACT).

Recently, Brookes has been working on partial-order semantic models for relaxed memory concurrency.

Research/Teaching Statement

My main interests concern the mathematical semantics of programming languages. I believe that proper attention to semantic foundations can yield significant benefits in developing techniques for proving properties of programs, in program design, in language design and implementation.

I am particularly interested in developing intensional semantic models, in which one is able to reason both about the correctness and efficiency of programs. This is in contrast to most traditional semantic models, which are extensional and focus on the input-output behavior of programs while abstracting away from computation strategy. I am working mainly on the semantic foundations of parallelism. This work includes the development of axiomatic proof techniques for establishing behavioral properties of parallel systems, design rules for parallel networks that guarantee desirable behavior such as deadlock-freedom, and the design and implementation of programming languages that employ parallelism uniformly and cleanly.

A semantics for a programming language is an assignment of meanings to program terms. For a semantics to be useful it should accurately capture the computational behavior of program terms, at an appropriate level of abstraction.

I believe that major improvements in the formal treatment of program properties can be achieved by paying careful attention to semantics. If we want to reason about a particular behavioral notion (such as partial correctness) we should first define a mathematical model for programs which precisely captures this behavior without being overly complicated. Ideally, we would like a fully abstract semantics: terms should be given the same meaning precisely when the terms would induce identical behavior in all program contexts. The construction of fully abstract models is by no means an easy task, and depends in any case on the underlying notion of behavior.

For modelling and reasoning about certain types of program behavior, such as partial or total correctness, an extensional semantics is satisfactory: the meaning of a program can be chosen to be a (partial) function from initial states to final states, and all details of how the program goes about its computation can be suppressed since all we really need to keep track of is the state transformation that the program induces. However, such a semantics is no use if we want to make comparisons between programs for the same function. In an extensional semantics all sorting programs have the same meaning, whereas we might well want to design a semantics with which we can compare sorting programs with different computation strategies. This motivation leads to a desire for a theory of intensional semantics. In an intensional semantics the meaning of a program is taken to be an algorithm rather than simply a function. An algorithm can be viewed as a function together with a (mathematical representation of a) computation strategy. I have recently developed a category-theoretic approach to the modelling of algorithms, and applied these ideas to the semantics of the lambda calculus. In the resulting semantic model, there is a complete partial order on algorithms and standard operations such as composition, application, and currying are continuous; thus, one may define algorithms recursively and use the standard techniques of denotational semantics (least fixed points) to reason about recursive programs, even at this intensional level. This approach using categories is rather general, and I am exploring several other possible applications.

Semantic principles and insights should be used in the design of new programming languages, to avoid the development of cumbersome languages in which the programmer may have to labor to overcome the syntactic quirks and idiosyncrasies of the programming language in order to express his algorithm as a program. I am particularly interested in designing a language that embodies parallelism uniformly: it ought to be as easy to specify parallel expression evaluation as it is to specify parallel execution of statements, and it ought to be easy to put together the results of parallel activities. The choice of an appropriate set of primitives for such a language should be guided by proper attention to semantic foundations, and I am carrying out research on this topic.

Publications