Verification of distributed programs using representative interleaving sequences

Summary We present a formal proof method for distributed programs. The semantics used to justify the proof method explicitly identifies equivalence classes of execution sequences which are equivalent up to permuting commutative operations. Each equivalence class is called an interleaving set or a run. The proof rules allow concluding the correctness of certain classes of properties for all execution sequences, even though such properties are demonstrated directly only for a subset of the sequences. The subset used must include a representative sequence from each interleaving set, and the proof rules, when applicable, guarantee that this is the case. By choosing a subset with appropriate sequences, simpler intermediate assertions can be used than in previous formal approaches. The method employs proof lattices, and is expressed using the temporal logic ISTL. Shmuel Katz received his B.A. in Mathematics and English Literature from U.C.L.A., and his M.Sc. and Ph.D. in Computer Science (1976) from the Weizmann Institute in Rechovot, Israel. From 1976 to 1981 he was at the IBM Israel Scientific Center. Presently, he is on the faculty of the Computer Science Department at the Technion in Haifa, Israel. In 1977–1978 he visited for a year at the University of California, Berkeley, and in 1984–1985 was at the University of Texas at Austin. He has been a consultant and visitor at the MCC Software Technology Program, and in 1988–1989 was a visiting scientist at the I.B.M. Watson Research Center. His research interests include the methodology of programming, specification methods, program verification and semantics, distributed programming, data structures, and programming languages. Doron Peled was born in 1962 in Haifa. He received his B.Sc. and M.Sc. in Computer Science from the Technion, Israel in 1984 and 1987, respectively. Between 1987 and 1991 he did his military service. He also completed his D.Sc. degree in the Technion during these years. Dr. Peled was with the Computer Science department at Warwick University in 1991–1992. He is currently a member of the technical staff with AT & T Bell Laboratories. His main research interests are specification and verification of programs, especially as related to partial order models, fault-tolerance and real-time. He is also interested in semantics and topology.This research was carried out while the second author was at the Department of Computer Science, The Technion, Haifa 32000, Israel     

Self-stabilization over unreliable communication media

Summary A self-stabilizing system has the property that it will converge to a desirable state when started from any state. Most previous researchers assumed that processes in self-stabilizing systems may communicate through shared variables while those that studied meassage passing systems allowed messages with unbounded size. This paper discusses the development of self-stabilizing systems which communicate through message passing, and in which messages may be lost in transit. The systems presented all use fixed size message headers. First, a selfstabilizing version of theAlternating Bit Protocol, a fundamental communication protocol for transmitting data across an unreliable communication medium, is presented. Secondly, the alternating-bit protocol is used to construct a self-stabilizing token ring. Yehuda Afek received a B.Sc. in Electrical Engineering from the Technion and an M.S. and Ph.D. in Computer Science from the University of California, Los Angeles. In 1985 he joined the Distributed Systems research Department in AT&T Bell Laboratories and in 1988 he joined the Department of Computer Science in Tel-Aviv University. His interests include communication protocols, distributed systems, and asynchronous shared memories. Geoffrey M. Brown received the BS degree in Engineering from Swarthmore College in 1982, the MS degree in Electrical Engineering from Stanford University in 1983, and the Ph.D. degree in Electrical Engineering from the University of Texas at Austin in 1987. From 1983 to 1984 he worked for Motorola in Austin, TX. Currently he is an Assistant Professor in the School of Electrical Engineering at Cornell University. In 1990, Brown was named a Presidential Young Investigator by the National Science Foundation.This work supported in part by NSF grant CCR-9058180     

Self-stabilizing extensions for meassage-passing systems

Summary A self-stabilizing program eventually resumes normal behavior even if excution begins in, an abnormal initial state. In this paper, we explore the possibility of extending an arbitrary program into a self-stabilizing one. Our contributions are: (1) a formal definition of the concept of one program being aself-stabilizing extension of another; (2) a characterization of what properties may hold in such extensions; (3) a demonstration of the possibility of mechanically creating such extensions. The computtional model used is that of an asynchronous distributed message-passing system whose communication topology is an arbitrary graph. We contrast the difficulties of self-stabilization in thismodel with those of themore common shared-memory models. Shmuel Katz received his B.A. in Mathematics and Englisch Literature from U.C.L.A., and his M.Sc. and Ph.D. in Computer Science (1976) from the Weizmann Institute in Rechovot, Israel. From 1976 to 1981 he was a research at the IBM Israel Scientific Center. Presently, he is an Associate Professor in the Computer Science Department at the Technion in Haifa, Israel. In 1977–78 he visited for a year at the University of California, Berkeley, and in 1984–85 was at the University of Texas at Austin. He has been a consultant and vistor at the MCC Software Technology Program, and in 1988–89 was a visiting scientist at the IBM Watson Research Center. His research interests include the methodology of programming, specification methods, program verification and semantics, distributed programming, data structure, and programming languages. Kenneth J. Pery has performed research in the area of distributed computing since obtaining Masters and Doctorate degrees in Computer Science from Cornell Univesity. His current interest is in studying problems of a partical nature in a formal context. He was graduated from Princeton University in 1979 with a B.S.E. degree in Electrical Engineering and Computer Science.The Research of this author was partially supported by Research Grant 120-749 and the Argentinian Research Fund at the Technion     

Bounded time-stamps

Summary Time-stamps are labels which a system adds to its data items. These labels enable the system to keep track of the temporal precedence relations among its data elements. Many distributed protocols and some applications use the natural numbers as time-stamps. The natural numbers however are not useful for bounded protocols. In this paper we develop a theory ofbounded time-stamps. Time-stamp schemes are defined and the complexity of their implementation is analyzed. This indicates a direction for developing a general tool for converting time-stamp based protocols to bounded protocols. Amos Israeli received his B.Sc. in Mathematics and Physics from Hebrew University in 1976, and his M.Sc. and D.Sc. in Computer Science from the Weizmann Institute in 1980 and the Technion in 1985, respectively. Currently he is a senior lecturer at the Tlectrical Engineering Department at the Technion. Prior to this he was a postdoctoral fellow at the Aiken Computation Laboratory at Harvard. His research interests are in Parallel and Distributed Computing and in Robotics. In particular he has worked on the design and analysis of Wait-Free and Self-Stabilizing distributed protocols. Ming Li received his M.S. and Ph.D. in Computer Science from Wayne State University in 1980 and Cornell University 1985, respectively. Currently he is an associate professor at the Computer Science Department at the University of Waterloo. His research interests are in Theory of Computing, Kolmogorov Complexity, and Machine Learning.Supported in part by the Weizmann fellowship and NSF Grant DCR-86-00379Supported in part by ONR Grant N00014-85-k-0445 and Army Research Office Grant DAAL03-86-K-0171 at Harvard University, by NSF Grant kDCR-86-06366 at Ohio State University, and by NSERC Operating Grant OGP0036747. Most of this work was done when the authors were at Aiken Computation Laboratory at Harvard University. The authors also acknowledge the hospitality of the computer science department at York University, Canada     

One-bit algorithms

Many algorithms in distributed systems assume that the size of a single message depends on the number of processors. In this paper, we assume in contrast that messages consist of a single bit. Our main goal is to explore how the one-bit translation of unbounded message algorithms can be sped up by pipelining. We consider two problems. The first is routing between two processors in an arbitrary network and in some special networks (ring, grid, hypercube). The second problem is coloring a synchronous ring with three colors. The routing problem is a very basic subroutine in many distributed algorithms; the three coloring problem demonstrates that pipelining is not always useful. Amotz Bar-Noy received his B.Sc. degree in Mathematics and Computer Science in 1981, and his Ph.D. degree in Computer Science in 1987, both from the Hebrew University of Jerusalem, Israel. Between 1987 and 1989 he was a post-doctoral fellow in the Department of Computer Science at Stanford University. He is currently a visiting scientist at the IBM Thomas J. Watson Research Center. His current research interests include the theoretical aspects of distributed and parallel computing, computational complexity and combinatorial optimization. Joseph (Seffi) Naor received his B.A. degree in Computer Science in 1981 from the Technion, Israel Institute of Technology. He received his M.Sc. in 1983 and Ph.D. in 1987 in Computer Science, both from the Hebrew University of Jerusalem, Israel. Between 1987 and 1988 he was a post-doctoral fellow at the University of Southern California, Los Angeles, CA. Since 1988 he has been a post-doctoral fellow in the Department of Computer Science at Stanford University. His research interests include combinatorial optimization, randomized algorithms, computational complexity and the theoretical aspects of parallel and distributed computing. Moni Naor received his B.A. in Computer Science from the Technion, Israel Institute of Technology, in 1985, and his Ph.D. in Computer Science from the University of California at Berkeley in 1989. He is currently a visiting scientist at the IBM Almaden Research Center. His research interests include computational complexity, data structures, cryptography, and parallel and distributed computation.Supported in part by a Weizmann fellowship and by contract ONR N00014-85-C-0731Supported by contract ONR N00014-88-K-0166 and by a grant from Stanford's Center for Integrated Systems. This work was done while the author was a post-doctoral fellow at the University of Southern California, Los Angeles, CAThis work was done while the author was with the Computer Science Division, University of California at Berkeley, and Supported by NSF grant DCR 85-13926     

Distributed algorithms for constructing a minimum-weight spanning tree in a broadcast network

Two distributed algorithms are presented for a network using a common communication channel (e.g. radio) in which all nodes are within signal range and in line of sight of each other: (a) an algorithm to compute all internode distances (in terms of propagation delays) in the network. the algorithm requires only 2 messages per node, and provides each node with the distances to all other nodes. (b) An algorithm for constructing a minimum-weight spanning tree (MST) in such a network. This algorithm starts out with the information provided by (a) and ends with each node possessing the explicit knowledge of the full MST. The algorithm requires at most log₂ N messages per node. The internal processing in each node needsO(N logN) time andO(N) space. All messages required by (a) and (b) contain at most one edge weight plus 2 log₂ N bits. Some possible applications of the algorithms are: position-location, tuning acknowledgement time-out mechanisms, tuning the scheduling functions of access protocols that are sensitive to individual internode propagation delays, and selecting performance effective transmission sequences for round robin access protocols.Yaron I. Gold received the B.Sc. (Cum Laude, 1970) and M.Sc. (1975), both in Electrical Engineering, from the Technion, Israel institute of Technology, and the Ph.D. (1981) in Computer Science, from the University of Minnesota, Minneapolis.From 1970 to 1975 Yaron Gold served as Research and Development Officer in the Israeli Defense Forces, leading a group of several scientists, engineers and technicians. From 1982 to 1984 he was on the faculty of the Department of Electrical Engineering the Department of Electrical Engineering and Computer Science at the University of Connecticut. During that period he also served as consultant for United Technologies Corporation and for Battelle Laboratories. Presently, Dr. Gold is on the faculty of the Computer Science Department at the Technion.His research interests include Computer Networks and Communications, Simulation and Intelligent Systems.Shlomo Moran received the B.Sc. and D.Sc. degrees in mathematics from Technion, Israel Institute of Technology, Haifa, in 1975 and 1979, respectively.From 1979 to 1981 he was assistant professor and a visiting research specialist at the University of Minnesota, Minneapolis. From 1981 to 1985 he was a senior lecturer at the Department of Computer Science, Technion, and from 1985 to 1986 he was a World Trade visitor at IBM Thomas J. Watson Research Center, Yorktown Heights. Currently he is associate professor at the Department of Computer Science, Technion.His research interests include distributed algorithms, computational complexity, combinatorics, graph theory and geometric aspects of communication networks.This work was supported in part by NSF grant ECS-8307186Part of this research was done while this author was with the University of ConnecticutPart of this research was done while this author was with IBM, Thomas J. Watson Research Center     

Efficient emulation of single-hop radio network with collision detection on multi-hop radio network with no collision detection

Summary This paper presents an efficient randomized emulation ofsingle-hop radio networkwith collision detection onmulti-hop radio networkwithout collision detection. Each step of the single-hop network is emulated by rounds of the multi-hop network and succeeds with probability 1–. (n is the number of processors,D the diameter and the maximum degree). It is shown how to emulate any polynomial algorithm such that the probability of failure remains . A consequence of the emulation is an efficient randomized algorithm for choosing a leader in a multi-hop network. Reuven Bar-Yehuda was born in Iran, on July 17th 1951. Received B.A., M.Sc., and D.Sc. in Computer Science from the Technion — Israel Institute of Technology, Haifa, Israel, in 1978, 1980, and 1983, respectively. He is currently a Senior Lecturer of Computer Science at the Technion. From 1984 to 1986, he was a visiting assistant professor in the Computer Science Dept. at the Duke Univesity His research interests include computational geometry, VLSI, graph algorithms and distributed algorithms. Oded Goldreich was born in Tel-Aviv, Israel, on February 4th 1957. Received B.A., M.Sc., and D.Sc. in Computer Science from the Technion — Israel Institute of Technology, Haifa, Israel, in 1980, 1982, and 1983, respectively. He is currently an Associate Professor of Computer Science at the Technion. From 1983 to 1986, he was a postdoctoral fellow at MIT's Laboratory for Computer Science. His research interests include cryptography and related areas, relation between randomness and algorithms, and distributed computation. Alon Itai was born in Scotland, on December 12th 1946. Received B.Sc. in Mathematics from the Hebrew University in Jerusalem in 1969. M.Sc., and Ph.D. in Computer Science from the Weizmann Institute of Science, Rehovot, Israel in 1971 and 1976. He is currently an Associate Professor of Computer Science at the Technion. His research interests include randomized and distributed algorithms, computational learning theory and performance evaluation.The second author was partially supported by grant No. 86-00301 from the United States—Israel Bi-national Science Foundation BSF), Jerusalem, Israel.     

Appraising fairness in languages for distributed programming

The relations among various languages and models for distributed computation and various possible definitions of fairness are considered. Natural semantic criteria are presented which an acceptable notion of fairness should satisfy. These are then used to demonstrate differences among the basic models, the added power of the fairness notion, and the sensitivity of the fairness notion to irrelevant semantic interleavings of independent operations. These results are used to show that from the considerable variety of commonly used possibilities, only strong process fairness is appropriate forCSP if these criteria are adopted. We also show that under these criteria, none of the commonly used notions of fairness are fully aceptable for a model with an n-way synchronization mechanism. The notion of fairness most often mentioned for Ada is shown to be fully acceptable. For a model with nonblockingsend operations, some variants of common fairness definitions are appraised, and two are shown to satisfy the suggested criteria. Krzysztof R. Apt was born in 1949 in Poland. Received his Ph.D. in 1974 from Polish Academy of Sciences in Warsaw in mathematical logic. From 1974 until 1981 worked at various scientific institutions in the Netherlands and from 1981 until 1987 at C.N.R.S. in Paris, France. Spent 1985 as a visiting scientist at IBM Research Centre in Yorktown Heights, U.S.A. Currently holding an Endowed Professorship at the Department of Computer Sciences at the University of Texas at Austin; also a senior research scientist at the Centre for Mathematics and Computer Science in Amsterdam, the Netherlands. His research interests include program correctness and semantics, methodology of distributed computing, use of logic as a programming language and non-standard forms of reasoning. He has served on editorial boards of a number of journals and program committees of numerous conferences in computer science. Lectured in a dozen countries on four continents. Also, he has run two marathons and crossed Sumatra on a bicycle. Shmuel Katz received his B.A. in Mathematics and English Literature from U.C.L.A., and his M.Sc. and Ph.D. in Computer Science (1976) from the Weizmann Institute in Rehovot, Israel. From 1976 to 1981 he was a researcher at the IBM Israel Scientific Center. Presently, he is a Senior Lecturer in the Computer Science Department at the Technion in Haifa, Israel. In 1977–78, he visited for a year at the University of California, Berkeley, and in 1984–85 was at the University of Texas at Austin. He has also been a consultant for the MCC Software Technology Program. His research interests include the methodology of programming, specification methods, program verification and semantics, distributed programming, data structures, and programming languages. Nissim Francez received his B.A. in Mathematics and Philosophy from the Hebrew University in Jerusalem, and his M.Sc. and Ph.D. in computer science (1976) from the Weizmann Institute of Science, Rehovot, Israel. In 1976–77 he spent a postdoctoral year at Queen's university, Belfast, where he was introduced by C.A.R. Hoare to CSP. In 1977–78 he was an assistant professor at USC, Los Angeles. From 1978 he is with the Computer Science Department at the Technion. In 1982–83 he was on a sabbatical leave at IBM T.J. Watson Research Center. He has been a consultant for MCC's software technology program, working on multiparty activities in distributed systems. He had summer appointments in Harvard University, IBM T.J. Watson Research Center, Utrecht University, CWI (Amsterdam) and at MCC. He also served in several program committees. His research interests include program verification and the semantics of programming languages, mainly for concurrent and distributed programming. Is also interested in logic programming and recursive query evaluation and in compiler constration. He is the author of the first book onFairness. Unfortunately, he is incapable of Marathon running...     

Atomic snapshots using lattice agreement

Summary Thesnapshot object is an important tool for constructing wait-free asynchronous algorithms. We relate the snapshot object to thelattice agreement decision problem. It is shown that any algorithm for solving lattice agreement can be transformed into an implementation of a snapshot object. The overhead cost of this transformation is only a linear number of read and write operations on atomic single-writer multi-reader registers. The transformation uses an unbounded amount of shared memory. We present a deterministic algorithm for lattice agreement that usedO (log² n) operations on 2-processorTest & Set registers, plusO (n) operations on atomic single-writer multi-reader registers. The shared objects are used by the algorithm in adynamic mode, that is, the identity of the processors that access each of the shared objects is determined dynamically during the execution of the algorithm. By a randomized implementation of 2-processorsTest & Set registers from atomic registers, this algorithm implies a randomized algorthm for lattice agreement that uses an expected number ofO (n) operations on (dynamic) atomic single-writer multi-reader registers. Combined with our transformation this yields implementations of atomic snapshots with the same complexity.Cambridge Research Laboratory, Digital Equipment Corporation Hagit Attiya received the B.Sc. degreeiin Mathematics and Computer Science from the Hebrew University of Jerusalem, in 1981, the M.Sc. and Ph.D. degrees in Computer Science from the Hebrew University of Jerusalem, in 1983 and 1987, respectively. She is presently a senior lecturer at the departtment of Computer Science at the Technion, Israel Institute of Technology. Prior to this, she has been a post-doctoral research associate at the Laboratory for Computer Science at M.I.T. Her general research interests are distributed computation and theoretical computer science. More specific interests include fault-tolerance, timing-based and asynchronous algorithms. Maurice Herlihy received the A.B. degree in Mathematics from Harvard University, and the M.S. and the Ph.D. degrees in Computer Science from M.I.T. From 1984 to 1989 he was a faculty member in the Computer Science Department at Carnegie Mellon University in Pittsburgh, PA. In 1989 he joined the research staff at the Digital Equipment Corporation's Cambridge Research Laboratory in Cambridge MA. Since 1994, he has been on the faculty at the Computer Science Department at Brown University. Dr. Herlihy's research interests encompass practical and theoretical aspects of distributed and concurrent computation. Ophir achman received a B.A. in computer science from the Technion, Haifa, Israel in 1989 and M.Sc. in computer science from the Technion, Haifa, Israel, in 1992. He is now studying for a D.Sc. in computer science at the Technion. His currentarea of research is distributed computing, and in particular, asynchronous shared memory systems.This work appeared in preliminary form in proceedings ofthe 6th International Workshop on Distributed Algorithms [12]. This research was partially supported by grant No. 92-0233 from the United States-Israel Binational Science Foundation (BSF), Jerusalem, Technion V.P.R. funds — B. and G. Greenberg Research Fund (Ottawa), and the fund for the promotion of research in the TechnionPart of the work of this author was performed while visiting DEC Cambridge Research Laboratory     

