Network-Conscious π-calculus – A Model of Pastry

A peer-to-peer (p2p) system provides the networking substrate for the execution of distributed applications. It is made of peers that interact over an overlay network. Overlay networks are highly dynamic, as peers can join and leave at any time. Traditional process calculi, such as π-calculus, CCS and others, seem inadequate to capture these kinds of networks, their routing mechanisms, and to verify their properties. In order to model network architecture in a more explicit way, in [Ugo Montanari and Matteo Sammartino. Network conscious π-calculus: A concurrent semantics. ENTCS, 286:291–306, 2012; Matteo Sammartino. A Network-Aware Process Calculus for Global Computing and its Categorical Framework. PhD thesis, University of Pisa, 2013. available at http://www.di.unipi.it/~sammarti/publications/thesis.pdf; Ugo Montanari and Matteo Sammartino. A network-conscious π-calculus and its coalgebraic semantics. Theor. Comput. Sci., 546:188–224, 2014] we have introduced the Network Conscious π-calculus (NCPi), an extension of the π-calculus with names representing network nodes and links. In [Ugo Montanari and Matteo Sammartino. A network–conscious π-calculus and its coalgebraic semantics. Theor. Comput. Sci., 546:188–224, 2014] (a simpler version of) NCPi has been equipped with a coalgebraic operational models, along the lines of Fiore-Turi presheaf-based approach [Marcelo P. Fiore and Daniele Turi. Semantics of name and value passing. In LICS 2001, pages 93–104. IEEE Computer Society, 2001], and with an equivalent History Dependent Automaton [Ugo Montanari and Marco Pistore. Structured coalgebras and minimal hd-automata for the π-calculus. Theor. Comput. Sci., 340(3):539–576, 2005], i.e., an (often) finite-state automaton suitable for verification. In this paper we first give a brief account of these results. Then, our contribution is the sketch of a NCPi representation of the p2p architecture Pastry. In particular, we give models of its overlay network and of a Distributed Hash Table built on top of it, and we give evidence of their correctness by proving convergence of routing mechanisms.