Advertisement

Region Analysis and a π-Calculus with Groups

  • Silvano Dal Zilio
  • Andrew D. Gordon
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1893)

Abstract

We show that the typed region calculus of Tofte and Talpin can be encoded in a typed π-calculus equipped with name groups and a novel effect analysis. In the region calculus, each boxed value has a statically determined region in which it is stored. Regions are allocated and de-allocated according to a stack discipline, thus improving memory management. The idea of name groups arose in the typed ambient calculus of Cardelli, Ghelli, and Gordon. There, and in our π-calculus, each name has a statically determined group to which it belongs. Groups allow for type-checking of certain mobility properties, as well as effect analyses. Our encoding makes precise the intuitive correspondence between regions and groups. We propose a new formulation of the type preservation property of the region calculus, which avoids Tofte and Talpin’s rather elaborate co-inductive formulation. We prove the encoding preserves the static and dynamic semantics of the region calculus. Our proof of the correctness of region de-allocation shows it to be a specific instance of a general garbage collection principle for the π-calculus with effects.

Keywords

Live Region Region Analysis Input Process Static Semantic Type Annotation 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    M. Abadi and A. D. Gordon. A calculus for cryptographic protocols: The spi calculus. Information and Computation, 148:1–70, 1999. An extended version appears as Research Report 149, Digital Equipment Corporation Systems Research Center, January 1998.Google Scholar
  2. 2.
    A. Aiken, M. Fähndrich, and R. Levien. Better static memory management: Improving region-based analysis of higher-order languages. In Proceedings PLDI’95, pages 174–185, 1995.Google Scholar
  3. 3.
    A. Banerjee, N. Heintze, and J. Riecke. Region analysis and the polymorphic lambda calculus. In Proceedings LICS’99, 1999.Google Scholar
  4. 4.
    L. Birkedal, M. Tofte, and M. Vejlstrup. From region inference to von Neumann machines via region representation inference. In Proceedings POPL’96, pages 171–183. 1996.Google Scholar
  5. 5.
    L. Cardelli, G. Ghelli, and A. D. Gordon. Ambient groups and mobility types. In Proceedings TCS2000, Lecture Notes in Computer Science. Springer, 2000. To appear.Google Scholar
  6. 6.
    L. Cardelli, G. Ghelli, and A. D. Gordon. Group creation and secrecy. In Proceedings Concur’00, Lecture Notes in Computer Science. Springer, 2000. To appear.Google Scholar
  7. 7.
    K. Crary, D. Walker, and G. Morrisett. Typed memory management in a calculus of capabilities. In Proceedings POPL’99, pages 262–275, 1999.Google Scholar
  8. 8.
    S. Dal Zilio and A. D. Gordon. Region analysis and a π-calculus with groups. Technical Report MSR-TR-2000-57, Microsoft Research, 2000.Google Scholar
  9. 9.
    C. Fournet and G. Gonthier. The reflexive CHAM and the Join-calculus. In Proceedings POPL’96, pages 372–385, 1996.Google Scholar
  10. 10.
    D. K. Gifford and J. M. Lucassen. Integrating functional and imperative programming. In Proceedings L &FP’86, pages 28–38, 1986.Google Scholar
  11. 11.
    J. Hughes and L. Pareto. Recursion and dynamic data-structures in bounded space: Towards embedded ML programming. In Proceedings ICFP’99, pages 70–81, 1999.Google Scholar
  12. 12.
    J. Launchbury and S. Peyton Jones. State in Haskell. Lisp and Symbolic Computation, 8(4):293–341, 1995.CrossRefGoogle Scholar
  13. 13.
    X. Leroy. A syntactic theory of type generativity and sharing. Journal of Functional Programming, 6(5):667–698, 1996.zbMATHMathSciNetGoogle Scholar
  14. 14.
    M. Merro and D. Sangiorgi. On asynchrony in name-passing calculi. In Proceedings ICALP’98, volume 1443 of Lecture Notes in Computer Science, pages 856–867. Springer, 1998.Google Scholar
  15. 15.
    R. Milner. Communicating and Mobile Systems: the π-Calculus. Cambridge University Press, 1999.Google Scholar
  16. 16.
    R. Milner and D. Sangiorgi. Barbed bisimulation. In Proceedings ICALP’92, volume 623 of Lecture Notes in Computer Science, pages 685–695. Springer, 1992.Google Scholar
  17. 17.
    R. Milner, M. Tofte, R. Harper, and D. MacQueen. The Definition of Standard ML (Revised). MIT Press, 1997.Google Scholar
  18. 18.
    E. Moggi and F. Palumbo. Monadic encapsulation of effects: a revised approach. In Proceedings HOOTS99, volume 26 of Electronic Notes in Theoretical Computer Science, pages 119–136. Elsevier, 1999.Google Scholar
  19. 19.
    B. Pierce and D. Sangiorgi. Typing and subtyping for mobile processes. Mathematical Structures in Computer Science, 6(5):409–454, 1996.zbMATHMathSciNetGoogle Scholar
  20. 20.
    B. C. Pierce and D. N. Turner. Pict: A programming language based on the pi-calculus. Technical Report CSCI 476, Computer Science Department, Indiana University, 1997. To appear in Proof, Language and Interaction: Essays in Honour of Robin Milner, G. Plotkin, C. Stirling, and M. Tofte, editors, MIT Press, 2000.Google Scholar
  21. 21.
    C. V. Russo. Standard ML type generativity as existential quantification. Technical Report ECS-LFCS-96-344, LFCS, University of Edinburgh, 1996.Google Scholar
  22. 22.
    D. Sangiorgi. Interpreting functions as π-calculus processes: a tutorial. Technical Report 3470, INRIA, 1998. Draft chapter to appear in The pi-calculus: a theory of mobile processes, D. Sangiorgi and W. Walker, Cambridge University Press, 2000.Google Scholar
  23. 23.
    M. Semmelroth and A. Sabry. Monadic encapsulation in ML. In Proceedings ICFP’99, pages 8–17, 1999.Google Scholar
  24. 24.
    J.-P. Talpin and P. Jouvelot. Polymorphic type, region and effect inference. Journal of Functional Programming, 2(3):245–271, 1992.zbMATHMathSciNetCrossRefGoogle Scholar
  25. 25.
    C. J. Taylor. Formalising and Reasoning about Fudgets. PhD thesis, University of Nottingham, 1998. Available as Technical Report NOTTCS-TR-98-4.Google Scholar
  26. 26.
    M. Tofte and J.-P. Talpin. Region-based memory management. Information and Computation, 132(2):109–176, 1997.zbMATHCrossRefMathSciNetGoogle Scholar
  27. 27.
    P. Wadler. The marriage of effects and monads. In Proceedings ICFP’98, pages 63–74, 1998.Google Scholar
  28. 28.
    D. Walker. Objects in the pi-calculus. Information and Computation, 116(2):253–271, 1995.zbMATHCrossRefMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2000

Authors and Affiliations

  • Silvano Dal Zilio
    • 1
  • Andrew D. Gordon
    • 1
  1. 1.Microsoft ResearchUSA

Personalised recommendations