Abstract We study distributed agreement in microbial distributed systems under stochastic population dynamics and competitive interactions. Motivated by recent applications in synthetic biology, we examine how the presence and absence of direct competition among microbial species influences their ability to reach majority consensus . In this problem, two species are designated as input species, and the goal is to guarantee that eventually only the input species which had the highest initial count prevails. We show that direct competition dynamics reach majority consensus with high probability even when the initial gap between the species is small, i.e., $$\Omega (\sqrt{n\log n})$$ , where n is the initial population size. In contrast, we show that absence of direct competition is not robust: solving majority consensus with constant probability requires a large initial gap of $$\Omega (n)$$ . To corroborate our analytical results, we use simulations to show that these consensus dynamics occur within practical biological time scales.

Biochemical Reaction Networks (BCRNs) model species and their interactions via reactions. They have been extensively used in chemistry and extended to biological settings by generalizing the reactions' kinetics. However, detailed models of biochemical processes tend to result in complex BCRN models. We present the Meta-species Oriented Biosystem Syntax (MobsPy), a language designed to simplify the modeling process using the concept of meta-species. Meta-species are constructed using a bottom-up approach from base species, which represent elementary, simple characteristics. These characteristics are then combined to create meta-species with all their complex behavior. The combined species have characteristics that are the Cartesian product of the base species' characteristics and feature inheritance of reactions involving the base species. New reactions can involve all the states of a meta-species or only a subset that is selected via a query. In particular, reactions of meta-species can express a state change of one of the reactants. MobsPy is deployed as a Python package. We showcase its modeling capabilities by building concise models for biochemical systems from the literature.

Permutation equivariance (PE) is a property widely present in mathematics and machine learning. Classic deep reinforcement learning (DRL) algorithms, such as Deep Q-Network (DQN), require thoroughly exploring the state space to achieve optimal performance. For a PE problem such as the Multi-Armed Bandit (MAB) problem, the PE property helps reduce the space that needs to be explored. This paper proposes PEDQN, a PE DRL framework based on DQN by applying a PE neural network structure. Our MAB experiments show that PEDQN has clear advantages compared to DQN with a fully connected network and achieves the same or better performance than UCB1 when tested in the same environment as the training.

One of the key challenges in synthetic biology is devising robust signaling primitives for engineered microbial consortia. In such systems, a fundamental signal amplification problem is the majority consensus problem: given a system with two input species with initial difference of Δ in population sizes, what is the probability that the system reaches a state in which only the initial majority species is present?

Dynamic digital timing analysis aims at substituting highly accurate but slow analog simulations of digital circuits with less accurate but fast digital approaches to facilitate tracing timing relations between individual transitions in a signal trace. This primarily requires gate delay models, where the input-to-output delay of a transition also depends on the signal history. We focus on a recently proposed hybrid delay model for CMOS multi-input gates, exemplified by a 2-input NOR gate, which is the only delay model known to us that faithfully captures both single-input switching (SIS) and multi-input switching (MIS) effects, also known as “Charlie effects”. Despite its simplicity as a first-order model, simulations have revealed that suitably parametrized versions of the model predict the actual delays of NOR gates accurately. However, the approach considers isolated gates without their interconnect. In this work, we augment the existing model and its theoretical analysis by a first-order interconnect, and conduct a systematic evaluation of the resulting modeling accuracy: Using SPICE simulations, we study both SIS and MIS effects on the overall delay of NOR gates under variation of input driving strength, wire length, load capacitance and CMOS technology, and compare it to the predictions of appropriately parametrized versions of our model. Overall, our results reveal a surprisingly good accuracy of our fast delay model.

Thresholded mode-switched ODEs are restricted dynamical systems that switch ODEs depending on digital input signals only, and produce a digital output signal by thresholding some internal signal. Such systems arise in recent digital circuit delay models, where the analog signals within a gate are governed by ODEs that change depending on the digital inputs.

