Informal and formal correctness proofs for programs
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.On Global-Time and inter-process communication
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:
On system executions and states
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.
On the mutual-exclusion problem---a quest for minimal solutions.
with Menachem MagidorTheoretical 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
Gordon and Breach, 1999.
Algebra, Logic and Application Series Volume 11.
A HREF="http://www.gbhap.com"> (Taylor & FrancisContents 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.
Bakery algorithms.
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).
The Achilles paradox,
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.
Self-Stabilizing 
-Exclusion.
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.)
WSS '97, Proceedings 1997, International
Informatics Series 7.
Self-Stabilizing Timestamps.
( 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.
- 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)
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.
Lazy Caching for lazy readers,
( 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 PinhasFundamenta 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).
