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.

#### Informal and formal correctness proofs for programs

#### Bakery algorithms.

#### Self-Stabilizing -Exclusion.

#### Self-Stabilizing Timestamps.

Skewed Timestamps

In the well known timestamp algorithm each writing process reads all the registers of the other processes, and then sets a higher timestamp (natural number) to itself. In the `skewed algorithm' a writer only reads the other writers with lower indices; so that only one writing process in each pair reads the other. ( compressed dvi 17 pp)Multiwriter Atomic Registers and bounded timestamps

The problem of implementing timestamps with bounded values is investigated, and its connection with the Multiwriter Atomic Register Problem is established in an unexpected way: Whereas in the unbounded case timestamps can be used to implement an atomic register, in the bounded case, as we show, it is the solution to the Multiwriter Atomic Register Problem which is extended in order to implement bounded timestamps. A new type of protocol for atomic registers is identified here. ( compressed dvi 35 pp)

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.

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.

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.

A
HREF="http://www.gbhap.com"> (Taylor & Francis

Contents and preface of the monograph: (ps)

For the Epilogue: (ps)

*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)

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.

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).

( 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