Consider an arbitrary network of communicating modules on a chip, each requiring a local signal telling it when to execute a computational step. There are three common solutions to generating such a local clock signal: 1) by deriving it from a single, central clock source; 2) by local, free-running oscillators; or 3) by handshaking between neighboring modules. Conceptually, each of these solutions is the result of a perceived dichotomy in which (sub)systems are either clocked or asynchronous. We present a solution and its implementation that lies between these extremes. Based on a distributed gradient clock synchronization (GCS) algorithm, we show a novel design providing modules with local clocks, the frequency bounds of which are almost as good as those of free-running oscillators, yet neighboring modules are guaranteed to have a phase offset substantially smaller than one clock cycle. Concretely, parameters obtained from a 15-nm application specific integrated circuit (ASIC) simulation running at 2 GHz yield mathematical worst-case bounds of 20 ps on the phase offset for a$32\,\, \times 32$node grid network.

Abstract Computing via synthetically engineered bacteria is a vibrant and active field with numerous applications in bio-production, bio-sensing, and medicine. Motivated by the lack of robustness and by resource limitation inside single cells, distributed approaches with communication among bacteria have recently gained in interest. In this paper, we focus on the problem of population growth happening concurrently, and possibly interfering, with the desired bio-computation. Specifically, we present a fast protocol in systems with continuous population growth for the majority consensus problem and prove that it correctly identifies the initial majority among two inputs with high probability if the initial difference is $$\varOmega (\sqrt{n\log n})$$ Ω ( n log n ) where n is the total initial population. We also present a fast protocol that correctly computes the Nand of two inputs with high probability. By combining Nand gates with the majority consensus protocol as an amplifier, it is possible to compute arbitrary Boolean functions. Finally, we extend the protocols to several biologically relevant settings. We simulate a plausible implementation of a noisy Nand gate with engineered bacteria. In the context of continuous cultures with a constant outflow and a constant inflow of fresh media, we demonstrate that majority consensus is achieved only if the flow is slower than the maximum growth rate. Simulations suggest that flow increases consensus time over a wide parameter range. The proposed protocols help set the stage for bio-engineered distributed computation that directly addresses continuous stochastic population growth.

In classical synchronous designs, supply voltage droops can be handled by accounting for them in clock margins. However, this results in a significant performance hit even if droops are rare. In contrast, adaptive strategies detect such potentially hazardous events and either initiate a rollback to a previous state or proactively reduce clock speed in order to prevent timing violations. The performance of such solutions critically depends on a very fast response to droops. State-of-the-art solutions incur synchronization delays in the order of several clock cycles to avoid, with sufficient probability, that the clock signal is affected by metastability. We present an all-digital circuit that can respond to droops within a fraction of a clock cycle. This is achieved by using potentially metastable measurement values to delay clock signalswhilethey undergo synchronization, instead ofafterthey are synchronized. The challenge is to ensure that this strategy does not lead to harmful glitches or metastable upsets within the circuit. To this end, we verify our solution by formally proving correctness. We complement our findings by simulations of a 65-nm ASIC design confirming the results of our analysis.

We introduce the Composable Involution Delay Model (CIDM) for fast and accurate digital simulation. It is based on the Involution Delay Model (IDM) [Függer et al., IEEE TCAD 2020], which has been shown to be the only existing candidate model for faithful glitch propagation. The IDM, however, has shortcomings that limit its applicability. Our CIDM thus reduces the characterization effort by allowing independent discretization thresholds, improves composability and increases the modeling power by exposing canceled pulse trains at the gate interconnect. We formally show that, despite these improvements, the CIDM still retains the IDM's faithfulness.

We introduce the prototype of a digital timing simulation and power analysis tool for integrated circuits that supports the involution delay model (Függer et al. 2019). Unlike the pure and inertial delay models typically used in digital timing analysis tools, the involution model faithfully captures short pulse propagation and related effects. Our Involution Tool facilitates experimental accuracy evaluation of variants of involution models, by comparing their timing and power predictions to those from SPICE and standard timing analysis tools. The tool is easily customizable w.r.t. instances of the involution model and circuits, and supports automatic test case generation and parameter sweeping. We demonstrate the capabilities of the Involution Tool by providing timing and power analysis results for three different circuits, namely, an inverter tree, the clock tree of an open-source processor, and a combinational circuit that involves multi-input NAND gates. Our evaluation uses two different technologies (15 nm and 65 nm CMOS), and three different variants of involution channels (Exp, Hill and SumExp-channels). It turns out that the timing and power predictions of all involution models are significantly better than the predictions obtained by standard digital simulations for the inverter tree and the clock tree, with the SumExp-channel channel clearly outperforming the others. For the NAND circuit, the performance of any involution model is generally comparable but not significantly better than that of standard models, however, which reveals some shortcomings of the existing involution channels for modeling multi-input gates.

