Skip to main content

Proving properties of PVM applications — A case study with CoCheck

  • Session F5: Extensions to PVM
  • Conference paper
  • First Online:
Parallel Virtual Machine — EuroPVM '96 (EuroPVM 1996)

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

Included in the following conference series:

Abstract

The results of a case study where we applied a formal method to prove properties of CoCheck, an extention of PVM for the creation of checkpoints of parallel applications on workstation clusters. Although the functionality of CoCheck had been demonstrated in experiments, there was no proof of the desired properties. Consequently, a formal method had to be applied which allows to prove those properties.

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

Access this chapter

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. T. E. Anderson, D. E. Culler, and D. A. Patterson. A case for NOW (networks of workstations). IEEE Micro, 15(1):54–64, February 1995.

    Google Scholar 

  2. R. M. Butler and E. L. Lusk. Monitors, messages and clusters: The p4 parallel programming system. Parallel Computing, 20(4):547–564, April 1994.

    Google Scholar 

  3. J. Casas, D. Clark, R. Konuru, S. Otto, R. Prouty, and J. Walpole. MPVM: A Migration Transparent Version of PVM. Technical Report, Dept. of Computer Science and Engineering, Oregon State Institute of Science and Technology, 20000 NW Walker Road, P.O.Box 91000, Portland, OR 97291-1000, 1994.

    Google Scholar 

  4. K. M. Chandy and L. Lamport. Distributed snapshots: Determining global states of distributed systems. ACM Transactions on Computer Systems, 3(1):63–75, February 1985.

    Google Scholar 

  5. L. Dikken. DynamicPVM: Task Migration in PVM. Technical Report, Shell Research, Amsterdam, November 1993.

    Google Scholar 

  6. A. Geist, A. Beguelin, J. Dongarra, W. Jiang, R. Manchek, and V. Sunderam. PVM: Parallel Virtual Machine — A Users' Guide and Tutorial for Networked Parallel Computing. Scientific and Engineering Computation. The MIT Press, Cambridge, MA, 1994.

    Google Scholar 

  7. W. Gropp, E. Lusk, and A. Skjellum. Using MPI — Portable Parallel Programming with the Message-Passing Interface. Scientific and Engineering Computation Series. The MIT Press, Cambridge, MA, 1994.

    Google Scholar 

  8. M. Litzkow, M. Livny, and M. Mutka. Condor — A Hunter of Idle Workstations. In Proceedings of the 8th International Conference on Distributed Systems, pages 104–111, Los Alamitos, CA, 1988. IEEE Computer Society Press.

    Google Scholar 

  9. Z. Manna and A. Pnueli. Completing the temporal picture. Theoretical Computer Science, 83:97–130, 1991.

    Google Scholar 

  10. Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer Verlag, 1991.

    Google Scholar 

  11. Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems: Safety. Springer Verlag, 1995.

    Google Scholar 

  12. R. Schwarz and F. Mattern. Detecting causal relationships in distributed computations: In search of the holy grail. SFB-Bericht, Institut für Informatik, Universität Kaiserslautern, Postfach 3049, D-6750 Kaiserslautern, December 1992.

    Google Scholar 

  13. G. Stellner. CoCheck: Checkpointing and Process Migration for MPI. In Proceedings of the IPPS'96, pages 526–531, Honolulu, HI, April 1996. IEEE Computer Society Press, Los Alamitos.

    Google Scholar 

  14. G. Stellner, A. Bode, S. Lamberts, and T. Ludwig. NXLib — A parallel programming environment for workstation clusters. In C. Halatsis, D. Maritsas, G. Philokyprou, and S. Theodoridis, editors, PARLE'94 Parallel Architectures and Languages Europe, volume 817 of Lecture Notes in Computer Science, pages 745–748, Berlin, July 1994. Springer Verlag.

    Google Scholar 

  15. G. Stellner and J. Pruyne. Resource Management and Checkpointing for PVM. In Proceedings of the 2nd European PVM Users' Group Meeting, pages 131–136, Lyon, September 1995. Editions Hermes.

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Arndt Bode Jack Dongarra Thomas Ludwig Vaidy Sunderam

Rights and permissions

Reprints and permissions

Copyright information

© 1996 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Menden, J., Stellner, G. (1996). Proving properties of PVM applications — A case study with CoCheck. In: Bode, A., Dongarra, J., Ludwig, T., Sunderam, V. (eds) Parallel Virtual Machine — EuroPVM '96. EuroPVM 1996. Lecture Notes in Computer Science, vol 1156. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3540617795_17

Download citation

  • DOI: https://doi.org/10.1007/3540617795_17

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-61779-2

  • Online ISBN: 978-3-540-70741-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics