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
- The framework itself, some instantiations of it, and important meta-theoretical results about it (the validity of the standard structural congruence rules, and the compositionality of strong labelled bisimilarity) have all been machine-checked in Isabelle/HOL-Nominal. Psi-calculi in Isabelle. In Theorem Proving in Higher Order Logics, volume 5674 of Lecture Notes in Computer Science, pp 99-114, Springer-Verlag, Berlin, 2009. (DOI).Psi-calculi: Mobile processes, nominal data, and logic. In Proc. 24th Annual IEEE Symposium on Logic in Computer Science, pp 39-48, IEEE, Piscataway, NJ, 2009. (DOI).
- The initial equivalence given for Psi-calculi is of the strong kind, i.e. it does not abstract from internal actions. We have defined a weak variant of Psi-calculi equivalence where certain internal actions are ignored, and thus we get a coarser equivalence that coincides with barbed equivalence. Much of this work has also been machine-checked. Weak Equivalences in Psi-calculi. In Proc. 25th Symposium on Logic in Computer Science: LICS 2010, pp 322-331, IEEE, Piscataway, NJ, 2010. (DOI).
- As defined, Psi-calculi are unsuitable for some kinds of automated reasoning; to overcome this we have developed a symbolic operational semantics for Psi-calculi, that is fully abstract with respect to the concrete one. This semantics also allows automated bisimulation checking for finite-state processes. Computing Strong and Weak Bisimulations for Psi-Calculi. In Journal of Logic and Algebraic Programming, volume 81, number 3, pp 162-180, Elsevier, 2012. (DOI).A Fully Abstract Symbolic Semantics for Psi-Calculi. In Proc. 6th Workshop on Structural Operational Semantics: SOS 2009, volume 18 of Electronic Proceedings in Theoretical Computer Science, pp 17-31, 2010. (DOI).
- The framework has been extended to model wireless broadcast communication, with machine-checked proofs of important meta-theoretical results. We have modelled a wireless ad-hoc routing algorithm (LUNAR). Presented at SEFM'11; a long version is in print. Broadcast psi-calculi with an application to wireless protocols. In Software and Systems Modeling, volume 14, number 1, pp 201-216, Springer, 2015. (DOI, fulltext:postprint).Broadcast Psi-calculi with an Application to Wireless Protocols. In Software Engineering and Formal Methods: SEFM 2011, volume 7041 of Lecture Notes in Computer Science, pp 74-89, Springer Berlin/Heidelberg, 2011. (DOI, fulltext:postprint).
- The framework has been extended to model higher-order communication, with machine-checked proofs of important meta-theoretical results. In addition to those results, we also have machine-checked proofs that we can lift any (first-order) Psi instance to an higher-order one, and that case statements and replication are encodable in such canonical higher-order instances. Higher-order psi-calculi. In Mathematical Structures in Computer Science, volume 24, number 2, Cambridge University Press, 2014. (DOI, fulltext:postprint).
- We have added sorting and generalised pattern-matching to the framework, in order to treat models where communication on transmitted data is important. This refinement also admits exact (strong operational) correspondences to value-passing CCS and standard pi-calculus extensions. A Sorted Semantic Framework for Applied Process Calculi (extended abstract). In Trustworthy Global Computing: TGC 2013, volume 8358 of Lecture Notes in Computer Science, pp 103-118, Springer Berlin/Heidelberg, 2014. (DOI).
- A prototype modelling and pre-orderbased verification tool has been developed (see below).
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. 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
- Broadcast psi-calculi with an application to wireless protocols. In Software and Systems Modeling, volume 14, number 1, pp 201-216, Springer, 2015. (DOI, fulltext:postprint).
- A Sorted Semantic Framework for Applied Process Calculi (extended abstract). In Trustworthy Global Computing: TGC 2013, volume 8358 of Lecture Notes in Computer Science, pp 103-118, Springer Berlin/Heidelberg, 2014. (DOI).
- Higher-order psi-calculi. In Mathematical Structures in Computer Science, volume 24, number 2, Cambridge University Press, 2014. (DOI, fulltext:postprint).
- Program Analysis and Verification Based on Kleene Algebra in Isabelle/HOL. In Interactive Theorem Proving: ITP 2013, volume 7998 of Lecture Notes in Computer Science, pp 197-212, Springer Berlin/Heidelberg, 2013. (DOI, fulltext:postprint).
- A Parametric Tool for Applied Process Calculi. 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).
- Kleene Algebra. In Archive of Formal Proofs, 2013. (External link).
- The impact of trace and adversary models on location privacy provided by K-anonymity. In Proc. 1st Workshop on Measurement, Privacy, and Mobility, ACM Press, New York, 2012. (DOI).
- Computing Strong and Weak Bisimulations for Psi-Calculi. In Journal of Logic and Algebraic Programming, volume 81, number 3, pp 162-180, Elsevier, 2012. (DOI).
- Broadcast Psi-calculi with an Application to Wireless Protocols. In Software Engineering and Formal Methods: SEFM 2011, volume 7041 of Lecture Notes in Computer Science, pp 74-89, Springer Berlin/Heidelberg, 2011. (DOI, fulltext:postprint).
- Maintaining Database Integrity with Refinement Types. In ECOOP 2011 – Object-Oriented Programming, volume 6813 of Lecture Notes in Computer Science, pp 484-509, Springer-Verlag, Berlin, 2011. (DOI).
- Verified Stateful Programs with Substructural State and Hoare Types. In Proc. 5th ACM Workshop on Programming Languages Meets Program Verification, pp 15-26, ACM Press, New York, 2011. (DOI).
- Refinement types for secure implementations. In ACM Transactions on Programming Languages and Systems, volume 33, number 2, pp 8:1-45, 2011. (DOI).
- Lower trees with fixed degrees: a recipe for efficient secure hierarchical aggregation in WSNs. In 2011 IEEE WIRELESS COMMUNICATIONS AND NETWORKING CONFERENCE (WCNC), pp 659-664, IEEE Computer Society, 2011. (DOI).
- Psi-calculi: a framework for mobile processes with nominal data and logic. In Logical Methods in Computer Science, volume 7, number 1, p 11, 2011. (DOI).
- Psi-calculi: a framework for mobile process calculi: Cook your own correct process calculus - just add data and logic. Ph.D. thesis, Uppsala Dissertations from the Faculty of Science and Technology nr 94, Acta Universitatis Upsaliensis, Uppsala, 2010. (fulltext).
- Weak Equivalences in Psi-calculi. In Proc. 25th Symposium on Logic in Computer Science: LICS 2010, pp 322-331, IEEE, Piscataway, NJ, 2010. (DOI).
- A Fully Abstract Symbolic Semantics for Psi-Calculi. In Proc. 6th Workshop on Structural Operational Semantics: SOS 2009, volume 18 of Electronic Proceedings in Theoretical Computer Science, pp 17-31, 2010. (DOI).
- Formalising the ?-calculus using nominal logic. In Logical Methods in Computer Science, volume 5, number 2, pp 16:1-36, 2009. (DOI, fulltext).
- Psi-calculi in Isabelle. In Theorem Proving in Higher Order Logics, volume 5674 of Lecture Notes in Computer Science, pp 99-114, Springer-Verlag, Berlin, 2009. (DOI).
- Psi-calculi: Mobile processes, nominal data, and logic. In Proc. 24th Annual IEEE Symposium on Logic in Computer Science, pp 39-48, IEEE, Piscataway, NJ, 2009. (DOI).
- Re?nement Types for Secure Implementations. In Proc. 21st IEEE Computer Security Foundations Symposium, pp 17-32, IEEE, Piscataway, NJ, 2008. (DOI, fulltext).
- Extended pi-Calculi. In Automata, Languages and Programming, PT 2: Proceedings of ICALP 2008, volume 5126 of Lecture Notes in Computer Science, pp 87-98, 2008. (DOI).
- Expressiveness of Process Algebras. In Electronical Notes in Theoretical Computer Science, volume 209, pp 173-186, 2008. (DOI).
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
Staff
Senior: Joachim Parrow (Contact), Björn Victor, Tjark Weber
Research Fellow: Johannes Borgström
Ph.D. students: Palle Raabjerg, Johannes Åman Pohjola, Ramunas Gutkovas
Earlier contributors: Jesper Bengtson, Shuqin Huang, Magnus Johansson, Amin KhorsandiAghai