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