We present methods to compute least fixed points of multiple monotone inflationary functions in parallel and distributed settings. While the classic Knaster-Tarski theorem addresses a single function with sequential iteration, modern computing systems require parallel execution with overwrite semantics, non-atomic updates, and stale reads. We prove three convergence theorems under progressively relaxed synchronization: (1) Interleaving semantics with fair scheduling, (2) Parallel execution with update-only-on-change semantics (processes write only on those coordinates whose values change), and (3) Distributed execution with bounded staleness (updates propagate within T rounds) and i-locality (each process modifies only its own component).

The atomic snapshot object (ASO) can be seen as a generalization of the atomic read/write register. ASO divides the object into$n$segments such that each node can update its own segment, and instantaneously scan all segments of the object. ASO is a powerful data structure that has many important applications, such as update-query state machines, linearizable conflict-free replicated data types, generalized lattice agreement, and cryptocurrency as in the form of an asset transfer object. This paper studies ASO in asynchronous message passing systems and proposes a framework for implementing efficient fault-tolerant snapshot objects. Denote by$D$the maximum message delay and$k$the actual number of failures in an execution. Our framework derives two ASO algorithms: •A crash-tolerant ASO algorithm that achieves O(√k. D) time complexity for both update and scan operations, and achieves amortized constant time operations if there are Ω(√k) operations. •A Byzantine ASO algorithm that achieves O(k.D) time complexity for both update and scan operations, and achieves amortized constant time operations if there is no Byzantine node in a given execution. The framework can also be adapted to implement sequentially consistent snapshot objects (SSO) that complete scan operations locally without any communication, and have the same time complexlty for update onerations as in our ASO algorithms.

The popular matching problem is of matching a set of applicants to a set of posts, where each applicant has a preference list, ranking a non-empty subset of posts in the order of preference, possibly with ties. A matching M is popular if there is no other matching M' such that more applicants prefer M' to M. We give the first NC algorithm to solve the popular matching problem without ties. We also give an NC algorithm that solves the maximum-cardinality popular matching problem. No NC or RNC algorithms were known for the matching problem in preference systems prior to this work. Moreover, we give an NC algorithm for a weaker version of the stable matching problem, that is, the problem of finding the "next" stable matching given a stable matching.

Finding the shortest path between nodes in a graph has wide applications in many important areas such as transportation and computer networks. However, the current reference algorithms for this task, Dijkstra's for single threaded environments and Δ-stepping for multi-threaded ones, leave performance and efficiency on the table by not taking advantage of additional information available about the graph. In this paper we present and experimentally evaluate novel algorithms SP1, SP2and ParSP2that leverage these constraints to solve the problem faster and more efficiently in key metrics. In single threaded execution, we show how SP1and SP2out-perform Dijsktra's algorithm by up to 46%. In multi-threaded execution we show how our algorithms compare favorably to Δ-stepping algorithm in the ability to establish the shortest path between the source and the median node.

We study the Byzantine lattice agreement (BLA) problem in asynchronous distributed message passing systems. In the BLA problem, each process proposes a value from a join semi-lattice and needs to output a value also in the lattice such that all output values of correct processes lie on a chain despite the presence of Byzantine processes. We present an algorithm for this problem with round complexity of O(log f) which tolerates f < n/5 Byzantine failures in the asynchronous setting without digital signatures, where n is the number of processes. This is the first algorithm which has logarithmic round complexity for this problem in asynchronous setting. Before our work, Di Luna et al give an algorithm for this problem which takes O(f) rounds and tolerates f < n/3 Byzantine failures. We also show how this algorithm can be modified to work in the authenticated setting (i.e., with digital signatures) to tolerate f < n/3 Byzantine failures.

We present a method to design parallel algorithms for constrained combinatorial optimization problems. Our method solves and generalizes many classical combinatorial optimization problems including the stable marriage problem, the shortest path problem and the market clearing price problem. These three problems are solved in the literature using Gale-Shapley algorithm, Dijkstra's algorithm, and Demange, Gale, Sotomayor algorithm. Our method solves all these problems by casting them as searching for an element that satisfies an appropriate predicate in a distributive lattice. Moreover, it solves generalizations of all these problems --- namely finding the optimal solution satisfying additional constraints called lattice-linear predicates. For stable marriage problems, an example of such a constraint is that Peter's regret is less than that of Paul. For shortest path problems, an example of such a constraint is that cost of reaching vertex v1 is at least the cost of reaching vertex v2. For the market clearing price problem, an example of such a constraint is that item1 is priced at least as much as item2. Our algorithm, called Lattice-Linear Predicate Detection (LLP) can be implemented in parallel without any locks or compare-and-set instructions. It just assumes atomicity of reads and writes.

We propose three algorithms for the Byzantine lattice agreement problem in synchronous systems. The first algorithm runs in min {3h(X) + 6,6√{f_a} + 6}) rounds and takes O(n² min{h(X), √{f_a}}) messages, where h(X) is the height of the input lattice X, n is the total number of processes in the system, f is the maximum number of Byzantine processes such that n ≥ 3f + 1 and f_a ≤ f is the actual number of Byzantine processes in an execution. The second algorithm takes 3log n + 3 rounds and O(n² log n) messages. The third algorithm takes 4 log f + 3 rounds and O(n² log f) messages. All algorithms can tolerate f < n/3 Byzantine failures. This is the first work for the Byzantine lattice agreement problem in synchronous systems which achieves logarithmic rounds. In our algorithms, we apply a slightly modified version of the Gradecast algorithm given by Feldman et al [Feldman and Micali, 1988] as a building block. If we use the Gradecast algorithm for authenticated setting given by Katz et al [Katz and Koo, 2006], we obtain algorithms for the Byzantine lattice agreement problem in authenticated settings and tolerate f < n/2 failures.

Tracking causality (or happened-before relation) between events is useful for many applications such as debugging and recovery from failures. Consider a concurrent system with n threads and m objects. For such systems, either a vector clock of size n is used with one component per thread or a vector clock of size m is used with one component per object. A natural question is whether one can use a vector clock of size strictly less than the minimum of m and n to timestamp events. We give an algorithm in this paper that uses a hybrid of thread and object components. Our algorithm is guaranteed to return the minimum number of components necessary for vector clocks. We first consider the case when the interaction between objects and threads is statically known. This interaction is modeled by a thread-object bipartite graph. Our algorithm is based on finding the maximum bipartite matching of such a graph and then applying König-Egerváry Theorem to compute the minimum vertex cover to determine the optimal number of components necessary for the vector clock. We also propose two mechanisms to compute such an vector clock when computation is revealed in an online fashion. Evaluation on different types of graphs indicates that our offline algorithm generates a size vector clock which is significantly less than the minimum of m and n. These mechanisms are more effective when the underlying bipartite graph is not dense.

We give parallel and distributed algorithms for the housing allocation problem. In this problem, there is a set of agents and a set of houses. Each agent has a strict preference list for a subset of houses. We need to find a matching such that some criterion is optimized. One such criterion is Pareto Optimality. A matching is Pareto optimal if no coalition of agents can be strictly better off by exchanging houses among themselves. We also study the housing market problem, a variant of the housing allocation problem, where each agent initially owns a house. In addition to Pareto optimality, we are also interested in finding the core of a housing market. A matching is in the core if there is no coalition of agents that can be better off by breaking away from other agents and switching houses only among themselves. In the first part of this work, we show that computing a Pareto optimal matching of a house allocation is in {\bf CC} and computing the core of a housing market is {\bf CC}-hard. Given a matching, we also show that verifying whether it is in the core can be done in {\bf NC}. We then give an algorithm to show that computing a maximum Pareto optimal matching for the housing allocation problem is in {\bf RNC}^2 and quasi-{\bf NC}^2. In the second part of this work, we present a distributed version of the top trading cycle algorithm for finding the core of a housing market. To that end, we first present two algorithms for finding all the disjoint cycles in a functional graph: a Las Vegas algorithm which terminates in $O(\log l)$ rounds with high probability, where $l$ is the length of the longest cycle, and a deterministic algorithm which terminates in $O(\log^* n \log l)$ rounds, where $n$ is the number of nodes in the graph. Both algorithms work in the synchronous distributed model and use messages of size $O(\log n)$.

This paper studies the lattice agreement problem in asynchronous systems and explores its application to building linearizable replicated state machines (RSM). First, we propose an algorithm to solve the lattice agreement problem in $O(\log f)$ asynchronous rounds, where $f$ is the number of crash failures that the system can tolerate. This is an exponential improvement over the previous best upper bound. Second, Faleiro et al have shown in [Faleiro et al. PODC, 2012] that combination of conflict-free data types and lattice agreement protocols can be applied to implement linearizable RSM. They give a Paxos style lattice agreement protocol, which can be adapted to implement linearizable RSM and guarantee that a command can be learned in at most $O(n)$ message delays, where $n$ is the number of proposers. Later on, Xiong et al in [Xiong et al. DISC, 2018] give a lattice agreement protocol which improves the $O(n)$ guarantee to be $O(f)$. However, neither protocols is practical for building a linearizable RSM. Thus, in the second part of the paper, we first give an improved protocol based on the one proposed by Xiong et al. Then, we implement a simple linearizable RSM using the our improved protocol and compare our implementation with an open source Java implementation of Paxos. Results show that better performance can be obtained by using lattice agreement based protocols to implement a linearizable RSM compared to traditional consensus based protocols.

This paper studies the lattice agreement problem and the generalized lattice agreement problem in distributed message passing systems. In the lattice agreement problem, given input values from a lattice, processes have to non-trivially decide output values that lie on a chain. We consider the lattice agreement problem in both synchronous and asynchronous systems. For synchronous lattice agreement, we present two algorithms which run in log(f) and min{O(log^2 h(L)), O(log^2 f)} rounds, respectively, where h(L) denotes the height of the input sublattice L, f < n is the number of crash failures the system can tolerate, and n is the number of processes in the system. These algorithms have significant better round complexity than previously known algorithms. The algorithm by Attiya et al. [Attiya et al. DISC, 1995] takes log(n) synchronous rounds, and the algorithm by Mavronicolasa [Mavronicolasa, 2018] takes min{O(h(L)), O(sqrt(f))} rounds. For asynchronous lattice agreement, we propose an algorithm which has time complexity of 2*min{h(L), f + 1} message delays which improves on the previously known time complexity of O(n) message delays. The generalized lattice agreement problem defined by Faleiro et al in [Faleiro et al. PODC, 2012] is a generalization of the lattice agreement problem where it is applied for the replicated state machine. We propose an algorithm which guarantees liveness when a majority of the processes are correct in asynchronous systems. Our algorithm requires min{O(h(L)), O(f)} units of time in the worst case which is better than O(n) units of time required by the algorithm in [Faleiro et al. PODC, 2012].

Current monitor based systems have some disadvantages for multi-object operations. They require the programmers to (1) manually determine the order of locking operations, (2) manually determine the points of execution where threads should signal other threads, (3) use global locks or perform busy waiting for operations that depend upon a condition that spans multiple objects. Transactional memory systems eliminate the need for explicit locks, but do not support conditional synchronization. They also require the ability to rollback transactions. In this paper, we propose new monitor based methods that provide automatic signaling for global conditions that span multiple objects. Our system provides automatic notification for global conditions. Assuming that the global condition is a Boolean expression of local predicates, our method allows efficient monitoring of the conditions without any need for global locks. Furthermore, our system solves the monitor composition problem without requiring global locks. We have implemented our constructs on top of Java and have evaluated their overhead. Our results show that on most of the test cases, not only our code is simpler but also faster than Java's reentrant- lock as well as the Deuce transactional memory system.

Enumerating all consistent states of a parallel computation that satisfy a given predicate is an important problem in debugging and verification of parallel programs. We give a fast algorithm to enumerate all consistent states of a parallel computation that satisfy a stable predicate. In addi- tion, we define a new category of global predicates called count predicates and give an algorithm to enumerate all consistent states (of the computation) that satisfy it. All existing predicate detection algorithms, such as BFS, DFS and Lex algorithms, do not exploit the knowledge about the nature of the predicates, and thus may visit all global states of the computation in the worst case. In comparison, our algorithms only visit the states that satisfy the given predicate, and thus take time and space that is a polynomial function of the number of states of interest. In doing so, they provide a significant reduction — exponential in many cases — in time complexities in comparison to existing algorithms.

