More Web Proxy on the site http://driver.im/

Article

Free access

Predicate path expressions

Author:

Sten AndlerAuthors Info & Claims

POPL '79: Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages

Pages 226 - 236

https://doi.org/10.1145/567752.567774

Published: 01 January 1979 Publication History

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]

{Campbell and Habermann 74} Campbell, R. H. and Habermann, A. N. The Specification of Process Synchronization by Path Expressions. In Gelenbe and Kaiser, editors, Lecture Notes in Computer Science, Vol. 16: Operating Systems, pages 89-102. Springer Verlag, 1974.

Digital Library

[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]

{Courtois et al 71} Courtois, P. J., Heymans, F., and Parnas, D. L. Concurrent control with "readers" and "writers". Communications of the ACM 14(10):667-668, Oct. 1971.

Digital Library

[8]

{Dijkstra 76} Dijkstra, E. W. A Discipline of Programming. Prentice Hall, Englewoods Cliffs, New Jersey, 1976.

Digital Library

[9]

{Flon 77} Flon, L. On the Design and Verification of Operating Systems. PhD thesis, Department of Computer Science, Carnegie-Mellon University, Pittsburgh, PA, May 1977.

Digital Library

[10]

{Flon and Habermann 76} Flon, L. and Habermann, A. N. Toward the Construction of Verifiable Software Systems. Proceedings of the ACM Conference on Data: Abstraction, Definition and Structure, SIGPLAN Notices 11(Special issue):141-148, March 1976.

Digital Library

