Professor of Computer Science
Carnegie Mellon University
5000 Forbes Avenue
Pittsburgh, PA 15213, USA

Phone: 412-268-8820
Fax: 412-268-4801
Email: brookes AT cs DOT cmu DOT edu

Research

My research concerns semantic models for programming languages and logics for reasoning about the behavior of concurrent programs.

I have been involved in the development of Concurrent Separation Logic, in collaboration with John Reynolds and Peter O'Hearn. I am currently investigating further extensions to this logic, and working out the semantic underpinnings needed to validate logics that combine concurrency with procedures and communication.

History

My Ph.D. thesis, A Model for Communicating Sequential Processes, was completed at Oxford University (January 1983), where my advisor was Tony Hoare.

With Tony Hoare and Bill Roscoe, I developed the failures model of CSP; later, Bill and I produced an improved failures model that became the basis for the implementation of the FDR model checker. I also collaborated with Bill Rounds on the possible futures model of CSP.

Over the years, I have produced a variety of semantic models for concurrent languages, including Idealized CSP and Parallel Algol. These languages combine simply-typed call-by-name procedures, and statically scoped blocks, with communication and shared-memory concurrency, respectively.

I have introduced a family of trace-based semantic models suitable for modelling programs in several concurrency paradigms, including shared-memory as well as asynchronous communicating processes and CSP-style synchronously communicating processes.

I have worked with my erstwhile students (Shai Geva, Denis Dancanet, Kathy Van Stone, Michel Schellekens) on various aspects of intensional semantics, and I continue to maintain an interest in this area. With Susan Older, I worked on models for various notions of fairness. My former student, Juergen Dingel, developed a methodology for systematic parallel programming.

Background

A mathematical model, or semantics, for a programming language can be used to support program analysis and synthesis, to validate a compiler, or may serve as the foundation for the design of a logic for program specification and proof.

I work mainly on the development of denotational semantic models, characterized by the property that the meaning of a program phrase is defined in terms of the meanings of its syntactic sub-phrases. This structural property ensures support for compositional (syntax-directed) reasoning. I also work with operational semantic models, in which program behavior is typically explained in terms of the computational behavior of an abstract machine. I aim to use semantic models to guide the design of techniques and logics for program proving.

My work aims to produce tractable semantic models whose structure is as simple as possible while accurately representing program behavior. This principle is usually expressed more formally as a desire for full abstraction with respect to the relevant notion of program behavior: a semantic model should distinguish between two program fragments precisely when there is a program context in which the phrases can induce observably different behavior.

Full abstraction means that the model is just concrete enough to support compositional program analysis in a manner faithful to the underlying notion of behavior. This principle can be used as a criterion for judging the utility of a semantic model with respect to a specific notion of program behavior. However, by itself full abstraction is not a panacea, and it can be difficult to achieve: ideally it is preferable to work with a model that is both sufficiently abstract to support accurate analysis and has a clean enough mathematical structure that it can be easily used to formalize concepts and perform proofs. Elegance is a virtue, and arguably a necessity. My foundational research has always been guided by such principles, seeking to simplify without over-simplification.

My main focus is on concurrent programming languages. A long-term goal is to improve our ability to design efficient, correct parallel systems and provide foundational support for the development of tools to facilitate concurrent programming design and analysis. Concurrent programs are widely used, hard to get right, and difficult to analyze.

In addition to partial correctness and total correctness, we often need to be able to establish safety properties, of the form that something bad never happens, and liveness properties, of the form that something good happens eventually. It is notoriously difficult to ensure that concurrent process interactions are sufficiently disciplined to preclude undesirable phenomena such as races, in which one process changes a piece of state that is being used by another process, with unreliable results.

Rather than relying on possibly unrealistic assumptions about the granularity of hardware primitives, it is preferable to use semantic models and proof techniques that can guarantee correct behavior and the absence of races. Further, we need to find ways to avoid or mitigate the combinatorial explosion inherent in analyzing the ways in which concurrent processes might interact.


In summary, my work addresses the need for semantic models, specification methods, and logics that support correctness proofs with a guarantee of race-freedom (and absence of other runtime errors).

Papers

A Semantics for Concurrent Separation Logic.
S. Brookes. In: Theoretical Computer Science, Vol. 375, Festschrift for John C. Reynolds's 70th Birthday, May 2007. Extended version of paper from CONCUR 15.
abstract paper

