Stabilizing data-link over non-FIFO channels with optimal fault-resilience

Self-stabilizing systems have the ability to converge to a correct behavior when started in any configuration. Most of the work done so far in the self-stabilization area assumed either communication via shared memory or via FIFO channels.This paper is the first to lay the bases for the design of self-stabilizing message passing algorithms over unreliable non-FIFO channels. We propose an optimal stabilizing data-link layer that emulates a reliable FIFO communication channel over unreliable capacity bounded non-FIFO channels (the channel capacity is known to the protocol).     

Exposure to deadlock for communicating processes is hard to detect

It is shown that the applicability of global state analysis as a tool for proving correctness of communication protocols is limited. Brand and Zafiropulo (1983) showed that reachability of global deadlock states for protocols with unbounded FIFO channels is undecidable. It is shown that the same is true for unbounded non-FIFO channels. For bounded FIFO channels the problem is shown to be PSPACE-hard.     

“Pay bursts only once” does not hold for non-FIFO guaranteed rate nodes

We consider end-to-end delay bounds in a network of guaranteed rate (GR) nodes. We demonstrate that, contrary to what is generally believed, the existing end-to-end delay bounds apply only to GR nodes that are FIFO per flow. We show this by exhibiting a counter example. Then, we show that the proof of the existing bounds has a subtle, but important, dependency on the FIFO assumption, which was never noticed before. Finally, we give a tight delay bound that is valid in the non-FIFO case; it is noticeably higher that the existing one. In particular, the phenomenon known as “pay bursts only once” does not apply to non-FIFO nodes. These findings are important in the context of differentiated services. Indeed the existing bounds have been applied to cases where a flow (in the sense of the GR definition) is an aggregate of end-user microflows, and it is not generally true that a router is FIFO per aggregate; thus, the GR node model of a differentiated services router cannot always be assumed to be FIFO per flow.     

Dual-Priority versus Background Scheduling: A Path-Wise Comparison

In this paper, two well-known scheduling policies for real-time systems, namely background scheduling (BS) and dual-priority (DP) are compared in terms of response times for soft real-time traffic (SRT). It is proved in the preemptive as well as in the non-preemptive case that, when the SRT traffic is FIFO, the DP policy always outperforms BS for all instances of SRT tasks. When the SRT traffic is not FIFO but if all tasks are of equal size then, in the non-preemptive case, the average response times is shown to be always better under DP than under BS. As a complementary result, some non-FIFO examples where BS behaves better than DP for some SRT tasks but also on the average of the SRT response times, are given. The proofs are based on a trajectorial method that may be used for comparing other scheduling policies.     

Automatically Verifying Concurrent Queue Algorithms

Concurrent FIFO queues are a common component of concurrent systems. Using a single shared lock to prevent concurrent manipulations of queue contents reduces system concurrency. Therefore, many algorithms were suggested to increase concurrency while maintaining the correctness of queue manipulations. This paper shows how to automatically verify partial correctness of concurrent FIFO queue algorithms using existing abstract interpretation techniques. In particular, we verify all the safety properties originally specified for two concurrent queue algorithms without imposing an a priori bound on the number of allocated objects and threads.     

Simulating perfect channels with probabilistic lossy channels

We consider the problem of deciding whether an infinite-state system (expressed as a Markov chain) satisfies a correctness property with probability 1. This problem is, of course, undecidable for general infinite-state systems. We focus our attention on the model of probabilistic lossy channel systems consisting of finite-state processes that communicate over unbounded lossy FIFO channels. Abdulla and Jonsson have shown that safety properties are decidable while progress properties are undecidable for non-probabilistic lossy channel systems. Under assumptions of “sufficiently high” probability of loss, Baier and Engelen have shown how to check whether a property holds of probabilistic lossy channel system with probability 1. In this paper, we consider a model of probabilistic lossy channel systems, where messages can be lost only during send transitions. In contrast to the model of Baier and Engelen, once a message is successfully sent to channel, it can only be removed through a transition which receives the message. We show that checking whether safety properties hold with probability 1 is undecidable for this model. Our proof depends upon simulating a perfect channel, with a high degree of confidence, using lossy channels.     

Fast batched data transfer with flush channels: A performance analysis

A flush channel offers the implementor of a distributed application the flexibility of specifying a message delivery order apropos of the demands of the application. This stands in marked contrast to the rigid FIFO (first-in-first-out) delivery order of communication with a FIFO channel. The more restrictive the delivery order, the less concurrency possible to exploit in message transmissions over a multi-path system. This paper investigates the possible gain in effective network bandwidth when a large amount of information, such as the transmission of image data, is transmitted over a multi-path flush channel as compared to a multi-path FIFO channel. Analytical and simulation results illustrate that the relaxed delivery order restrictions of the flush channel may reduce the mean message response time by a factor of the number of message fragments. This difference may be critical in meeting real-time requirements of an application.     