Self-stabilizing depth-first token circulation on networks

Summary This paper proposes a self-stabilizing protocol which circulates a token on a connected network in nondeterministic depth-first-search order, rooted at a special node. Starting with any initial state in which the network may have no token at all or more than one token, the protocol eventually makes the system stabilize in states having exactly one circulating token. With a slight modification to the protocol —by removing nondeterminism in the search — a depth-first-search tree on the network can be constructed. The proposed protocol runs on systems that allow parallel operations. Shing-Tsaan Huang was born in Taiwan on September 4, 1949. He got his Ph.D. degree in 1985 from Department of Computer Science, University of Maryland at College Park. Before he pursued his Ph.D. degree, he had worked several years in the computer industry in Taiwan. Professor Huang is currently the chairman of the Department of Computer Science, Tsing Hua University, Taiwan, Republic of China. His research interests include interconnection networks, operating systems and distributed computing. He is a senior member of the IEEE Computer Society and a member of the Association for Computing Machinery. Nian-Shing Chen was born in Taiwan on October 21, 1961. He received his Ph.D. degree in computer science from National Tsing Hua University in 1990. Dr. Chen is currently an associate professor with the Department of Information Management at Sun Yat-Sen University of Taiwan. His research interests include distributed systems, computer networks, computer viruses and expert systems. He is a member of IEEE and Phi Tau Phi honorary society.This research is supported by National Science Council of the Republic of China under the contract NSC81-0408-E-007-05 and NSC82-0408-E-007-027     

Closed schedulers: a novel technique for analyzing asynchronous protocols

Summary Analyzing distributed protocols in various models often involves a careful analysis of the set ofadmissible runs, for which the protocols should behave correctly. In particular, the admissible runs assumed by at-resilient protocol are runs which are fair for all but at mostt processors. In this paper we defineclosed sets of runs, and suggest a technique to prove impossibility results fort-resilient protocols, by restricting the corresponding sets of admissible runs to smaller sets, which are closed, as follows: For each protocolPR and for each initial configurationc, the set of admissible runs ofPR which start fromc defines a tree in a natural way: the root of the tree is the empty run, and each vertex in it denotes a finite prefix of an admissible run; a vertexu in the tree has a sonv iffv is also a prefix of an admissible run, which extendsu by one atomic step.The tree of admissible runs described above may contain infinite paths which are not admissible runs. A set of admissible runs isclosed if for every possible initial configurationc, each path in the tree of admissible runs starting fromc is also an admissible run. Closed sets of runs have the simple combinatorial structure of the set of paths of an infinite tree, which makes them easier to analyze. We introduce a unified method for constructing closed sets of admissible runs by using a model-independent construction of closedschedulers, and then mapping these schedulers to closed sets of runs. We use this construction to provide a unified proof of impossibility of consensus protocols. Ronit Lubitch received her B.Sc. degree in Mathematics and Computer Science from Tel Aviv University in 1989, and her Master degree in Computer Science from the Technion, in 1993. From 1992 she is working in Graffiti Software Industries, which expertise in the design and development of advanced photo realistic rendering, and animation software systems. Shlomo Moran received his B.Sc. and Ph.D. degrees in Mathematics from the Technion in 1975 and 1979 resp. In 1979–1981 he was at the University of Minnesota as a visiting research specialist. In 1981 he joined the Computer Science Department at the Technion, where he is now a full professor. In 1985–1986 he visited at IBM T.J. Watson Research Center. In 1992–1993 he visited at AT&T Bell Laboratories and in Centrum voor Wiskunde en Informatica, Amsterdam. His research interests include distributed computing, Combinatorics and Graph Theory, and Complexity Theory.A preliminary extended version of this paper appeared in the Proceedings of 6-th International Workshop on Distributed Algorithms, Haifa, November 1992This work was supported in part by the Technion V.P.R. fund. Part of this research was conducted while this author was visiting at AT&T Bell Labs at Murray Hill and at CWI, Amsterdam     

