Detecting whether a finite execution trace (or a computation) of a distributed program satisfies a given predicate, called predicate detection, is a fundamental problem in distributed systems. It finds applications in many domains such as testing, debugging, and monitoring of distributed programs. However predicate detection suffers from the state explosion problem - the number of possible global states of the program increases exponentially with the number of processes.

Formal verification of Systems-on-Chips (SoCs) is an immense challenge to current industrial practice. Most existent formal verification techniques are extremely computation intensive and produce good results only when used on individual sub-components of SoCs. Without major modifications they are of little e#ectiveness in the SoC world. We attack the problem of SoC verification using an elegant abstraction mechanism, called computation slicing, and show that it enables e#ective temporal property verification on large designs. The technique targets a set of execution sequences, that is exhaustive with respect to an intended subset of system level properties, and automatically finds counter-example execution sequences in case of errors in the design. We have obtained exponential gains in reducing the global state space using a polynomial-time algorithm, and also applied a polynomial-time algorithm for checking global liveness and safety properties. We have successfully applied the technique to verify properties on two high level transaction based designs - the MSI cache coherence protocol and an admittedly academic SoC having a bus arbiter and a parameterizable number of devices connected to a PCI bus backbone.

The predicate control problem involves synchronizing a distributed computation to maintain a given global predicate. In contrast with many popular distributed synchronization problems such as mutual exclusion, readers writers, and dining philosophers, predicate control assumes a look-ahead, so that the computation is an o#-line rather than an on-line input. Predicate control is targeted towards applications such as rollback recovery, debugging, and optimistic computing, in which such computation look-ahead is natural.

In this note, we discuss the applications of lattice theory to solving problems in distributed systems. The rst problem we consider is that of detecting a predicate in a computation, i.e., determining whether there exists a consistent cut of the computation satisfying the given predicate. The second problem involves computing the slice of a computation with respect to a predicate. A slice is a concise representation of all those global states of the computation that satisfy the given predicate. The third problem we consider is that of analyzing a partial order trace of a distributed program to determine whether it satis es the given temporal logic formula.

Global predicate detection is a fundamental problem in distributed computing in the areas of distributed debugging and software fault-tolerance. It requires searching the global state lattice of a computation to determine if any consistent global state satisfies the given predicate. We give an efficient algorithm that perform the lex traversal of the lattice. We also give a space efficient algorithm for the breadth-first-search (BFS) traversal.

We address the problem of how best to get a group of machines on a network to learn of each others existence; this is referred to as the Resource Discovery Problem (RDP). Straightforward algorithms for RDP are slow or have high communication cost. Harchol et al. [3] recently presented name-dropper, a randomized distributed algorithm for RDP which has low time and communication complexity. However, name-dropper has significant limitations - (1.) the use of randomization precludes it from providing a guaranteed bound on runtime, and, more significantly, (2.) it has no mechanism by which convergence can be detected; in order to provide a high probability of convergence, the number of machines on the network must be known a priori to all machines. We present fast-leader, a deterministic distributed algorithm for RDP which overcomes these limitations while matching name-dropper's time and communication costs.

Since radio spectrum is a scarce resource, efficient allocation of frequency channels is critical for the performance of mobile systems. The update approach is a way to allocate radio channels among cells in distributed fashion. In update-based algorithms, each cell maintains its local knowledge about channels available for its use by exchanging messages among cells in its interference neighborhood. The existing update algorithms suffer from high message complexity or high storage overhead. In this paper, we present a distributed update-based algorithm that imposes lower message complexity, while requiring smaller storage overhead than existing algorithms.

This paper discusses efficient detection of global predicates in a distributed program. Previous work in efficient detection of global predicates was restricted to predicates that could be specified as a boolean formula of local predicates. Many properties in distributed systems, however, use the state of channels. In this paper, we introduce the concept of a channel predicate and provide an efficient algorithm to detect any boolean formula of local and channel predicates.

Failure detection is one of the most fundamental modules of any fault-tolerant distributed system. The failure detectors discussed in the literature so far are either impossible to implement in an asynchronous system, or their exact guarantees have not been discussed. We introduce a failure detector called infinitely often accurate failure detector which can be implemented in an asynchronous system. We provide one such implementation and show its application to the fault-tolerant server maintenance problem. We also show that some natural timeout based failure detectors implemented on Unix are not sufficient to guarantee infinitely often accuracy.

In traditional optimistic distributed simulation protocols, a logical process(LP) receiving a straggler rolls back and sends out anti-messages. Receiver of an anti-message may also roll back and send out more anti-messages. So a single straggler may result in a large number of anti-messages and multiple rollbacks of some LPs. In our protocol, an LP receiving a straggler broadcasts its rollback. On receiving this announcement, other LPs may roll back but they do not announce their rollbacks. So each LP rolls back at most once in response to each straggler. Antimessages are not used. This eliminates the need for output queues and results in simple memory management. It also eliminates the problem of cascading rollbacks and echoing, and results in faster simulation. All this is achieved by a scheme for maintaining transitive dependency information. The cost incurred includes the tagging of each message with extra dependency information and the increased processing time upon receiving a message. We also present the similarities between the two areas of distributed simulation and distributed recovery. We show how the solutions for one area can be applied to the other area.

We illustrate a technique for proving properties of distributed programs. Our technique avoids the notion of global time or global state. Furthermore, it does not require any use of temporal logic. All properties are proven using induction on the happenedbefore relation and its complement. We illustrate our technique by providing a formal proof of Lamport's algorithm for mutual exclusion.

A system for specification and proof of distributed programs is presented. The method is based directly on the partial order of local states (poset) and avoids the notions of time and simultaneity. Programs are specified by documenting the relationship between local states which are adjacent to each other in the poset. Program properties are defined by stating properties of the poset. Many program properties can be expressed succinctly and elegantly using this method because poset properties inherently account for varying processor execution speeds. The system utilizes a proof technique which uses induction on the complement of the causally precedes relation and is shown to be useful in proving poset properties. We demonstrate the system on three example algorithms: vector clocks, mutual exclusion, and direct dependency clocks.

Properties of distributed computations can be either on their global states or on their control flows. This paper addresses control flow properties. It first presents a simple yet powerful logic for expressing general properties on control flows, seen as sequences of local states. Among other properties, we can express invariance, sequential properties (to satisfy such a property a control flow must match a pattern described as a word on some alphabet) and non-sequential properties (these properties are on several control flows at the same time).

We show that the problem of predicate detection in distributed systems is NP-complete. In the past, efficient algorithms have been developed for special classes of predicates such as stable predicates, observer-independent predicates, and conjunctive predicates. We introduce a class of predicates, semi-linear predicates, which properly contains all of the above classes.

We present an efficient algorithm to detect if the conjunction of two nonlocal predicates is possibly true in a distributed computation. For offline detection of such global predicates, our algorithm is significantly more efficient than the previous algorithms by Cooper and Marzullo, and by Stoller and Schneider.

computations is a fundamental problem with applications in distributed monitoring systems and faulttolerance. Fidge and Mattern's vector clocks capture the order relationship with vectors of size N in a system with N processes. Since many distributed applications use synchronous messages, it is natural to ask if the overhead can be reduced for these applications. In this paper, we present a new method of timestamping messages and events in synchronous computations that capture the order relationship with vectors of size less than or equal to the size of the vertex cover of the communication topology of the system. Our method is fundamentally different from that of Fidge and Mattern's technique. The timestamps in our method do not use one component per process but still guarantee that the order relationship is captured accurately. Our algorithm is online and only requires piggybacking of timestamps on program messages. It is applicable to all programs that either use programming languages which use synchronous communication such as CSP, or use synchronous remote procedure calls.

In this paper, we define a max-plus algebra of signals for the evaluation of timing behavior of discrete event systems modeled by timed event graphs. We restrict ourselves to infinite, periodic sequences for which we can compute finite representations called signals. This framework allows us to implement a max-plus algebra for computing supremal controllers for real-time, discrete event systems.

We define and implement a (max,+) algebra of signals for the timing analysis of discrete event systems expressed as timed event graphs. A system is defined by the infinite, periodic time sequences of its events. Each sequence has a finite representations called a signal. The resulting tool can also compute supremal controllers for timed discrete event systems.

We define probabilistic languages and probabilistic automata over a finite set of events. We also define operators under which the set of probabilistic languages(p-languages) is closed, thus forming an algebra of p-languages. We show that this set is a complete partial order and our operators are continuous in it. Hence, recursive equations may be defined in this algebra using fixpoints of continuous functions. Thus, p-languages form a suitable theoretical foundation for specifying and analyzing probabilistic systems. The model can easily be extended for performance analysis by associating timing information with each event. We define many performance indices for systems expressed using this model and derive techniques to compute them. 1 Introduction The theory for supervisory control of discrete event dynamical systems has been an active area of research since its initiation by Ramadge and Wonham [21, 22, 20]. Most research in this area has used theory of deterministic formal languag...

The formalism of probabilistic languages has been introduced for modeling the qualitative behavior of stochastic discrete event systems. A probabilistic language is a unit interval valued map over the set of traces of the system satisfying certain consistency constraints. Regular language operators such as choice, concatenation, and Kleene-closure have been defined in the setting of probabilistic languages to allow modeling of complex systems in terms of simpler ones. The set of probabilistic languages is closed under such operators thus forming an algebra. It also is a complete partial order under a natural ordering in which the operators are continuous. Hence recursive equations can be solved in this algebra. This is alternatively derived by using contraction mapping theorem on the set of probabilistic languages which is shown to be a complete metric space. The notion of regularity, i.e., finiteness of automata representation of probabilistic languages has been defined and shown that...

Fault-tolerance techniques based on checkpointing and message logging have been increasingly used in real-world applications to reduce service downtime. Most industrial applications have chosen pessimistic logging because it allows fast and localized recovery. The price that they must pay, however, is the higher failure-free overhead. In this paper, we introduce the concept of K-optimistic logging where K is the degree of optimism that can be used to fine-tune the tradeoff between failure-free overhead and recovery efficiency. Traditional pessimistic logging and optimistic logging then become the two extremes in the entire spectrum spanned by K-optimistic logging. Our approach is to prove that only dependencies on those states that may be lost upon a failure need to be tracked on-line, and so transitive dependency tracking can be performed with a variable-size vector. The size of the vector piggybacked on a message then indicates the number of processes whose failures may revoke the me...

In this paper we study supervisory control of discrete event systems using state variables for representation and specification. The motivation is two fold: firstly, a state variable representation allows a concise characterization of systems with infinitely many states, and secondly, state variable specification allows characterization of qualitative properties of general nondeterministic systems. An assignment program consisting of state variables and a finite set of conditional assignment statements is used for representing a discrete event system, and a set of forbidden states is used for representing a control specification. Although the state avoidance control of infinite state systems has been studied in literature, there is little work on computation of supervisors for general infinite state systems (except for certain classes of Petri nets). This is not unexpected since as we show, the control synthesis problem is undecidable in general. The contribution of this paper is to s...

In this paper we study supervisory control of discrete event systems using state variables for representation and specification. The motivation is two fold: firstly, a state variable representation allows a concise characterization of systems with infinitely many states, and secondly, state variable specification allows characterization of qualitative properties of general nondeterministic systems. An assignment program consisting of state variables and a finite set of conditional assignment statements is used for representing a discrete event system, and a set of forbidden states is used for representing a control specification. Although the state avoidance control of infinite state systems has been studied in literature, there is little work on computation of supervisors for general infinite state systems (except for certain classes of Petri nets). The contribution of this paper is to show that the supervisory control problem in such settings reduces to that of solving arith...

The class of timed discrete event systems which can be modelled by automata known as timed event graphs are structurally related to finite state machines. Consequently, supervisory control problems for these timed DES can be addressed using methods similar to those developed for their untimed counterparts. When the desired behavior takes the form of minimum separation times between events, it also can be expressed as a timed event graph. Supervised behavior is then defined by the synchronous operation of the plant and specification automata. Controllability and the existence of optimal behaviors can be evaluated in this framework. 1. Introduction Discrete event systems (DES) which are subject to synchronization constraints in time can be modelled by automata known as timed event graphs [2]. A timed event graph (TEG) is a Petri net in which a delay or processing time is associated with each place and such that forks and joins occur only at its transitions. Each transition in the graph ...

Causally ordered message delivery is a required property for several distributed applications particularly those that involve human interactions (such as teleconferencing and collaborative work). In this paper, we present an efficient protocol for causal ordering in mobile computing systems. This protocol requires minimal resources on mobile hosts and wireless links. The proposed protocol is scalable and can easily handle dynamic change in the number of participating mobile hosts in the system. Our protocol, when compared to previous proposals, offers a low unnecessary delay, low message overhead and optimized handoff cost. 1 Introduction The emergence of mobile computing devices, such as notebook computers and personal digital assistants with communication capabilities, has had a significant impact on distributed computing. These devices provide users the freedom to move anywhere under the service area while retaining network connection. However, mobile computing devices have limite...

The traditional Distributed Shared Memory (DSM) model provides atomicity at levels of read and write on single objects. Therefore, multi-object operations such as double compare and swap, and atomic m-register assignment cannot be efficiently expressed in this model. We extend the traditional DSM model to allow operations to span multiple objects. We show that memory consistency conditions such as sequential consistency and linearizability can be extended to this general model. We also provide algorithms to implement these consistency conditions in a distributed system. 1 Introduction Applications such as distributed file systems, transaction systems and cache coherence for multiprocessors require concurrent accesses to shared data. The underlying system must provide certain guarantees about the values returned by data accesses, possibly to distinct copies of a single logical data object. A consistency condition specifies what guarantees are provided by the system. The consistency co...

Debugging distributed programs is considerably more difficult than debugging sequential programs. We address issues in debugging distributed programs and provide a general framework for observing and controlling a distributed computation and its applications to distributed debugging. Observing distributed computations involves solving the predicate detection problem. We present the main ideas involved in developing efficient algorithms for predicate detection. Controlling distributed computations involves solving the predicate control problem. Predicate control may be used to restrict the behavior of the distributed program to suspicious executions. We also present an example of how predicate detection and predicate control can be used in practice to facilitate distributed debugging.

The happened before model has been widely used to model distributed computations. In particular, it has been used to model the logical time and the potential causality aspects of a distributed computation. Though it is a good model for logical time, we argue that it is not a good model for potential causality. We introduce a better model for potential causality that extends happened before to allow independent local events to be partially ordered. This potential causality model has marked advantages over the happened before model in applications areas such as debugging and recovery. 1

