Home » forums » LtU Forum

Process Algebras: Whats the point?

There seems to be quiet a few parallel/concurrent oriented languages (Erlang) and dialects of languages (Split C, Titanium (java variant), Hi Performance Fortran), and language specific libraries that enable parallelization (MPI, OpenMP, JPPF). With respect to process algebras, what type of analysis do process algebras allow us to do? Simply characterize the different implementations? Provide us a framework to improve the different implementatons? Have process algebras had any impact on real world languages and compilers?

So, process algebra, what have you done for me lately?

By markt at 2007-12-28 23:45 | LtU Forum | previous forum topic | next forum topic | other blogs | 11404 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Several things

So, process algebra, what have you done for me lately?

Several things. They've given us:

  • Mental models that allow one to develop a better intuition for concurrent behavior (I've found understanding even the shared-memory concurrency supported by most languages easier to understand by thinking about it -- informally -- in terms of process algebraic expressions).
  • A way to formally describe concurrent computations (akin to the lambda calculus) in a compositional manner (compositionality being something that other formalisms for concurrency have problems with).
  • A way to define equivalences between different concurrent processes -- see bisimulation (in its various forms), may- and must-testing, trace-equivalence, failures-equivalence, etc. etc.
  • A way to formally define the semantics of concurrent programming languages (e.g. the semantics of core Erlang have been defined in the pi-calculus, the semantics of VHDL have been defined in CSP, and so on).
  • Proof techniques (theorem proving on denotational semantics, various algebraic proof techniques such as "cones and foci", proofs of simulation and bisimulation on labelled transition systems) in order to check that abstract system models preserve certain desirable properties.
  • The ability to mechanically check for system properties such as safety, deadlock-freedom, and liveness using model-checkers.

Impact on real-world languages and compilers? Here are the ones I can think of off the top of my head (there are undoubtedly more, which other LtU readers will hopefully be able to tell us about):

  • Occam - heavily influenced by CSP, and occam developers have been known to use to CSP models to analyze their design prior to coding.
  • Bell Labs' Alef and Limbo languages (both used extensively in the Plan-9 OS and its successors) - both influenced by CSP.
  • Pict - based on the asynchronous pi-calculus.
  • Esterel - originally influenced by SCCS (Synchronous CCS).
  • Mozart/Oz - the kernel language is (IIRC) defined as a process calculus.
  • Concurrent ML - drew on ideas from process calculi.
  • Jocaml - implements the join calculus.
  • Ada and Eiffel - concurrency model(s) influenced by CSP.

Process algebraic models have also been used to break security protocols, verify the design of fault-tolerant systems, model biological systems, specify and verify telecommunications systems, provide formal semantics for UML notations, and the list goes on...

By Allan McInnes at Sat, 2007-12-29 01:34 | login or register to post comments

Perfect

Thanks Allan, thats just the sort of info dense response I was hoping for. Do you have any links to relevant papers etc... ? How about textbooks, have you used any in a class that you'd recommend?

By markt at Sun, 2007-12-30 00:32 | login or register to post comments

A few links and references

Probably the single best place to start for understanding where process algebra(s) came from, and where they're going, is the proceedings of the BRICS workshop "Algebraic Process Calculi: The First Twenty Five Years and Beyond" (available online here). It includes papers by such process algebra luminaries as Tony Hoare, Robin Milner, Jan Bergstra, Jan Klop, Bill Roscoe, David Sangiorgi, and Stephen Brookes. A good overview of the history of process algebra is Baeten's A Brief History of Process Algebra.

Links to info on Alef and other Bell Labs efforts are available here

The Wikipedia CSP article includes several references to occam, and to industrial uses of CSP. It also includes links to Hoare's original CSP textbook, as well as Bill Roscoe's more recent one (both now available online).

The Wikipedia pi-calculus article includes a brief discussion of some applications, and links to information on various languages that have been influenced by the pi-calculus.

The paper on using pi-calculus for the semantics of Erlang is Noll and Roy, Modeling Erlang in the Pi–Calculus, 2005 Erlang Workshop (the only link I know of is an ACM one). The CSP/VHDL paper is Chapman and Hwang, A Process-Algebraic Semantics for VHDL, available here.

If there are specific areas you're interested in, I'd be happy to provide more specific guidance on relevant papers. As for textbooks, I'm quite partial to Bill Roscoe's The Theory and Practice of Concurrency (link mentioned above) -- in my opinion, it does a good job of covering the basics of process algebra, the deep theory of several different semantic models, and some practical applications. However, it is very much about CSP. If you're looking for something more CCS/pi-calculus oriented, then Milner's Communicating and Mobile Systems: the Pi-Calculus is a pretty good place to start.

By Allan McInnes at Sun, 2007-12-30 06:35 | login or register to post comments

Embodiment in languages?

It seems sad to me that what with deadlock and other evils being so evil + multi core on the rise, that we don't have better formal approaches in a language that could be 'industrial ready' (by which I mean: has a debugger, has at least an Emacs mode if not an Eclipse plugin, etc.). I guess there is the possibly-un-dead-again JCSP? Scala's or Erlang's actors don't seem formal enough to me.

By raould at Fri, 2008-02-22 01:55 | login or register to post comments

Real World

I would say right now that the most real-world instance of a formal process calculus provided at the language level is JoCaml. See how it fared, for example, in the Wide Finder project.

By Paul Snively at Fri, 2008-02-22 13:40 | login or register to post comments

Erlang and Oz

Paul beat me to the punch with JoCaml. Aside from that, there are a couple of other options:

  • While Erlang wasn't necessarily designed from a formal basis, it has, as I pointed out above, been given a formal interpretation in the pi-calculus. So you could in theory carry out a formal analysis on an Erlang actor system if you wanted to. I'm not sure if anyone has. I don't know about Scala actors - I haven't looked at them in much depth yet - but it wouldn't surprise me to find that someone has given them an interpretation in the pi-calculus.
  • Mozart/Oz. Peter gave us a recent reminder that kernel Oz is in fact a process calculus. Gert Smolka's original paper on the Oz calculus can be found here. Granted, I'm not aware of anything like model-checker support for the Oz calculus. But it does at least support formal reasoning. And there's certainly an Emacs mode :-)
By Allan McInnes at Fri, 2008-02-22 16:32 | login or register to post comments

thanks

Thanks!

By markt at Wed, 2008-01-02 17:34 | login or register to post comments

EPFL

[edit: er, i got confused about links while searching. this is 'regular' ESC/J stuff, which is fine and good, but not what i thought i was looking at.]

seems to have some interesting stuff [pdf], although in the grand tradition of /. i've only skimmed the web site, not used the system.

By raould at Mon, 2008-02-25 06:41 | login or register to post comments