On the complexity of computation in the presence of link failures: the case of a ring

Summary We investigate the message complexity of distributed computations on rings of asynchronous processors. In such computations, each processor has an initial local value and the task is to compute some predetermined function of all local values. Our work deviates from previous works concerning the complexity of ring computations in that we consider the effect oflink failures. A link is said to fail if some message sent through it never reaches its destination. We show that the message complexity of any function, which is sensitive to all its inputs, is (n logn) whenn, the number of processors, is a-priori known; and is (n ² ) whenn is not known. Interestingly, these tight bounds do not depend on whether the identity of a leader is a-priori known before the computation starts. These results stand in sharp contrast to the situation in asynchronous rings with no link failures, where the message complexity is affected by the a-priori knowledge of a leader but is not affected by the knowledge ofn. Oded Goldreich was born in Tel-Aviv, Israel, on February 4th 1957. Received B.A., M.Sc., and D.Sc. in Computer Science from the Technion — Israel Institute of Technology, Haifa, Israel, in 1980, 1982, and 1983, respectively. He is currently an Associate Professor of Computer Science in the Technion. From 1983 to 1986, he was a postdoctoral fellow in MIT's Laboratory for Computer Science. His research interests include cryptography and related areas, relation between randomness and algorithms, and distributed computation. Luiba Shrira was born in Vilnius, Lithuania. Received B.A., M.Sc., and D.Sc. in Computer Science from the Technion—Israel Institute of Technology, Haifa, Israel in 1977, 1980, and 1985, respectively. from 1986 to 1989 she was a postdoctoral fellow at Laboratory for Computer science at MIT, where she is currently a Research Associate. Her research interests include highly-available and reliable distributed algorithms and systems, persistent object systems, and programming methodology.Part of the work has been done while the first author was in the Laboratory for Computer Science of MIT and the second author was in the Computer Science Department of the Technion. First author was partially supported by a Weizmann Postdoctoral Fellowship, an IBM Postdoctoral Fellowship, and Albert Einstein Research Fund (through Technion's V.P.R. Fund)     

A self-stabilizing algorithm for coloring planar graphs

Summary This paper describes an algorithm for coloring the nodes of a planar graph with no more than six colors using a self-stabilizing approach. The first part illustrates the coloring algorithm on a directed acyclic version of the given planar graph. The second part describes a selfstabilizing algorithm for generating the directed acyclic version of the planar graph, and combines the two algorithms into one. Sukumar Ghosh received his Ph.D. degree in Computer Science from Calcutta University in 1971. From 1969 to 1984, he taught at Jadavpur University, Calcutta. During 1976–77, he was a Fellow of the Alexander von Humboldt Foundation at the University of Dortmund, Germany. Since 1984, he is with the Department of Computer Science of the University of Iowa. His current research interests are in the areas of Distributed Systems, Petri Nets and Self-Stabilizating Systems. Mehmet Hakan Karaata received the Sc. B. degree in Computer Science and Engineering from Hacettepe University in Turkey in 1987, and the M.S. degree in Computer Science from the University of Iowa in 1990. He is currently studying towards his Ph.D. at the same university. His research interests are in the areas of Distributed Systems, Self-Stabilizing Systems and Database Systems.This research was supported in part by the National Science Foundation under grant CCR-9109078, and the Old Gold Summer Fellowship of the University of Iowa. An abstract of this paper was presented at the 29th Allerton Conference on Control, Communication & Computing in October 1991.     

On the message complexity of binary byzantine agreement under crash failures

Summary The binary Byzantine Agreement problem requiresn–1 receivers to agree on the binary value broadcast by a sender even when some of thesen processes may be faulty. We investigate the message complexity of protocols that solve this problem in the case of crash failures. In particular, we derive matching upper and lower bounds on the total, worst and average case number of meassages needed in the failure-free executions of such protocols.More specifically, we prove that any protocol that tolerates up tot faulty processes requires a total of at leastn+t–1 messages in its failure-free executions —and, therefore, at least [(n+t–1)/2] messages in the worst case and min (P ₀,P ₁)·(n+t–1) meassages in the average case, whereP _v is the probability that the value of the bit that the sender wants to broadcast isv. We also give protocols that solve the problem using only the minimum number of meassages for these three complexity measures. These protocols can be implemented by using 1-bit messages. Since a lower bound on the number of messages is also a lower bound on the number of meassage bits, this means that the above tight bounds on the number of messages are also tight bounds on the number of meassage bits. Vassos Hadzilacos received a BSE from Princeton University in 1980 and a PhD from Harvard University in 1984, both in Computer Science. In 1984 he joined the Department of Computer Science at the University of Toronto where he is currently an Associate Professor. In 1990–1991 he was visiting Associate Professor in the Department of Computer Science at Cornell University. His research interests are in the theory of distributed systems. Eugene Amdur obtained a B. Math from the University of Waterloo in 1986 and a M.Sc. from the University of Toronto in 1988. He is currently employed by the Vision and Robotics group at the University of Toronto in both technical and research capacities. His current areas of interest are vision, robotics, and networking. Samuel Weber received his B.Sc. in Mathematics and Computer Science and his M.Sc. in Computer Science from the University of Toronto. Currently, he is at Cornell University as a Ph.D. student in Computer Science with a minor in Psychology. His research interests include distributed systems, and the semantics of programming languages.     

