Parallel Processing Letters

This paper focuses on the formal proof of parallel programs dedicated to distributed memory symmetric interconnection networks; communications are realized by message passing. We have developed a method to formally verify the computational correctness of this kind of application. Using the notion of Cayley graphs to model the networks in the Nqthm theorem prover, we have formally specified and mechanically proven correct a large set of collective communication primitives. Our compositional approach allows us to reuse these libraries of pre-proven procedures to validate complex application programs within Nqthm. This is illustrated by three examples.

The assumption of the existence of global time, which significantly simplifies the analysis of distributed systems, is generally safe since most of the conclusions obtained under the global time axiom can be transferred to the frame where no such assumption is made. In this note, we show that the compositionality of the well-known correctness condition for concurrent objects called linearizability does not satisfy this simplification rule: we present a simple non-linearizable system composed of two objects which are individually linearizable.

This paper presents a quorum-based self-stabilizing protocol for the phase synchronization problem. In the protocol, nodes proceed in a cyclic sequence of K phases, K > 2. The phases for any two nodes in the system can be at most one apart. This protocol is suited to work with many existing quorum-based protocols.

A heuristic has shown that the results achieved by earlier algorithms for gossiping on cube-connected-cycles (CCCs) in the unit-cost telephone model were not optimal, but no general pattern was revealed. In this paper new gossiping algorithms are presented that apply to CCCs of all sizes. Most importantly, we show that for gossiping on the "k-dimensional" network, CCC_k, with k even, gossiping can be performed in 5/2 · k - 2 communication rounds, which exactly matches the lower bound, thus completely solving the gossiping problem for these networks. For odd k we improve upon the best previous algorithm without matching the lower bound.

In this paper, we present a coding method to capture QoS information in hypercube multicomputers. The coding method is based on a localized algorithm where each node interacts with its neighbors to gather QoS information. Specifically, each node maintains a QoS vector where the k-th element represents the guaranteed QoS performance to a destination that is k hops away. The localized algorithm exhibits desirable properties of self-stabilizing, self-optimizing, and self-healing. Simulation results show that this coding method provides a good approximation of the minimum QoS value to a k-hop destination and, at the same time, uses a relatively small number of packets to propagate a change in link state (QoS value) compared with the classical distributed Bellman-Ford method.

In this paper, we address the goal of executing Java parallel applications in a group of nodes of a Beowulf cluster transparently chosen by a metacomputing system oriented to efficient execution of Java bytecode, with support for scientific computing. To this end, we extend the Java virtual machine by providing a message passing interface and quick access to distributed high performance resources. Also, we introduce the execution of parallel linear algebra methods for large objects from sequential Java applications by invoking SPLAM, our parallel linear algebra package.

This paper focuses on the improvement in the quality of computation provided by parallelism. The problem of interest is that of computing the maximum of a nonlinear feedback function in a real-time environment. We show that the solution obtained in parallel is significantly, provably, and consistently better than a sequential one. It is important to note that our purpose is not to demonstrate merely that a parallel computer can obtain a solution to a computational problem that is of higher quality than one derived sequentially. The latter is an interesting (and often surprising) observation in its own right, but we wish to go further. It is shown here that the improvement in quality due to parallelism can be arbitrarily high. To be specific, the ratio of the parallel solution to the sequential one is typically superlinear in the number of processors used by the parallel computer. This result is akin to superlinear speedup—a phenomenon itself originally thought to be impossible.

In this paper we present and analyze new sequential and parallel heuristics to approximate the Minimum Linear Arrangement problem (MinLA). The heuristics consist in obtaining a first global solution using Spectral Sequencing and improving it locally through Simulated Annealing. In order to accelerate the annealing process, we present a special neighborhood distribution that tends to favor moves with high probability to be accepted. We show how to make use of this neighborhood to parallelize the Metropolis stage on distributed memory machines by mapping partitions of the input graph to processors and performing moves concurrently. The paper reports the results obtained with this new heuristic when applied to a set of large graphs, including graphs arising from finite elements methods and graphs arising from VLSI applications. Compared to other heuristics, the measurements obtained show that the new heuristic improves the solution quality, decreases the running time and offers an excellent speedup when ran on a commodity network made of nine personal computers.