Department of Information Technology

Applied Calculi

Motivation

With increasing numbers of processor cores, cache coherence algorithms for globally consistent shared memory become very costly, and chip manufacturers (Cell, SCC) and systems builders (BarrelFish) instead turn towards using and implementing explicit message-passing. A successful means of modelling message-passing concurrent systems is process calculi,
miniature formal languages which enable formal reasoning about a system and its semantics.

When modelling real world problems in pure process calculi one soon discovers that the model becomes big and hard to understand due to a lack of more complex datatypes and constructs. To address this, several "applied" calculi have emerged, e.g. the spi-calculus and the applied pi-calculus. So far, they have mainly been used for verification of security protocols.

In an attempt to unify these extensions and to get simpler semantics we are developing a framework in which these extensions can be formulated. Since the meta-theory of applied process calculi is complicated and prone to errors, we formalize the theory in the theorem prover Isabelle/HOL-Nominal as it is being developed, thereby ensuring that the theory is indeed correct.

Long Term Goal

Developing formally verified theory and tool support for modelling message-passing systems and programs.

Much of this work will be generally applicable to a wide range of fields, but in the context of UPMARC the focus is on enabling the modelling and formal verification of multicore protocols and algorithms, ensuring the correctness of multicore systems.

Expected Results

A family of process calculi, with members that faithfully model interesting parallel communicating systems, and tool support for debugging and verifying aspects of such models.

Approach

  • Development of theoretical frameworks for defining applied process calculi for modelling certain classes of message-passing systems.
  • Formal verification of the meta-thory of the framework and the validity of definitions of calculi in the theorem prover Isabelle/Hol-Nominal.
  • Validation of the framework by modelling interesting message-passing programs and systems.
  • Development of tool support for simulation and equivalence proofs for models in calculi within the framework.

Results

We have developed Psi-calculi, a framework for defining applied calculi. By instantiating three data types and four operators that must respect a handful of requirements we show that you get a process calculus that is compositional and respects the usual structural rules. The data types are terms (used for both communication channels and data), conditions (used for tests), and assertions (used for statements about data). The operators are channel equivalence (saying which terms are deemed to be equal channels), composition (saying how to compose assertions), unit (an assertion being the unit element of the composition operator), and entailment (saying which conditions can be entailed from which assertions).

Achievements

Software

  • Automated Psi instantiation: Framework in Isabelle for automated instantiation proofs for Psi. Master's thesis project of Johannes Åman Pohjola.
  • A Psi Workbench. The tool contains functionality common to all instances of the psi-calculus, while the tool user starts by implementing the parameters of a psi-calculus instance in ML. Currently the tool provides computation of the symbolic transition graph of a process, and computation of logical conditions for bisimilarity of two processes. The symbolic transition constraints and the bisimulation constraints are solved by user-provided constraint solvers. One novelty is the support for both unicast and broadcast communication in the same model. The tool is in active development.
    A Parametric Tool for Applied Process Calculi. Johannes Borgström, Ramunas Gutkovas, Ioana Rodhe, and Björn Victor. In 13th International Conference on Application of Concurrency to System Design (ACSD 2013), International Conference on Application of Concurrency to System Design, pp 180-185, IEEE Computer Society, 2013. (DOI).

Publications

Presentations, PR, press clippings, awards

  • Extended pi-calculi. Reykjavik, July 2008, at ICALP 2008. (presentation by Magnus Johansson)
  • Verifying psi-calculi. Uppsala University, October 2008, master's thesis presentation. (presentation by Johannes Åman Pohjola )
  • Three holy grails of programming models. KTH, May 2009, invited seminar. (presentation by Joachim Parrow )
  • Psi-calculi: Mobile processes, nominal data, and logic. UCLA, July 2009, at LICS 2009 (presentation by Joachim Parrow )
  • Psi-calculi in Isabelle. TU Munich, August 2009, at TPHOLs 2009. (presentation by Jesper Bengtson)
  • A fully abstract symbolic semantics for psi-calculi. Bologna, August 2009, at SOS 2009. (presentation by Magnus Johansson)
  • Three holy grails of programming models. Ecole Polytechnique, Paris, May 2009, invited seminar (presentation by Joachim Parrow )
  • Concurrency: Semantics, models and proofs. Uppsala, March 2010, at the UPMARC review (presentation by Joachim Parrow )
  • Psi-calculi. Cambridge, November 2010, at the MSRC type wrestling seminar. (presentation by Johannes Borgström )
  • Weak equivalences in psi-calculi. Edinburgh, July 2010, at LICS 2010. (presentation by Björn Victor )
  • Commemoration of Robin Milner. Perpignan, September 2010, invited talk at SAS 2010 (presentation by Joachim Parrow )
  • Concurrency and Proofs. Gothenburgh, October 2010, part of the distinguished lecture series. (presentation by Joachim Parrow )
  • Concurrency and Proofs. Turku, November 2010, invited talk at NWPT 2010. (presentation by Joachim Parrow )
  • From pi to extended pi to Psi to extended Psi. Aalborg, November 2010. Seminar at Aalborg University. (presentation by Palle Raabjerg )
  • Exercising Psi-calculi: A Psi-calculi Workbench. Uppsala University, June 2011, master's thesis presentation. (presentation by Ramunas Gutkovas )
  • Shortest ever talk on the Psi-calculus. Bayrischzell, August 2011. Student talk at International Summer School Marktoberdorf. (presentation by Palle Raabjerg )
  • Applied process calculi made easy as pi. Aachen, September 2011, invited talk at EXPRESS'11 (presentation by Björn Victor )
  • Psi-calculi: mobile processes from nominal data and logic. Edinburgh, November 2011, talk at the LFCS lunch seminar (presentation by Johannes Borgström )
  • Broadcast Psi-calculi with an application to wireless protocols. Montevideo, November 2011, presentation at SEFM 2011 Björn Victor and Johannes Åman Pohjola).
  • The pi-calculus: Origin and recent development. Edinburgh, April 2012, invited talk at the Robin Milner memorial symposium. (presentation by Joachim Parrow)
  • A Parametric Tool for Applied Process Calculi: Psi-Calculi Workbench. Barcelona, July 2013, presentation at ACSD 2013 by Ramunas Gutkovas
  • A Sorted Semantic Framework for Applied Process Calculi. Buenos Aires, September 2013, presentation at TGC 2013 by Björn Victor

Updated  2014-01-15 10:35:52 by Johannes Borgström.