Temporal disjunctive logic programming

In this paper we introduce the logic programming languageDisjunctive Chronolog which combines the programming paradigms of temporal and disjunctive logic programming. Disjunctive Chronolog is capable of expressing dynamic behaviour as well as uncertainty, two notions that are very common in a variety of real systems. We present the minimal temporal model semantics and the fixpoint semantics for the new programming language and demonstrate their equivalence. We also show how proof procedures developed for disjunctive logic programs can be easily extended to apply to Disjunctive Chronolog programs. Manolis Gergatsoulis, Ph.D.: He received his B.Sc. in Physics in 1983, the M.Sc. and the Ph.D. degrees in Computer Science in 1986 and 1995 respectively all from the University of Athens, Greece. Since 1996 he is a Research Associate in the Institute of Informatics and Telecommunications, NCSR ‘Demokritos’, Athens. His research interests include logic and temporal programming, program transformations and synthesis, as well as theory of programming languages. Panagiotis Rondogiannis, Ph.D.: He received his B.Sc. from the Department of Computer Engineering and Informatics, University of Patras, Greece, in 1989, and his M.Sc. and Ph.D. from the Department of Computer Science, University of Victoria, Canada, in 1991 and 1994 respectively. From 1995 to 1996 he served in the Greek army. From 1996 to 1997 he was a visiting professor in the Department of Computer Science, University of Ioannina, Greece, and since 1997 he is a Lecturer in the same Department. In January 2000 he was elected Assistant Professor in the Department of Informatics at the University of Athens. His research interests include functional, logic and temporal programming, as well as theory of programming languages. Themis Panayiotopoulos, Ph.D.: He received his Diploma on Electrical Engineering from the Department of Electrical Engineering, National Technical Univesity of Athens, in 1984, and his Ph.D. on Artificial Intelligence from the above mentioned department in 1989. From 1991 to 1994 he was a visiting professor at the Department of Mathematics, University of the Aegean, Samos, Greece and a Research Associate at the Institute of Informatics and Telecommunications of “Democritos” National Research Center. Since 1995 he is an Assistant Prof. at the Department of Computer Science, University of Piraeus. His research interests include temporal programming, logic programming, expert systems and intelligent agent architectures.     

On the complexity of global computation in the presence of link failures: the general case

Summary This paper presents (m logn) and (mn) messages lower bounds on the problem of computing a gobal sensitive function in biderectional networks with link failures (i.e., dynamically changing topology), wheren andm are the total number of nodes and links in the network. The (m logn) lower bound is under the assumption thatn is a-priori known to the nodes, while the second bound is for the case in which such knowledge is not available. A global sensitive function ofn variables is a function that may not be computed without the knowledge of the values of all then variables (e.g. maximum, sum, etc). Thus, computing such a function at one node of a distributed network requires this node to communicate with every other node in the network. Though lower bounds higher than (m) messages are known for this problem in the context of link failures, none holds for dense bidirectional networks. Moreover, we are not aware of any other nontrivial lower bound higher than (m) for dense bidirectional networks. Yehuda Afek received a B.Sc. in Electrical Engineering from the Technion and an M.Sc. and Ph.D. in Computer Science from the University of California, Los-Angeles. In 1985 he joined the Distributed Systems Research Department in AT&T Bell Laboratories as a Member of Technical Staff. In 1988 he joined the Computer Science Department in Tel-Aviv University, where he now holds a permanent position. From 1989 to 1994 he was also a consultant for AT&T Bell Laboratories. His interests include communication protocols, distributed computing and asynchronous shared memory systems. Danny Hendler was born in Kiryat-Haim near Haifa, Israel, on April 17th 1961. He received his B.Sc. and M.Sc. in Computer Science from Tel-Aviv University, Israel, in 1986 and 1993, respectively. In the past 8 years he has worked as a free lance software-consultant, specializing mainly in communication, telephony and voice-mail applications.     

Fairness and hyperfairness in multi-party interactions

