Abstract
In a distributed system where many processors are connected by a network and communicate using message passing, many users can be allowed to access to the same facilities. A public utility is usually an expensive or limited resource whose use has to be regulated. Guardians are abstractions that can be used to regulate the use of resources by scheduling their access, providing protection, and implementing recovery from hardware failures. We present a language construct called a primitive serializer which can be used to express efficient implementations of guardians in a modular fashion. We have developed a proof methodology for proving strong properties of network utilities e.g. the utility is guaranteed to respond to each request which it is sent. This proof methodology is illustrated by proving properties of a hardcopy guardian which manages two printing devices.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
XII — Bibliography
Atkinson, R. and Hewitt, C. "Specification and Proof Techniques for Serializers" IEEE Transactions on Software Engineering SE-5. No. 1. January 1979. pp 10–23.
Birtwistle, G. M.; Dahl, O.; Myhrhaug, B.; and Nygaard, K. "SIMULA Begin" Auerbach. 1973.
Borning, A. H. "THINGLAB — A Constraint-Oriented Simulation Laboratory", Stanford PhD thesis, March 1979. Revised version to appear as Xerox PARC SSL-79-3.
Brinch Hansen, P. "The Programming Language Concurrent Pascal" IEEE Transactions on Software Engineering. June, 1975. pp 199–207.
Clark, D. G.; Greif, I.; Liskov, B.; and Svobodova, L. "Progress Report of the Distributed Systems Group 1977–1978" MIT Computation Structures Group Memo. October 1978.
Dijkstra, E. W. "Guarded Commands, Nondeterminancy, and Formal Derivation of Programs" CACM. Vol. 18. No. 8. August 1975. pp 453–457.
Friedman and Wise. "A Note on Conditional Expressions" CACM. Vol 21. No. 11. November 1978. pp 931–933.
Gjessing, S. "Compile Time Preparations for Run Time Scheduling in Monitors" Research Report No. 17, Institute of Informatics, University of Oslo, June 1977.
Hewitt, C. and Baker, H. "Laws for Communicating Parallel Processes" MIT Artificial Intelligence Working Paper 134. December 1976. Invited paper at IFIP-77.
Hewitt, C. "Evolving Parallel Programs" MIT AI Lab Working Paper 164. December 1978. Revised January 1979.
Hewitt, C. "Concurrent Systems Need Both Sequences and Serializers" MIT AI Lab Working Paper 179. December 1978. Revised February 1979.
Hewitt, C.; Attardi, G.; and Lieberman, H. "Security and Modularity in Message Passing" MIT AI Lab Working Paper 180. December 1978. Revised February 1979.
Hoaie, C. A. R. "Monitors: An Operating System Structuring Concept" CACM. October 1974.
Hoare, C. A. R. "Language Hierarchies and Interfaces" Lecture Notes in Computer Science No. 46. Springer, 1976. pp 242–265.
Hoare, C.A.R. "Communicating Sequential Processes" CACM, Vol 21, No. 8. August 1978. pp. 666–677.
Kay, A. Private communication. November 1972.
Manna, Z. and McCarthy, J. "Properties of Programs and Partial Function Logic" Machine Intelligence 5 B. Meltzer and D. Michie, editors. Edinburgh Univ. Press. 1970. pp 27–37.
Owicki, S. "Verifying concurrent Programs With Shared Data Classes" Formal Description of Programming Concepts edited by E. J. Neuhold. North Holland. 1978.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1979 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hewitt, C., Attardi, G., Lieberman, H. (1979). Specifying and proving properties of guardians for distributed systems. In: Kahn, G. (eds) Semantics of Concurrent Computation. Lecture Notes in Computer Science, vol 70. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0022477
Download citation
DOI: https://doi.org/10.1007/BFb0022477
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-09511-8
Online ISBN: 978-3-540-35163-4
eBook Packages: Springer Book Archive