Advertisement

The Calculus of Handshake Configurations

  • Luca Fossati
  • Daniele Varacca
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5504)

Abstract

Handshake protocols are asynchronous protocols that enforce several properties such as absence of transmission interference and insensitivity from delays of propagation on wires. We propose a concurrent process calculus for handshake protocols. This calculus uses two mechanisms of synchronization: rendez-vous communication à la CCS, and shared resource usage. To enforce the handshake discipline, the calculus is endowed with a typing system.

We provide an LTS semantics of the calculus and show that typed processes denote handshake protocols. We give the calculus another semantics in terms of a special kind of Petri nets called handshake Petri nets. We show that this semantics is complete and fully abstract with respect to weak bisimilarity.

Keywords

Handshake protocols Petri nets process calculus types 

References

  1. 1.
    Abramsky, S., Gay, S., Nagarajan, R.: Interaction categories and the foundations of types concurrent programming. In: Proc. of the 1994 Marktoberdorf Summer School on Deductive Program Design, pp. 35–113. Springer, Heidelberg (1996)Google Scholar
  2. 2.
    Arun-Kumar, S., Hennessy, M.: An efficiency preorder for processes. Acta Informatica 29(9), 737–760 (1992)MathSciNetCrossRefzbMATHGoogle Scholar
  3. 3.
    Bardsley, A.: Balsa: an asynchronous circuit synthesis system. Master’s thesis. Department of Computer Science, University of Manchester (1998)Google Scholar
  4. 4.
    Fossati, L.: Modeling the Handshake Protocol for Asynchrony. PhD thesis, Dip. di Informatica, Univ. di Torino & Lab. Preuves Programmes et Systèmes (PPS), Univ. Paris 7 (2009)Google Scholar
  5. 5.
    Fossati, L., Varacca, D.: The calculus of handshake configurations (extended version) (2008), http://www.di.unito.it/~fossati/
  6. 6.
    Fossati, L., Varacca, D.: A Petri net model of handshake circuits. In: Proc. of First International Workshop on Interactive Concurrency Experience, ICE 2008. ENTCS. Elsevier, Amsterdam (to be published, 2008), http://www.di.unito.it/~fossati/ Google Scholar
  7. 7.
    Gelernter, D.: Generative communication in Linda. ACM Transactions on Programming Languages and Systems 7(1), 80–112 (1985)CrossRefzbMATHGoogle Scholar
  8. 8.
    Ghica, D.R.: Geometry of synthesis: a structured approach to VLSI design. In: Proc. of POPL 2007, pp. 363–375. ACM Press, New York (2007)Google Scholar
  9. 9.
  10. 10.
    Josephs, M., Udding, J., Yantchev, Y.: Handshake algebra. Technical Report SBU-CISM-93-1, School of Computing, Information Systems and Mathematics, South Bank University, London (1993)Google Scholar
  11. 11.
    Kobayashi, N., Pierce, B., Turner, D.: Linearity and the π-calculus. ACM Transactions on Programming Languages and Systems 21(5), 914–947 (1999)CrossRefGoogle Scholar
  12. 12.
    Mackie, I.: The geometry of interaction machine. In: Proc. of POPL 1995, pp. 198–208. ACM Press, New York (1995)Google Scholar
  13. 13.
    Milner, R.: Communication and Concurrency, 2nd edn. Prentice-Hall, Englewood Cliffs (1991)zbMATHGoogle Scholar
  14. 14.
    Milner, R., Sangiorgi, D.: Techniques for “weak bisimulation up-to”. Revised version of a paper that appeared in: Cleaveland, W.R. (ed.) CONCUR 1992. LNCS, vol. 630. Springer, Heidelberg (1992); available on Sangiorgi’s webpageGoogle Scholar
  15. 15.
    Reisig, W.: Petri Nets: An Introduction. Monographs in Theoretical Computer Science. An EATCS Series, vol. 4. Springer, Heidelberg (1985)CrossRefzbMATHGoogle Scholar
  16. 16.
    Roscoe, A.W.: Unbounded nondeterminism in CSP. Journal of Logic and Computation 3(2), 131–172 (1993); Previously appeared in Two Papers on CSP, tech. monograph PRG-67, Oxford University Computing Laboratory(July 1988)MathSciNetCrossRefzbMATHGoogle Scholar
  17. 17.
    Udding, J.: Classification and Composition of Delay-Insensitive Circuits. PhD thesis, Department of Math. and C.S., Eindhoven University of Technology, Eindhoven (1984)Google Scholar
  18. 18.
    Van Berkel, K.: Handshake Circuits: an Asynchronous Architecture for VLSI Design. Cambridge International Series on Parallel Computation, vol. 5. Cambridge University Press, Cambridge (1993)zbMATHGoogle Scholar
  19. 19.
    Yoshida, N., Honda, K., Berger, M.: Linearity and bisimulation. In: Nielsen, M., Engberg, U. (eds.) FOSSACS 2002. LNCS, vol. 2303, pp. 417–433. Springer, Heidelberg (2002)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2009

Authors and Affiliations

  • Luca Fossati
    • 1
    • 2
  • Daniele Varacca
    • 2
  1. 1.Dip. di InformaticaUniversità di TorinoItalia
  2. 2.PPS - CNRS & Univ. Paris DiderotFrance

Personalised recommendations