Agreeing on a common value among a set of agents is a fundamental problem in distributed computing, which occurs in several variants: In contrast to exact consensus, approximate variants are studied in systems where exact agreement is not possible or required, e.g., in human-made distributed control systems and in the analysis of natural distributed systems, such as bird flocking and opinion dynamics. We study the time complexity of two classical agreement problems: non-terminating asymptotic consensus and terminating approximate consensus. Asymptotic consensus, requires agents to repeatedly set their outputs such that the outputs converge to a common value within the convex hull of initial values; approximate consensus requires agents to eventually stop setting their outputs, which must then lie within a predefined distance of each other. We prove tight lower bounds on the contraction ratios of asymptotic consensus algorithms subject to oblivious message adversaries, from which we deduce bounds on the time complexity of approximate consensus algorithms. In particular, the obtained bounds show optimality of asymptotic and approximate consensus algorithms presented by Charron-Bost et al. (ICALP’16) for certain systems, including the strongest oblivious message adversary in which asymptotic and approximate consensus are solvable. As a corollary we also obtain asymptotically tight bounds for asymptotic consensus in the classical asynchronous model with crashes. Central to the lower-bound proofs is an extended notion of valency, the set of reachable limits of an asymptotic consensus algorithm starting from a given configuration. We further relate topological properties of valencies to the solvability of exact consensus, shedding some light on the relation of these three fundamental problems in dynamic networks.

Computing with synthetically engineered bacteria is a vibrant and active field with numerous applications in bio-production, bio-sensing, and medicine. Motivated by the lack of robustness and by resource limitation inside single cells, distributed approaches with communication among bacteria have recently gained in interest. In this paper, we focus on the problem of population growth happening concurrently, and possibly interfering, with the desired bio-computation. Specifically, we present a fast protocol in systems with continuous population growth for the majority consensus problem and prove that it correctly identifies the initial majority among two inputs with high probability if the initial difference is $Ω(\sqrt{n\log n})$ where $n$ is the total initial population. We also present a fast protocol that correctly computes the NAND of two inputs with high probability. We demonstrate that combining the NAND gate protocol with the continuous-growth majority consensus protocol, using the latter as an amplifier, it is possible to implement circuits computing arbitrary Boolean functions.

A nonsplit graph is a directed graph where each pair of nodes has a common incoming neighbor. We show that the radius of such graphs is in O(loglogn), where n is the number of nodes. This is an exponential improvement on the previously best known upper bound of O(logn). We then generalize the result to products of nonsplit graphs. The analysis of nonsplit graph products has direct implications in the context of distributed systems, where processes operate in rounds and communicate via message passing in each round: communication graphs in several distributed systems naturally relate to nonsplit graphs and the graph product concisely represents relaying messages in such networks. Applying our results, we obtain improved bounds on the dynamic radius of such networks, i.e., the maximum number of rounds until all processes have received a message from a common process, if all processes relay messages in each round. We finally connect the dynamic radius to lower bounds for achieving consensus in dynamic networks.

Függer et al. (2016) proved that no existing digital circuit model, including those based on pure and inertial delay channels, faithfully captures glitch propagation: for the short-pulse filtration (SPF) problem similar to that of building a one-shot inertial delay, they showed that every member of the broad class of bounded single-history channels either contradicts the unsolvability of SPF in bounded time or the solvability of SPF in unbounded time in physical circuits. In this article, we propose binary circuit models based on novel involution channels that do not suffer from this deficiency. Namely, in sharp contrast to bounded single-history channels, SPF cannot be solved in bounded time with involution channels, whereas it is easy to provide an unbounded SPF implementation. Hence, binary-valued circuit models based on involution channels allow to solve SPF precisely when this is possible in physical circuits. Additionally, using both SPICE simulations and physical measurements of an inverter chain instrumented by high-speed analog amplifiers, we demonstrate that our model provides good modeling accuracy with respect to real circuits as well. Consequently, our involution channel model is not only a promising basis for sound formal verification but also allows to seamlessly improve existing dynamic timing analysis.