We show that many techniques developed in the context of predicate detection are applicable to the stable marriage problem. The standard Gale-Shapley algorithm can be derived as a special case of detecting linear predicates. We also show that techniques in computation slicing can be used to represent the set of all constrained stable matchings.

The happened-before model (or the poset model) has been widely used for modeling the computations (execution traces) of parallel programs and detecting predicates (user-specified conditions). This model captures potential causality as well as locking constraints among the executed events of computations using Lamport's happened-before relation. The detection of a predicate in a computation is performed by checking if the predicate could become true in any reachable global state of the computation. In this paper, we argue that locking constraints are fundamentally different from potential causality. Hence, a poset is not an appropriate model for debugging purposes when the computations contain locking constraints. We present a model called Locking Poset, or a Loset, that generalizes the poset model for locking constraints. Just as a poset captures possibly an exponential number of total orders, a loset captures possibly an exponential number of posets. Therefore, detecting a predicate in a loset is equivalent to detecting the predicate in all corresponding posets. Since determining if a global state is reachable in a computation is a fundamental problem for detecting predicates, this paper first studies the reachability problem in the loset model. We show that the problem is NP-complete. Afterwards, we introduce a subset of reachable global states called lock-free feasible global states such that we can check whether a global state is lock-free feasible in polynomial time. Moreover, we show that lock-free feasible global states can act as "reset" points for reachability and be used to drastically reduce the time for determining the reachability of other global states. We also introduce strongly feasible global states that contain all reachable global states and show that the strong feasibility of a global state can be checked in polynomial time. We show that strong feasibility provides an effective approximation of reachability for many practical applications.

Verifying the correctness of executions of concurrent and distributed programs is difficult because they show nondeterministic behavior due to different process scheduling order. Predicate detection can alleviate this problem by predicting whether the user-specified condition (predicate) could have become true in any global state of the given concurrent or distributed computation. The method is predictive because it generates inferred global states from the observed execution path and then checks if those global states satisfy the predicate. An important part of the predicate detection method is global states enumeration, which generates the consistent global states, including the inferred ones, of the given computation. Cooper and Marzullo gave the first enumeration algorithm based on a breadth first strategy (BFS). Later, many algorithms have been proposed to improve the space and time complexity. Among the existing algorithms, the Tree algorithm due to Jegou et al. has the smallest time complexity and requires O(|P|) space, which is linear to the size of the computation P. In this paper, we present a fast algorithm, QuickLex, to enumerate global states in the lexical order. QuickLex requires much smaller space than O(|P|). From our experiments, the Tree algorithm requires 2-10 times more memory space than QuickLex. Moreover, QuickLex is 4 times faster than Tree even though the asymptotic time complexity of QuickLex is higher than that of Tree. The reason is that the worst case time complexity of QuickLex happens only in computations that are not common in practice. Moreover, Tree is built on linked-lists and QuickLex can be implemented using integer arrays. In comparison with the existing lexical algorithm (Lex), QuickLex is 7 times faster and uses almost the same amount of memory as Lex. Finally, we implement a parallel-and-online predicate detector for concurrent programs using QuickLex, which can detect data races and violation of invariants in the programs.

Monitor objects are used extensively for thread-safety and synchronization in shared memory parallel programs. They provide ease of use, and enable straightforward correctness analysis. However, they inhibit parallelism by enforcing serial executions of critical sections, and thus the performance of parallel programs with monitors scales poorly with number of processes. Their current design and implementation is also ill-suited for thread synchronization across multiple thread-safe objects. We present ActiveMonitor - a framework that allows multi-object synchronization without global locks, and improves parallelism by exploiting asynchronous execution of critical sections. We evaluate the performance of Java based implementation of ActiveMonitor on micro-benchmarks involving light and heavy critical sections, as well as on single-source-shortest-path problem in directed graphs. Our results show that on most of these problems, ActiveMonitor based programs outperform programs implemented using Java's reentrant-lock and condition constructs.

Verifying the correctness of the executions of a concurrent program is difficult because of its nondeterministic behavior. One of the verification methods is predicate detection, which predicts whether the user specified condition (predicate) could become true in any global states of the program. The method is predictive because it generates inferred execution paths from the observed execution path and then checks the predicate on the global states of inferred paths. One important part of predicate detection is global states enumeration, which generates the global states on inferred paths. Cooper and Marzullo gave the first enumeration algorithm based on a breadth first strategy (BFS). Later, many algorithms have been proposed to improve space and time complexity. None of them, however, takes parallelism into consideration. In this paper, we present the first parallel and online algorithm, named ParaMount, for global state enumeration. Our experimental results show that ParaMount speeds up the existing sequential algorithms by a factor of 6 with 8 threads. We have implemented an online predicate detector using ParaMount. For predicate detection, our detector based on ParaMount is 10 to 50 times faster than RV runtime (a verification tool that uses Cooper and Marzullo’s BFS enumeration algorithm).

Most programming languages use monitors with explicit signals for synchronization in shared-memory programs. Requiring programmers to signal threads explicitly results in many concurrency bugs due to missed notifications, or notifications on wrong condition variables. In this paper, we describe an implementation of an automatic signaling monitor in Java called AutoSynch that eliminates such concurrency bugs by removing the burden of signaling from the programmer. We show that the belief that automatic signaling monitors are prohibitively expensive is wrong. For most problems, programs based on AutoSynch are almost as fast as those based on explicit signaling. For some, AutoSynch is even faster than explicit signaling because it never uses signalAll, whereas the programmers end up using signalAll with the explicit signal mechanism.

Consider a network of n processes, each of which has a d-dimensional vector of reals as its input. Each process can communicate directly with all the processes in the system; thus the communication network is a complete graph. All the communication channels are reliable and FIFO (first-in-first-out).

Analyzing a distributed computation is a hard problem in general due to the combinatorial explosion in the size of the state-space with the number of processes in the system. By abstracting the computation, unnecessary state explorations can be avoided. Computation slicing is an approach for abstracting distributed computations with respect to a given predicate. We focus on regular predicates, a family of predicates that covers many commonly used predicates for runtime verification. The existing algorithms for computation slicing are centralized - a single process is responsible for computing the slice in either offline or online manner. In this paper, we present first distributed online algorithm for computing the slice of a distributed computation with respect to a regular predicate. Our algorithm distributes the work and storage requirements across the system, thus reducing the space and computation complexity per process.

Replication is the prevalent solution to tolerate faults in large data structures hosted on distributed servers. To tolerate f crash faults (dead/unresponsive data structures) among n distinct data structures, replication requires f + 1 replicas of each data structure, resulting in nf additional backups. We present a solution, referred to as fusion that uses a combination of erasure codes and selective replication to tolerate f crash faults using just f additional fused backups. We show that our solution achieves O(n) savings in space over replication. Further, we present a solution to tolerate f Byzantine faults (malicious data structures), that requires only nf + f backups as compared to the 2nf backups required by replication. We explore the theory of fused backups and provide a library of such backups for all the data structures in the Java Collection Framework. The theoretical and experimental evaluation confirms that the fused backups are space-efficient as compared to replication, while they cause very little overhead for normal operation. To illustrate the practical usefulness of fusion, we use fused backups for reliability in Amazon's highly available key-value store, Dynamo. While the current replication-based solution uses 300 backup structures, we present a solution that only requires 120 backup structures. This results in savings in space as well as other resources such as power.

No abstract available.

The paper describes a technique to correct crash faults in large data structures hosted on distributed servers, based on the concept of fused backups. The prevalent solution to this problem is replication. To correct f crash faults among n distinct data structures, replication requires nf additional replicas. If each of the primaries contains O(m) nodes of O(s) size each, this translates to O(nmsf) total backup space. Our technique uses a combination of erasure correcting codes and selective replication to correct f crash faults using just f additional backups consuming O(msf) total backup space, while incurring minimal overhead during normal operation. Since the data is maintained in the coded form, recovery is costly as compared to replication. However, in a system with infrequent faults, the savings in space outweighs the cost of recovery. We explore the theory and algorithms for these fused backups and provide a library of such backups for all the data structures in the Java 6 Collection framework. Our experimental evaluation confirms that fused backups are space-efficient as compared to replication (almost n times), while they cause very little overhead for updates. Many real world distributed systems such as Amazon's Dynamo data store use replication to achieve reliability. An alternate, fusion-based design can result in significant savings in space as well as other resources such as power.

This paper presents a weighted version of the Byzantine Agreement Problem and its solution under various conditions. In this version, each machine is assigned a weight depending on the application. Instead of assuming that at most f out of N machines fail, the algorithm assumes that the total weight of the machines that fail is at most f/N. When each machine has weight 1/N, this problem reduces to the standard Byzantine Generals Agreement Problem. By choosing weights appropriately, the weighted Byzantine Agreement Problem can be applied to situations where a subset of processes are more trusted. By using weights, the system can reach consensus in the presence of Byzantine failures, even when more than N/3 processes fail, so long as the total weight of the failed processes is less than 1/3. Also, a method to update the weights of the processes after execution of the weighted Byzantine Agreement is given. The update method guarantees that the weight of any correct process is never reduced and the weight of any faulty process, suspected by correct processes whose total weight is at least 1/4, is reduced to 0 for future instances. A short discussion of some weight assignment strategies is also given.

The Byzantine Agreement (BA) problem requires non-faulty processes to agree on a common value. In many applications, it is important that the processes agree on the correct value. In this paper, we present a problem called Accurate Byzantine Agreement with Feedback (ABAF) in which all processes receive common feedback from the environment indicating if the value they agreed upon was correct or not (accuracy). We present an algorithm that solves the ABAF problem based on a standard solution to the BA problem and a multiplicative method to maintain and update process weights indicative of how often they are correct. We make guarantees on the accuracy of the algorithm based on assumptions on the accuracy of the processes and the proportion of faulty and non-faulty processes in the system. For each iteration, if the weight of accurate processes is at least 3/4th the weight of the non-faulty processes, the algorithm always decides on the correct value. When the non-faulty processes are accurate with probability greater than 1/2, the algorithm decides on the correct value with very high probability after some initial number of mistakes. In fact, among n processes, if there exists even one process which is accurate for all iterations, the algorithm is wrong only O(log n) times for any large number of iterations of the algorithm.

Existing algorithms for global snapshots in distributed systems are not scalable when the underlying topology is complete. There are primarily two classes of existing algorithms for computing a global snapshot. Algorithms in the first class use control messages of size 0(1) but require O(N) space and O(N) messages per processor in a network with JV processors. Algorithms in the second class use control messages (such as rotating tokens with vector counter method) of size O(N), use multiple control messages per channel, or require recording of message history. As a result, algorithms in both of these classes are not efficient in large systems when the logical topology of the communication layer such as MPI is complete. In this paper, we propose three scalable algorithms for global snapshots: a grid-based, a tree-based, and a centralized algorithm. The grid-based algorithm uses O(N) space but only O(¿(N)) messages per processor each of size O(¿(N)). The tree-based and centralized algorithms use only O(1) size messages. The tree-based algorithm requires O(1) space and O(log N log(W/N)) messages per processor where W is the total number of messages in transit. The centralized algorithm requires O(1) space and O(log(W/N)) messages per processor. We also have a matching lower bound for this problem. We also present hybrid of centralized and tree-based algorithms that allow trade-off between the decentralization and the message complexity. Our algorithms have applications in checkpointing, detecting stable predicates, and implementing synchronizers.

Stream computing research is moving from terascale to petascale levels. It aims to rapidly analyze data as it streams in from many sources and make decisions with high speed and accuracy in fields as diverse as security surveillance and financial services including stock trading. We specifically consider real-time text indexing and search with high input data rates (10 GB/s or more) along with small index age-off (expiry) time. This makes it necessary to have maximal indexing rates for large volumes of data as well as minimal latency for indexing (time between start of indexing for a document and its availability for search) while maintaining very-low search response time. In addition, future massively parallel architectures with storage class memories will enable high speed in-memory real-time indexing, where index can be completely stored in a high capacity storage class memory. In this paper, we present the design of distributed data-structures and distributed real-time text indexing algorithm for parallel systems having large (thousands to hundred thousand) number of cores/processors, while simultaneously providing acceptable search performance [1]. The inherent trade-offs involved in index space, indexing throughput and search response time make this problem particularly challenging. Our algorithm uses group-based index construction and leverages novel index data structures that reduce load imbalance and make text indexing and merge process more scalable and efficient. We show analytically that the asymptotic parallel time complexity of our distributed indexing algorithm, is at least ?(log(P)) factor better than typical indexing approaches, where P is the number of indexing nodes in a group. We further demonstrate the performance and scalability of our distributed indexing algorithm, on an MPP architecture (Blue Gene/L) using actual IBM intranet data. We achieved high indexing throughput of around 312 GB/min on an 8 K node Blue Gene/L machine. In comparison with parallel indexing implemented using typical approaches like CLucene, this is 3?-7? better. To the best of our knowledge, this is the first published result on indexing throughput at such a large scale, with sustained search performance. We further show that our approach is scalable to 128 K nodes, giving an estimated indexing throughput of 5 T B/min. We also achieved indexing latency that is around 10? better than typical indexing approaches.

Given a set of n different deterministic finite state machines (DFSMs) modeling a distributed system, we examine the problem of tolerating f crash or Byzantine faults in such a system. The traditional approach to this problem involves replication and requires n middot f backup DFSMs for crash faults and 2 middot n middot f backup DFSMs for Byzantine faults. For example, to tolerate two crash faults in three DFSMs, a replication based technique needs two copies of each of the given DFSMs, resulting in a system with six backup DFSMs. In this paper, we question the optimality of such an approach and present an approach called (f, m)-fusion that permits fewer backups than the replication based approaches. Given n different DFSMs, we examine the problem of tolerating f faults using just m additional DFSMs. We introduce the theory of fusion machines and provide an algorithm to generate backup DFSMs for both crash and Byzantine faults. We have implemented our algorithms in Java and have used them to automatically generate backup DFSMs for several examples.

Concurrent and distributed systems, such as system-on-chips (SoCs), present an immense challenge for verification due to their complexity and inherent concurrency. Traditional approaches for eliminating errors in concurrent and distributed systems include formal methods and simulation. We present an approach toward combining formal methods and simulation in a technique called predicate detection (aka runtime verification), while avoiding the complexity of formal methods and the pitfalls of ad hoc simulation. Our technique enables efficient formal verification on execution traces of actual scalable systems. Traditional simulation methodologies are woefully inadequate in the presence of concurrency and subtle synchronization. The bug in the system may appear only when the ordering of concurrent events is different from the ordering in the simulation trace. We use a partial order trace model rather than the traditional total order trace model and we get the benefit of properly dealing with concurrent events and especially of detecting errors from analyzing successful total order traces. Surprisingly, checking properties, even on a finite partial order trace, is NP-complete in the size of the trace description (aka state-explosion problem). Our approach to ameliorating state explosion in partial order trace model uses two techniques: 1) slicing and 2) exploiting the structure of the property itself-by imposing restrictions-to evaluate its value efficiently for a given execution trace. Intuitively, the slice of a trace with respect to a property is a subtrace that contains all of the global states of the trace that satisfy the property such that it is computed efficiently (without traversing the state space) and represented concisely (without explicit representation of individual states). We present temporal slicing algorithms with respect to properties in temporal logic RCTL+. We show how to use the slicing algorithms for efficient predicate detection of design properties. We have developed a prototype system, partial order trace analyzer (POTA), which implements our algorithms. We verify several scalable and industrial protocols, including CORBA's general inter-ORB protocol, PCI-based system-on-chip, ISO's asynchronous transfer mode ring, cache coherence, and mutual exclusion. Our experimental results indicate that slicing can lead to exponential reduction over existing techniques, such as the ones in SPIN model checker, both in time and space

Given a distributed computation and a global predicate, predicate detection involves determining whether there exists at least one consistent cut (or global state) of the computation that satisfies the predicate. On the other hand, computation slicing is concerned with computing the smallest subcomputation (with the least number of consistent cuts) that contains all consistent cuts of the computation satisfying the predicate. In this paper, we investigate the relationship between predicate detection and computation slicing and show that the two problems are actually equivalent. Specifically, given an algorithm to detect a predicate b in a computation C, we derive an algorithm to compute the slice of C with respect to b. The time complexity of the (derived) slicing algorithm is O(n|E|T), where n is the number of processes, E is the set of events, and O(T) is the time complexity of the detection algorithm. We discuss how the "equivalence" result of this paper can be utilized to derive a faster algorithm for solving the general predicate detection problem in many cases. Slicing algorithms described in our earlier papers are all offline in nature. In this paper, we also present two online algorithms for computing the slice. The first algorithm can be used to compute the slice for a general predicate. Its amortized time complexity is O(n(c + n)T) per event, where c is the average concurrency in the computation and O(T) is the time complexity of the detection algorithm. The second algorithm can be used to compute the slice for a regular predicate. Its amortized time complexity is only O(n2) per event.

An important problem in distributed systems is observation of global properties of distributed computations. What makes this problem difficult is that events in the computation can be concurrent, i.e. the relation between events forms a partial order, not a total order. One of the fundamental parameters of a partial order is the width, which corresponds to the maximum number of mutually incomparable elements. For example, a process-time diagram that shows this partial order decomposition in minimum number of chains can be very useful in monitoring or debugging such computations. In this paper, we present an incremental algorithm to compute the optimal chain partition. We compare our algorithm with existing chain reduction algorithms. From a practical point of view, performance evaluation shows that our approach achieves up to 90% run-time improvement over the previously known algorithms.

Existing algorithms for global snapshots in distributed systems are not scalable when the underlying topology is complete. In a network with N processors, these algorithms require O(N) space and O(N) messages per processor. As a result, these algorithms are not efficient in large systems when the logical topology of the communication layer such as MPI is complete. In this paper, we propose three algorithms for global snapshot: a grid-based, a tree-based and a centralized algorithm. The grid-based algorithm uses O(N) space but only O(√N) messages per processor. The tree-based algorithm requires only O(1) space and O(logNlog w) messages per processor where w is the average number of messages in transit per processor. The centralized algorithm requires only O(1) space and O(log w) messages per processor. We also have a matching lower bound for this problem. Our algorithms have applications in checkpointing, detecting stable predicates and implementing synchronizers. We have implemented our algorithms on top of the MPI library on the Blue Gene/L supercomputer. Our experiments confirm that the proposed algorithms significantly reduce the message and space complexity of a global snapshot.

This paper developed power consumption profiles of mobile multimedia terminal for typical application scenarios of WCDMA communications. The power consumptions and their efficiencies are investigated for the terminal architecture featuring with the combined application of the BF antenna and the OFDM technologies. Processing MIPs requirement for media data processor is also investigated together with the evaluation of the power saving effect of applying the multi-level supply voltages and operating frequencies, which is named as a dynamic voltage scaling (DVS) technology. Average power saving of 25% can be achieved for high-speed multimedia terminals using the DVS along with the OFDM modulation scheme

Partial order (p.o.) reduction techniques are a popular and effective approach for tackling state space explosion in the verification of concurrent systems. These techniques generate a reduced search space that could be exponentially smaller than the complete state space. Their major drawback is that the amount of reduction achieved is highly sensitive to the properties being verified. For the same program, different properties could result in very different amounts of reduction achieved.We present a new approach which combines the benefits of p.o. reduction with the added advantage that the size of the constructed state space is completely independent of the properties being verified. As in p.o. reduction, we use the notion of persistent sets to construct a representative interleaving for each maximal trace of the program. However, we retain concurrency information by assigning vector timestamps to the events in each interleaving. Our approach hinges upon the use of efficient algorithms that parse the encoded concurrency information in the representative interleaving to determine whether a safety violation exists in any interleaving of the corresponding trace. We show that, for some types of predicates, reachability detection can be performed in time that is polynomial in the length of the interleaving. Typically, these predicates exhibit certain characteristics that can be exploited by the detection algorithm.We implemented our algorithms in the popular model checker SPIN, and present experimental results that demonstrate the effectiveness of our techniques. For example, we verified a distributed dining philosophers protocol in 0.03 seconds, using 1.253 MB of memory. SPIN, using traditional p.o. reduction techniques, took 759.71 seconds and 439.116 MB of memory.

In a concurrent system with N processes, vector clocks of size N are used for tracking dependencies between the events. Using vectors of size N leads to scalability problems. Moreover, association of components with processes makes vector clocks cumbersome and inefficient for systems with a dynamic number of processes. We present a class of logical clock algorithms, called chain clock, for tracking dependencies between relevant events based on generalizing a process to any chain in the computation poset. Chain clocks are generally able to track dependencies using fewer than N components and also adapt automatically to systems with dynamic number of processes. We compared the performance of Dynamic Chain Clock (DCC) with vector clock for multithreaded programs in Java. With 1% of total events being relevant events, DCC requires 10 times fewer components than vector clock and the timestamp traces are smaller by a factor of 100. Although DCC requires shared data structures, it is still 10 times faster than vector clock in our experiments.

We study supervisory control of discrete event systems with potentially infinite state-space using state variables for representation and specification. An assignment program model consisting of state variables and a finite set of conditional assignment statements is used for representing a discrete event system, and a predicate over state variables is used for representing a state avoidance control specification. The contribution of this paper is to show how to perform supervisory control computations symbolically. In the case of a Petri net (vector addition system) with the set of forbidden states being a right-closed set, we present a finitely terminating algorithm for maximally permissive supervision. Discrete-event systems are systems with discrete states that evolve in response to discrete events. The state space of such systems can be finite or infinite. The latter case occurs when the state-variables can take infinitely many values such as integers. Certain states in a given system may be "bad", such as a deadlocking state. Then, controllers must be designed to restrict the system behavior by dynamically disabling events occurring in the system so that system never reaches the bad states. Also, certain events can be uncontrollable and cannot be disabled. State-avoidance control of potentially infinite-state discrete-event systems is studied in this paper. A compact program-like modeling formalism has been adopted. Although the control problem for infinite-state systems is in general not solvable in an automated fashion owing to its undecidability established We develop a symbolic technique, that is iterative in nature and can be automated, for computing a control strategy. If the iteration terminates (there is no guarantee though), a controller is computed. We illustrate through several examples where the iterative computation does terminate. Finally, we show that for a certain class of infinite-state systems that can be modeled as Petri nets, the iterative computation is guaranteed to terminate whenever the state-avoidance set is lower-bounded (every state that "dominates" a bad state is itself bad).

Summary form only given. Given a distributed computation and a global predicate, predicate detection involves determining whether there exists at least one consistent cut (or global state) of the computation that satisfies the predicate. On the other hand, computation slicing is concerned with computing the smallest sub-computation - with the least number of consistent cuts - that contains all consistent cuts of the computation satisfying the predicate. We investigate the relationship between predicate detection and computation slicing and show that the two problems are equivalent. Specifically, given an algorithm to detect a predicate b in a computation C, we derive an algorithm to compute the slice of C with respect to b. The time-complexity of the (derived) slicing algorithm is O(n|E|) times the time-complexity of the detection algorithm, where n is the number of processes and E is the set of events. We discuss how the "equivalence " result can be utilized to derive a faster algorithm for solving the general predicate detection problem. Slicing algorithms described in our earlier papers are all off-line in nature. We also give an online algorithm for computing the slice for a predicate that can be detected efficiently. The amortized time-complexity of the algorithm is O(n(c + n)) times the time-complexity of the detection algorithm, where c is the average concurrency in the computation.

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 effectiveness in the SoC world. We attack the problem of SoC verification using an elegant abstraction mechanism, called computation slicing, and show that it enables effective 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.

Writing correct distributed programs is hard. In spite of extensive testing and debugging, software faults persist even in commercial grade software. Many distributed systems, especially those employed in safety-critical environments, should be able to operate properly even in the presence of software faults. Monitoring the execution of a distributed system, and, on detecting a fault, initiating the appropriate corrective action is an important way to tolerate such faults. This gives rise to the predicate detection problem which involves finding a consistent cut of a distributed computation, if it exists, that satisfies the given global predicate. Detecting a predicate in a computation is, however, an NP-complete problem. To ameliorate the associated combinatorial explosion problem, we introduce the notion of computation slice in our earlier papers [5, 10]. Intuitively, slice is a concise representation of those consistent cuts that satisfy a certain condition. To detect a predicate, rather than searching the state-space of the computation, it is much more efficient to search the state-space of the slice. In this paper we provide efficient algorithms to compute the slice for several classes of predicates. Our experimental results demonstrate that slicing can lead to an exponential improvement over existing techniques in terms of lime and space.

Determining order relationship between events in distributed 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 in a system with 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.

We introduce the notion of a slice of a distributed computation. A slice of a distributed computation with respect to a global predicate is a computation which captures those and only those consistent cuts of the original computation which satisfy the global predicate. We show that a slice exists for a global predicate iff the predicate is a regular predicate. We then give an efficient algorithm for computing the slice and show applications of slicing to testing and debugging of distributed programs.

Monitoring of global predicates is a fundamental problem in asynchronous distributed systems. This problem arises in various contexts, such as design, testing and debugging, and fault tolerance of distributed programs. In this paper, we establish that the problem of determining whether there exists a consistent cut of a computation that satisfies a predicate in k-CNF (k/spl ges/2), in which no two clauses contain variables from the same process, is NP-complete in general. A polynomial-time algorithm to find the consistent cut, if it exists, that satisfies the predicate for special cases is provided. We also give algorithms (albeit exponential) that can be used to achieve an exponential reduction in time over existing techniques for solving the general version. Furthermore, we present an algorithm to determine whether there exists a consistent cut of a computation for which the sum x/sub 1/+x/sub 2/+/spl middot//spl middot//spl middot/+x/sub n/ exactly equals some constant k, where each x/sub i/ is an integer variable on a process p/sub i/ such that it is incremented or decremented by at most one at each step. As a corollary, any symmetric global predicate on Boolean variables, such as absence of simple majority and exclusive-OR of local predicates, can now be detected. Additionally, the problem is proved to be NP-complete if each x/sub i/ can be changed by an arbitrary amount at each step. Our results solve the previously open problems in predicate detection proposed by V.K. Garg (1997) and bridge the wide gap between the known tractability and intractability results that have existed until now.

In this paper, we show the connection between vector clocks used in distributed computing and dimension theory of partially ordered sets. Based on this connection, we provide lower bounds on the number of coordinates for timestamping events in a distributed computation for capturing the happened- before relation. To this end, we introduce the notion of a string realizer and the string dimension of a poset. For distributed computing and other applications, the concept of string realizer is more natural than the chain realizer used in the classical dimension theory. We establish the relationship between the string dimension and the chain dimension of a poset. Using this relationship and Dilworth's theorem for the chain dimension of finite distributive lattices, we obtain the desired lower bound. The concept of strings also has applications in efficient encoding of partial orders because it requires fewer bits to encode a string realizer than a chain realizer.

Distributed programs are hard to write. A distributed debugger equipped with the mechanism to re-execute the traced computation in a controlled fashion can greatly facilitate the detection and localization of bugs. This approach gives rise to a general problem, called predicate control problem, which takes a computation and a safety property specified on the computation, and outputs a controlled computation that maintains the property. We define a class of global predicates, called region predicates, that can be controlled efficiently in a distributed computation. We prove that the synchronization generated by our algorithm is optimal. Further, we introduce the notion of an admissible sequence of events and prove that it is equivalent to the notion of predicate control. We then give an efficient algorithm for the class of disjunctive predicates based on the notion of an admissible sequence. 1.

The paper discusses the quality of service (QoS) requirements for each traffic class in a wireless environment and problems in implementing the QoS requirements in the CDMA based Universal Mobile Telecommunication Service (UMTS) network. In UMTS networks, the medium access control (MAC)/link access control (LAC) sublayer of the OSI layer 2 will be used for priority handling, QoS monitoring, and radio resource management for traffic flows from several users. The paper presents some suggestions to realize QoS requirements in the MAC/LAC sublayer along with restrictions imposed by the W-CDMA air interface.

The problem of recovering distributed systems from crash failures has been widely studied in the context of traditional non-threaded processes. However, extending those solutions to the multi-threaded scenario presents new problems. We identify and address these problems for optimistic logging protocols. There are two natural extension to optimistic logging protocols in the multi-threaded scenario. The first extension is process-centric, where the points of internal non-determinism caused by threads are logged. The second extension is thread-centric, where each thread is treated as a separate process. The process-centric approach suffers from false causality while the thread-centric approach suffers from high causality tracking overhead. By observing that the granularity of failures can be different from the granularity of rollbacks, we design a new balanced approach which incurs low causality tracking overhead and also eliminates false causality.

There has been very little research in distributed predicate detection for faulty, asynchronous environments. We define a class of predicates called set decreasing predicates which can be detected in such an environment. We introduce a set of failure detectors called infinitely often accurate detectors which are implementable in asynchronous systems. Based on these failure detectors we present an algorithm to detect conjunction of local predicates and send-monotonic channel predicates. Since perfect failure detection is impossible in an asynchronous system, we cannot guarantee that our detection algorithm will not have false detections. However, if the predicate ever holds then it is guaranteed to be detected.

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.

The partial-order model of distributed computations based on the happened before relation has been criticized for allowing false causality between events. Our strong causality model addresses this problem by allowing multiple local threads of control. This paper addresses the predicate detection problem for the class of weak conjunctive predicates in the strong causality model. We show that, in general, the problem is NP-complete. However, an efficient solution is demonstrated for a useful sub-case. Further, this solution can be used to achieve an exponential reduction in time for solving the general problem. Our predicate detection algorithms can be applied to distributed debugging when processes have independent events, as in multi-threaded processes.