A Brief History of Shared Memory.
S. Brookes. Invited talk, MFPS XXIII, New Orleans, April 2007. Elsevier ENTCS 173.
abstract paper slides

Concurrent Separation Logic.
S. Brookes. Lectures, Summer School on Dependable Software Systems, Lugano, Switzerland, July 2007.
Lecture 1 Lecture 2

Variables as Resource for Shared Memory Programs: Semantics and Soundness.
S. Brookes. MFPS XXII, Genova, Italy, May 2006. Elsevier ENTCS 158.
abstract paper slides

Concurrent separation logic: semantics and soundness.
S. Brookes. Tutorial, with Peter O'Hearn, MFPS XXII, Genova, Italy, May 2006.
slides

A Semantics for Concurrent Permission Logic.
S. Brookes. Talk presented in a workshop at Cambridge University, March 2006.
slides

A Grainless Semantics for Parallel Programs with Shared Mutable Data.
S. Brookes. MFPS XXI, Birmingham, England, May 2005. Elsevier ENTCS 155.
Also presented at Geometry of Computation (Geocal'06), Marseilles, February 2006.
abstract paper slides

Retracing CSP.
S. Brookes. In Algebraic Process Calculi: The First 25 Years and Beyond, Bertinoro, Italy, August 2005.
Elsevier ENTCS 162.
abstract paper slides

A race-detecting semantics for concurrent programs.
S. Brookes. MFPS XX, Pittsburgh, May 2004.
slides

A Semantics for Concurrent Separation Logic.
S. Brookes. Invited paper, CONCUR 15, London, Springer LNCS 3170, August 2004. Slides from tutorial on Concurrent Separation Logic (joint with Peter O'Hearn).
abstract paper slides

Retracing the Semantics of CSP.
S. Brookes. Invited paper, Conference on 25 Years of CSP, London, July 2004.
Full version in: 25 Years of CSP, A. Abdullah, C. B. Jones, and J. Sanders, eds. Springer LNCS Festschrift Series, vol. 3525 (2005).
abstract paper slides

Using transition traces to model a security protocol.
S. Brookes. Manuscript, March 2003.
paper

Semantics of Parallel Programs.
S. Brookes. Lecture given at Queens University, Kingston, Ontario, February 2003.
slides

The Essence of Parallel Algol.
S. Brookes. Information and Computation 179(1), 2002. Extended version of paper from LICS'96.
abstract paper

Traces: a unifying semantic framework for parallel programming languages.
S. Brookes. MFPS 18, New Orleans, March 2002.
abstract slides

Trace Semantics: Towards a Unification of Parallel Paradigms.
S. Brookes. Invited talk. Irish Conference on Mathematical Foundations of Computer Science and Information Technology (MFCSIT'02), National University of Ireland, Galway, 2002.
slides

Traces, Pomsets, Fairness and Full Abstraction for Communicating Processes.
S. Brookes. CONCUR 2002, Brno, Czech Republic, August 2002. Springer LNCS 2421.
abstract paper slides

Transfer Principles for Reasoning about Concurrent Programs.
S. Brookes. MFPS 17, Aarhus, Denmark, May 2001. Elsevier ENTCS 45.
abstract paper

Deconstructing CCS and CSP: Asynchronous Communication, Fairness, and Full Abstraction.
S. Brookes. MFPS 16, Hoboken, April 2000.
abstract paper slides

Reasoning about Recursive Processes: Expansion is not always Fair.
S. Brookes. MFPS 15, New Orleans, May 1999. Elsevier ENTCS 20.
abstract paper

The Essence of Parallel Algol.
S. Brookes. 11th Conference on Logic in Computer Science (LICS'96), July 1996, IEEE Computer Society Press.
Carnegie Mellon Technical Report CMU-CS-97-124.
Reprinted with permission as Chapter 21 of Algol-like Languages, vol. 2, pp. 331-348, edited by P. O'Hearn and R. D. Tennent, Birkhauser (1997).
abstract paper slides

Communicating Parallel Processes.
S. Brookes. In: Millenium Perspectives in Computer Science, 1999 Oxford-Microsoft Symposium in honour of Sir Tony Hoare, edited by J. Davies, A. W. Roscoe, and J. Woodcock. Palgrave, 2000.
abstract paper slides

On the Kahn Principle and Fair Networks.
S. Brookes. MFPS 14, Queen Mary Westfield College, London, May 1998.
Extended version: Technical Report CMU-CS-98-156, August 1998.
abstract paper slides report

Objects in Idealized CSP.
S. Brookes. Talk given at Dagstuhl Seminar. 1998.
slides

Idealized CSP: Combining Procedures with Communicating Processes.
S. Brookes. MFPS 13, Pittsburgh, March 1997.
Elsevier ENTCS vol. 6.
abstract paper slides

Programming language expressiveness and circuit complexity.
D. Dancanet and S. Brookes. MFPS 12, Boulder, Colorado, June 1996.
abstract paper

How to be Fair.
S. Brookes. Distinguished Lecture, Kansas State University, 1996.
slides

Parallel Algol: Combining Procedures with Concurrency.
S. Brookes. Talk given at Kansas State University, 1996.
slides

Full Abstraction for a Shared-Variable Parallel Language.
S. Brookes. Information and Computation 127(2):145-163, Academic Press, June 1996.
abstract paper

Full Abstraction for Strongly Fair Communicating Processes.
S. Brookes and S. Older. MFPS 11, Elsevier ENTCS vol. 1, March 1995.
abstract paper

Sequential Algorithms, Deterministic Parallelism, and Intensional Expressiveness.
S. Brookes and D. Dancanet. ACM Symposium on Principles of Programming Languages (POPL'95), ACM Press, January 1995.
abstract paper

Fair Communicating Processes.
S. Brookes. Chapter 4 of: A Classical Mind: Essays in Honour of C. A. R. Hoare, edited by A. W. Roscoe. Prentice-Hall International, January 1994.
paper

Reasoning about Parallel Programs with Local Variables
S. Brookes. Talk given at MFPS 10, Manhattan, Kansas, 1994.
slides

Using Fixed Point Theorems to Prove Retiming Lemmas.
S. Brookes. Formal Methods in System Design, vol. 2, no. 1, Springer Netherlands, February 1993.
abstract paper

Full Abstraction for a Shared-Variable Parallel Language.
S. Brookes. Proc. 8th Conference on Logic in Computer Science, Montreal, IEEE Computer Society Press, pp 98-109, June 1993.
abstract paper

Monads and Comonads in Intensional Semantics.
S. Brookes and K. van Stone, Carnegie Mellon Computer Science Technical Report CMU-CS-93-140.
abstract report

Deadlock Analysis in Networks of Communicating Processes.
S. Brookes and A. W. Roscoe
Distributed Computing 4:209-230, 1991.
abstract paper

Towards a Theory of Intensional Semantics.
S. Brookes and S. Geva. Talk given at Oxford, Edinburgh, and Imperial College, July-August 1992.
slides

A Cartesian Closed Category of Parallel Algorithms between Scott Domains.
S. Brookes and S. Geva. Dagstuhl Seminar on Concurrency, June 1991.
In: Semantics of Programming Languages and Model Theory, edited by M. Droste and Y. Gurevich, Gordon and Breach Science Publishers, 1993.
Also published as Technical Report CMU-CS-91-159.
abstract report

Sequential Functions on Indexed Domains and Full Abstraction for a Sub-language of PCF.
S. Brookes and S. Geva. MFPS 9, New Orleans, 1993. Springer LNCS 802, 1994. Technical Report CMU-CS-93-163, April 1993.
abstract report

Historical introduction to "Concrete domains" by G. Kahn and G. D. Plotkin
S. Brookes. Theoretical Computer Science 121, pp. 179-186 (1993).
paper

Towards a Theory of Parallel Algorithms on Concrete Data Structures.
S. Brookes and S. Geva. Theoretical Computer Science 101, pp. 177-221 (1992).
Also Technical Report CMU-CS-91-157.
abstract paper report

Stable and Sequential Functions on Scott Domains.
S. Brookes and S. Geva. Technical Report CMU-CS-92-121, June 1992.
abstract report

Stable and Sequential Functions on Scott Domains,
dI-domains and FM-domains
.
S. Brookes and S. Geva.
Talk given at MFPS 8, Oxford, 1992.
slides

Computational Comonads and Intensional Semantics.
S. Brookes and S. Geva. Applications of Categories in Computer Science, Proc. London Mathematical Society Symposium, LMS Lecture Notes Series, vol. 177, edited by M. Fourman, P. T. Johnstone, and A. M. Pitts, Cambridge University Press (1992).
Technical Report CMU-CS-91-190. October 1991.
abstract paper report

Possible Futures, Acceptances, Refusals, and Communicating Processes.
S. Brookes and W. C. Rounds. 22nd IEEE Symposium on Foundations of Computer Science, IEEE Press, October 1991.
abstract paper

Continuous Functions and Parallel Algorithms on Concrete Data Structures.
S. Brookes and S. Geva. MFPS 7, Pittsburgh, March 1991. Springer LNCS vol. 598 (May 1992).
Technical Report CMU-CS-91-160.
abstract report

Towards a Theory of Parallel Algorithms on Concrete Data Structures.
S. Brookes and S. Geva. In: Semantics for Concurrency, Leicester 1990, Proceedings of the International BCS-FACS Workshop, edited by M. Z. Kwiatkowska, M. W. Shields, and R. M. Thomas, Springer-Verlag (July 1990).
abstract paper

An Operational Semantics for CSP.
S. Brookes, A. W. Roscoe, and D. J. Walker. Manuscript, 1988.
paper

Semantically Based Axiomatics.
S. Brookes. MFPS 4, Boulder, 1988. Springer LNCS 298, pp. 312-330.
abstract paper

A Semantically Based Proof System for Partial Correctness and Deadlock in CSP.
S. Brookes. LICS'86, Cambridge, Massachusetts, IEEE Press, June 1986.
abstract paper

An Axiomatic Treatment of Partial Correctness and Deadlock in a Shared Variable Parallel Language.
S. Brookes. Expanded and improved version of paper from Logics of Programs (1985). Technical Report CMU-CS-92-154, June 1992.
abstract paper

An Axiomatic Treatment of a Parallel Language.
S. Brookes. In: Logics of Programs, Proceedings of the International Conference, Brooklyn, edited by R. Parikh, Springer LNCS 193, June 1985.

A Fully Abstract Semantics and a Proof System for an Algol-like Language with Sharing.
S. Brookes. Proc. 1st MFPS Conference, Manhattan, Kansas. Springer LNCS vol. 239, April 1985. Revised, August 1989.
abstract paper

On the Axiomatic Treatment of Concurrency.
S. Brookes. NSF-SERC Seminar on Concurrency, Pittsburgh, July 1984. Springer LNCS 197, 1985. Technical Report CMU-CS-85-106.
abstract paper

An Improved Failures Model for Communicating Processes.
S. Brookes and A. W. Roscoe
NSF-SERC Seminar on Concurrency, Pittsburgh, July 1984. Springer LNCS 197, pp. 281-305, 1985.
abstract paper

A Theory of Communicating Sequential Processes.
S. Brookes, C. A. R. Hoare, and A. W. Roscoe, J. ACM vol. 31, pp. 560-599, July 1984.
abstract paper

On the Relationship of CCS and CSP.
S. Brookes. ICALP'83, Barcelona, Springer LNCS 158, July 1983.
abstract paper

Behavioral Equivalence Relations Induced by Programming Logics.
S. Brookes and W. C. Rounds. ICALP'83, Barcelona, Springer LNCS 58, July 1983.
abstract paper

A Model for Communicating Sequential Processes.
S. Brookes. Ph.D. thesis, Oxford University, 1983.
Technical Report CMU-CS-83-149 and Oxford University Programming Research Group Technical Monograph PRG-35 (1983).
abstract thesis

Current Students

  • Ruy Ley-Wild
  • Carsten Varming (jointly advised by John Reynolds)

Former Students

  • Kathy Van Stone
    • Thesis: A Denotational Approach to Measuring Complexity in Functional Programs (2003)
  • Juergen Dingel
    • Thesis: Systematic Parallel Programming (1999)
    • Current position: Associate Professor, School of Computing, Queens University, Kingston, Ontario
  • Denis Dancanet
    • Thesis: Intensional Investigations (1998)
    • Current position: investment bank, London.
  • Susan Older
    • Thesis: A Denotational Framework for Fair Communicating Processes (1996)
    • Current position: Associate Professor, Syracuse University
  • Michel Schellekens
    • Thesis: The Smyth Completion: a Common Topological Foundation for Denotational Semantics and Complexity Analysis (1995)
    • Current position: Associate Professor, Department of Computer Science, National University of Ireland, Cork
  • Shai Geva
    • Thesis: A Study of Higher-Order Sequential Computation (1995)
    • Current position: Chief Scientist, Mercado Software