Credo on concurrency

Uri Abraham



The state-based approach to concurrency is almost universally accepted. According to this view a state is an instantaneous global picture that gives the values of all variables, and a history of a system is described as a series of states, each resulting from the previous one by activating one of the agents (or processes). This interleaving of agents' actions obey transition rules which determine those states that can immediately follow a given state.

My work in computer science supports an alternative view, and the aim of this page is to describe it and to serve as a tour-guide for the interested reader. In this view there are no global states (but local states are used by the serial processes that compose the programs). System executions are used to specify the communication devices and to complete the semantics of the concurrent programs.

There are many competing approaches to concurrency and you surely ask what is the reason for adding another model? Unfortunately I have no short and easy answer, but I will try the following... A main advantage of the model theoretic non-interleaving approach is that a single framework can deal with several levels of granularity. At the higher-level of the proofs, the protocol is completely forgotten, and only abstract mathematical relations are investigated. The main motivation for my approach is the ``practical'' need of proving the correctness of rather difficult concurrent algorithms. I am convinced that no assertional method will work conveniently to prove difficult protocols such as the one for the N-writers atomic registers given in On interprocess communication and the implementation of multi-writer atomic registers. This work and paper have shaped my views on concurrency, so that it can serve as an introduction; it is self-contained. A more up-to-date exposition is Concurrency without global states: a case study. A very simple exposition of some ideas is in a short lecture Two approaches to concurrencty

In my monograph (Gordon and Breach, 1999) I explicate concurrency in model-theoretic terms, and apply the resulting theory to Producer/Consumer protocols. The monograph deals with the semantics of concurrency and some other theoretical issues.

I will try to write expository papers that are not as long as the monograph and give a reasonable idea on my approach. Unfortunately these papers are quite long, and necessarily they contain repetitions. Yet they contain additional material (not from the monograph) and especially they represent my actual view that set-theoretical history structures can be used. Concurrency without global states: a case study. I used here the notion of hereditarily finite sets over a collection of urelements in order to be able to use standard definitions used in mathematics (sequences, functions etc). Exercises in Style. With appologies to Queneau, this paper deals with the Alpha Architecture Reference Manual.


List of papers in Computer Science

    with S. Ben-David, unpublished. ( pdf.). In a sense, my work in concurrency is singly motivated by the desire to find a framework in which concurrent systems can be specified and proved correct at both the intuitive and formal levels. It is interesting to note that this aim was clearly formulated twenty years ago in an unpublished paper written with Shai en-David (Nov. 1987) which is posted here since it is so meaningful for me. In addition to ``philosophical'' discussion of the role of proofs in CS, we deal here with Lamport's system executions and show how the addition of two axioms lead to a characterization of system executions and their representation, thus giving a better explication of this concept. (Independently F. Anger obtaine and published similar results.) For a systematic study of concurrency the notion of time must be clarified. Identifying time with real numbers can be useful in many cases, but a different point of view is often more appropriate. For example retaining only the temporal precedence relation on events suffices for many applications and often leads to a clearer understanding of protocols. Chapter 2 of my monograph gives some basic results on interval orderings (due to Russell and Wiener) which explains our temporal framework. Deeper questions concerning global time were investigated with Menachem Magidor, Shai Ben-David and with Ben-David and Shlomo Moran. (The global time assumption is a natural assumption which should not be confused with the much stronger global clock assumption) These investigations can be found in the following two papers.

    with Shai Ben-David and Menachem Magidor,
    in M. Z. Kwiatkowska et al., eds., Proceedings of the International BCS-FACS Workshop on Semantics for Concurrency, (Leicester, 1990) 311--323 Workshops in Computing, a Springer Series edited by C. J. van Rijsbergen. (No electronic file available.)

    How should time be represented in models for inter-process communication? The global-time axiom implies that all events can be represented by intervals on one time-axis. Its use simplifies the analysis of protocols and allows for intuitive proofs of their properties. On the other hand some researchers believe it is too strong an assumption which should be avoided. We analyze the theory of interval partial orders and our final result is that in many cases the global time axiom can be safely used: It will not lead to any conclusions about the protocol that could not also be obtained without it.

    I may also point to the work of Ben-David concerning this question which can be found in: The global-time assumption and semantics for concurrent systems, 7th Annual ACM Symp. PODC 1988, 223--232.


    On the limitation of the Global-Time assumption in distributed systems (extended abstract)

    with Shai Ben-David and Shlomo Moran, in S. Toueg, P. G. Spirakis, and L. Kirousis (editors), Distributed Algorithms 5th International Workshop, WDAG '91, Lecture Notes in Computer Science 579, Springer-Verlag. ( compressed postscript, 8 pp).

    In this note we demonstrate a protocol that is guaranteed to perform well as long as it is run in a system that enjoys the existence of global time, yet it may fail in some other conceivable circumstances. The protocol is very simple and is often used as a basic step in protocols for mutual exclusion.


    I would like to mention my indebtedness to Leslie Lamport's paper ``On interprocess communication, parts I and II'' Dist. Comp. 1989. Not only that his notion of system execution is important in my view, but my approach has developed while trying to solve concrete ``mutual exclusion'' and ``atomic register'' questions with which he dealt. In this course I had to extend his system executions, and to view them in a general model theoretic setting. As far as I know, L. Lamport has changed his point of view and he believes that a precise and formal specification of concurrent algorithms requires the use of global states and histories rather than system-executions. The final result and my definition of system executions has appeared in the following two papers:

    J. of Applied Intelligence 3,17-30 (1993). ( compressed dvi) ( compressed ps). (The journal version contains an additional section ``An Example: Implementing a Buffer'', which you will not find here. Please ask me for a copy if you want to read it.)

    An approach for modeling dynamic situations where several processes execute concurrently is described in this paper. We address basic issues such as what is an `event'? What is a `state' of a system? How should time be represented? etc. In this, we use the concepts `system execution' and `pomset' defined by Lamport and Gischer, and we relate them to the `core' of Gaifman.
    The notion of a system execution is extended in such a way that a state is just a peculiar system execution, one in which no event precedes another---it is the description of a moment. This allows to demonstrate within a single framework the duality between two approaches to modeling concurrency: the one based on events and the other on states.

    I would like to thank Frank Anger for prompting me to publish this paper. At that time my papers received so many rejections, that his trust in the value of this work should be mentioned.


    What is a state of a system? (an outline)

    in: M. Droste and Y. Gurevich eds., Semantics of programming languages and model theory. Vol. 5 In the series Algebra, Logic and Application (R. Gobel ed.) Gordon and Breach (1993). ( compressed dvi 31pp) ( compressed ps 31pp).

    This paper is more technical than the previous; there is certain overlap and the same concepts are developed somewhat differently.

    For sequential processes, a state is simply the complete information on all the variables and control positions at a particular instant. For concurrent communicating processes, the notion `state' has no such simple definition. Considering its central place, it is surprising that the general notion state has received so little attention.

    In this note the notion `pomset' is extended in such a way that a state is just a pomset with no temporal precedence relation on its events---it is the description of an instant (Section 3.3). This allows to demonstrate within a single framework the duality between two approaches to modeling concurrency: the one based on events and the other on states.

    The paper gives a denotational semantics for a simple concurrent language. The last section describes a modified version of Scott's definition of `information systems' which I find more natural.


    An advantage of a mathematical modeling of computation is that it allows for a negative result of the kind ``there is no protocol such that x''. An example which deals with regular registers is the following work with Menachem Magidor which study the family of mutual exclusion protocols that use regular registers.

    with Menachem Magidor
    Theoretical Computer Science 129 (1994) 1-38. Ask for reprints.

    The main result in this paper is that there is no solution with regular registers to the critical-section problem for n processes whose registers are of total size 3n-1. For n=2 this is the best result since for total size six, solutions exist, and are presented here. The impossibility proof depends on a careful analysis of infinite protocol automata, and therefore a detailed definition of such automata and their semantics is developed first.


    Models for Concurrency

    A HREF="http://www.gbhap.com"> (Taylor & Francis
    Contents and preface of the monograph: (ps)
    For the Epilogue: (ps)


    On interprocess communication and the implementation of multi-writer atomic registers,

    Theoretical Computer Science, 149 (1995) 257--298. ( compressed ps 56 pp)

    Two protocols are described and verified formally in this paper. Both implement an atomic multi-readers multi-writers register out of single-writer registers. The correctness proof is done in two stages: a lower-level and a higher-level stage. The correctness of a protocol that implements an atomic register is proved here in two stages: (1) A formulation of higher-level specifications and a proof that the protocol satisfies these specifications. (2) A proof of atomicity assuming that the specifications hold. This division enables a better understanding of the protocols, and the fact that both protocols share the same higher-level specifications reduces the length of the correctness proof.
    A preliminary version of this paper was submitted (to another journal) in June 88. I worked quite hard to find the algorithm, but I worked even harder to find the right way to prove its correctness. The usage of higher-level properties in an axiomatic way in order to facilitate the correctness proof was developed for that protocol. Struggling with this paper I have realized that it is much harder to write proofs in computer science than in mathematics (finding them is another issue of course). Questions of style are more important, and it is not enough to write a correct and more or less complete proof in order to convince the reader. There is a tradition in mathematics which makes it easier to write and read---whereas in some areas of computer science there are no accepted paradigms and no common assumptions that the writer can share with his readers. Fortunate are those writers that know that their work is read and whose work is alive in the mind of their readers. I believe that this writer--readers interaction is a major force in closing the writer/reader gap and in finding the right level of details in which the work should be presented. I hope that one day I will find my readers too, and perhaps it will be seen then that what I want to say is quite trivial.
    I thank John Tromp and Ludwik Czaja who helped me with good advices concerning this paper.


    My colleague and friend Ludwik Czaja from Warsaw University is one of the organizers of the yearly Concurrency, Specification, and Programming workshop, and I participated in three of these meetings in 1993, 1995, and 2001. If your library doesn't have the proceedings of these conferences, you can ask Ludwik (lczaja@mimuw.edu.pl). The paper ``Bakery Algorithms'' was presented in 1993, and I still hope to publish a journal version since there are several interesting open problems there. The paper on the Achilles paradox was presented in the 1995 conference, and was finally incorporated in my monograph.

    in: H.-D. Burkhard, L. Czaja and P. Starke eds., Proc. of the Concurrency , Specification and Programming Workshop, (Warszawa 1993) 7--40. ( compressed ps 39 pp)

    The paper studies the Bakery Algorithm of Lamport and some variants (these are all mutual exclusion protocols), and its main contribution is a protocol which is similar to the Bakery Algorithm but only uses bounded values. Another variant uses local clocks to coordinate the protocol's execution, and conditions on the clocks are determined that suffice for the protocol's correctness.
    In what sense is our bounded algorithm similar to the unbounded Bakery Algorithm? In that both satisfy the ``Bakery Definability property'' (which is a strong form of the First Come First Serve property).
    Our proof consists of two stages: In the higher-level stage, abstract properties of system executions are assumed and their desired consequences are proved. At the lower-level stage these abstract properties are shown to hold in every execution of the protocol. An advantage of this two stage approach is demonstrated by the correctness proofs given to these variants of the Bakery Algorithm: Since they are shown to share with the Bakery Algorithm the same higher-level properties, their correctness proofs are reduced to only one stage (the lower level).

    in: H.-D. Burkhard, L. Czaja and P. Starke eds., Proc. of the Concurrency , Specification and Programming Workshop, (Warszawa 1995) 7--16. ( compressed ps 9 pp)

    I think it is a good exercise to check how your favorite specification approach can deal with questions that are not directly related to computer science, and this paradox of Zeno is an interesting candidate. The paper formalizes the well known paradox of Zeno using models (in the sense of Tarski).
    The paper was rewritten as section 5 of Chapter 2 in my monograph.


    Self-stabilization of a system means that after transient malfunctioning, in which several processes may crash, the system automatically resumes normal operating mode. Self-stabilizing protocols are harder to find and are more complex than their regular counterparts. The following two papers are about self-stabilization. The first about the l-exclusion problem and the second about self-stabilizing timestamps. They solve two problems from
    Y. Afek, D. Dolev, E. Gafni, M. Merritt and N. Shavit, ``A Bounded First-In, First-Enabled Solution to the l-exclusion Problem,'' ACM Transactions on Programming Languages and Systems, Vol. 16, No. 3, pp. 939-953, 1994.
    I was introduced to this subject of self-stabilization by Shlomi Dolev.

    with Shlomi Dolev, Ted Herman, and Irit Koll,
    Theoretical Computer Science B, 266/1-2 (2001) 653--692.
    ( compressed ps 43 pp)

    This work presents a self-stabilizing solution to the -exclusion problem. (A well-known generalization of the mutual-exclusion problem in which up to , but never more than , processes are allowed simultaneously in their critical sections.) Self-stabilization means that even when transient failures occur and some processes crash, the system finally resumes its regular and correct behavior. The model of communication assumed here is that of shared memory, in which processes use single-writer multiple-reader regular registers.

    A preliminary version of this work was published as
    Self-Stabilizing -Exclusion, with Shlomi Dolev, Ted Herman, and Irit Koll,
    In Sukumar Ghosh and Ted Herman (Eds.) Self-Stabilizing Systems. 3rd Workshop,
    WSS '97, Proceedings 1997, International Informatics Series 7.

    ( compressed ps 75 pp)
    Theoretical Computer Science, Vol. 308/1--3 pp 449-515, 2003.

    The problem of implementing self-stabilizing timestamps with bounded values is investigated and a solution is found which is applied to the -exclusion problem and to the Multiwriter Atomic Register problem. Thus we get self-stabilizing solutions to these two well-known problems. A new type of weak timestamps is identified here, and some evidence is brought to show its usefulness.

    This paper combines three papers written in the last ten years which I have no intention to publish since their main ideas are included in the ``Self-Stabilizing Timestamps'' paper. However, they may still have some limited value for those who are not especially interested in self-stabilization.


    Self Stabilizing weak snapshots and timestamps
    Usually, self-stabilization is expressed in terms of state, but there are situations in which it seems that states would be cumbersome. For example suppose that we want to prove that a protocol that employs regular registers self stabilizes. Since expressing regularity of registers with states is not natural and system executions are more appropriate, it seems that for such protocols we better specify self stabilization in terms of behavior rather than states. ( pdf)


    Concurrency without global states: a case study,

    in preparation ( dvi 43 pp)

    A distributed variant of the Lazy Caching algorithm of Afek, Brown, and Merritt is described and proved to be sequentially consistent. This variant is distributed in the sense that (unlike the original algorithm it does not consider a compound action that contains several instructions as an atomic operation. Only elementary operations on queues are atomic. The correctness proof exemplifies a new approach to concurrency in which there are no global states, and part of the proof (the higher-level part) is an abstract reasoning about system executions. A former version of this work contains an additional algorithm which may be of some interest.

    ( dvi 64 pp)

    The two variant algorithms presented here share the same higher-level part. This expresses in a formal way the similarity between the two algorithms.


    Exercises in Style (Alpha Specifications),

    with Tamar Pinhas
    Fundamenta Informaticae 54 (2-3) (2003) 107--135.
    ( dvi 32 pp) ( for a pdf)

    We compare two documents: the Alpha Architecture Reference Manual (from Compaq Computer Corporation) and the TLA+ specification of the Alpha memory model (by Lamport, Sharma, Tuttle, and Yu). We compare the styles, the languages employed, and the fundamental assumptions (that is the basic frameworks of the two texts). We conclude that the TLA+ specification is not so much a formalization of the Alpha Manual text as it is a translation into a different framework. We believe that a formalization of the alpha Manual can be useful, and we propose one.

    An abstract of this paper is published in the proceedings of the Concurrency, Specification and Programming (CS&P) Workshop, held at Humboldt University, October 7-9, 2002. (edited by H-D. Burkhard, L. Czaja, G. Lindemann, A. Skowron, and P. Starke).


    How to prove the correctnes of a (Cache Coherence) Protocol,

    ( dvi file)

    Formal specification writers and researchers whose main interest is mathematical correctness proofs do not usually {\em explain} their protocols. Engineers and system builders are usually not very interested in the formal details involved in a correctness proof, although they surely want the readers to understand the subtleties of their constructions. We want to narrow this gap by suggesting that a mathematical investigation of higher-level properties of protocols can contribute to the process of learning and understanding them. To exemplify our approach, a cache coherence protocol is described and explained informally. Part of this explanation is an abstract, higher-level proof that the desirable properties of the protocol (cache coherence) follow from some basic properties (Called here axioms).



Last modified: January 2003.


.


This is Jimy (``Poushka'') from On system executions and states