Accurate delay models are important for static and dynamic timing analysis of digital circuits, and mandatory for formal verification. However, Függer et al. [IEEE TC 2016] proved that pure and inertial delays, which are employed for dynamic timing analysis in state-of-the-art tools like ModelSim, NC-Sim and VCS, do not yield faithful digital circuit models. Involution delays, which are based on delay functions that are mathematical involutions depending on the previous-output-to-input time offset, were introduced by Függer et al. [DATE'15] as a faithful alternative (that can easily be used with existing tools). Although involution delays were shown to predict real signal traces reasonably accurately, any model with a deterministic delay function is naturally limited in its modeling power. In this paper, we thus extend the involution model, by adding non-deterministic delay variations (random or even adversarial), and prove analytically that faithfulness is not impaired by this generalization. Albeit the amount of non-determinism must be considerably restricted to ensure this property, the result is surprising: the involution model differs from non-faithful models mainly in handling fast glitch trains, where small delay shifts have large effects. This originally suggested that adding even small variations should break the faithfulness of the model, which turned out not to be the case. Moreover, the results of our simulations also confirm that this generalized involution model has larger modeling power and, hence, applicability.

We study the problem of asymptotic consensus as it occurs in a wide range of applications in both man-made and natural systems. In particular, we study systems with directed communication graphs that may change over time. We recently proposed a new family of convex combination algorithms in dimension one whose weights depend on the received values and not only on the communication topology. Here, we extend this approach to arbitrarily high dimensions by introducing two new algorithms: the ExtremePoint and the Centroid algorithm. Contrary to classical convex combination algorithms, both have component-wise contraction rates that are constant in the number of agents. Paired with a speed-up technique for convex combination algorithms, we get a convergence time linear in the number of agents, which is optimal. Besides their respective contraction rates, the two algorithms differ in the fact that the Centroid algorithm's update rule is independent of any coordinate system while the ExtremePoint algorithm implicitly assumes a common agreed-upon coordinate system among agents. The latter assumption may be realistic in some man-made multi-agent systems but is highly questionable in systems designed for the modelization of natural phenomena. Finally we prove that our new algorithms also achieve asymptotic consensus under very weak connectivity assumptions, provided that agent interactions are bidirectional.

In digital circuits, metastability can cause deteriorated signals that neither are logical 0 nor logical 1, breaking the abstraction of Boolean logic. Synchronizers, the only traditional countermeasure, exponentially decrease the odds of maintained metastability overtime. We propose a fundamentally different approach: It is possible to deterministically contain metastability by fine-grained logical masking so that it cannot infect the entire circuit. At the heart of our approach lies a time- and value-discrete model for metastability in synchronous clocked digital circuits, in which metastability is propagated in a worst-case fashion. The proposed model permits positive results and passes the test of reproducing Marino's impossibility results. We fully classify which functions can be computed by circuits with standard registers. Regarding masking registers, we show that more functions become computable with each clock cycle, and that masking registers permit exponentially smaller circuits for some tasks. Demonstrating the applicability of our approach, we present the first fault-tolerant distributed clock synchronization algorithm that deterministically guarantees correct behavior in the presence of metastability. As a consequence, clock domains can be synchronized without using synchronizers, enabling metastability-free communication between them.

In this work we study the performance of asymptotic and approximate consensus algorithms in dynamic networks. The asymptotic consensus problem requires a set of agents to repeatedly set their outputs such that the outputs converge to a common value within the convex hull of initial values. This problem, and the related approximate consensus problem, are fundamental building blocks in distributed systems where exact consensus among agents is not required, e.g., man-made distributed control systems, and have applications in the analysis of natural distributed systems, such as flocking and opinion dynamics. We prove new nontrivial lower bounds on the contraction rates of asymptotic consensus algorithms, from which we deduce lower bounds on the time complexity of approximate consensus algorithms. In particular, the obtained bounds show optimality of asymptotic and approximate consensus algorithms presented in [Charron-Bost et al., ICALP'16] for certain classes of networks that include classical failure assumptions, and confine the search for optimal bounds in the general case. Central to our lower bound proofs is an extended notion of valency, the set of reachable limits of an asymptotic consensus algorithm starting from a given configuration. We further relate topological properties of valencies to the solvability of exact consensus, shedding some light on the relation of these three fundamental problems in dynamic networks.

We introduce a new class of distributed algorithms for the approximate consensus problem in dynamic rooted networks, which we call amortized averaging algorithms. They are deduced from ordinary averaging algorithms by adding a value-gathering phase before each value update. This results in a drastic drop in decision times, from being exponential in the number n of processes to being polynomial under the assumption that each process knows n. In particular, the amortized midpoint algorithm is the first algorithm that achieves a linear decision time in dynamic rooted networks with an optimal contraction rate of 1/2 at each update step. We then show robustness of the amortized midpoint algorithm under violation of network assumptions: it gracefully degrades if communication graphs from time to time are non rooted, or under a wrong estimate of the number of processes. Finally, we prove that the amortized midpoint algorithm behaves well if processes can store and send only quantized values, rendering it well-suited for the design of dynamic networked systems. As a corollary we obtain that the 2-set consensus problem is solvable in linear time in any dynamic rooted network model.

We argue that a hexagonal grid with simple intermediate nodes is a robust alternative to buffered clock trees typically used for clock distribution in VLSI circuits, multi-core processors, and other applications that require accurate synchronization: Our HEX grid is Byzantine fault-tolerant, self-stabilizing, and seamlessly integrates with multiple synchronized clock sources, as used in multi-synchronous Globally Synchronous Locally Asynchronous (GALS) architectures. Moreover, HEX guarantees a small clock skew between neighbors even for wire delays that are only moderately balanced. We provide both a theoretical analysis of the worst-case skew and simulation results that demonstrate a very small average skew.

We show that no existing continuous-time, binary value-domain model for digital circuits is able to correctly capture glitch propagation. Prominent examples of such models are based on pure delay channels (P), inertial delay channels (I), or the elaborate Delay Degradation Model (DDM) channels proposed by Bellido-Diaz et al. We accomplish our goal by considering the border between solvability and non-solvability of a simple problem called short-pulse filtration (SPF), which is closely related to arbitration and synchronization. On one hand, we prove that SPF is solvable in bounded time in any such model that provides channels with non constant delay, like I and DDM. This is in opposition to the impossibility of solving bounded SPF in real (physical) circuit models. On the other hand, for binary circuit models with constant-delay channels, we prove that SPF cannot be solved even in unbounded time; again in opposition to physical circuit models. Consequently, indeed none of the binary value-domain models proposed so far (and that we are aware of) faithfully captures glitch propagation of real circuits. We finally show that these modeling mismatches do not hold for the weaker eventual SPF problem.

Fast digital timing simulations based on continuous-time, digital-value circuit models are an attractive and heavily used alternative to analog simulations. Models based on analytic delay formulas are particularly interesting here, as they also facilitate formal verification and delay bound synthesis of complex circuits. Recently, Függer et al. (arXiv:1406.2544 [cs.OH]) proposed a circuit model based on so-called involution channels. It is the first binary circuit model that realistically captures solvability of short-pulse filtration, a non-trivial glitch propagation problem related to building one-shot inertial delays.

International audience

Link reversal is a versatile algorithm design paradigm, originally proposed by Gafni and Bertsekas in 1981 for routing and subsequently applied to other problems including mutual exclusion, leader election, and resource allocation. Although these algorithms are well known, until now there have been only preliminary results on time complexity, even for the simplest link reversal algorithm for routing, called Full Reversal. In Full Reversal, a sink reverses all its incident links, whereas in other link reversal algorithms (e.g., Partial Reversal), a sink reverses only some of its incident links. Charron-Bost et al. introduced a generalization, called LR, that includes Full and Partial Reversal as special cases. In this article, we present an exact expression for the time complexity of LR. The expression is stated in terms of simple properties of the initial graph. The result specializes to exact formulas for the time complexity of any node in any initial acyclic directed graph for both Full and Partial Reversal. Having the exact formulas provides insight into the behavior of Full and Partial Reversal on specific graph families. Our first technical insight is to describe the behavior of Full Reversal as a dynamical system and to observe that this system is linear in min-plus algebra. Our second technical insight is to overcome the difficulty posed by the fact that LR is not linear by transforming every execution of LR from an initial graph into an execution of Full Reversal from a different initial graph while maintaining the execution's work and time complexity.

We present a runtime verification framework that allows on-line monitoring of past-time Metric Temporal Logic (ptMTL) specifications in a discrete time setting. We design observer algorithms for the time-bounded modalities of ptMTL, which take advantage of the highly parallel nature of hardware designs. The algorithms can be translated into efficient hardware blocks, which are designed for reconfigurability, thus, facilitate applications of the framework in both a prototyping and a post-deployment phase of embedded real-time systems. We provide formal correctness proofs for all presented observer algorithms and analyze their time and space complexity. For example, for the most general operator considered, the time-bounded Since operator, we obtain a time complexity that is doubly logarithmic both in the point in time the operator is executed and the operator's time bounds. This result is promising with respect to a self-contained, non-interfering monitoring approach that evaluates real-time specifications in parallel to the system-under-test. We implement our framework on a Field Programmable Gate Array platform and use extensive simulation and logic synthesis runs to assess the benefits of the approach in terms of resource usage and operating frequency.

Today’s hardware technology presents a new challenge in designing robust systems. Deep submicron VLSI technology introduces transient and permanent faults that were never considered in low-level system designs in the past. Still, robustness of that part of the system is crucial and needs to be guaranteed for any successful product. Distributed systems, on the other hand, have been dealing with similar issues for decades. However, neither the basic abstractions nor the complexity of contemporary fault-tolerant distributed algorithms match the peculiarities of hardware implementations. This article is intended to be part of an attempt striving to bridge over this gap between theory and practice for the clock synchronization problem. Solving this task sufficiently well will allow to build an ultra-robust high-precision clocking system for hardware designs like systems-on-chips in critical applications. As our first building block, we describe and prove correct a novel distributed, Byzantine fault-tolerant, probabilistically self-stabilizing pulse synchronization protocol, called FATAL, that can be implemented using standard asynchronous digital logic: Correct FATAL nodes are guaranteed to generate pulses (i.e., unnumbered clock ticks) in a synchronized way, despite a certain fraction of nodes being faulty. FATAL uses randomization only during stabilization and, despite the strict limitations introduced by hardware designs, offers optimal resilience and smaller complexity than all existing protocols. Finally, we show how to leverage FATAL to efficiently generate synchronized, self-stabilizing, high-frequency clocks.

We present the first implementation of a distributed clock generation scheme for Systems-on-Chip that recovers from an unbounded number of arbitrary transient faults despite a large number of arbitrary permanent faults. We devise self-stabilizing hardware building blocks and a hybrid synchronous/asynchronous state machine enabling metastability-free transitions of the algorithm's states. We provide a comprehensive modeling approach that permits to prove, given correctness of the constructed low-level building blocks, the high-level properties of the synchronization algorithm (which have been established in a more abstract model). We believe this approach to be of interest in its own right, since this is the first technique permitting to mathematically verify, at manageable complexity, high-level properties of a fault-prone system in terms of its very basic components. We evaluate a prototype implementation, which has been designed in VHDL, using the Petrify tool in conjunction with some extensions, and synthesized for an Altera Cyclone FPGA.

In this paper, we show how to build synchronized clocks of arbitrary size atop of existing small-sized clocks, despite arbitrary faults. Our solution is both self-stabilizing and Byzantine fault-tolerant, and needs merely single-bit channels. It involves a reduction to Byzantine fault-tolerant consensus, which allows different consensus algorithms to be plugged in for matching the actual clock sizes and resilience requirements best. We demonstrate the practicability of our approach by means of an FPGA implementation and its experimental evaluation. To also address the cases where deterministic algorithms hit fundamental limits, we provide a novel randomized self-stabilizing Byzantine consensus algorithm that works very well also in these settings, along with its correctness proof and stabilization time analysis.

We argue that grid structures are a very promising alternative to the standard approach for distributing a clock signal throughout VLSI circuits and other hardware devices. Traditionally, this is accomplished by a delay-balanced clock tree, which distributes the signal supplied by a single clock source via carefully engineered and buffered signal paths.

Designing algorithms for distributed systems that provide a round abstraction is often simpler than designing for those that do not provide such an abstraction. Further, distributed systems need to tolerate various kinds of failures. The concept of a synchronizer deals with both: It constructs rounds and allows masking of transmission failures. One simple way of dealing with transmission failures is to retransmit a message until it is known that the message was successfully received. We calculate the exact value of the average rate of a retransmission-based synchronizer in environments with probabilistic message loss, within which the synchronizer shows nontrivial timing behavior. We show how to make this calculation efficient, and present analytical results on the convergence speed. The theoretic results, based on Markov theory, are backed up with Monte Carlo simulations.

Classic distributed computing abstractions do not match well the reality of digital logic gates, which are the elementary building blocks of Systems-on-Chip (SoCs) and other Very Large Scale Integrated (VLSI) circuits: Massively concurrent, continuous computations undermine the concept of sequential processes executing sequences of atomic zero-time computing steps, and very limited computational resources at gate-level make even simple operations prohibitively costly. In this paper, we introduce a modeling and analysis framework based on continuous computations and zero-bit message channels, and employ this framework for the correctness & performance analysis of a distributed fault-tolerant clocking approach for Systems-on-Chip (SoCs). Starting out from a “classic” distributed Byzantine fault-tolerant tick generation algorithm, we show how to adapt it for direct implementation in clockless digital logic, and rigorously prove its correctness and derive analytic expressions for worst case performance metrics like synchronization precision and clock frequency. Rather than on absolute delay values, both the algorithm’s correctness and the achievable synchronization precision depend solely on the ratio of certain path delays. Since these ratios can be mapped directly to placement & routing constraints, there is typically no need for changing the algorithm when migrating to a faster implementation technology and/or when using a slightly different layout in an SoC.

Although substantial analysis has been done on the Full Reversal (FR) routing algorithm since its introduction by Gafni and Bertsekas in 1981, a complete understanding of its functioning---especially its time complexity---has been missing until now. In this paper, we derive the first exact formula for the time complexity of FR: given any (acyclic) graph the formula provides the exact time complexity of any node in terms of some simple properties of the graph. Our major technical insight is to describe executions of FR as a dynamical system, and to observe that this system is linear in the min-plus algebra.

No abstract available.

Deterministic replay is used during testing to reproduce a scenario and drive the system under test to a given state. In this work, we replay ana prioridefined bus traffic to influence the clock synchronization mechanism. Beyond testing this distributed mechanism itself, our aim is to draw conclusions on the nodes' bus receiver operation. Since these replay activities are part of a transparent online test procedure, it is important to ensure that they do not represent a threat for proper system operation. We show this for TTP/C by means of a generic formal proof, while for the case of FlexRay we formally prove that the system precision can be bounded according to the replay operation applied. Experimental results confirm and illustrate our approach.

Systems on chip (SoC) have much in common with traditional (networked) distributed systems in that they consist of largely independent components with dedicated communication interfaces. Therefore the adoption of classic distributed algorithms for SoCs suggests itself. The implementation complexity of these algorithms, however, significantly depends on the underlying failure models. In traditional software-based solutions this is normally not an issue, such that the most unconstrained, namely the Byzantine, failure model is often applied here. Our case study of a hardware implemented tick synchronization algorithm shows, however, that in an SoC-implementation substantial hardware savings can result from restricting the failure model to benign failures (omissions, crashes). On the downside, it turns out that such restricted failure models have a fairly poor coverage with respect to the hardware faults occurring in practice, and that additional measures to enforce these restrictions may entail an implementation overhead that outweighs the gain obtained in the implementation of a simpler algorithm. As a remedy we investigate the potential of failure transformation in this context and show that this technique may indeed yield an optimized overall solution.