Predicate path expressions

ABSTRACT

Path expressions are a tool for synchronization of concurrent processes. They are an integral part of the data abstraction mechanism in a programming language, and specify synchronization entirely in terms of the allowable sequences of operations on an object of the abstract data type. This paper describes an attempt to push the path expression synchronization construct along three dimensions - specification, verification, and implementation - into a useful theoretical and practical tool. We define Predicate Path Expressions (PPEs), which allow for a more convenient specification of many synchronization problems. The predicate is a powerful extension to path expressions that increases their expressiveness. We formally define the semantics of PPEs by a transformation to a corresponding nondeterministic program, thus allowing the use of known verification techniques for nondeterministic programs to be used for proving properties of the PPE and the data abstraction of which it is a part. We also describe our existing implementation, in Algol 68, of a data abstraction mechanism that incorporates PPEs.

REFERENCES

• 1: {Andler 78} Andler, S. Synchronization Primitives and the Verification of Concurrent Programs. In Proceedings of the Second International Symposium on Operating Systems. IRIA, Le Chesnay, France, Oct. 1978.
• 2: {Andler and Hibbard 77} Andler, S., and Hibbard, P. G. Types in Algol 68. In Proceedings of the Fifth Annual III Conference on the Implementation and Design of Algorithmic Languages, pages 124-144. IRIA, Le Chesnay, France, May 1977.
• 3: {Andler et al 78} Andler, S., Feiler, P., Habermann, A. N., Prasad, V. R., and Tichy, W. Letter to the Editor. Operating Systems Review 12(1):6-11, Jan. 1978.
• 4: {Berzins 77} Berzins, V. Denotational and Axiomatic Definitions for Path Expressions. Computation Structures Group Memo 153-1, Laboratory for Computer Science, M.I.T., Cambridge, Mass., Nov. 1977.
• 5: Roy H. Campbell , A. Nico Habermann, The specification of process synchronization by path expressions, Operating Systems, Proceedings of an International Symposium, p.89-102, April 23-25, 1974
• 6: {Campbell and Miller 78} Campbell, R. H., and Miller, T. J. A Path Pascal Language. Draft, Department of Computer Science, University of Illinois at Champaign-Urbana, Urbana, Illinois, April 1978.
• 7: P. J. Courtois , F. Heymans , D. L. Parnas, Concurrent control with “readers” and “writers”, Communications of the ACM, v.14 n.10, p.667-668, Oct. 1971 [doi>10.1145/362759.362813]
• 8: Edsger Wybe Dijkstra, A Discipline of Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1997
• 9: Lawrence Flon, On the design and verification of operating systems., 1977
• 10: L. Flon , A. N. Habermann, Towards the construction of verifiable software systems, Proceedings of the 1976 conference on Data : Abstraction, definition and structure, p.141-148, March 22-24, 1976, Salt Lake City, Utah, United States
• 11: {Flon and Suzuki 78} Flon, L. and Suzuki, N. Consistent and Complete Proof Rules for the Total Correctness of Parallel Programs. In Proceedings of the Nineteenth Annual IEEE Conference on the Foundations of Computer Science. Ann Arbor, Michigan, Oct. 1978.
• 12: {Floyd 67} Floyd, R. W. Assigning Meanings to Programs. In J. T. Schwartz, editor, Mathematical Aspects of Computer Science, Vol. 19, pages 19-32. American Mathematical Society, Providence, R.I., 1967.
• 13: A. J. Gerber, Process synchronization by counter variables, ACM SIGOPS Operating Systems Review, v.11 n.4, p.6-17, October 1977 [doi>10.1145/850648.850649]
• 14: {Gerber 78} Gerber, A. J. Letter to the Editor. Operating Systems Review 12(3):5-10, July 1978.
• 15: {Habermann 73} Habermann, A. N. Operations on shared data controlled by function modules in type definitions. Department of Computer Science, Carnegie-Mellon University, Pittsburgh, PA, Sept. 1973.
• 16: {Habermann 75} Habermann, A. N. Path Expressions. Technical Report, Department of Computer Science, Carnegie-Mellon University, Pittsburgh, PA, June 1975.
• 17: {Habermann et al 78} Habermann, A. N., Flon, L., Cooprider, L., Feiler, P., Guarino, L., and Schwanke, R. S. Modularization and Hierarchy in a Family of Operating Systems. Technical Report CMU-CS-78-101, Department of Computer Science, Carnegie-Mellon University, Pittsburgh, PA, Feb. 1978.
• 18: {Hibbard et al 76} Hibbard, P. G., Knueven, P. and Leverett, B. W. A Stackless Run-time Implementation Scheme. In Proceedings of the International Conference on Algorithmic Languages, pages 176-192. Courant Institute, New York, 1976.
• 19: C. A. R. Hoare, An axiomatic basis for computer programming, Communications of the ACM, v.12 n.10, p.576-580, Oct. 1969 [doi>10.1145/363235.363259]
• 20: {Lauer and Campbell 74} Lauer, P. E., and Campbell, R. H. A Description of Path Expressions by Petri Nets. Technical Report, Computing Laboratory, University of Newcastle Upon Tyne, Newcastle Upon Tyne, Great Britain, May 1974.
• 21: {Robert and Verjus 77} Robert, P., and Verjus, J.-P. Toward Autonomous Descriptions of Synchronization Modules. In B. Gilchrist, editor, Information Processing 77, IFIP, pages 981-986. North-Holland Publ. Co., 1977.
• 22: {Schmid 76} Schmid, H. A. On the Efficient Implementation of Conditional Critical Regions and the Construction of Monitors. Acta Informatica 6:227-249, 1976.