Article

Free access

What it means for a concurrent program to satisfy a specification: why no one has specified priority

Author:

Leslie LamportAuthors Info & Claims

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

Pages 78 - 83

https://doi.org/10.1145/318593.318616

Published: 01 January 1985 Publication History

Abstract

The formal correspondence between an implementation and its specification is examined. It is shown that existing specifications that claim to describe priority are either vacuous or else too restrictive to be implemented in some reasonable situations. This is illustrated with a precisely formulated problem of specifying a first-come-first-served mutual exclusion algorithm, which it is claimed cannot be solved by existing methods.

References

[1]

{1} John Bethel, ed. Webster's New Collegiate Dictionary. G. & C. Meriam Co., Springfield, Mass. (1956).

[2]

{2} P. J. Courtois, F. Heymans and D. L. Parnas. Concurrent Control with "Readers" and "Writers". Comm. ACM 14, 10 (October 1971), 667-668.

Digital Library

[3]

{3} E. W. Dijkstra. Solution of a Problem in Concurrent Programming Control. Comm. ACM 17, 11 (November 1974), 643-644.

Digital Library

[4]

{4} Susan Gerhart et al. An Overview of AFFIRM: A Specification and Verification System, IFIP Congress 80, (Oct. 1980).

[5]

{5} Irene Greif. A Language for Formal Problem Specification, Comm. ACM 20, 12 (Dec. 1977), 931-935.

Digital Library

[6]

{6} J. V. Guttag and J. J. Horning. Formal Specification as a Design Tool. Proc. ACM Symposium on Principles of Programming Languages, Las Vegas, (January 1980), 251-261.

Digital Library

[7]

{7} J. V. Guttag and J. J. Horning. An Introduction to the Larch Shared Language. Proc. IFIP Congress '83, Paris, (1983).

[8]

{8} Brent Hailpern. Verifying Concurrent Processes Using Temporal Logic, Lecture Notes in Computer Science 129, Springer-Verlag (1982).

Digital Library

[9]

{9} Howard Katseff. A Solution to the Critical Section Problem with a Totally Wait-free FIFO Doorway. Technical Memorandum, Computer Science Division, University of California, Berkeley.

[10]

{10} Leslie Lamport. A New Solution of Dijkstra's Concurrent Programming Problem, Comm. ACM 17, 8 (Aug. 1974), 453-455.

Digital Library

[11]

{11} Leslie Lamport. Specifying Concurrent Program Modules, ACM Trans. on Prog. Lang. and Systems 5, 2 (Apr. 1983), 190-222.

Digital Library

[12]

{12} Leslie Lamport. What Good is Temporal Logic? Information Processing 83, R. E. Mason (ed.), Elsevier Science Publishers (North-Holland), 1983, 657-668.

[13]

{13} Amy Lansky and Susan S. Owicki. GEM: A Tool for Concurrency Specification and Verification, Proc. of the Second Annual ACM Symposium on Principles of Dietributed Computing (Aug. 1983), 198-212.

Digital Library

[14]

{14} Peter E. Lauer, P. Torrigiani and M. Shields. COSY: A System Specification Language Based on Paths and Processes, Acta Informatica 12 (1979), 109-158.

Digital Library

[15]

{15} Robin Milner. A Calculus of Communicating Systems , Lecture Notes in Computer Science 92, Springer-Verlag (1980).

Digital Library

[16]

{16} Richard L. Schwartz and P. M. Melliar-Smith. Temporal Logic Specification of Distributed Systems, Proc. of the IEEE Conjerence on Distributed Systems, (Apr. 1979).

[17]

{17} Richard L. Schwartz, P. M. Melliar-Smith and F. H. Vogt. An Interval Logic for Higher-Level Temporal Reasoning, Proc. of the Second Annual ACM Symposium on Principles of Distributed Computing (Aug. 1983), 198-212.

Digital Library

[18]

{18} Pierre Wolper. Specification and Synthesis of Communicating Processes Using an Extended Temporal Logic, Proc. of the Conference on the Principles of Programming Languages, Albuquerque (Jan. 1982).

Digital Library

Cited By

Jiang KChait-Roth DDeStefano ZWalfish MWies T(2023)Less is more: refinement proofs for probabilistic proofs2023 IEEE Symposium on Security and Privacy (SP)10.1109/SP46215.2023.10179393(1112-1129)Online publication date: May-2023
https://doi.org/10.1109/SP46215.2023.10179393
Moses YPatkin K(2015)Under the Hood of the Bakery AlgorithmPost-Proceedings of the 22nd International Colloquium on Structural Information and Communication Complexity - Volume 943910.1007/978-3-319-25258-2_28(399-413)Online publication date: 14-Jul-2015
https://dl.acm.org/doi/10.1007/978-3-319-25258-2_28
Janicki R(2008)Relational structures model of concurrencyActa Informatica10.1007/s00236-008-0071-645:4(279-320)Online publication date: 14-May-2008
https://dl.acm.org/doi/10.1007/s00236-008-0071-6
Show More Cited By