[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.

Digital Library

[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]

{Gerber 77} Gerber, A. J. Process Synchronization by Counter Variables. Operating Systems Review 11(4):6-17, Oct. 1977.

Digital Library

[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]

{Hoare 69} Hoare, C .A .R. An Axiomatic Basis for Computer Programming. Communications of the ACM 12(10):576-580,583, Oct. 1969.

Digital Library

[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.

Digital Library

Cited By

Xiong HDai QChang RQiu MWang RShen WZhou YChristakis MPradel M(2024)Atlas: Automating Cross-Language Fuzzing on Android Closed-Source LibrariesProceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis10.1145/3650212.3652133(350-362)Online publication date: 11-Sep-2024
https://dl.acm.org/doi/10.1145/3650212.3652133
Guo SGu YMa YZhang YWeng WLiu JDai WChen YSerra ESpezzano F(2024)Information Retrieval Optimization for Non-Exemplar Class Incremental LearningProceedings of the 33rd ACM International Conference on Information and Knowledge Management10.1145/3627673.3679631(717-726)Online publication date: 21-Oct-2024
https://dl.acm.org/doi/10.1145/3627673.3679631
Hogrefe JCruz EJaiswal CRiofrio J(2024)AITracker: A neural network designed for efficient and affordable eye tracking2024 IEEE 15th Annual Ubiquitous Computing, Electronics & Mobile Communication Conference (UEMCON)10.1109/UEMCON62879.2024.10754664(100-107)Online publication date: 17-Oct-2024
https://doi.org/10.1109/UEMCON62879.2024.10754664
Show More Cited By

Recommendations

Transition predicate abstraction and fair termination
POPL '05: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Predicate abstraction is the basis of many program verification tools. Until now, the only known way to overcome the inherent limitation of predicate abstraction to safety properties was to manually annotate the finite-state abstraction of a program. We ...
Transition predicate abstraction and fair termination
Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Predicate abstraction is the basis of many program verification tools. Until now, the only known way to overcome the inherent limitation of predicate abstraction to safety properties was to manually annotate the finite-state abstraction of a program. We ...
Ranked predicate abstraction for branching time: complete, incremental, and precise
ATVA'06: Proceedings of the 4th international conference on Automated Technology for Verification and Analysis

Predicate abstraction frameworks are a powerful means of combating the state explosion problem in model checking as they automatically synthesize abstract models that either verify compliance with a property, give rise to a genuine counter-example or ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

POPL '79: Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages

January 1979

290 pages

ISBN:9781450373579

DOI:10.1145/567752

Conference Chairs:
Alfred V. Aho
Bell Laboratories, Murray Hill, NJ
,
Stephen N. Zilles
IBM Research, San Jose, CA
,
Program Chair:
Barry K. Rosen
IBM Thomas J. Watson Research Center, Yorktown Heights, NY

Copyright © 1979 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 January 1979

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Acceptance Rates

POPL '79 Paper Acceptance Rate 27 of 146 submissions, 18%;

Overall Acceptance Rate 824 of 4,130 submissions, 20%

Upcoming Conference

POPL '25

Sponsor:
sigplan

The 52nd Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 19 - 25, 2025

Denver , CO , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

69
Total Citations
View Citations
1,142
Total Downloads

Downloads (Last 12 months)302
Downloads (Last 6 weeks)21

Reflects downloads up to 12 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Xiong HDai QChang RQiu MWang RShen WZhou YChristakis MPradel M(2024)Atlas: Automating Cross-Language Fuzzing on Android Closed-Source LibrariesProceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis10.1145/3650212.3652133(350-362)Online publication date: 11-Sep-2024
https://dl.acm.org/doi/10.1145/3650212.3652133
Guo SGu YMa YZhang YWeng WLiu JDai WChen YSerra ESpezzano F(2024)Information Retrieval Optimization for Non-Exemplar Class Incremental LearningProceedings of the 33rd ACM International Conference on Information and Knowledge Management10.1145/3627673.3679631(717-726)Online publication date: 21-Oct-2024
https://dl.acm.org/doi/10.1145/3627673.3679631
Hogrefe JCruz EJaiswal CRiofrio J(2024)AITracker: A neural network designed for efficient and affordable eye tracking2024 IEEE 15th Annual Ubiquitous Computing, Electronics & Mobile Communication Conference (UEMCON)10.1109/UEMCON62879.2024.10754664(100-107)Online publication date: 17-Oct-2024
https://doi.org/10.1109/UEMCON62879.2024.10754664
Samira Maliyeva S(2023)BIOMEDICAL SMART HOME SYSTEMSPIRETC-Proceeding of The International Research Education & Training Centre10.36962/PIRETC23022023-12523:02(125-133)Online publication date: 19-Apr-2023
https://doi.org/10.36962/PIRETC23022023-125
Lazaro JGarcia RLinsangan NPellegrino RAranda RBundoc GGranada N(2023)Electrooculography for control of Emoji board for Patients with Classical Locked-in Syndrome usingProceedings of the 2023 13th International Conference on Biomedical Engineering and Technology10.1145/3620679.3620698(116-123)Online publication date: 15-Jun-2023
https://dl.acm.org/doi/10.1145/3620679.3620698
Chen QZhang TNie MWang ZXu SShi WCao ZWang ZLong CXu SGan BShi WCao ZChua T(2023)Fashion-GPT: Integrating LLMs with Fashion Retrieval SystemProceedings of the 1st Workshop on Large Generative Models Meet Multimodal Applications10.1145/3607827.3616844(69-78)Online publication date: 2-Nov-2023
https://dl.acm.org/doi/10.1145/3607827.3616844
Sadok HChaibi HSaadane R(2023)An exploratory study on the contribution of Artificial Intelligence in improving the bank credit analysis processProceedings of the 6th International Conference on Networking, Intelligent Systems & Security10.1145/3607720.3607784(1-4)Online publication date: 24-May-2023
https://dl.acm.org/doi/10.1145/3607720.3607784
Caballa SLizano DAranda MZegarra DCastellano GRiek LCakmak MLeite I(2023)RoPiCompanion of the 2023 ACM/IEEE International Conference on Human-Robot Interaction10.1145/3568294.3580198(845-848)Online publication date: 13-Mar-2023
https://dl.acm.org/doi/10.1145/3568294.3580198
Al-Karaki JOmar MGawanmeh AJones A(2023)Advancing CyberSecurity Education and Training: Practical Case Study of Running Capture the Flag (CTF) on the Metaverse vs. Physical Settings2023 International Conference on Intelligent Metaverse Technologies & Applications (iMETA)10.1109/iMETA59369.2023.10294722(1-7)Online publication date: 18-Sep-2023
https://doi.org/10.1109/iMETA59369.2023.10294722
Busheska ASabella NAlmeida NRocha E(2023)Machine Learning and Thermography Applied to the Detection and Classification of Cracks in Buildings2023 IEEE Conference on Technologies for Sustainability (SusTech)10.1109/SusTech57309.2023.10129614(247-251)Online publication date: 19-Apr-2023
https://doi.org/10.1109/SusTech57309.2023.10129614
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents