Search

The concept of Design for Verifiability is introduced as a means of attacking the complexity problem encountered when verifying the correctness of hardware designs using mathematical proof techniques. The inherent complexity of systems implemented as integrated circuits results in a comparable descriptive complexity when modelling them in any framework which supports formal verification. Performing formal verification then rapidly becomes intractable as a consequence of this descriptive complexity. In this paper we propose a strategy for dealing, at least in part, with this problem. We advocate the use of a particular design strategy involving the use of structural design rules which constrain the behaviour of a design resulting in a less complex design verification. The term Design for Verifiability is used to capture this concept in an analogous way to the term Design for Testability. [ABSTRACT FROM AUTHOR]

A logic simulator can prove the correctness of a digital circuit when it can be shown that only circuits implementing the system specification will produce a particular response to a sequence of simulation commands. By simulating a circuit symbolically, verification can avoid the combinatorial explosion that would normally occur when evaluating circuit operation over many combinations of input and initial state. In this paper, we describe our methodology for verifying synchronous circuits using the stack circuit of Mead and Conway as an illustrative example. [ABSTRACT FROM AUTHOR]

Circuits are not designed to work in all environments: a contract exists between a circuit and the environments in which it correctly operates. The contract is specified by constraints, predicates that must be satisfied by the inputs supplied to the circuit by its environment. A verifier employs contraints during verification to ignore behaviors that will not arise. This paper systematically investigates constraints. We show that: the standard verification condition needs to be revamped to avoid technical and philosophical problems; that there are two important classes of constraints; that one of these classes can be automatically generated; and that constraints arise from an interaction between models and abstractions. [ABSTRACT FROM AUTHOR]

The promise of cost savings and guaranteed product reliability that have been claimed for formal verification of digital hardware have yet to be realised in practice. Largely, this is because it can be extraordinarily difficult and tedious verifying even a simple design. A large part of this difficulty is caused by the absence of much of real-world engineering theory in available theorem provers. The paper describes the formalisation of deterministic and non-deterministic state-machine theory in the HOL theorem prover. Proofs using the theory are not only shorter, but are much more tractable, and follow standard engineering reasoning much more closely than direct proofs without using the theory. [ABSTRACT FROM AUTHOR]

This paper addresses the synthesis of a circuit structure from a sequential behavioral specification. The problem is formally stated as a sequence of behavior-preserving transformations of a data- and control-flow graph. Behavior equivalence is defined strongly, so that it implies equal output sequences for equal input sequences and equal initial state. The transformations introduce the minimum number of control steps. The resulting structure includes both control and data-path. The combinational logic in this structure is passed to logic synthesis for further optimization. Several examples illustrate these techniques, giving results down to the logic level. [ABSTRACT FROM AUTHOR]

We describe a project for synthesizing circuits from a high-level language description. The aims of this project are to guarantee the correctness of the resulting designs while allowing the designer flexibility in interacting with the system. In this paper we discuss two components of the project. The first starts with a state transition system and generates a specification of a datapath and an implementation of a controller as a microcode ROM. The second generates correct CMOS implementations of boolean expressions. This component produces highly optimized circuits which contain transmission gates as well as series and parallel networks of transistors. These two components are part of a larger goal: to go from programs to transistors with a flexible, yet guaranteed correct system. [ABSTRACT FROM AUTHOR]

Many large scale circuits and systems contain a mixture of synchronous and asynchronous (self-timed) subsystems; examples include digital control units and sequencers, processing units that have asynchronous interfaces to busses or memories, and systems that contain modules that are clocked by independent, locally generated clocks. This paper addresses some of the formal issues that arise in the specification and synthesis of such "mixed-mode" systems. In particular, we outline a specification technique suitable for such systems, formalize the notion of timing disciplines in this context, and indicated how the introduction of timing disciplines into a design affect the associated specifications. We also outline the correlations between the semantic models underlying such specifications, called temporally annotated labeled event structures (abbreviated TALES) and timing diagrams that are commonly used for specifying some of the temporal characteristics of interfaces. Some experiments in prototyping some of the implementation strategies for asynchronous, self-timed and mixed-mode systems are summarized. [ABSTRACT FROM AUTHOR]

Logical organization refers to a system's decomposition into functional units, processes, and so on; it is sometimes called the ‘structural' aspect of system description. In an approach to digital synthesis based on functional algebra, logical organization is developed using a class of transformations called system factorizations. These transformations isolate subsystems and encapsulate them as applicative combinators. Factorizations have a variety of uses, ranging from the refinement of actual architecture to the synthesis of certain kinds of verification conditions. This paper outlines the foundations for this algebra and presents several examples. [ABSTRACT FROM AUTHOR]

Clio is a system for verifying properties of expressions written in Caliban, a higher-order polymorphic strongly-typed lazy functional language akin to Turner's Miranda. Clio was designed for verifying each step in the implementation of a program: the specification, the high-level language, the assembly language, the microcode, and the hardware. This paper describes the use of Clio for verifying the correctness of an instruction pipelined microprocessor design. The abstract and the realization levels of behavior of the processor are modeled as infinite streams. The abstract specification describes the behavior in terms of a suitably chosen programmer's model of the processor. A realization specification gives a description of the design of the processor by describing the activities that happen in the circuit over a single microcycle. We develop a general criterion of correctness to relate the two levels which is verified using a form of fixed-point induction. [ABSTRACT FROM AUTHOR]

Until recently, algorithms for deciding bisimulation equivalence between normed context-free processes have all been nondeterministic. The optimal such algorithm, due to Huynh and Tian, is in Σ2P=NPNP: it guesses a proof of equivalence and validates this proof in polynomial time using oracles freely answering questions which are in NP. Hirshfeld, Jerrum and Moller have since demonstrated that this problem is actually decidable in polynomial time. However, this algorithm is far from being practical, giving a O(n13) algorithm, where n is (roughly) the size of the grammar defining the processes, that is, the number of symbols in its description. In this paper we present a deterministic algorithm which runs in time O(n4v) where v is the norm of the processes being compared, which corresponds to the shortest distance to a terminating state of the process, or the shortest word generated by the corresponding grammar. Though this may be exponential, it still appears to be efficient in practice, when norms are typically of moderate size. Also, the algorithm tends to behave well even when the norm is exponentially large. Furthermore, we believe that the techniques may lead to more efficient polynomial algorithms; indeed we have not been able to find an example for which our optimised algorithm requires exponential time. [ABSTRACT FROM AUTHOR]

In this paper we extend some of the results presented by German and Sistla in [4]. Their framework for concurrent systems, at a certain level of abstraction, is suitable for modeling a number of resource-oriented problems in concurrency in which there is a unique control process (called the synchronizer) and an arbitrary number of identical user processes [13, 2]. Communication between processes is via synchronous actions in the style of Milner's Calculus of Communicating Systems [12]. In the first part of the paper, we consider certain "specialized" execution semantics instead of the "general" execution semantics considered in [4]. These semantics are aimed at "restricting" communications between processes that would otherwise be possible. Without such restrictions, it is not possible to model problems in which there is a need to distinguish processes based on either the current states of the user processes, or their indices, etc. In contrast to the work done in [4], we show that the reachability problem for each of the specialized execution semantics we consider is undecidable. As a consequence, both deadlock detection and the Model Checking problem for the synchronizer when reasoning with logics such as Linear temporal logic LTL [4], Linear Temporal Logic without the nexttime operator LTL/X [8], and Restricted Temporal Logic RTL [14] are also undecidable. In the second part of the paper we consider the problem of detecting whether there are infinitely many model sizes k such that some execution of k user processes and the synchronizer deadlocks, assuming unrestricted execution semantics, and we show that this problem is decidable. This result extends a known result, namely, that detecting a single instance of deadlock in such a model, is decidable [4]. We say that models exhibit "strong stability" if and only if there are a "bounded" number of model sizes for which a potential deadlock exists, and thus we show that that detecting strong stability is decidable. We also consider a framework in which we allow an arbitrary number of synchronizers to participate in an execution, and show that strong stability is decidable in this case as well. [ABSTRACT FROM AUTHOR]

In this paper, we consider a strict generalization of context-free processes, the pushdown processes, which are particularly interesting for three reasons: First, in contrast to context-free processes that do not support the construction of distributed systems, they are closed under parallel composition with finite state systems. Second, they are the smallest extension of context-free processes allowing parallel composition with finite state processes. Third, they can be model checked by means of an elegant adaptation to pushdown automata of the second order model checker introduced in [BuS92]. As arbitrary parallel composition between context-free processes provides Turing power, and therefore destroys every hope for automatic verification, pushdown processes can be considered as the appropriate generalization of context-free processes for frameworks for automatic verification. [ABSTRACT FROM AUTHOR]

Decidability of modal logics is not limited to finite systems. The alternationfree mu-calculus can be model checked for sequential systems given in a context-free form (or even a more general one). But the parallel composition of such systems introduces undecidabilities. Nevertheless, several instances can be handled as it is shown in this paper. The known model check techniques prove to be not extendable to parallel compositions. A new tableau system is introduced which is complete in the sequential case and for parallel compositions involving at most one infinite system. The verification of a queue which results from the parallel composition of two (context-free) stacks demonstrates its ability to cope with nontrivial compositions of infinite systems, too. [ABSTRACT FROM AUTHOR]

In this paper we address the problem of solving recursive domain equations using uncountable limits of domains. These arise for instance, when dealing with the ω1-continuous function-space constructor and are used in the (generative) denotational semantics of programming languages which feature non-deterministic fair constructs implemented with unbounded choice. It is well known that such features cannot be modeled using just Scott-continuous functions; they can be modeled conveniently, instead, using functions which satisfy the weaker continuity property of ω1-continuity. Surprisingly, the category of cpo's and ω1-continuous embeddings is not ω0-cocomplete. Hence the standard technique of Adámek and Koubek for solving reflexive domain equations involving these constructs fails. This phenomenon was not noticed before in the literature. We discuss two alternative methods that can be used to solve the required domain equations. The first one is an application of the method of Adámek and Koubek to a different category. The second one, instead, is a genuine extension of their method and amounts to considering cones instead of limits. We put both methods on solid categorical grounds and discuss some applications. Finally we utilise the second method in order to give a model for the untyped λ-calculus whose theory is precisely the λβη theory. Thus we show that ω1-lambda models are complete for the λβη-calculus. [ABSTRACT FROM AUTHOR]

In classical applied mathematics time is treated as an independent variable. The equations which govern the behaviour of a system enable one to determine, in principle, what happens at a given time. This approach has led to powerful techniques for calculating numerical quantities of interest in engineering. The temporal behaviour of reactive systems, however, is difficult to treat from this viewpoint and it has been customary to rely on logical rather than dynamic methods. In this paper we describe the theory of min-max functions, [6, 11, 15], which permits a dynamic approach to the time behaviour of a restricted class of reactive systems. Our main result is a proof of the Duality Conjecture for min-max functions of dimension 2. [ABSTRACT FROM AUTHOR]

The Petri Box Calculus (PBC), based on Milner's CCS, has been developed to provide a compositional semantics of high level programming constructs in terms of a class of Petri nets with interfaces, called Petri Boxes. In this paper we present a structural operational semantics for Box expressions which provide the syntax for the PBC. We show that the use of equations in addition to action rules leads to a uniform theory consisting essentially of a single action rule, a set of context rules, and a set of equations. To capture what is basically the standard Petri net transition rule, we introduce an overbarring and underbarring technique which is related to that used in the event systems due to Boudol and Castellani. We define step sequence rules and show their consistency and completeness with respect to the counterparts from net theory. The results hold also for expressions involving unguarded recursion. [ABSTRACT FROM AUTHOR]

In this paper we study a special operator for sequential composition, which is defined relative to a dependency relation over the actions of a given system. The idea is that actions which are not dependent (intuitively because they share no common resources) do not have to wait for one another to proceed, even if they are composed sequentially. Such a notion has been studied before in a linear-time setting, but until recently there has been no systematic investigation in the context of process algebras. We give a structural operational semantics for a process algebraic language containing such a sequential composition operator, which shows some interesting interplay with choice. We give a complete axiomatisation of strong bisimilarity and we show consistency of the operational semantics with an event-based denotational semantics developed recently by the second author. The axiom system allows to derive the communication closed layers law, which in the linear time setting has been shown to be a very useful instrument in correctness preserving transformations. We conclude with a couple of examples. [ABSTRACT FROM AUTHOR]

This paper embeds durations in an interval temporal logic proposed by Venema. The resulting logic, DCL, is a conservative extension of the original Duration Calculus with two extra chopping operators. In contrast to the original Duration Calculus, DCL can be used to specify and verify abstract liveness and fairness properties of systems. In fact, it is shown that durations are useful for specifying such properties on a dense time domain. The example of a simple oscillator is used to illustrate specification and verification of a simple liveness property. Fairness is illustrated using a Round-Robin scheduler with preemption. The relationship with linear time Temporal Logic is discussed and illustrated using an example of a resource allocator. [ABSTRACT FROM AUTHOR]

This paper presents a new characterization of the bisimulation congruence and D-bisimulation equivalences of the π-calculus. The characterization supports a bisimulation-like proof technique which avoids explicit case analysis by taking a dynamic point of view of actions a process may perform, thus providing a new way of proving bisimulation congruence. The semantic theory of the π-calculus is presented here without the notion of α-equivalence. [ABSTRACT FROM AUTHOR]

This paper presents a framework for the abstract interpretation of processes that pass values. We define a process description language that is parameterized with respect to the set of values that processes may exchange and show that an abstraction over values induces an abstract semantics for processes. Our main results state that if the abstract value interpretation safely/optimally approximates the ground interpretation, then the resulting abstracted processes safely/optimally approximate those derived from the ground semantics (in a precisely defined sense). As the processes derived from an abstract semantics in general have far fewer states than those derived from a concrete semantics, our technique enables the automatic analysis of systems that lie beyond the scope of existing techniques. [ABSTRACT FROM AUTHOR]

In this paper I characterize a class of infinitasy GSOS specifications, obtained by relaxing some of the finiteness constraints of the original format of Bloom, Istrail and Meyer, which generate regular processes. I then show how the techniques of Aceto, Bloom and Vaandrager can be adapted to give a procedure for converting any such language definition to a complete equational axiom system for strong bisimulation of processes which does not use infinitary proof rules. Equalities between recursive, regular processes can be established in the resulting inference systems by means of standard axioms to unwind recursive definitions, and the so-called Recursive Specification Principle (RSP). [ABSTRACT FROM AUTHOR]

The objective of this paper is to bridge the gap between ACP and TCSP. To this end, ACP is extended with two non-deterministic choice operators in a setting of bisimulation semantics. With these operators, we can express safety properties of systems without the use of silent steps, and we can verify safety properties in a setting in which no assumption on fairness (or unfairness) has been made. [ABSTRACT FROM AUTHOR]

In this paper, we have first considered a number of popular recurrent neural network architectures. Then, two subclasses of general recurrent neural network architectures are introduced. It is shown that all these popular recurrent neural network architectures can be grouped under either of these two subclasses of general recurrent neural network architectures. It is also inferred that these two subclasses of recurrent neural network architectures are distinct, in that it is not possible to transform from one form to the other. Two recently introduced recurrent neural network architectures specifically designed for special purposes, viz., for overcoming long term temporal dependency, and for data structure classifications are also considered. Once the architectural aspects of the class of networks are settled, then one could consider the training aspects. This will be considered in a companion paper [31]. [ABSTRACT FROM AUTHOR]

We have described a series of predictive models which have been developed for capturing some kind of dependency inside non stationary sequences. Although the precise motivations and the inspiration sources for these different models have been multi-fold, they are aimed at the same goal. Other attempts have been developed which we have not described here. An important class of models which uses parametric trajectories is that of Segment Models, a review and a comparison with HMMs may be found in [37]. Up to now, predictive models have not led to better results than classical multi-gaussian HMMs. Most of the time, the experiments reported by the different authors are performed on small sized or limited complexity problems. However, some authors also report excellent performances of some predictive models on different tasks. In the second part of the paper, we have described a non linear predictive HMM, which is based on regressive neural networks. We have presented experiments on two relatively large tasks where the model reaches state of the art performances. [ABSTRACT FROM AUTHOR]

The difference in the complexity of branching and linear model checking has been viewed as an argument in favor of the branching paradigm. In particular, the computational advantage of CTL model checking over LTL model checking makes CTL a popular choice, leading to efficient model-checking tools for this logic. Can we use these tools in order to verify linear properties? In this survey paper we describe two approaches that relate branching and linear model checking. In the first approach we associate with each LTL formula ψ a CTL formula ψA that is obtained from ψ by preceding each temporal operator by the universal path quantifier A. In particular, we characterize when ψ is logically equivalent to ψA. Our second approach is motivated by the fact that the alternation-free Μ-calculus, which is more expressive than CTL, has the same computational advantage as CTL when it comes to model checking. We characterize LTL formulas that can be expressed in the alternation-free Μ-calculus; these arc precisely the formulas that are equivalent to deterministic Büchi automata. We then claim that these results are possibly of theoretical, rather than of practical interest, since in practice, LTL model checkers seem to perform rather nicely on formulas that are equivalent to CTL or alternation-free Μ-calculus formulas. [ABSTRACT FROM AUTHOR]

The paper presents the new computational model of Herbrand engines which combines finite-state control with uninterpreted data and function registers, thus yielding a finite representation of infinite-state machines. Herbrand engines are used to provide a high-level model of out-of-order execution in the design of micro-processors. The problem of verifying that a highly parallel design for out-of-order execution correctly implements the Instruction Set Architecture is reduced to establishing the equivalence of two Herbrand engines. We show that, for a reasonably restricted class of such engines, the equivalence problem is decidable, and present two algorithms for solving this problem. Ultimately, the appropriate statement of correctness is that the out-of-order execution produces the same final state (and all relevant intermediate actions, such as writes to memory) as a purely sequential machine running the same program. [ABSTRACT FROM AUTHOR]

In [18, 19], we presented a theory of concurrent combinators for the asynchronous monadic π-calculus without match or summation operator [7, 16]. The system of concurrent combinators is based on a finite number of atoms and fixed interaction rules, but is as expressive as the original calculus, so that it can represent diverse interaction structures, including polyadic synchronous name passing [23] and input guarded summations [26]. The present paper shows that each of the five basic combinators introduced in [18] is indispensable to represent the whole computation, i.e. if one of the combinators is missing, we can no longer express the original calculus up to weak bisimilarity. Expressive power of several interesting subsystems of the asynchronous π-calculus is also measured by using appropriate subsets of the combinators and their variants. Finally as an application of the main result, we show there is no semantically sound encoding of the calculus into its proper subsystem under a certain condition. [ABSTRACT FROM AUTHOR]

In this paper we propose finding winning strategies of abstract games as an approach to verification problems which permits both a variable level of abstraction and on-the-fly exploration. We describe a generic algorithm which, when instantiated with certain functions specific to the concrete game, computes a winning strategy. We apply this technique to bisimulation and model-checking of value-passing processes, and to timed automata. [ABSTRACT FROM AUTHOR]

Alternating transition systems are a general model for composite systems which allow the study of collaborative as well as adversarial relationships between individual system components. Unlike in labeled transition systems, where each transition corresponds to a possible step of the system (which may involve some or all components), in alternating transition systems, each transition corresponds to a possible move in a game between the components. In this paper, we study refinement relations between alternating transition systems, such as "Does the implementation refine the set A of specification components without constraining the components not in A?" In particular, we generalize the definitions of the simulation and trace containment preorders from labeled transition systems to alternating transition systems. The generalizations are called alternating simulation and alternating trace containment. Unlike existing refinement relations, they allow the refinement of individual components within the context of a composite system description. We show that, like ordinary simulation, alternating simulation can be checked in polynomial time using a fixpoint computation algorithm. While ordinary trace containment is PSPACE-complete, we establish alternating trace containment to be EXPTIME-complete. Finally, we present logical characterizations for the two preorders in terms of ATL, a temporal logic capable of referring to games between system components. [ABSTRACT FROM AUTHOR]

This paper presents a complete axiomatization of fully decidable propositional real-time linear temporal logics with past: the Event Clock Logic (ECL) and the Metric Interval Temporal Logic with past (MITL). The completeness proof consists of an effective proof building procedure for ECL. From this result we obtain a complete axiomatization of MITL by providing axioms translating MITL formulae into ECL formulae, the two logics being equally expressive. Our proof is structured to yield a similar axiomatization and procedure for interesting fragments of these logics, such as the linear temporal logic of the real numbers (LTR). [ABSTRACT FROM AUTHOR]

During the last decade, CCS has been extended in different directions, among them priority and real time. One of the most satisfactory results for CCS is Milner's complete proof system for observational congruence [28]. Observational congruence is fair in the sense that it is possible to escape divergence, reflected by an axiom recX.(Τ.X + P)=recX.Τ.P. In this paper we discuss observational congruence in the context of interactive Markov chains, a simple stochastic timed variant CCS with maximal progress. This property implies that observational congruence becomes unfair, i.e. it is not always possible to escape divergence. This problem also arises in calculi with priority. So, completeness results for such calculi modulo observational congruence have been unknown until now. We obtain a complete proof system by replacing the above axiom by a set of axioms allowing to escape divergence by means of a silent alternative. This treatment can be profitably adapted to other calculi. [ABSTRACT FROM AUTHOR]

The dynamics of many calculi can be most clearly defined by a reduction semantics. To work with a calculus, however, an understanding of operational congruences is fundamental; these can often be given tractable definitions or characterisations using a labelled transition semantics. This paper considers calculi with arbitrary reduction semantics of three simple classes, firstly ground term rewriting, then left-linear term rewriting, and then a class which is essentially the action calculi lacking substantive name binding. General definitions of labelled transitions are given in each case, uniformly in the set of rewrite rules, and without requiring the prescription of additional notions of observation. They give rise to bisimulation congruences. As a test of the theory it is shown that bisimulation for a fragment of CCS is recovered. The transitions generated for a fragment of the Ambient Calculus of Cardelli and Gordon, and for SKI combinators, are also discussed briefly. [ABSTRACT FROM AUTHOR]

This paper introduces a compositional Hoare logics for reasoning about the correctness of systems composed of a dynamically evolving collection of processes (also called objects) which interact only via an asynchronous communication mechanism based on FIFO buffers. [ABSTRACT FROM AUTHOR]

In this paper we solve the following problem: "given a digital circuit composed of gates whose real-valued delays are in an integer-bounded interval, is there a way to discretize time while preserving the qualitative behavior of the circuit?" This problem is described as open in [BS94]. When "preservation of qualitative behavior" is interpreted in a strict sense, as having all original sequences of events with their original ordering we obtain the following two results:1)For acyclic (combinatorial) circuits whose inputs change only once, the answer is positive: there is a constant δ, depending on the maximal number of possible events in the circuit, such that if we restrict all events to take place at multiples of δ, we still preserve qualitative behaviors.2)For cyclic circuits the answer is negative: a simple circuit with three gates can demonstrate a qualitative behavior which cannot be captured by any discretization. Nevertheless we show that a weaker notion of preservation, similar to that of [HMP92], allows in many cases to verify discretized circuits with δ=1 such that the verification results are valid in dense time. [ABSTRACT FROM AUTHOR]

In this paper, we present a partial-order reduction method for timed systems based on a local-time semantics for networks of timed automata. The main idea is to remove the implicit clock synchronization between processes in a network by letting local clocks in each process advance independently of clocks in other processes, and by requiring that two processes resynchronize their local time scales whenever they communicate. A symbolic version of this new semantics is developed in terms of predicate transformers, which enjoys the desired property that two predicate transformers are independent if they correspond to disjoint transitions in different processes. Thus we can apply standard partial order reduction techniques to the problem of checking reachability for timed systems, which avoid exploration of unnecessary interleavings of independent transitions. The price is that we must introduce extra machinery to perform the resynchronization operations on local clocks. Finally, we present a variant of DBM representation of symbolic states in the local time semantics for efficient implementation of our method. [ABSTRACT FROM AUTHOR]

Petri nets with read arcs are investigated w.r.t their unfolding, where read arcs model reading without consuming, which is often more adequate than the destructive-read-and-rewrite modelled with loops in ordinary nets. The paper redefines the concepts of a branching process and unfolding for nets with read arcs and proves that the set of reachable markings of a net is completely represented by its unfolding. The specific feature of branching processes of nets with read arcs is that the notion of a co-set is no longer based only on the binary concurrency relation between the elements of the unfolding, contrary to ordinary nets. It is shown that the existing conditions for finite prefix construction (McMillan's one and its improvement by Esparza et al.) can only be applied for a subclass of nets with read arcs, the so-called read-persistent nets. Though being restrictive, this subclass is sufficiently practical due to its conformance to the notion of hazard-freedom in logic circuits. The latter appear to be one of the most promising applications for nets with read arcs. [ABSTRACT FROM AUTHOR]

The mixed product gives a global representation of concurrent systems modelled by interacting automata. In this paper we study the opposite operation: we characterise the transition systems which may be viewed as products and we build some of their decompositions. For a large subclass of systems, we exhibit a minimal decomposition. We finally extend this study to asynchronous automata whose components may be non-deterministic and present an optimal characterisation of the corresponding transition systems. Thus, we state precisely the shape of the transition systems which are associated to three kinds of system; in that way, we obtain axioms which are similar to those identified for the synthesis problem of Petri nets. [ABSTRACT FROM AUTHOR]

The explosion of the web has led to a situation where a majority of the traffic on the Internet is web related. Today, practically all of the popular web sites arc served from single locations. This necessitates frequent long distance network transfers of data (potentially repeatedly) which results in a high response time for users, and is wasteful of the available network bandwidth. Moreover, it commonly creates a single point of failure between the web site and its Internet provider. This paper presents a new approach to web replication, where each of the replicas resides in a different part of the network, and the browser is automatically and transparently directed to the "best" server. Implementing this architecture for popular web sites will result in a better response-time and a higher availability of these sites. Equally important, this architecture will potentially cut down a significant fraction of the traffic on the Internet, freeing bandwidth for other uses. [ABSTRACT FROM AUTHOR]

In the totally anonymous shared memory model of asynchronous distributed computing, processes have no id's and run identical programs. Moreover, processes have identical interface to the shared memory, and in particular, there are no single-writer registers. This paper assumes that processes do not fail, and the shared memory consists only of read/write registers, which are initialized to some default value. A complete characterization of the functions and relations that can be computed within this model is presented. The consensus problem is an important relation which can be computed. Unlike functions, which can be computed with two registers, the consensus protocol uses a linear number of shared registers and rounds. The paper proves logarithmic lower bounds on the number of registers and rounds needed for solving consensus in this model, indicating the difficulty of computing relations in this model. [ABSTRACT FROM AUTHOR]

In this paper we present failure detectors that detect transient failures, i.e. corruption of the system state without corrupting the program of the processors. We distinguish task which is the problem to solve, from implementation which is the algorithm that solve the problem. A task is specified as a desired output of the distributed system. The mechanism used to produce this output is not a concern of the task but a concern of the implementation. In addition we are able to classify both the distance locality and the history locality property of tasks. The distance locality is related to the diameter of the system configuration that a failure detector has to maintain in order to detect a transient fault. The history locality is related to the number of consecutive system configurations that a failure detector has to maintain in order to detect a transient fault. [ABSTRACT FROM AUTHOR]

The paper addresses the problem of solving classic distributed algorithmic problems under the practical model of Broadcast Communication Networks. Our main result is a new Leader Election algorithm, with O(n) time complexity and O(n · lg(n)) message transmission complexity. Our distributed solution uses a special form of the propagation of information with feedback (PIF) building block tuned to the broadcast media, and a special counting and joining approach for the election procedure phase. The latter is required for achieving the linear time. It is demonstrated that the broadcast model requires solutions which are different from the classic point to point model. [ABSTRACT FROM AUTHOR]

This paper presents protocols for Byzantine agreement, i.e. for reliable broadcast, among a set of n players, some of which may be controlled by an adversary. It is well-known that Byzantine agreement is possible if and only if the number of cheaters is less than n/3. In this paper we consider a general adversary that is specified by a set of subsets of the player set (the adversary structure), and any one of these subsets may be corrupted by the adversary. The only condition we need is that no three of these subsets cover the full player set. A result of Hirt and Maurer implies that this condition is necessary and sufficient for the existence of a Byzantine agreement protocol, but the complexity of their protocols is generally exponential in the number of players. The purpose of this paper is to present the first protocol with polynomial message and computation complexity for any (even exponentially large) specification of the adversary structure. This closes a gap in a recent result of Cramer, Damgård and Maurer on applying span programs to secure multi-party computation. [ABSTRACT FROM AUTHOR]

The (n, k, l)-renaming problem requires that names from the set {1,..., l} are assigned to processes from a set of size n, provided that no more than k ≤ l processes axe simultaneously either holding or trying to acquire a name. A solution to this problem supplies a renaming object supporting both acquire and release operations so that no two processes ever simultaneously hold the same name. The protocol is waitfree if each participant successfully completes either operation in a bounded number of its own steps regardless of the speed of other processes; it is long-lived if it there is no bound on the number of operations that can be applied to the object; it is fast if the number of steps taken by any process before it completes an operation is independent of n; and it is name-space-optimal if l = k. This paper presents the first renaming algorithm for atomic read/write registers that is waitfree, long-lived, fast, and name-space-optimal. Since optimal name space is impossible for deterministic renaming algorithms, our algorithm is randomized. The maximum number (over schedulers and processes) of the expected number (over coin flips) of accesses to read/write registers required to complete either an acquire or release operation is θ(k2). We also define a notion of amortized expected complexity that measures the throughput of a system. The amortized expected step complexity of the new renaming algorithm is θ(k log k), which is a substantial improvement, in this amortized sense, over any preceding long-lived renaming algorithm for read/write registers (whether name-space-optimal or not). The notion of amortized complexity of waitfree protocols may be of independent interest since it seems to suggest that waitfreedom may not be as impractical as is sometimes suspected. [ABSTRACT FROM AUTHOR]

Loop agreement is a family of wait-free tasks that includes set agreement and approximate agreement tasks. This paper presents a complete classification of loop agreement tasks. Each loop agreement task can be assigned an algebraic signature consisting of a finitely-presented group G and a distinguished element g in G. This signature completely characterizes the task's computational power. If G and H are loop agreement tasks with respective signatures 〈G, g〉 and 〈H, h〉, then G implements H if and only if there exists a group homomorphism Φ: G → H carrying g to h. [ABSTRACT FROM AUTHOR]

Certain types of system faults, notably data errors due to transient faults, can be repaired by software. The repair consists of identifying faulty variables and then rewriting data to correct the fault. If fault identification is imprecise, repair procedures can contaminate non faulty processes from data originating at faulty processes. This contamination danger is resolved by delaying data correction for a sufficiently long period. In order to delay correction, processes use a repair timer. This paper considers the problem of how asynchronous processes can implement a repair timer that is itself subject to faults. The main results are requirement specifications for a distributed repair timer and a repair timer algorithm. The algorithm self-stabilizes in O(D) rounds, where D is the diameter of the network, and provides reliable timing from k-faulty configurations within O(k) rounds. [ABSTRACT FROM AUTHOR]

In Java, some memory updates are necessarily visible to some threads but never to others. A definition of Java memory consistency must take this fact into consideration to capture the semantics of non-terminating systems, such as a Java operating system. This paper presents a programmer-centered formal definition of Java memory behavior that captures those semantics. Our definition is employed to prove that it is impossible to provide fundamental process coordination in Java, such as critical sections and producer/consumer coordination, without the use of the synchronized and volatile constructs. However, we introduce a form of synchronization that is weaker than volatiles and would suffice to solve some of these problems in Java. [ABSTRACT FROM AUTHOR]

We consider three popular types of shared memory that support one of the following sets of operations: {CAS, read, write}, {LL, SC, VL, read, write}, or {RLL, RSC, read, write}. We present algorithms that, together with Moir's [Moi97], efficiently implement each shared memory above from any of the other two. Our implementations are wait-free and have constant time and space complexity. Thus, concurrent programs developed for one of the above memories can be ported to any other without incurring any increase in time complexity. Further, since our implementations are wait-free, a wait-free concurrent program remains wait-free even after porting. This work is similar in spirit to [IR94, AM95, Moi97]. The main difference is that in these earlier works the write operation is not included in the set of implemented operations. Specifically, earlier works implement {CAS, read} from {LL, SC} and vice versa, but to our knowledge there are no existing implementations of either of {CAS, read, write} and {LL, SC, VL, read, write} from the other. Consequently, it is not possible to port concurrent programs between systems supporting {CAS, read, write} and {LL, SC, VL, read, write}. The implementations in this paper help overcome this drawback. At first glance, adding write to the set of implemented operations might appear easy. However, there is ample evidence to suggest that simple modifications to earlier implementations do not work. Our implementations are therefore quite different from the ones in earlier works. [ABSTRACT FROM AUTHOR]

We present deadlock-free packet (wormhole) routing algorithms based on multi-dimensional interval schemes for certain multiprocessor interconnection networks and give their analysis in terms of the compactness and the size (the maximum number of buffers per node (per link)). The issue of a simultaneous reduction of the compactness and the size is fundamental, worth to investigate and of practical importance, as interval routing and wormhole routing have been realized in INMOS Transputer C104 Router chips. In this paper we give an evidence that for some well-known interconnection networks there are efficient deadlock-free multidimensional interval routing schemes (DFMIRS) despite of a provable nonexistence of efficient deterministic shortest path interval routing schemes (IRS). For d-dimensional butterflies we give a d-dimensional DFMIRS with constant compactness and size, while each shortest path IRS is of the compactness at least 2d/2. For d-dimensional cube connected cycles we show a d-dimensional DFMIRS with compactness and size polynomial in d, while each shortest path IRS needs compactness at least 2d/2. For d-dimensional hypercubes (tori) we present a d-dimensional DFMIRS of compactness 1 and size 2 (4), while for shortest path IRS we can achieve the reduction to 2 (5) buffers with compactness 2d−1 (O(nd−1)). We also present a nonconstant lower bound (in the form √d) on the size of deadlock-free packet routing (based on acyclic orientation covering) for a special set of routing paths on d-dimensional hypercubes. [ABSTRACT FROM AUTHOR]

The bandwidth demands on the World Wide Web continue to grow at an exponential rate. To address this problem, many research activities are focusing on the design of Web caches. Unfortunately, Web caches exhibit poor performance with a hit rate of about 30%. A solution to improve this rate, consists of groups of cooperating caches. In its most general form, a cooperative cache system includes protocols for hierarchical and transversal caching. Although such a system brings better performance, its drawback lies in the resulting network load due to the number of messages that need to be exchanged to locate an object. This paper introduces a new protocol for transversal cooperative caching, which significantly reduces the associated network load compared to that induced by existing systems. ... [ABSTRACT FROM AUTHOR]

This paper presents an Optimistic Atomic Broadcast algorithm (OPT-ABcast) that exploits the spontaneous total order message reception property experienced in local area networks, in order to allow fast delivery of messages. The OPT-ABcast algorithm is based on the Optimistic Consensus problem (OPT-Consensus) that allows processes to decide optimistically or conservatively. A process optimistically decides if it knows that the spontaneous total order message reception property holds, otherwise it decides conservatively. We evaluate the efficiency of the OPT-ABcast and the OPT-Consensus algorithms using the notion of latency degree. [ABSTRACT FROM AUTHOR]