Index Terms

What it means for a concurrent program to satisfy a specification: why no one has specified priority
1. Computing methodologies
  1. Concurrent computing methodologies
    1. Concurrent programming languages
2. Software and its engineering
  1. Software creation and management
    1. Designing software
      1. Requirements analysis
  2. Software notations and tools
    1. General programming languages
      1. Language types
        Concurrent programming languages

Recommendations

Specification, Refinement and Verification of Concurrent Systems—An Integration of Object-Z and CSP

This paper presents a method of formally specifying, refining and verifying concurrent systems which uses the object-oriented state-based specification language Object-Z together with the process algebra CSP. Object-Z provides a convenient way of ...
The state-based CCS semantics for concurrent Z specification
ICFEM '97: Proceedings of the 1st International Conference on Formal Engineering Methods

Presents a formal method which combines the Z notation and value-passing CCS (Calculus of Communicating Systems) for specifying concurrent systems. In order to provide a sound theoretical basis for the method, the state-based semantics for value-passing ...
Equational specification and verification of concurrent systems

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

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

January 1985

340 pages

ISBN:0897911474

DOI:10.1145/318593

Chairmen:
Mary S. Van Deusen
IBM Watson Research
,
Zvi Galil
Columbia University, New York, NY
,
Brian K. Reid
Stanford Univ., Stanford, CA

Copyright © 1985 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 1985

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Acceptance Rates

Overall Acceptance Rate 860 of 4,328 submissions, 20%

Upcoming Conference

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

22
Total Citations
View Citations
421
Total Downloads

Downloads (Last 12 months)59
Downloads (Last 6 weeks)8

Reflects downloads up to 06 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Jiang KChait-Roth DDeStefano ZWalfish MWies T(2023)Less is more: refinement proofs for probabilistic proofs2023 IEEE Symposium on Security and Privacy (SP)10.1109/SP46215.2023.10179393(1112-1129)Online publication date: May-2023
https://doi.org/10.1109/SP46215.2023.10179393
Moses YPatkin K(2015)Under the Hood of the Bakery AlgorithmPost-Proceedings of the 22nd International Colloquium on Structural Information and Communication Complexity - Volume 943910.1007/978-3-319-25258-2_28(399-413)Online publication date: 14-Jul-2015
https://dl.acm.org/doi/10.1007/978-3-319-25258-2_28
Janicki R(2008)Relational structures model of concurrencyActa Informatica10.1007/s00236-008-0071-645:4(279-320)Online publication date: 14-May-2008
https://dl.acm.org/doi/10.1007/s00236-008-0071-6
Janicki RKoutny M(2005)Deriving histories of nets with priority relationPARLE'94 Parallel Architectures and Languages Europe10.1007/3-540-58184-7_136(623-634)Online publication date: 2-Jun-2005
https://doi.org/10.1007/3-540-58184-7_136
Koutny M(2005)Modelling systems with dynamic prioritiesAdvances in Petri Nets 199210.1007/3-540-55610-9_174(251-266)Online publication date: 13-Jun-2005
https://doi.org/10.1007/3-540-55610-9_174
Janicki RKoutny M(2005)Invariant semantics of nets with inhibitor arcsCONCUR '9110.1007/3-540-54430-5_97(317-331)Online publication date: 4-Jun-2005
https://doi.org/10.1007/3-540-54430-5_97
Janicki RKoutny M(2005)Invariants and paradigms of concurrency theoryPARLE '91 Parallel Architectures and Languages Europe10.1007/3-540-54152-7_58(59-74)Online publication date: 8-Jun-2005
https://doi.org/10.1007/3-540-54152-7_58
Lam SShankar A(2005)Refinement and projection of relational specificationsStepwise Refinement of Distributed Systems Models, Formalisms, Correctness10.1007/3-540-52559-9_75(454-486)Online publication date: 4-Jun-2005
https://doi.org/10.1007/3-540-52559-9_75
Katz SPeled D(2005)Interleaving set temporal logicTemporal Logic in Specification10.1007/3-540-51803-7_20(21-43)Online publication date: 25-May-2005
https://doi.org/10.1007/3-540-51803-7_20
Li DMaibaum T(2005)A top-down step-wise refinement methodology for protocol specificationCONCURRENCY 8810.1007/3-540-50403-6_41(197-221)Online publication date: 1-Jun-2005
https://doi.org/10.1007/3-540-50403-6_41
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

Figures

Tables

Media

View Table of Conten