From a specification to an equivalence proof in object-oriented parallelism | SpringerLink
Skip to main content
Springer Nature Link
Log in

From a specification to an equivalence proof in object-oriented parallelism

  • Conference paper
  • First Online:
Parallel and Distributed Processing (IPPS 1999)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1586))

Included in the following conference series:

Abstract

We investigate the use of a TLA specification for modeling and proving parallelization within an object-oriented language.

Our model is based on Eiffel// a parallel extension of Eiffel, where sequential programs can be reused for parallel or concurrent programming with very minor changes. We want to prove that both versions of a given program (sequential and parallel) are equivalent with respect to some properties.

This article presents a description in TLA+ that captures the general Eiffel// execution model, and, as a case-study, specifies a program (a binary search tree) in both its sequential and parallel form. We then prove a property that demonstrates a behavioral equivalence for the two versions.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. R. Amadio, I. Castellani, and D. Sangiorgi. On bisimulations for the asynchronous π-calculus. In Proc. CONCUR’96, volume 1119. LNCS, Springer-Verlag, 1996.

    Google Scholar 

  2. I. Attali, D. Caromel, S. Ehmety, and S. Lippi. Semantic-based visualization for parallel object-oriented programming. In Proceedings of OOPSLA’96, volume 31 of ACM Sigplan Notices, San Jose, CA, October 1996. ACM Press.

    Google Scholar 

  3. E. Bruneton. Implantation d’un traducteur eiffel//—π-calcul. Rapport de stage deuxième année, Ecole Polytechnique, juillet 1996.

    Google Scholar 

  4. Concurrent Object-Oriented Programming. Communications of the ACM, 36 (9), 1993. Special issue.

    Google Scholar 

  5. D. Caromel. Service, Asynchrony and Wait-by-necessity. Journal of Object-Oriented Programming, 2(4):12–22, November 1989.

    Google Scholar 

  6. D. Caromel. Concurrency and Reusability: From Sequential to Parallel. Journal of Object-Oriented Programming, 3(3):34–42, September 1990.

    Google Scholar 

  7. D. Caromel. Towards a Method of Object-Oriented Concurrent Programming. Communications of the ACM, 36(9):90–102, September 1993.

    Article  Google Scholar 

  8. Denis Caromel, Fabrice Belloncle, and Yves Roudier. The C++//Language. MIT Press, 1996. ISBN 0-262-73118-5.

    Google Scholar 

  9. D. Doligez. Conception, réalisation et certification d’un glaneur de cellules concurrent. PhD thesis, Université Paris VII, 1995.

    Google Scholar 

  10. Urban Engberg. The tlp system. http://www.daimi.aau.dk/~urban/tlp/tlp.html.

    Google Scholar 

  11. G. Gontheir. Verifying the safety of a practical concurrent garbage collector. In Proc. of the Eighth International Conference on Computer-Aided Verification, ACM, New Brunswick, New Jersey, 1996.

    Google Scholar 

  12. S. Hodges and C. B. Jones. Non-interferance properties of a concurrent object-based language: Proofs based on an operational semantics. In Object Orientation with Parallelism and Persistance. Kluwer Academic Publishers, 1996. ISBN 0-7923-9770-3.

    Google Scholar 

  13. L. Lamport. Hybrid systems in tla+. In Hybrid Systems, pages 77–102. Springer Verlag LNCS 736, 1993.

    Google Scholar 

  14. L. Lamport. The Temporal Logic of Actions. ACM Transactions on Programming Languages and Systems, 16(3):872–923, May 1994.

    Article  Google Scholar 

  15. L. Lamport. The Module Structure of TLA+. Technical Report 1996-002, DEC SRC, September 1996.

    Google Scholar 

  16. L. Lamport. The operators of TLA+. Technical Report 1997-006a, DEC SRC, April 1997.

    Google Scholar 

  17. L. Lamport and S. Merz. Specifying and verifying fault-tolerant systems. In H. Langmaack, W. P. de Roever, and J. Vytopil, editors, Formal Techniques in real-time and fault-tolerant systems, volume 863 of Lecture Notes in Computer Science, pages 41–76. Springer-Verlag, 1994.

    Google Scholar 

  18. X. Liu and D. Walker. Confluence of processes and systems of objects. In Proc. of Theory and Practice of Software Development (TAPSOFT’95) 6th International Joint Conference CAAP/FASE, 1995.

    Google Scholar 

  19. B. Mayer. Object-Oriented Software Construction. Prentice-Hall, 1988.

    Google Scholar 

  20. R. Milner, J. Parrow, and D. Walker. A Calculus of Mobile Processes, i and ii. Journal of Information and Computation, 100:1–77, 1992.

    Article  MATH  MathSciNet  Google Scholar 

  21. O. Nierstrasz. The next 700 concurrent object-oriented languages—reflections on the future of object-based concurrency. Object composition, Centre Universitaire d’Informatique, University of Geneva, June 1991.

    Google Scholar 

  22. O. Nierstrasz, P. Ciancarini, and A. Yonezawa, editors. Rule-based Object Coordination. LNCS 924. Springer-Verlag, 1995.

    Google Scholar 

  23. David Sagnol. π-calcul pour les langages à objects parallèles. Rapport de stage de DEA, Université de Nice-Sophia Antipolis, Juin 1995.

    Google Scholar 

  24. P. Wegner. Design issues for object-based concurrency. In Proc. of the ECOOP ’91 Workshop on Object-Based Concurrent Computing, LNCS 612, 1992.

    Google Scholar 

  25. G. Wilson and P. Lu, editors. Parallel Programing Using C++. MIT Press, 1996. ISBN 0-262-73118-5.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. INRIA Sophia Antipolis, CNRS-I3S-Univ. Nice Sophia Antipolis, BP 93, 06902, Sophia Antipolis Cedex, France

    Isabelle Attali, Denis Caromel & Sylvain Lippi

Authors
  1. Isabelle Attali
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Denis Caromel
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Sylvain Lippi
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

José Rolim Frank Mueller Albert Y. Zomaya Fikret Ercal Stephan Olariu Binoy Ravindran Jan Gustafsson Hiroaki Takada Ron Olsson Laxmikant V. Kale Pete Beckman Matthew Haines Hossam ElGindy Denis Caromel Serge Chaumette Geoffrey Fox Yi Pan Keqin Li Tao Yang G. Chiola G. Conte L. V. Mancini Domenique Méry Beverly Sanders Devesh Bhatt Viktor Prasanna

Rights and permissions

Reprints and permissions

Copyright information

© 1999 Springer-Verlag

About this paper

Cite this paper

Attali, I., Caromel, D., Lippi, S. (1999). From a specification to an equivalence proof in object-oriented parallelism. In: Rolim, J., et al. Parallel and Distributed Processing. IPPS 1999. Lecture Notes in Computer Science, vol 1586. Springer, Berlin, Heidelberg . https://doi.org/10.1007/BFb0098003

Download citation

  • DOI: https://doi.org/10.1007/BFb0098003

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-65831-3

  • Online ISBN: 978-3-540-48932-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation