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.
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.
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:
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.
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.
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.
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.
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).
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.
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.)
WSS '97, Proceedings 1997, International
Informatics Series 7.
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.
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.
The two variant algorithms presented here share the same higher-level part. This expresses in a formal way the similarity between the two algorithms.
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).
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).