Abstract
This paper studies parallel recursions. The trace specification language used in this paper incorporates sequentiality, nondeterminism, reactiveness (including infinite traces), conjunctive parallelism and general recursion. The language is the minimum of its kind and thus provides a context in which we can study parallel recursions in general. In order to use Tarski’s theorem to determine the fixpoints of recursions, we need to identify a well-founded partial order. A theorem of this paper shows that no appropriate order exists. Tarski’s theorem alone is not enough to determine the fixpoints of parallel recursions. Instead of using Tarski’s theorem directly, we reason about the fixpoints of terminating and nonterminating behaviours separately. Such reasoning is supported by the laws of a new composition called partition. We propose a fixpoint technique called the partitioned fixpoint, which is the least fixpoint of the nonterminating behaviours after the terminating behaviours reach their greatest fixpoint. The surprising result is that although a recursion may not be monotonic with regard to the lexical order, it must have the partitioned fixpoint, which equals the least lexical-order fixpoint. Since the partitioned fixpoint is well defined in any complete lattice, the results are applicable to various semantic models. Major existing fixpoint techniques simply become special cases of the partitioned fixpoint. For example, an Egli-Milner-monotonic recursion has its least Egli-Milner fixpoint, which can be shown to be the same as the partitioned fixpoint. The new technique is more general than the least Egli-Milner fixpoint in that the partitioned fixpoint can be determined even when a recursion is not Egli-Milner monotonic. Examples of non-monotonic recursions with fair-interleaving parallelism are studied. Their partitioned fixpoints are shown to be consistent with our intuitions.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
R. J. R. Back and K. Sere. Stepwise refinement of action systems. In Mathematics of Program Construction, volume 375 of LNCS, pages 115–138. Springer-Verlag, 1989.
J. A. Bergstra and J.W. Klop. Algebra of communicating processes with abstraction. Theoretical Computer Science, 37(1):77–121, 1985.
M. M. Bonsangue and J. N. Kok. The weakest precondition calculus: Recursion and duality. Formal Aspects of Computing, 6(A):788–800, 1994.
S. Brookes. Full abstraction for a shared-variable parallel language. Information and Computation, 127(2):145–163, 1996.
Y. Chen. How to write a healthiness condition. In 2nd International Conference on Integrated Formal Methods, volume 1945 of LNCS, pages 299–317. Springer-Verlag, 2000.
Y. Chen. A fixpoint theorey for non-monotonic parallelism. Technical Report 38, Department of Maths & Computer Science, University of Leicester, 2001.
Y. Chen and J. W. Sanders. Logic of global synchrony. In 12th Internationa conference on Concurrency Theory, volume 2154 of LNCS, pages 487–501. Springer-Verlag, 2001.
J. Davies and S. Schneider. A brief history of timed CSP. Theoretical Computer Science, 138(2):243–271, 1995.
E. W. Dijkstra. Guarded commands, nondeterminacy and the formal derivation of programs. Communications of the ACM, 18(8):453–457, 1975.
E. W. Dijkstra and C. S. Scholten. Semantics of recursive procedures. EWD 859, 1983.
E. W. Dijkstra and A. J. M. von Gasteren. A simple fixed-point argument without the restriction to continuity. Acta Informatica, 23(1):1–7, 1986.
S. E. Dunne. Recasting Hoare and He’s relational theory of programs in the context of general correctness. Technical report, School of Computing and Mathematics University of Teesside, 2000.
S. Fortune and J. Wyllie. Parallelism in random access machines. In 10th Annual ACM Symposium on Theory of Computing, pages 114–118, 1978.
C. A.R. Hoare. Communicating Sequential Processes. Prentice Hall, 1985.
C.A.R. Hoare and J. He. Unifying Theories of Programming. Prentice Hall, 1998.
W. F. McColl. Scalability, portability and predictability: The BSP approach to parallel programming. Future Generation Computer Systems, 12:265–272, 1996.
C. C. Morgan and A. McIver. Unifying wp and wlp. Information Processing Letters, 59:159–163, 1996.
G. Nelson. A generalisation of Dijkstra’s calculus. ACM Transactions on Programming Languages and Systems, 11(4):517–561, 1989.
D.M.R. Park. On the semantics of fair parallelism. In Abstract Software Specification, volume 86 of LNCS, pages 504–526. Springer-Verlag, 1980.
G.D. Plotkin. Lecture notes on domain theory. The Pisa Notes, 1983.
A. Pnueli. The temporal semantics of concurrent programs. Theoretical Computer Science, 13:45–60, 1981.
A.W. Roscoe. The Theory and Practice of Concurrency. Prentice Hall, 1998.
A. Tarski. A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics, 5:285–309, 1955.
L. G. Valiant. A bridging model for parallel computation. Communications of the ACM, 33(8):103–111, 1990.
J. Woodcock and J. Davis. Using Z: specification, refinement, and proof. Prentice Hall, 1991.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Chen, Y. (2002). A Fixpoint Theory for Non-monotonic Parallelism. In: Bradfield, J. (eds) Computer Science Logic. CSL 2002. Lecture Notes in Computer Science, vol 2471. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45793-3_9
Download citation
DOI: https://doi.org/10.1007/3-540-45793-3_9
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-44240-0
Online ISBN: 978-3-540-45793-0
eBook Packages: Springer Book Archive