In earlier papers [3, 2, 1] we introduced the formalism of probabilistic languages for modeling the stochastic qualitative behavior of discrete event systems (DESs). In this paper we present a framework for their supervisory control, where control is exercised by dynamically disabling certain controllable events. The control objective is to design a supervisor such that the controlled system never executes any illegal traces (their occurrence probability is zero), and legal traces occur with minimum prespecified occurrence probabilities. We provide a condition for the existence of a supervisor. We also present an algorithm to test this existence condition when the probabilistic languages are regular (so that they admit probabilistic automata representation with finitely many states). 1 Introduction The non-stochastic behavior of a discrete event system can be viewed as a binary valued map over the set of all possible sequences of events, called traces. (A trace is mapped to one if an...

In our earlier papers [7, 6, 5] we introduced the formalism of probabilistic languages for modeling the stochastic qualitative behavior of discrete event systems (DESs). We presented a framework for their supervisory control in [11], where control is exercised by dynamically disabling certain controllable events thereby nulling the occurrence probabilities of disabled events, and increasing the occurrence probabilities of enabled events proportionately. The control objective is to design a supervisor such that the controlled system never executes any illegal traces (their occurrence probability is zero), and legal traces occur with minimum prespecified occurrence probabilities. In other words, the probabilistic language of the controlled system lies within a prespecified range, where the upper bound is a

A genetic algorithm was implemented for finding an approximative solution to the problem of fitting a combination of Lorentzian lines to a measured Mossbauer spectrum. This iterative algorithm exploits the idea of letting several solutions (individuals) compete with each other for the opportunity of being selected to create new solutions (reproduction). Each solution was represend as a string of binary digits (chromossome). In addition, the bits in the new solutions may be switched randomly from zero to one or conversely (mutation). The input of the program that implements the genetic algorithm consists of the measured spectrum, the maximum velocity, the peak positions and the expected number of Lorentzian lines in the spectrum. Each line is represented with the help of three variables, which correspond to its intensity, full line width at hald maxima and peak position. An additional parameter was associated to the background level in the spectrum. A chi-2 test was used for determining the quality of each parameter combination (fitness). The results obtained seem to be very promising and encourage to further development of the algorithm and its implementation.

Keywords: genetic algorithms

The formalism of probabilistic languages has been introduced for modeling the qualitative behavior of stochastic discrete event systems. A probabilistic language is a unit interval valued map over the set of traces of the system satisfying certain consistency constraints. Regular language operators such as choice, concatenation, and Kleene-closure have been defined in the setting of probabilistic languages to allow modeling of complex systems in terms of simpler ones. The set of probabilistic languages is closed under such operators thus forming an algebra. It also is a complete partial order under a natural ordering in which the operators are continuous. Hence recursive equations can be solved in this algebra. This is alternatively derived by using contraction mapping theorem on the set of probabilistic languages which is shown to be a complete metric space. The notion of regularity, i.e., finiteness of automata representation of probabilistic languages has been defined and shown that...

Fault-tolerance techniques based on checkpointing and message logging have been increasingly used in real-world applications to reduce service downtime. Most industrial applications have chosen pessimistic logging because it allows fast and localized recovery. The price that they must pay, however, is the higher failure-free overhead. In this paper, we introduce the concept of K-optimistic logging where K is the degree of optimism that can be used to fine-tune the tradeoff between failure-free overhead and recovery efficiency. Traditional pessimistic logging and optimistic logging then become the two extremes in the entire spectrum spanned by K-optimistic logging. Our approach is to prove that only dependencies on those states that may be lost upon a failure need to be tracked on-line, and so transitive dependency tracking can be performed with a variable-size vector. The size of the vector piggybacked on a message then indicates the number of processes whose failures may revoke the me...

Since radio spectrum is a scarce resource, efficient allocation of frequency channels is critical for the performance of mobile computing systems. The update approach is a way to allocate radio channels among cells in distributed fashion. In update-based algorithms, each cell maintains its local knowledge about channels available for its use by exchanging messages among cells in its interference neighborhood. An advantage of the update approach is its low channel acquisition delay, which is defined as the time between the send event of channel requests and the moment that a channel is successfully acquired. However, the existing update algorithms suffer from high message complexity or high storage overhead. In this paper, we present a distributed update-based algorithm that imposes lower message complexity, while requiring smaller storage overhead than existing algorithms. Keywords Distributed channel allocation, mobile computing, distributed network algorithm. 1 Introduction The radi...

A number of important problems in asynchronous distributed systems can be formulated as special cases of the notion of controlling a distributed system to maintain global properties. We formalize this notion by defining the predicate control problem in terms of boolean global predicates and a model of distributed control. The problem arises in both off-line and on-line scenarios. We prove that general off-line predicate control is NP-Hard. However, we present an efficient solution for the class of disjunctive predicates. We show that on-line predicate control, on the other hand, is impossible to achieve even for disjunctive predicates. However, by placing restrictions on the underlying system, we are able to present an effective on-line control strategy. 1 Introduction An intrinsic problem in asynchronous distributed systems is that while no one process can have a global view, we still require the system as a whole to maintain global properties. This conflict has led to the design of...

Keywords: distributed software,

Keywords: short paper,

We propose a new algorithm for recovering asynchronously from failures in a distributed computation. Our algorithm is based on two novel concepts - a fault-tolerant vector clock to maintain causality information in spite of failures, and a history mechanism to detect orphan states and obsolete messages. These two mechanisms together with checkpointing and messagelogging are used to restore the system to a consistent state after a failure of one or more processes. Our algorithm is completely asynchronous. It handles multiple failures and network partitioning, does not assume any message ordering, causes the minimum amount of rollback and restores the maximum recoverable state with low overhead. Earlier optimistic protocols lack one or more of the above properties. 1 Introduction For fault-resilience, a process periodically records its state on a stable storage [15]. This action is called checkpointing and the recorded state is called a checkpoint. The checkpoint is used to restore a pr...

Many problems in distributed computing systems require execution of events shared by multiple processes. In this paper, a fair and efficient algorithm for multiprocess shared events is presented. We also present its application to distributed implementation of generalized CSP alternative command. We show that our algorithm is simpler and has lower message and time complexity than proposed implementations for generalized CSP alternative command, and distributed algorithms for N-party interactions. 1. Introduction Wide availability of computer networks, and low cost of hardware has made it desirable to use distributed systems. Distributed systems, however, are difficult to design and often need tricky synchronization between multiple processes. The synchronization is required to coordinate multiple processes for events, which must be executed either by all, or none of them. Some examples of such shared events are distributed transactions in databases that require commit by either all o...

This paper discusses efficient distributed detection of global conjunctive predicates in a distributed program. Previous work in detection of such predicates is based on a checker process. The checker process requires O(n 2 m) time and space where m is the number of messages sent or received by any process and n is the number of processes over which the predicate is defined. In this paper, we introduce token-based algorithms which distribute the computation and space requirements of the detection procedure. The distributed algorithm has O(n 2 m) time, space and message complexity, distributed such that each process performs O(nm) work. We describe another distributed algorithm with O(Nm) total work, where N is the total number of processes in the system. The relative values of n and N determine which algorithm is more efficient for a specific application. 1 Introduction Detection of a global predicate is a fundamental problem in distributed computing. This problem arises in many ...

This paper discusses detection of global predicates in a distributed program. A run of a distributed program results in a set of sequential traces, one for each process. These traces may be combined to form many global sequences consistent with the single run of the program. A strong global predicate is true in a run if it is true for all global sequences consistent with the run. We present algorithms which detect if the given strong global predicate became true in a run of a distributed program. 1 Introduction Detection of global predicates is a fundamental problem in distributed computing. It arises in the designing, debugging and testing of distributed programs. Global predicates can be classified into two types - stable and unstable. A stable predicate is one which never turns false once it becomes true. An unstable predicate is one without such a property. Its value may alternate between true and false. Detection of stable predicates has been addressed in the literature by means ...

Distributed systems are difficult to design and the simplest of them can have subtle errors. Conventional automatic analysis techniques to catch these errors may be infeasible because the system may have a large, or even an unknown, number of processes. These techniques, which are based on state space exploration, run into the state explosion problem. Since most distributed systems have one or more sets of identical processes, we exploit the symmetry to reduce the state space for automatic analysis techniques. We describe a model called Decomposed Petri Net that facilitates such analysis. We present symbolic and induction techniques to analyze concurrent systems described using Decomposed Petri Net. We illustrate our techniques by analyzing several examples: 2-out-of-3 problem, dining philosophers problem and mutual exclusion problem. These techniques are applicable to systems that are configured either in a star topology or a ring topology. We also show how to extend these techniques ...

Observation of global properties of a distributed program is required in many applications such as debugging of programs and fault-tolerance in distributed systems. I present a survey of algorithms for observing various classes of global properties. These properties include those possibly true in a computation, definitely true in a computation and those based on the control flow structure of the computation.

: Linearizability is a consistency condition for concurrent objects (objects shared by concurrent processes) that exploits the semantics of abstract data types. It provides the illusion that each operation applied by concurrent processes takes effect instantaneously at some point between the beginning and the end of its execution. When compared with other consistency conditions (such as sequential consistency) Linearizability satisfies the Locality property (i.e, a system is linearizable if each object taken individually is linearizable) and the Non-Blocking property (i.e., termination of an invoked operation does not depend on other pending invocations). Those are noteworthy properties as they allow concurrent systems to be designed and constructed in a modular fashion. This paper introduces a consistency condition called Normality that is less constraining than Linearizability (in the sense it does not refer to a global real-time order) and still satisfies Locality and Non-Blocking....

The ability to detect global predicates is important for distributed fault monitoring systems as well as distributed debugging. In this paper, we present an efficient algorithm to detect if the conjunction of two nonlocal predicates is possibly true in a distributed computation. For such global predicates, our algorithm is significantly more efficient than the previous algorithms by Cooper and Marzullo, and by Stoller and Schneider. 1 Introduction The detection of global conditions is a fundamental problem in an asynchronous distributed system. In such a system a process cannot know the state of other processes at any given time. This creates difficulty in detecting conditions, or predicates, spread across the system. Deadlock and termination are two such global predicates. Detection of these predicates is useful for distributed debugging, monitoring distributed systems for faults, and other areas of distributed computing. There are two interpretations of truthness of a global p...

We study the problem of determining which message ordering specifications can be implemented in a distributed system. Further, if a specification can be implemented, we give a technique to determine whether it can be implemented by tagging information with user messages or if it requires control messages. To specify the message ordering, we use a novel method called forbidden predicates. All existing message ordering guarantees such as FIFO, flush channels, causal ordering, and logically synchronous ordering, (as well as many new message orderings) can be concisely specified using forbidden predicates. We then present an algorithm that determines from the forbidden predicate the type of protocol needed to implement that specification. Keywords: Message ordering, forbidden predicate, predicate graph, protocols and specifications. 1 Introduction A distributed computation or a run describes an execution of a distributed program. At an abstract level, a run can be defined as a partiall...

Keywords: book, text, time, mutual exclusion, predicates,

Abstract Linearizability is a consistency condition for concurrent objects (objects shared by concurrent processes) that exploits the semantics of abstract data types. It provides the illusion that each operation applied by concurrent processes takes effect instantaneously at some point between the beginning and the end of its execution. When compared with other consistency conditions (such as sequential consistency) Linearizability satisfies the Locality property (i.e, a system is linearizable if each object taken individually is linearizable) and the Non-Blocking property (i.e., termination of an invoked operation does not depend on other pending invocations). Those are noteworthy properties as they allow concurrent systems to be designed and constructed in a modular fashion. This paper introduces a consistency condition called Normality that is less constraining than Linearizability (in the sense it does not refer to a global real-time order) and still satisfies Locality and Non-Blocking. As it does not refer to a global real-time, Normality is well-suited to objects supported by asynchronous distributed systems and can consequently be seen as an adaptation of Linearizability for these systems.

R'esum'e Cet article pr'esente un crit`ere de coh'erence, appel'e Normalit'e, pour les objets d'efinis `a partir de types abstraits et acc'ed'es par des processus concurrents. La d'efinition est moins contraignante que celle de la lin'earisabilit'e, tout en pr'eservant comme cette derni`ere, les propri'et'es cruciales que sont la localit'e et le non-blocage. La normalit'e est particuli`erement int'eressante car, tout en formalisant la s'emantique intuitive classiquement utilis'ees par les programmeurs, elle ne fait pas r'ef'erence `a un temps physique global et `a ce titre s'adapte naturellement au contexte r'eparti asynchrone.

Keywords: Concurrent Objects, Consistency Condition, Linearizability, Locality Property, Non-Blocking Property, Mots cl'es absence de blocage, coh'erence, lin'earisabilit'e, localit'e, objets concurrents

This paper is a survey of our work on controlling discrete event systems modelled by timed event graphs. Such systems are structurally related to finite state machines in that both can be described by linear equations over an appropriate algebra. Using this structural similarity, we have extended supervisory control techniques developed for untimed DES to the timed case. When behavioral constraints are given as a a range of acceptable schedules, it is possible to compute an extremal controllable subset or superset of the desired behavior. When constraints are expressed in terms of minimum separation times between events, it is possible to determine whether there is a controllable schedule which realizes the desired behavior.

We formalize the notion of optimal supervisory control of discrete event dynamical systems (DEDS's) in the framework of Ramadge and Wonham. A DEDS is modeled as a state machine, and is controlled by disabling some of its transitions. We define two types of cost functions: a cost of control function corresponding to disabling transitions in the state machine, and a penalty of control function corresponding to reaching some undesired states, or not reaching some desired states in the controlled system. The control objective is to design an optimal control mechanism, if it exists, so that the net cost is minimized. Since a DEDS is represented as a state machine-a directed graph-network flow techniques are naturally applied for designing optimal supervisors. We also show that our techniques can be used for solving supervisory control problems under complete as well as partial observation. In particular, we obtain, for the first time, techniques for computing the supremal controllable a...

Many discrete event systems (DESs) such as manufacturing systems, data base management systems, communication networks, traffic systems, etc., can be modeled as input-output discrete event systems (I/O DESs). In this paper we formulate and study the problem of stable realization of such systems in the logical setting. Given an input and an output language describing the sequences of events that occur at the input and the output, respectively, of an I/O DES, we study whether it is possible to realize the system as a unit consisting of a given set of buffers of finite capacity, called a dispatching unit. The notions of stable, conditionally stable, dispatchable and conditionally dispatchable units are introduced as existence of stable (or input-output bounded), and causal (or prefix preserving) input-output maps, and effectively computable necessary and sufficient conditions for testing them are obtained. 1 Introduction and Motivation A discrete event system (DES) is one in which the ...

Earlier work concerning control of discrete event systems usually assumed that a correct model of the system to be controlled was available. A goal of this wok is to provide an algorithm for determining the correct model from a set of models. The result of the algorithm is a finite language which can be used to test for the correct model or notification that the remaining models cannot be controllably distinguished. We use the finite state machine model with controllable and uncontrollable events presented by Ramadge and Wonham 1 . Keywords: Discrete Event Systems, System Identification AMS(MOS) subject classification: 93A,93B Supported in part by National Science Foundation CCR-911065, and in part by the University Research Institute, University of Texas at Austin. 1 A preliminary version of this paper appeared as [18]. Another version will appear in SIAM Journal of Control and Optimization. 1 Introduction A discrete event system (DES) is one which responds to distinct eve...

This paper discusses efficient detection of global predicates in a distributed program. Previous work in efficient detection of global predicates was restricted to predicates that could be specified as a boolean formula of local predicates. Many properties in distributed systems, however, use the state of channels. In this paper, we introduce the concept of a channel predicate and provide an efficient algorithm to detect any boolean formula of local and channel predicates. We define a property called monotonicity for channel predicates. Monotonicity is crucial for efficient detection of global predicates. We show that many problems studied earlier such as detection of termination and computation of global virtual time are special cases of the problem considered in this paper. The message complexity of our algorithm is bounded by the number of messages used by the program. The main application of our results are in debugging and testing of distributed programs. Our algorithms have been ...

This paper discusses efficient detection of global predicates in a distributed program. Previous work in detection of global predicates was restricted to predicates that could be specified as a boolean formula of local predicates. Many properties in distributed systems, however, use the state of channels. In this paper, we introduce the concept of a channel predicate and provide an efficient algorithm to detect any boolean formula of local and channel predicates. We define a property called monotonicity for channel predicates. Monotonicity is crucial for efficient detection of global predicates. We show that many problems studied earlier, such as detection of termination and computation of global virtual time are special cases of the problem considered in this paper. The message complexity of our algorithm is bounded by the number of messages used by the program. The main application of our results are in debugging and testing of distributed programs. Our algorithms have been incorpora...

In this paper we study supervisory control of discrete event systems using state variables for representation and specification. The motivation is two fold: firstly, a state variable representation allows a concise characterization of systems with infinitely many states, and secondly, state variable specification allows characterization of qualitative properties of general nondeterministic systems. An assignment program consisting of state variables and a finite set of conditional assignment statements is used for representing a discrete event system, and a set of forbidden states is used for representing a control specification. The control synthesis problem is undecidable in the general setting. However, in the special case when a single uncontrollable event is present, we show that the problem of computing a maximally permissive supervisor reduces to that of solving an arithmetic equation. Also, in another special case when the system can be represented as a vector addition system...

Keywords: parallel programming,

The behavior of timed DES can be described by sequences of event occurrence times. These sequences can be ordered to form a lattice. Since logical (untimed) DES behaviors described by regular languages also form a lattice, questions of controllability for timed DES may be treated in much the same manner as they are for untimed systems. In this paper we establish conditions for the controllability of timed DES performance specification which are expressed as inequations on the lattice. Thses specifications may take the form of sets of acceptable event occurrence times, maximum or minimum occurrence times, or limits on the separation times between events. Optimal behaviors are found as extremal solutions to these inequations using fixed point results for lattices. Keywords: Discrete event systems, supervisory control, maxalgebra, lattices. Supported in part by NSF Grant CCR-9110605, Army Grant N00039-91-C-0082, a TRW faculty assistantship award, General Motors Fellowship, and an IBM g...

A discrete event system (DES) is a dynamic system which evolves in response to the occurrence of specific events at discrete points in time. Ramadge and Wonham have established a control theory of DES modeled by state machines which has been expanded by others to include the concepts of observability and stability. Previous work by Ramadge extended the concept of controllable languages to infinite languages and presented conditions for the existence of a supervisor for systems modeled by Buchi automata. The goal of this paper is to derive requirements for the existence of a supervisor under less restrictive conditions on the constraint language for plants which satisfy certain conditions. This supervisor is shown to approach the prescribed closed loop behavior and retain all behaviors within a specified error bound of the desired behavior. Both deterministic and nondeterministic supervisors are considered. The construction for such a supervisor is given along with example...

We present algorithms to optimally choose sensors and actuators to control a given discrete event system so that the closed loop behavior satisfies a specified constraint. The main results of this paper are algorithms which demonstrate: the polynomial solution to the choice of actuators, the polynomial solution to the choice of sensors for certain supervisory control problems, and the solution to the general choice of sensors 1 . Keywords: Discrete Event Systems, Observability, Controllability 1 Introduction This work addresses the question of how to choose sensors and actuators to control a discrete event system to attain a specified behavior. Supervision Supported in part by NSF CCR-911065 and TRW Faculty Assistantship Award. y Supported in part by a DuPont Fellowship. 1 A preliminary version of this paper appeared as [18]. of such systems is achieved by observing events and disabling those which are not desired or lead to undesirable behavior. A supervisor uses sensors ...

: Properties of distributed computations can be either on their global states or on their control flows. This paper addresses control flow properties. It first presents a simple yet powerful logic for expressing general properties on control flows, seen as sequences of local states. Among other properties, we can express invariance, sequential properties (to satisfy such a property a control flow must match a pattern described as a word on some alphabet) and non-sequential properties (these properties are on several control flows at the same time). A decentralized detection algorithm for properties described by this logic is then presented. This algorithm, surprisingly simple despite the power of the logic, observes the underlying distributed computation, does not alter its control flows and uses message tags to carry detection-related information. Key-words: behavioral property, distributed computation, distributed debugging, on the fly detection, control flows. (R'esum'e : tsvp) ...

: Properties of distributed computations can be either on their global states or on their control flows. This paper addresses control flow properties. It first presents a simple yet powerful logic for expressing general properties on control flows, seen as sequences of local states. Among other properties, we can express invariance, sequential properties (to satisfy such a property a control flow must match a pattern described as a word on some alphabet) and non-sequential properties (these properties are on several control flows at the same time). A decentralized detection algorithm for properties described by this logic is then presented. This algorithm, surprisingly simple despite the power of the logic, observes the underlying distributed computation, does not alter its control flows and uses message tags to carry detection-related information. Key-words: behavioral property, distributed computation, distributed debugging, on the fly detection, control flows. (R'esum'e : tsvp) ...

: A class of properties of distributed computations is described and an algorithm which detects them is presented. This class of properties called regular patterns allows the user to specify an expected (or unwanted) behavior of a computation as sequences of relevant events (or as sequences of local predicates that must be successively verified). The sequences are defined by a finite state automaton (hence the name regular patterns). A computation verifies the property if and only if one of its causal paths matches a sequence. Key-words: behavioral property, distributed computation, distributed debugging, on the fly detection, regular pattern. (R'esum'e : tsvp) This paper will appear in the proceedings of the 23 th Int. Conf. on Parallel Processing, Pennsylvanie State Univ., August 1994. IRISA - Campus de Beaulieu, 35042 RENNES cedex - FRANCE, e-mail:ffromenti, raynalg@irisa.fr Dept. of ECE - University of Texas at AUstin, Austin TX, e-mail: fvijay,alextg@pine.ece.utexas.edu ...

: A class of properties of distributed computations is described and an algorithm which detects them is presented. This class of properties called regular patterns allows the user to specify an expected (or unwanted) behavior of a computation as sequences of relevant events (or as sequences of local predicates that must be successively verified). The sequences are defined by a finite state automaton (hence the name regular patterns). A computation verifies the property if and only if one of its causal paths matches a sequence. Key-words: behavioral property, distributed computation, distributed debugging, on the fly detection, regular pattern. (R'esum'e : tsvp) This paper will appear in the proceedings of the 23 th Int. Conf. on Parallel Processing, Pennsylvanie State Univ., August 1994. IRISA - Campus de Beaulieu, 35042 RENNES cedex - FRANCE, e-mail:ffromenti, raynalg@irisa.fr Dept. of ECE - University of Texas at AUstin, Austin TX, e-mail: fvijay,alextg@pine.ece.utexas.edu...

This paper develops a method for maintaining global assertions on a network of distributed processes. The global assertion has the form (X 1 1 X 1 2 Delta Delta Delta X 1 N 1 ) + : : : + (X M 1 X M 2 Delta Delta Delta X M NM ) K, where X j i is a variable which is local to one process in a distributed system and K is a constant. It is assumed that the initial values of all local variables are known and that the global assertion initially holds. This form is more general than the summation form considered in earlier work. This research has applications in distributed software development, and as a general synchronization mechanism. Many classical synchronization problems (mutual exclusion, dining philosophers, readers /writers) can be solved with the results of this work. Research supported in part by NSF Grant CCR 9110605, Navy Grant N00039-88-C-0082, TRW faculty assistantship award, IBM Agreement 153, and a Microelectronics Computer Development Fellowship. 1 Intr...

This paper discusses efficient detection of global predicates in a distributed program. Previous work in efficient detection of global predicates was restricted to predicates that could be specified as a boolean formula of local predicates. Many properties in distributed systems, however, use the state of channels. In this paper, we introduce the concept of a channel predicate and provide an efficient algorithm to detect any boolean formula of local and channel predicates. We define a property called monotonicity for channel predicates. Monotonicity is crucial for efficient detection of global predicates. We show that many problems studied earlier such as detection of termination and computation of global virtual time are special cases of the problem considered in this paper. The message complexity of our algorithm is bounded by the number of messages used by the program. The main application of our results are in debugging and testing of distributed programs. Our algorithms ...

We illustrate a technique for proving properties of distributed programs. Our technique avoids the notion of global time or global state. Furthermore, it does not require any use of temporal logic. All properties are proven using induction on the happenedbefore relation and its complement. We illustrate our technique by providing a formal proof of Lamport's algorithm for mutual exclusion. 1 Introduction We define a distributed system as a collection of processors geographically distributed which do not share any memory or clock. Further, it is assumed that different clocks cannot be perfectly synchronized due to uncertainty in communication delays. The importance of distinction between causality and time in such an environment was first emphasized by Leslie Lamport in [9]. It is now well understood that the concept of time can be replaced by that of causality with many advantages. For example, even though it is impossible to detect a global property that became true at some physical t...

The domain of a global function is the set of all global states of an execution of a distributed program. We show how to monitor a program in order to determine if there exists a global state in which the sum x 1 +x 2 + : : : +xN exceeds some constant K, where x i is defined in process i. We examine the cases where x i is an integer variable and where x i is a boolean variable. For both cases we provide algorithms, prove their correctness and analyze their complexity. 1 Introduction As a distributed program executes, each process proceeds through a sequence of local states. The set S of all local states is partially ordered by Lamport's happens before relation[Lam78], denoted by !. A global state is a subset of S in which no two elements are ordered by !. Given a global state c of some execution, it is impossible to determine if c actually occurred in an execution. However, it is known that c is consistent with some global state that did occur in the execution [CL85, Mat89]. In ot...

: A class of properties of distributed computations is described and an algorithm which detects them is presented. This class of properties called regular patterns allows the user to specify an expected (or unwanted) behavior of a computation as sequences of relevant events (or as sequences of local predicates that must be successively verified). The sequences are defined by a finite state automaton (hence the name regular patterns). A computation verifies the property if and only if one of its causal paths matches a sequence. Key-words: behavioral property, distributed computation, distributed debugging, on the fly detection, regular pattern. (R'esum'e : tsvp) This paper will appear in the proceedings of the 23 th Int. Conf. on Parallel Processing, Pennsylvanie State Univ., August 1994. IRISA - Campus de Beaulieu, 35042 RENNES cedex - FRANCE, e-mail:ffromenti, raynalg@irisa.fr Dept. of ECE - University of Texas at AUstin, Austin TX, e-mail: fvijay,alextg@pine.ece.utexas.edu ...

Global virtual time (GVT) is used in distributed simulations to reclaim memory, commit output, detect termination, and handle errors. It is a global function that is computed many times during the course of a simulation. A small GVT latency (delay between its occurrence and detection) allows for more efficient use of resources. We present an algorithm which minimizes the latency, and we prove its correctness. The algorithm is unique in that a target virtual time (TVT) is predetermined by an initiator who then detects when GVT TVT. This approach eliminates the avalanche effect because the collection phase is spread out over time, and it allows for regular and timely GVT updates.

This paper develops a method for maintaining global assertions on a network of distributed processes. The global assertion has the form (X N 1 ) + : : : + NM ) K, where X i is a variable which is local to one process in a distributed system and K is a constant. It is assumed that the initial values of all local variables are known and that the global assertion initially holds. This form is more general than the summation form considered in earlier work.

This paper studies the characteristics of synchronous ordering of messages. Synchronous ordering of messages defines synchronous communication based on the causality relation rather than time. We present the necessary characteristics of any algorithm providing deadlock-free synchronous ordering of the messages. We also present the sufficient conditions, based on the causality relations, for any algorithm to provide synchronous ordering. The paper proposes an algorithm using acknowledgment messages to implement the sufficient conditions. The acknowledgment messages are used to satisfy the causality relation between the events. The algorithm is deadlock-free, and provides a higher degree of concurrency then the algorithms which define synchronous communication based on time. 1 Introduction Distributed programs are difficult to design and test due to their non-deterministic nature. That is, a distributed program may exhibit multiple behaviors on the same external input. This nondetermini...