We describe a hierarchical technique that allows a class of non deterministic timed Petri nets to be analyzed using the (max,+) algebra (F. Baccelli et al., 1992; G. Brat and V.K. Garg, 1998) of periodic signals. We show that the timing and controllability analysis of such systems is possible via the use of sup- and inf-convolution operations within the (max,+) framework. We apply this technique to the verification of timing constraints in an intelligent structural control system and compare our technique to other modeling tools for real time systems.

In the recovery of failed processes in a distributed program, causal logging schemes offer several benefits. These benefits include no rollback of unfailed processes and simple approaches to output commit. Unfortunately, previous approaches to the recovery of multiple simultaneous failures require that the distributed execution be blocked or that recovering processes coordinate. The latter requires assumptions which are not satisfactory. In this paper we present a solution that has neither of these drawbacks.

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.

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 message, and K corresponds to the system-imposed upper bound on the vector size.

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 message-logging 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, 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.

No abstract available.

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. Our algorithms can be executed on line as well as off line. Moreover, our algorithms do not assume that underlying channels satisfy FIFO ordering.

Designing and debugging distributed systems requires the detection of conditions across the entire system. As an illustration, monitoring the status of an application requires detection of termination, and using virtual time requires the periodic calculation of the global virtual time. The generalized conjunctive predicate (GCP) detector offers a method to derive detection algorithms for these and other problems based on optimizing the base algorithm.

This paper discusses efficient distributed detection of global conjunctive predicates in a distributed program. Our methods correctly detect the first consistent cut in which the predicate is true, even if the predicate is unstable. Previous work in detection of such predicates is based on a centralized checker process. In this paper we introduce algorithms which distribute the computation and space requirements of the detection procedure. Two algorithms are presented. The first algorithm requires O (n/sup 2/ m) time and space where m is the number of messages sent by any process and n is the number of processes over which the predicate is defined. This algorithm has identical time complexity to the original centralized algorithm. However computation, space and message requirements are distributed evenly over the n processes. The second algorithm requires 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. Parallelism can be introduced into either distributed algorithm, reducing the average case time complexity. We show that the worst-case time complexity can not be improved beyond O(mn) with any on-line detection algorithm.

The paper studies the characteristics of synchronous ordering of messages. Synchronous ordering of messages defines synchronous communication based on the causality rather than time. We present the sufficient conditions, based on the causality relations, for any algorithm to provide synchronous ordering. We also propose an algorithm using acknowledgment messages to implement the sufficient conditions. The algorithm is deadlock-free, and provides a higher degree of concurrency than existing algorithms.>

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.

In a distributed system, many algorithms need repeated computation of a global function. These algorithms generally use a static hierarchy for gathering the necessary data from all processes. As a result, they are unfair to processes at higher levels of the hierarchy, which have to perform more work than processes at lower levels do. In this paper, we present a new revolving hierarchical scheme in which the position of a process in the hierarchy changes with time. This reorganization of the hierarchy is achieved concurrently with its use. It results in algorithms that are not only fair to all processes but also less expensive in terms of messages. The reduction in the number of messages is achieved by reusing messages for more than one computation of the global function. The technique is illustrated for a distributed branch-and-bound problem and for asynchronous computation of fixed points.>

This paper discusses detection of global predicates in a distributed program. Earlier algorithms for detection of global predicates proposed by Chandy and Lamport (1985) work only for stable predicates. A predicate is stable if it does not turn false once it becomes true. Our algorithms detect even unstable predicates, without excessive overhead. In the past, such predicates have been regarded as too difficult to detect. The predicates are specified by using a logic described formally in this paper. We discuss detection of weak conjunctive predicates that are formed by conjunction of predicates local to processes in the system. Our detection methods will detect whether such a predicate is true for any interleaving of events in the system, regardless of whether the predicate is stable. Also, any predicate that can be reduced to a set of weak conjunctive predicates is detectable. This class of predicates captures many global predicates that are of interest to a programmer. The message complexity of our algorithm is bounded by the number of messages used by the program. The main applications of our results are in debugging and testing of distributed programs. Our algorithms have been incorporated in a distributed debugger that runs on a network of Sun workstations in UNIX.>

The authors present a revolving hierarchical scheme in which the logical position of a process in the hierarchy changes with time so that the reorganization of hierarchy is achieved concurrently with its use. The technique is useful for repeated computation of global functions that require information from all processes. It results in algorithms that are not only fair to all nodes, but also less expensive in terms of messages. The reduction in the number of messages is achieved by reusing messages for more than one computation of the global function. The technique is illustrated for hierarchical snapshot computation and distributed branch-and-bound problems.>

The symmetry of distributed systems that have one or more sets of identical processes, is used to reduce the state space for automatic analysis techniques. A model called the Synchronous Token-based Communicating State Model (STOCS) is proposed to facilitate specification and analysis of symmetric distributed systems. Symbolic and inductive techniques to analyze the STOCS are described. The techniques are demonstrated by analyzing the 2-out-of-3, readers-writers, dining philosophers, and mutual exclusion problems.>

Genesis is a software-engineering-based programming environment geared to support big software projects. The authors first discuss a reusability-driven development methodology that advocates software development based on reusability considerations. Then, they discuss the tools and techniques provided in Genesis to support this methodology. Techniques are suggested for improving the retrievability, composability, and understandability of software resources. Retrievability is improved by use of ESL (entity specification language) for tying resources through attributes and relations. Composability is improved through a mechanism called functional composition that provides considerably more generality than Unix pipes for composing programs. Understandability is improved by the use of program abstractors.>

It is asserted that ad-hoc programming techniques do not work in the development of big software systems. The programs faced in developing large software include starting from fuzzy and incomplete requirements; enforcing a methodology on the developers; coordinating multiple programmers and managers; achieving desired reliability and performance in the system; managing a multitude of resources in a meaningful way; and completing the system within a limited time frame. The authors examine some of the trends in requirement specification; life cycle modeling; programming environments; design tools; and other software engineering areas for tackling the above problems. The authors suggest several phase-independent and phase-dependent techniques for programming in the large. It is shown how research in automatic programming, knowledge-based systems, metrics, and programming environments can make a significant difference in the ability to develop large systems.