Summary In this paper, a new fairness notion is proposed for languages withmulti-party interactions as the sole interprocess synchronization and communication primitive. The main advantage of this fairness notion is the elimination of starvation occurring solely due to race conditions (i.e., ordering of independent actions). Also, this is the first fairness notion for such languages which is fully adequate with respect to the criteria presented in [2]. The paper defines the notion, proves its properties, and presents examples of its usefulness. Orna Grumberg received her B.Sc. degree, M.Sc. and Ph.D. in the Computer Science Department at the Technion—Israel Institute of Technology. Since 1984 she is a faculty member in the Computer Science Department at the Technion. Her research interests include verification of distributed systems, computer-aided verification, model checking, temporal logics and automata. Paul Attie received a B.A. degree in engineering science from the University of Oxford, and an M.Sc. degree in computer science from the University of London. Since 1986, Paul has been with the Microelectronics and Computer Technology Corporation, where he is currently a member of technical staff. He is also a candidate for the Ph.D. in computer science degree at the University of Texas at Austin. His research interests include temporal logic, fairness, algebraic process theory, formal semantics, and concurrent program verification.The photograph and autobiography of Dr. Nissim Francez were published in Volume 2, Issue No. 4, 1988 on page 226     

Distributed deadlock detection

We describe a simple and efficient algorithm to detect deadlocks in distributed systems. In our model, processes requestN resources from a pool of sizeM. This is a generalization of the well-knownAND-OR request model. The algorithm is incrementally derived and proven correct. Its communication, computational, and space requirements are lower than those of the best previously known algorithms for the simplerAND-OR model.Gabriel Bracha received his B.Sc. Degree in Mathematics (Computer Science option) from Tel-Aviv University, Israel, in 1980, and his Ph.D. degree in Computer Science from Cornell University, Ithaca, NY, in 1985.In 1985, he joined Daisy System, in Tel-Aviv, Israel, where he is currently a Senior Researcher His current research interests include computational geometry, distributed computing, and fault-tolerance.Partial support for this work was provided by the National Science Foundation under grant MCS 83-03135For photograph and biography see Distributed Computing (1987) 2:80–94     

Atomicm-register operations

Summary We investigate systems where it is possible to access several shared registers in one atomic step. We characterize those systems in which the consensus problem can be solved in the presence of faults and give bounds on the space required. We also describe a fast solution to the mutual exclusion problem using atomicm-register operations. Michael Merritt received a B.S. degree in Philosophy and in Computer Science from Yale College in 1978, the M.S. and Ph. D. degrees in Information and Computer Science in 1980 and 1983, respectively, from the Georgia Institute of Technology. Since 1983 he has been a member of technical staff at AT&T Bell Laboratories, and has taught as an adjunct or visiting lecturer at Stevens Institute of Technology and Columbia University. In 1989 he was program chair for the ACM Symposium on Principles of Distributed Computing. His research interests include distributed and concurrent computation, both algorithms and formal methods for verifying their correctness, cryptography, and security. He is an editor for Distributed Computing and for Information and Computation, recently coauthored a book on database concurrency control algorithms, and is a member of the ACM and of Computer Professionals for Social Responsibility. Gadi Taubenfeld received the B.A., M.Sc. and Ph.D. degrees in Computer Science from the Technion (Israel Institute of Technology), in 1982, 1984 and 1988, respectively. From 1988 to 1990 he was a research scientist at Yale University. Since 1991 he has been a member of technical staff at AT&T Bell Laboratories. His primary research interests are in concurrent and distributed computing.A preliminary version of this workappeared in theProceedings of the Fifth International Workshop on Distributed Algorithms, Delphi, Greece, October 1991, pp 289–294     

Adaptive solutions to the mutual exclusion problem

Summary Algorithms for mutual exclusion that adapt to the current degree of contention are developed. Afilter and a leader election algorithm form the basic building blocks. The algorithms achieve system response times that are independent of the total number of processes and governed instead by the current degree of contention. The final algorithm achieves a constant amortized system response time. Manhoi Choy was born in 1967 in Hong Kong. He received his B.Sc. in Electrical and Electronic Engineerings from the University of Hong Kong in 1989, and his M.Sc. in Computer Science from the University of California at Santa Barbara in 1991. Currently, he is working on his Ph.D. in Computer Science at the University of California at Santa Barbara. His research interests are in the areas of parallel and distributed systems, and distributed algorithms. Ambuj K. Singh is an Assistant Professor in the Department of Computer Science at the University of California, Santa Barbara. He received a Ph.D. in Computer Science from the University of Texas at Austin in 1989, an M.S. in Computer Science from Iowa State University in 1984, and a B.Tech. from the Indian Institute of Technology at Kharagpur in 1982. His research interests are in the areas of adaptive resource allocation, concurrent program development, and distributed shared memory.A preliminary version of the paper appeared in the 12th Annual ACM Symposium on Principles of Distributed ComputingWork supported in part by NSF grants CCR-9008628 and CCR-9223094