An oversimplified history of CSP -Talk by Douglas Creager


An oversimplified history of CSP

Communicating Sequential Processes (CSP) was first described by Tony Hoare in 1978. Since then, there have been two main "branches" of further development. In the first branch, CSP inspired how concurrency is handled in an ongoing series of programming languages — most recently (and famously) in Go. In the second branch, CSP was refined into a rigorous "process calculus", and has since been used to formally prove various safety and liveness properties of concurrent and distributed systems.

This talk will be a whirlwind history of CSP, a high-level overview of the process calculus, and some live demos of using a refinement checker to prove things about interesting systems. (No proving things by hand!)

CAR Hoare. "Communicating Sequential Processes (", CACM 21(8), pp. [masked], 1978.

CAR Hoare. Communicating Sequential Processes. Prentice Hall, 1985.

AW Roscoe. The theory and practice of concurrency. Prentice Hall, 1998.

Douglas Creager is a software engineer at Google. He first learned about CSP as a grad student at Oxford. In the not-too-distant past, he used CSP to do something empirically useful (