一种新的高速ASI的设计与实现

介绍了一种新的高速ASI的设计与实现。该接口以CYPRESS公司的CY7B923和CY7B933的基础,辅之以EPLD和FIFO,实现了ASI的发送与接收功能。接口符合DVB－ASI接口规范,实现了高速270Mbit/s的Mpeg-2传输流传输。文中首先介绍了ASI的特点,构成：接着以本文实现的DVB－ASI为重点,详细阐述了它的硬件组成与硬件实现;最后给出了DVB－ASI接口的测试实验。本文设计的DVB－ASI接口经在多节目复用器,码流发生分析仪,高清编码器和解码器中的成功应用,证明了其设计的正确性与可靠性。     

CHAUS: Scalable VM-Based Channels for Unbounded Streaming

Stream processing is a special form of the dataflow execution model that offers extensive opportunities for optimization and automatic parallelism. A streaming application is represented by a graph of computation stages that communicate with each other via FIFO channels. In shared-memory environment, an FIFO channel is classically a common, fixed-size synchronized buffer shared between the producer and the consumer. As the number of concurrent stage workers increases, the synchronization overheads, such as contention and waiting times, rise sharply and severely impair application performance. In this paper, we present a novel multithreaded model which isolates memory between threads by default and provides a higher level abstraction for scalable unicast or multicast communication between threads — CHAUS (Channel for Unbounded Streaming). The CHAUS model hides the underlying synchronization details, but requires the user to declare producer-consumer relationship of a channel in advance. It is the duty of the runtime system to ensure reliable data transmission at data item granularity as declared. To achieve unbounded buffer for streaming and reduce the synchronization overheads, we propose a virtual memory based solution to implement a scalable CHAUS channel. We check the programmability of CHAUS by successfully porting dedup and ferret from PARSEC as well as implementing MapReduce library with Phoenix-like API. The experimental results show that workloads built with CHAUS run faster than those with Pthreads, and CHAUS has the best scalability compared with two Pthread versions. There are three workloads whose CHAUS versions only spend no more than 0.17x runtime of Pthreads on both 16 and 32 cores.     

The inhibition spectrum and the achievement of causal consistency

Summary.  We consider the problem of distinguishing causally-consistent global states in asynchronous distributed systems. Such states are fundamental to asynchronous systems, because they correspond to possible simultaneous global states; their detection arises in a variety of distributed applications, including global checkpointing, deadlock detection, termination detection, and broadcasting. A consistent-cut protocol is a protocol which in every run will designate for each processor a state, in such a way that these states together form a consistent cut. We analyze the cost of achieving causal consistency in terms of the extent to which a consistent-cut protocol delays events of the underlying system. We refer to the delaying action of a protocol as inhibition. A protocol using local inhibition may cause the delay of some of a processor’s events until that processor has performed some number of local actions; a protocol using global inhibition may force the delay of some of a processor’s events until that processor has received some communication from other processors. Based on a variety of system and protocol characteristics, including the ability to locally or globally inhibit particular types of events, we give three impossibility results and examine some existing protocols. We are then able to present a thirty-six case summary of protocols and impossibility results for the determination of causally-consistent states as a function of those characteristics. In particular, we demonstrate that local inhibition is necessary and sufficient to solve this problem for general FIFO systems, while global send inhibition is necessary and sufficient for general non-FIFO systems. Received: January 1993 / Accepted: January 1996     

异步FIFO的FPGA实现

本文提出了一种用FPGA芯片实现异步FIFO的方案，重点强调了异步FIFO握手信号FULL、EMPTY的设计，并用VHDL语言给以实现。     

基于双排序原理的先进先出数据核销高速通用算法

本文按照软件中台的思想,设计了一个针对先进先出(First-In First-Out,FIFO)[1]数据核销的通用实现框架及其对应的入库数据模型、消费数据模型和匹配核销模型.同时,设计了基于双排序原理的先进先出数据核销高速实现方法.该方法按照匹配规则先对数据进行排序,然后对两个有序队列进行单循环匹配查找,避免了传统先...     

Multi-server blind quantum computation over collective-noise channels

