Abstract
We propose weakening the definition of progress to a branching-time operator, making it more amenable to compositional proof and simplifying the predicates needed to reason about highly asynchronous programs. The new progress operator (“achieves”) coincides with the “leads-to” operator on all “observable” progress properties (those where the target predicate is stable) and satisfies the same composition properties as leads-to, including the PSP theorem. The advantage of achievement lies in its compositionality: a program inherits all achievement properties of its “decoupled components”. (For example, a dataflow network inherits achievement properties from each of its processes.) The compositionality of achievement captures, in a UNITY-like logic, the well-known operational trick of reasoning about an asynchronous program by considering only certain well-behaved executions.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
K. M. Chandy and J. Misra. Parallel Program Design: A Foundation. Addison-Wesley, Reading, MA, 1988
E. Cohen. Modular Progress Proofs of Asynchronous Programs PhD. Thesis, University of Texas at Austin, 1993. Available from ftp://ftp.research.telcordia.com/pub/ernie/research/diss.ps.gz
Ernie Cohen. Separation and reduction. In Mathematics of Program Construction, 5th International Conference, Portugal, July 2000. Science of Computer Programming, pages 45–59. Springer-Verlag, 2000.
E. Cohen, L. Lamport. Reduction in TLA. In CONCUR98 Springer-Verlag, 1998.
E. Dijkstra and C. Scholten. Predicate transformers and Program Semantics Springer-Verlag.
K. P. Eswaran, J. N. Gray, R. A. Lorie, I. L. Traiger. The notions of consistency and predicate locks in a database system. CACM, 19 (11): 624–633, 1976.
R. Joshi. Immediacy: a technique for reasoning about asynchrony. PhD. Thesis, University of Texas at Austin, 1999.
G. Kahn. The semantics of a simple language for parallel programming. In Proceedings of IFIP Congress ‘74 North-Holland, 1974.
S. Katz, D. Peled. Verification of Distributed Programs using Representative Interleaving Sequences. Distributed Computing, 6:107–120, Springer-Verlag, 1992.
R. J. Lipton. Reduction: A Method of Proving Properties of Parallel Programs. CACM 18 (12): 717–721, 1975.
J. Misra. Loosely Coupled Programs. In Parallel Architectures and Languages Europe, pages 1–26, June 1991.
J. Misra. A discipline of multiprogramming — programming theory for distributed applications. Springer-Verlag, 2001.
J. Pachl. A simple proof of a completeness result for leads-to in the UNITY logic. IPL, January 1992.
J. R. Rao. Extensions of the UNITY Methodology, Compositionality, Fairness and Probability in Parallelism. Springer LNCS #908, 1995.
A. Valmari. Stubborn Sets for Reduced State Space Generation. 10th International Confeence on Application and Theory of petri Nets, Bonn (2) pp 1–22, 1989.
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer Science+Business Media New York
About this chapter
Cite this chapter
Cohen, E. (2003). Asynchronous progress. In: McIver, A., Morgan, C. (eds) Programming Methodology. Monographs in Computer Science. Springer, New York, NY. https://doi.org/10.1007/978-0-387-21798-7_3
Download citation
DOI: https://doi.org/10.1007/978-0-387-21798-7_3
Publisher Name: Springer, New York, NY
Print ISBN: 978-1-4419-2964-8
Online ISBN: 978-0-387-21798-7
eBook Packages: Springer Book Archive