Blind quantum computation (BQC) enables ordinary clients to securely outsource their computation task to costly quantum servers. Besides two essential properties, namely correctness and blindness, practical BQC protocols also should make clients as classical as possible and tolerate faults from nonideal quantum channel. In this paper, using logical Bell states as quantum resource, we propose multi-server BQC protocols over collective-dephasing noise channel and collective-rotation noise channel, respectively. The proposed protocols permit completely or almost classical client, meet the correctness and blindness requirements of BQC protocol, and are typically practical BQC protocols.     

Design and analysis of a fifo linked loosely coupled dual processor system

This paper describes the design, implementation and performance analysis of a loosely coupled dual processor system employing FIFO based communication links. Two cards, each supporting a FIFO queue with 8-bit static RAMs and associated counters, are used to connect two IBM PCs. The circuit is controlled entirely by an Altera EP900 which facilitates possible modifications of hardware in the future. Overflow and conflict error conditions trigger and interrupt request and provisions have been made to retry the last operation upon the occurrence of such error conditions. Details on the software developed for interprocessor communication have been provided. The performance of the dual processor system has been analysed with matrix multiplication operations and it is found that when compared to a single processor system, the dual processor system offers a higher throughput when the order of the matrices is seven or above. The system is currently being used as an aid for teaching various concepts on parallel programming and design aspects for developing hardware for multiprocessor systems and subsystems.     

A functional correspondence between call-by-need evaluators and lazy abstract machines

We bridge the gap between compositional evaluators and abstract machines for the lambda-calculus, using closure conversion, transformation into continuation-passing style, and defunctionalization of continuations. This article is a followup of our article at PPDP 2003, where we consider call by name and call by value. Here, however, we consider call by need.We derive a lazy abstract machine from an ordinary call-by-need evaluator that threads a heap of updatable cells. In this resulting abstract machine, the continuation fragment for updating a heap cell naturally appears as an ‘update marker’, an implementation technique that was invented for the Three Instruction Machine and subsequently used to construct lazy variants of Krivine's abstract machine. Tuning the evaluator leads to other implementation techniques such as unboxed values. The correctness of the resulting abstract machines is a corollary of the correctness of the original evaluators and of the program transformations used in the derivation.     

动态可重构总线数据传输管理方法设计与实现

为实现总线多通道数据并发高速传输与容错,解决故障状态下的总线数据动态重构问题,设计一种动态可重构总线数据传输管理方法。采用四体先入先出队列(FIFO)进行数据缓冲存储,利用通道故障状态表,通过4×32矩阵开关数据,传输管理阵列组织与4个FIFO缓冲区及所有有效通道间的数据传输。在8通道系统中的实验结果表明,最高通信速率可达到800 Mb/s,能对7个通道故障进行动态容错。     

Towards Acceptability of Optimizations: An Extended View of Compiler Correctness

The theory of relative program correctness and its preservation allows for elaborate and practically adequate definitions of correct implementation notions as they are established by transformations implemented in a compiler. It generalizes Hoare's and Floyd's partial and total program correctness and correctness preservation by classifying finite and infinite errors to be either acceptable (unavoidable) or unacceptable (chaotic, to be avoided). We will define correct implementation by particular compositional diagram commutativities, and we will further extend this theory also to express correctness of compiling specifications and of compiler programs and their implementations in the same uniform relational setting. Unacceptable error outcomes can semantically model pre-conditions such as well-formedness conditions for compilers or optimization pre-conditions for user programs. Our theory allows to distinguish between different correct implementation requirements, for instance (horizontally) for user programs or (vertically) for the compiler implementation, just as if we would switch on and off compiler options and tune one compiler to appropriately preserve correctness in different application domains.     

An optimistic approach to lock-free FIFO queues

First-in-first-out (FIFO) queues are among the most fundamental and highly studied concurrent data structures. The most effective and practical dynamic-memory concurrent queue implementation in the literature is the lock-free FIFO queue algorithm of Michael and Scott, included in the standard Java ^TM Concurrency Package. This work presents a new dynamic-memory concurrent lock-free FIFO queue algorithm that in a variety of circumstances performs better than the Michael and Scott queue. The key idea behind our new algorithm is a novel way of replacing the singly-linked list of Michael and Scott, whose pointers are inserted using a costly compare-and-swap (CAS) operation, by an “optimistic” doubly - linked list whose pointers are updated using a simple store, yet can be “fixed” if a bad ordering of events causes them to be inconsistent. We believe it is the first example of such an “optimistic” approach being applied to a real world data structure. A preliminary version of this paper appeared in the proceedings of the 18th International Conference on Distributed Computing (DISC) 2004, pages 117–131.