Trace-history-dependent effects such as drafting and multi-input switching are poorly modeled in static timing analysis, yet do not justify excessive transistor-level analog simulations. We present a closed-form analytic delay model for fast digital dynamic timing analysis of interconnected NOR gates, which captures both effects. Our delay formulas are derived from a thresholded hybrid gate model based on non-constant-coefficient differential equations, which can be analytically parametrized via a few characteristic gate delay values. By utilizing our formulas in the discrete-event simulator-based Involution Tool, we show that accurate circuit simulation can be done at roughly inertial-delay cost. The significantly improved timing prediction accuracy of our delay model is demonstrated by two representative benchmark circuits.

We provide a complete characterization of the solvability/impossibility of deterministic stabilizing consensus in virtually any computing model with benign process and communication faults using point-set topology. Relying on the topologies for infinite executions introduced by Nowak, Schmid and Winkler (JACM, 2024) for terminating consensus, we show that semi-open decision sets and semi-continuous decision functions as introduced by Levin (AMM, 1963) are the appropriate means for this characterization: Unlike the continuous decision functions for terminating consensus, semi-continuous functions do not require the inverse image of an open set to be open and hence allow to map a connected space to a disconnected one. We also show that multi-valued stabilizing consensus with weak and strong validity are equivalent, as is the case for terminating consensus. By applying our results to (variants of) all the known possibilities/impossibilities for stabilizing consensus, we easily provide a topological explanation of these results.

Investigating the temporal behavior of digital circuits is a crucial step in system design, usually done via analog or digital simulation. Analog simulators like SPICE iteratively solve the differential equations characterizing the circuits' components numerically. Although unrivaled in accuracy, this is only feasible for small designs, due to the high computational effort even for short signal traces. Digital simulators use digital abstractions for predicting the timing behavior of a circuit. We advocate a novel approach, which generalizes digital traces to traces consisting of sigmoids, each parameterized by threshold crossing time and slope. For a given gate, we use an artificial neural network for implementing the transfer function that predicts, for any trace of input sigmoids, the parameters of the generated output sigmoids. By means of a prototype simulator, which can handle circuits consisting of inverters and NOR gates, we demonstrate that our approach operates substantially faster than an analog simulator, while offering a much better accuracy than a digital simulator.

We develop a new lower bound for k-set agreement in synchronous message-passing systems connected by an arbitrary directed communication network, where up to t processes may crash. Our result thus generalizes the ⌊t/k⌋ + 1 lower bound for complete networks in the t-resilient model by Chaudhuri, Herlihy, Lynch, and Tuttle [JACM 2000]. Moreover, it generalizes two lower bounds for oblivious algorithms in synchronous systems connected by an arbitrary undirected communication network known to the processes, namely, the domination number-based lower bound by Castañeda, Fraigniaud, Paz, Rajsbaum, Roy, and Travers [TCS 2021] for failure-free processes, and the radius-based lower bound in the t-resilient model by Fraigniaud, Nguyen, and Paz [STACS 2024]. Our topological proof non-trivially generalizes and extends the connectivity-based approach for the complete network, as presented in the book by Herlihy, Kozlov, and Rajsbaum (2013). It is based on a sequence of shellable carrier maps that, starting from a shellable input complex, determine the evolution of the protocol complex: During the first ⌊t/k⌋ rounds, carrier maps that crash exactly k processes per round are used, which ensure high connectivity of their images. A Sperner’s lemma style argument can thus be used to prove that k-set agreement is still impossible by that round. From round ⌊t/k⌋ + 1 up to our actual lower bound, a novel carrier map is employed, which maintains high connectivity. As a by-product, our proof also provides a strikingly simple lower-bound for k-set agreement in synchronous systems with an arbitrary communication network, where exactly t ≥ 0 processes crash initially, i.e., before taking any step. We demonstrate that the resulting additional agreement overhead can be expressed via an appropriately defined radius of the communication graphs, and show that the usual input pseudosphere complex for k-set agreement can be replaced by an exponentially smaller input complex based on Kuhn triangulations, which we prove to be also shellable.

Abstract We provide novel epistemic logical language and semantics for modeling and analysis of byzantine fault-tolerant multi-agent systems, with the intent of not only facilitating reasoning about the agents’ fault status but also supporting model updates for repair and state recovery. Besides the standard knowledge modalities, our logic provides additional agent-specific hope modalities capable of expressing that an agent is not faulty, and also dynamic modalities enabling change to the agents’ correctness status. These dynamic modalities are interpreted as model updates that come in three flavors: fully public, more private, and/or involving factual change. Tailored examples demonstrate the utility and flexibility of our logic for modeling a wide range of fault-detection, isolation, and recovery (FDIR) approaches in mission-critical distributed systems. By providing complete axiomatizations for all variants of our logic, we also create a foundation for building future verification tools for this important class of fault-tolerant applications.

Abstract We study the problem of solving consensus in synchronous directed dynamic networks, in which communication is controlled by an oblivious message adversary that picks the communication graph to be used in a round from a fixed set of graphs $$\textbf{D}$$ D arbitrarily. In this fundamental model, determining consensus solvability and designing efficient consensus algorithms is surprisingly difficult. Enabled by a decision procedure that is derived from a well-established previous consensus solvability characterization for a given set $$\textbf{D}$$ D , we study, for the first time, the time complexity of solving consensus in this model: We provide both upper and lower bounds for this time complexity, and also relate it to the number of iterations required by the decision procedure. Among other results, we find that reaching consensus under an oblivious message adversary can take exponentially longer than both deciding consensus solvability and broadcasting the input value of some unknown process to all other processes.

We provide a complete characterization of both uniform and non-uniform deterministic consensus solvability in distributed systems with benign process and communication faults using point-set topology. More specifically, we non-trivially extend the approach introduced by Alpern and Schneider in 1985, by introducing novel fault-aware topologies on the space of infinite executions: the process-view topology, induced by a distance function that relies on the local view of a given process in an execution, and the minimum topology, which is induced by a distance function that focuses on the local view of the process that is the last to distinguish two executions. Consensus is solvable in a given model if and only if the sets of admissible executions leading to different decision values is disconnected in these topologies. By applying our approach to a wide range of different applications, we provide a topological explanation of a number of existing algorithms and impossibility results and develop several new ones, including a general equivalence of the strong and weak validity conditions.

Dynamic digital timing analysis is a promising alternative to analog simulations for verifying particularly timing-critical parts of a circuit. A necessary prerequisite is a digital delay model, which allows to accurately predict the input-to-output delay of a given transition in the input signal(s) of a gate. Since all existing digital delay models for dynamic digital timing analysis are deterministic, however, they cannot cover delay fluctuations caused by PVT variations, aging and analog signal noise. The only exception known to us is the η-IDM introduced by Függer et al. at DATE’18, which allows to add (very) small adversarially chosen delay variations to the deterministic involution delay model, without endangering its faithfulness. In this paper, we show that it is possible to extend the range of allowed delay variations so significantly that realistic PVT variations and aging are covered by the resulting extended η-IDM.

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.

To facilitate the analysis of timing relations between individual transitions in a signal trace, dynamic digital timing analysis offers a less accurate but much faster alternative to analog simulations of digital circuits. It primarily requires gate delay models, which account for the fact that the input-to-output delay of a particular input transition also depends on the temporal distance to the previous output transitions. In the case of multi-input gates, this delay also experiences variations caused by multi-input switching (MIS) effects, i.e., transitions at different inputs that occur in close temporal proximity. In this paper, we advocate the development of hybrid delay models for CMOS gates obtained by replacing transistors with time-variant resistors. We exemplify our approach by applying it to a NOR gate (and, hence, to the dual NAND gate) and a Muller C gate. We analytically solve the resulting first-order differential equations with non-constant coefficients and derive analytic expressions for the resulting MIS gate delays. The resulting formulas not only pave the way to a sound model parametrization procedure but are also instrumental in implementing a fast and efficient digital timing simulation. By comparison with analog simulation data, we show that our models faithfully represent all relevant MIS effects. Using an implementation in the Involution Tool, we also demonstrate that our models surpass all alternative digital delay models known to us in terms of accuracy, with comparably short running times.

We study the problem of solving consensus in synchronous directed dynamic networks, in which communication is controlled by an oblivious message adversary that picks the communication graph to be used in a round from a fixed set of graphs 𝐃 arbitrarily. In this fundamental model, determining consensus solvability and designing efficient consensus algorithms is surprisingly difficult. Enabled by a decision procedure that is derived from a well-established previous consensus solvability characterization for a given set 𝐃, we study, for the first time, the time complexity of solving consensus in this model: We provide both upper and lower bounds for this time complexity, and also relate it to the number of iterations required by the decision procedure. Among other results, we find that reaching consensus under an oblivious message adversary can take exponentially longer than both deciding consensus solvability and broadcasting the input value of some unknown process to all other processes.

Faithfully representing small delay variations caused by transitions on different inputs in close temporal proximity is a challenging task for digital circuit delay models. In this paper, we show that a simple hybrid model, derived from considering transistors as ideal switches in a simple RC model, leads to a surprisingly accurate model. By analytically solving the resulting ODEs for a NOR gate, explicit expressions for the delay are derived. In addition, we experimentally compare our model's predictions to SPICE simulations and to existing delay models.

The celebrated 1999 Asynchronous Computability Theorem (ACT) of Herlihy and Shavit characterized distributed tasks that are wait-free solvable and uncovered deep connections with combinatorial topology. We provide an alternative characterization of those tasks by means of the novel concept of continuous tasks, which have an input/output specification that is a continuous function between the geometric realizations of the input and output complex: We state and prove a precise characterization theorem (CACT) for wait-free solvable tasks in terms of continuous tasks. Its proof utilizes a novel chromatic version of a foundational result in algebraic topology, the simplicial approximation theorem, which is also proved in this paper. Apart from the alternative proof of the ACT implied by our CACT, we also demonstrate that continuous tasks have an expressive power that goes beyond classic task specifications, and hence open up a promising venue for future research: For the well-known approximate agreement task, we show that one can easily encode the desired proportion of the occurrence of specific outputs, namely, exact agreement, in the continuous task specification.

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 study optimal election sequences for repeatedly selecting a (very) small group of leaders among a set of participants (players) with publicly known unique ids. In every time slot, every player has to select exactly one player that it considers to be the current leader, oblivious to the selection of the other players, but with the overarching goal of maximizing a given parameterized global (“social”) payoff function in the limit. We consider a quite generic model, where the local payoff achieved by a given player depends, weighted by some arbitrary but fixed real parameter, on the number of different leaders chosen in a round, the number of players that choose the given player as the leader, and whether the chosen leader has changed w.r.t. the previous round or not. The social payoff can be the maximum, average or minimum local payoff of the players. Possible applications include quite diverse examples such as rotating coordinator-based distributed algorithms and long-haul formation flying of social birds. Depending on the weights and the particular social payoff, optimal sequences can be very different, from simple round-robin where all players chose the same leader alternatingly every time slot to very exotic patterns, where a small group of leaders (at most 2) is elected in every time slot. Moreover, we study the question if and when a single player would not benefit w.r.t. its local payoff when deviating from the given optimal sequence, i.e., when our optimal sequences are Nash equilibria in the restricted strategy space of oblivious strategies. As this is the case for many parameterizations of our model, our results reveal that no punishment is needed to make it rational for the players to optimize the social payoff.

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.

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.

We consider a real-time setting where an environment releases sequences of firm-deadline tasks, and an online scheduler chooses on-the-fly the ones to execute on a single processor so as to maximize cumulated utility. The competitive ratio is a well-known performance measure for the scheduler: it gives the worst-case ratio, among all possible choices for the environment, of the cumulated utility of the online scheduler versus an offline scheduler that knows these choices in advance. Traditionally, competitive analysis is performed by hand, while automated techniques are rare and only handle static environments with independent tasks. We present a quantitative-verification framework for precedence-aware competitive analysis, where task releases may depend on preceding scheduling choices, i.e., the environment can respond to scheduling decisions dynamically. We consider two general classes of precedences: 1) follower precedences force the release of a dependent task upon the completion of a set of precursor tasks, while and 2) pairing precedences modify the characteristics of a dependent task provided the completion of a set of precursor tasks. Precedences make competitive analysis challenging, as the online and offline schedulers operate on diverging sequences. We make a formal presentation of our framework, and use a GPU-based implementation to analyze ten well-known schedulers on precedence-based application examples taken from the existing literature: 1) a handshake protocol (HP); 2) network packet-switching; 3) query scheduling (QS); and 4) a sporadic-interrupt setting. Our experimental results show that precedences and task parameters can vary drastically the best scheduler. Our framework thus supports application designers in choosing the best scheduler among a given set automatically.

Distributed computations in a synchronous system prone to message loss can be modeled as a game between a (deterministic) distributed algorithm versus an omniscient message adversary. The latter determines, for each round, the directed communication graph that specifies which messages can reach their destination. Message adversary definitions range from oblivious ones, which pick the communication graphs arbitrarily from a given set of candidate graphs, to general message adversaries, which are specified by the set of sequences of communication graphs (called admissible communication patterns) that they may generate. This paper provides a complete characterization of consensus solvability for closed message adversaries, where every inadmissible communication pattern has a finite prefix that makes all (infinite) extensions of this prefix inadmissible. Whereas every oblivious message adversary is closed, there are also closed message adversaries that are not oblivious. We provide a tight non-topological, purely combinatorial characterization theorem, which reduces consensus solvability to a simple condition on prefixes of the communication patterns. Our result not only non-trivially generalizes the known combinatorial characterization of the consensus solvability for oblivious message adversaries by Coulouma, Godard, and Peters (Theor. Comput. Sci., 2015), but also provides the first combinatorial characterization for this important class of message adversaries that is formulated directly on the prefixes of the communication patterns.

The winner of the 2019 Principles of Distributed Computing Doctoral Dissertation Award is Dr. Sepehr Assadi for his dissertation Combinatorial Optimization on Massive Datasets: Streaming, Distributed, and Massively Parallel Computation, written under the supervision of Prof. Sanjeev Khanna at the University of Pennsylvania.

In this paper, we provide a rigorous characterization of consensus solvability in synchronous directed dynamic networks controlled by an arbitrary message adversary using point-set topology: We extend the approach introduced by Alpern and Schneider in 1985 by introducing two novel topologies on the space of infinite executions: the process-view topology, induced by a distance function that relies on the local view of a given process in an execution, and the minimum topology, which is induced by a distance function that focuses on the local view of the process that is the last to distinguish two executions. We establish some simple but powerful topological results, which not only lead to a topological explanation of bivalence arguments, but also provide necessary and sufficient topological conditions on the admissible graph sequences of a message adversary for solving consensus. In particular, we characterize consensus solvability in terms of connectivity of the set of admissible graph sequences. For non-compact message adversaries, which are not limit-closed in the sense that there is a convergent sequence of graph sequences whose limit is not permitted, this requires the exclusion of all "fair'' and "unfair'' limit sequences that coincide with the forever bivalent runs constructed in bivalence proofs. For both compact and non-compact message adversaries, we also provide tailored characterizations of consensus solvability, i.e., tight conditions for impossibility and existence of algorithms, based on the broadcastability of the connected components of the set of admissible graph sequences.

We study the following data dissemination problem: In a set of n nodes, every node has a unique piece of information. The communication of the nodes is organized in discrete synchronous lock-step rounds. In each round every node sends all currently known pieces of information to all other nodes. Which nodes receive this message is determined by the actual communication graph, which may change from round to round. Recently, Charron-Bost, Függer, and Nowak proved an upper bound of O(nlogn) rounds for the case where every communication graph is an arbitrary rooted tree. We present a new formalism, which facilitates a concise proof of this result. Moreover, we establish linear-time data dissemination bounds for certain subclasses of rooted trees. In particular, we prove that only (n−1) rounds are needed if the underlying graph is a directed path. An analogous result for undirected paths is also established. Furthermore, for trees with a fixed root we relate the dissemination time to the sizes of the subtrees of the root.

We consider the problem of solving consensus using deterministic algorithms in a synchronous dynamic network with unreliable, directional point-to-point links, which are under the control of a message adversary. In contrast to the large body of existing work that focuses on message adversaries that pick the communication graphs from a predefined set of candidate graphs arbitrarily, we consider message adversaries that also allow to express eventual properties, like stable periods that occur only eventually. Such message adversaries can model systems that exhibit erratic boot-up phases or recover after repeatedly occurring, massive transient faults. We precisely determine how much eventual stability is necessary and sufficient, and provide an optimal consensus algorithm. Unlike in the case of longer stability periods, where standard algorithms can be adapted for solving consensus, different algorithmic techniques are needed in the case of short-lived stability.

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 describe a simple self-stabilizing point-to-point communication protocol for multi-synchronous GALS (globally asynchronous locally synchronous) systems. Its implementation is based on a ring buffer, which compensates for the clock deviations of sender and receiver. Read and write pointers separated by a suitable offset facilitate metastability-free operation without the need for synchronizers. We conduct a detailed analysis of the required buffer size and offset, which allows to tailor the protocol to given clock parameters like frequency bounds and synchronization precision. Simulation results obtained by means of a VHDL implementation of our approach prove its practical feasibility.

The Dijkstra Prize Committee has decided to grant the 2018 Edsger W. Dijkstra Prize in Distributed Computing to Bowen Alpern and Fred B. Schneider for their paper:

This paper is devoted to automatic competitive analysis of real-time scheduling algorithms for firm-deadline tasksets, where only completed tasks contribute some utility to the system. Given such a taskset $${\mathcal {T}}$$ , the competitive ratio of an on-line scheduling algorithm $${\mathcal {A}}$$ for $${\mathcal {T}}$$ is the worst-case utility ratio of $${\mathcal {A}}$$ over the utility achieved by a clairvoyant algorithm. We leverage the theory of quantitative graph games to address the competitive analysis and competitive synthesis problems. For the competitive analysis case, given any taskset $${\mathcal {T}}$$ and any finite-memory on-line scheduling algorithm $${\mathcal {A}}$$ , we show that the competitive ratio of $${\mathcal {A}}$$ in $${\mathcal {T}}$$ can be computed in polynomial time in the size of the state space of $${\mathcal {A}}$$ . Our approach is flexible as it also provides ways to model meaningful constraints on the released task sequences that determine the competitive ratio. We provide an experimental study of many well-known on-line scheduling algorithms, which demonstrates the feasibility of our competitive analysis approach that effectively replaces human ingenuity (required for finding worst-case scenarios) by computing power. For the competitive synthesis case, we are just given a taskset $${\mathcal {T}}$$ , and the goal is to automatically synthesize an optimal on-line scheduling algorithm $${\mathcal {A}}$$ , i.e., one that guarantees the largest competitive ratio possible for $${\mathcal {T}}$$ . We show how the competitive synthesis problem can be reduced to a two-player graph game with partial information, and establish that the computational complexity of solving this game is Np-complete. The competitive synthesis problem is hence in Np in the size of the state space of the non-deterministic labeled transition system encoding the taskset. Overall, the proposed framework assists in the selection of suitable scheduling algorithms for a given taskset, which is in fact the most common situation in real-time systems design.

We study distributed agreement in synchronous directed dynamic networks, where an omniscient message adversary controls the presence/absence of communication links. We prove that consensus is impossible under a message adversary that guarantees weak connectivity only, and introduce eventually vertex-stable source components (VSSCs) as a means for circumventing this impossibility: A VSSC ( k , d ) message adversary guarantees that, eventually, there is an interval of d consecutive rounds where every communication graph contains at most k strongly connected components consisting of the same processes (with possibly varying interconnect topology), which have no incoming links from outside processes. We present a consensus algorithm that works correctly under a VSSC ( 1 , 4 E + 2 ) message adversary, where E is the dynamic network depth. Our algorithm maintains local estimates of the communication graphs, and applies techniques for detecting network stability and univalent system configurations. Several related impossibility results and lower bounds, in particular, that neither a VSSC ( 1 , E − 1 ) message adversary nor a VSSC ( 2 , ∞ ) one allow to solve consensus, reveal that there is not much hope to deal with (much) stronger message adversaries here. However, we show that gracefully degrading consensus, which degrades to general k -set agreement in case of unfavorable network conditions, allows to cope with stronger message adversaries: We provide a k -universal k -set agreement algorithm, where the number of system-wide decision values k is not encoded in the algorithm, but rather determined by the actual power of the message adversary in a run: Our algorithm guarantees at most k decision values under a VSSC ( n , d ) + MAJINF ( k ) message adversary, which combines VSSC ( n , d ) (with some small value of d , ensuring termination) with some information flow guarantee MAJINF ( k ) between certain VSSCs (ensuring k -agreement). Since related impossibility results reveal that a VSSC ( k , d ) message adversary is too strong for solving k -set agreement and that some information flow between VSSCs is mandatory for this purpose as well, our results provide a significant step towards the exact solvability/impossibility border of general k -set agreement in directed dynamic networks. Finally, we relate (the eventually-forever-variants of) our message adversaries to failure detectors. It turns out that even though VSSC ( 1 , ∞ ) allows to solve consensus and to implement the Ω failure detector, it does not allow to implement Σ. This contrasts the fact that, in asynchronous message-passing systems with a majority of process crashes, ( Σ , Ω ) is a weakest failure detector for solving consensus. Similarly, although the message adversary VSSC ( n , d ) + MAJINF ( k ) allows to solve k -set agreement, it does not allow to implement the failure detector Σ k , which is known to be necessary for k -set agreement in asynchronous message-passing systems with a majority of process crashes. Consequently, it is not possible to adapt failure-detector-based algorithms to work in conjunction with our message adversaries.

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

We present a k-set agreement algorithm for synchronous dynamic distributed systems with unidirectional links controlled by an omniscient adversary. Our algorithm automatically adapts to the actual network properties: If the network is sufficiently well-connected, it solves consensus, while degrading gracefully to general k-set agreement in less well-behaved runs. The algorithm is oblivious to the maximum number of system-wide decision values k, which is bounded by the number of certain strongly connected components occurring in the dynamically changing network in a run. Related impossibility results reveal that this bound is close to the solvability border for k-set agreement. To the best of our knowledge, this is the first consensus algorithm that degrades in a graceful way in a dynamic network.

We present a flexible framework for the automated competitive analysis of on-line scheduling algorithms for firm-deadline real-time tasks based on multi-objective graphs: Given a task set and an on-line scheduling algorithm specified as a labeled transition system, along with some optional safety, liveness, and/or limit-average constraints for the adversary, we automatically compute the competitive ratio of the algorithm w.r.t. A clairvoyant scheduler. We demonstrate the flexibility and power of our approach by comparing the competitive ratio of several on-line algorithms, including Dover, that have been proposed in the past, for various task sets. Our experimental results reveal that none of these algorithms is universally optimal, in the sense that there are task sets where other schedulers provide better performance. Our framework is hence a very useful design tool for selecting optimal algorithms for a given application.

We present generic transformations, which allow to translate classic fault-tolerant distributed algorithms and their correctness proofs into a real-time distributed computing model (and vice versa). Owing to the non-zero-time, non-preemptible state transitions employed in our real-time model, scheduling and queuing effects (which are inherently abstracted away in classic zero step-time models, sometimes leading to overly optimistic time complexity results) can be accurately modeled. Our results thus make fault-tolerant distributed algorithms amenable to a sound real-time analysis, without sacrificing the wealth of algorithms and correctness proofs established in classic distributed computing research. By means of an example, we demonstrate that real-time algorithms generated by transforming classic algorithms can be competitive even w.r.t. optimal real-time algorithms, despite their comparatively simple real-time analysis.

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.

This paper presents two weak partially synchronous system models Manti(n-k)and Msink(n-k), which are just strong enough for solving k-set agreement: We introduce the generalized (n-k)-loneliness failure detector L(k), which we first prove to be sufficient for solving k-set agreement, and show that L(k) but not L(k-1) can be implemented in both models. Manti(n-k)and Msink(n-k)are hence the first message passing models that lie between models where Ω (and therefore consensus) can be implemented and the purely asynchronous model. We also address k-set agreement in anonymous systems, that is, in systems where (unique) process identifiers are not available. Since our novel k -set agreement algorithm using L(k) also works in anonymous systems, it turns out that the loneliness failure detector L=L(n-1) introduced by Delporte et al. is also the weakest failure detector for set agreement in anonymous systems. Finally, we analyze the relationship between L(k) and other failure detectors suitable for solving k-set agreement.

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.

In this paper, we introduce the powerful framework of graph games for the analysis of real-time scheduling with firm deadlines. We introduce a novel instance of a partial-observation game that is suitable for this purpose, and prove decidability of all the involved decision problems. We derive a graph game that allows the automated computation of the competitive ratio (along with an optimal witness algorithm for the competitive ratio) and establish an NP-completeness proof for the graph game problem. For a given on-line algorithm, we present polynomial time solution for computing (i) the worst-case utility; (ii) the worst-case utility ratio w.r.t. a clairvoyant off-line algorithm; and (iii) the competitive ratio. A major strength of the proposed approach lies in its flexibility w.r.t. incorporating additional constraints on the adversary and/or the algorithm, including limited maximum or average load, finiteness of periods of overload, etc., which are easily added by means of additional instances of standard objective functions for graph games.

We introduce an automated method for parameterized verification of fault-tolerant distribed algorithms. It rests on a novel parametric interval abstraction (PIA) technique, which works for systems with multiple parameters, for instance, where n and t are parameters describing the system size and the bound on the number of faulty processes, respectively. The PIA technique allows to map typical threshold-range intervals like [1,t+1) and [t+1,n-t) to values from a finite abstract domain. Applying PIA to both the local states of the processes and the global system state, the parameterized verification problem can be reduced to finite-state model checking. We demonstrate the practical feasibility of our method by verifying several variants of the well-known consistent broadcasting algorithm by Srikanth and Toueg for different fault models. To the best of our knowledge, this is the first successful automated parameterized verification of a Byzantine fault-tolerant distributed algorithm for message-passing systems.

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.

This paper presents the architecture and a detailed design analysis of a digital measurement chip which facilitates long-term irradiation experiments of basic asynchronous circuits. It combines radiation targets like Muller C-elements and elastic pipelines as well as standard combinational gates and flip-fops with an elaborate on-chip measurement infrastructure. Major architectural challenges result from the fact that the latter must operate reliably under the same radiation conditions the target circuits are exposed to, without wasting precious die area for a rad-hard design. A measurement architecture based on multiple non-rad-hard counters is used, which we show to be resilient against double faults, as well as many triple and even higher-multiplicity faults. The analysis is done by means of comprehensive fault injection experiments, which are based on detailed Spice models of the circuits in conjunction with a standard double-exponential current injection model for single-event transients. We also provide probabilistic calculations of the sustainable particle flow rates, based on the results of a detailed area analysis in conjunction with experimentally determined cross section data for the ASIC implementation technology used. The results confirm that the overall architecture indeed supports significant target hit rates, without exceeding the resilience bound of the measurement infrastructure.

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.

No abstract available.

WE INTRODUCE A COMPREHENSIVE HYBRID FAILURE MODEL FOR SYNCHRONOUS DISTRIBUTED SYSTEMS, WHICH EXTENDS A CONVENTIONAL HYBRID PROCESS FAILURE MODEL BY ADDING COMMUNICATION FAILURES: Every process in the system is allowed to commit up to fℓs send link failures and experience up to fℓr receive link failures per round here, without being considered faulty; up to some fℓsa≤fℓs and fℓra≤fℓr among those may even cause erroneous messages rather than just omissions. In a companion paper (Schmid et al. (2009) [14]), devoted to a complete suite of related impossibility results and lower bounds, we proved that this model surpasses all existing link failure modeling approaches in terms of the assumption coverage in a simple probabilistic setting.In this paper, we show that several well-known synchronous consensus algorithms can be adapted to work under our failure model, provided that the number of processes required for tolerating process failures is increased by small integer multiples of fℓs, fℓr, fℓsa, fℓra. This is somewhat surprising, given that consensus in the presence of unrestricted link failures and mobile (moving) process omission failures is impossible. We provide detailed formulas for the required number of processes and rounds, which reveal that the lower bounds established in our companion paper are tight. We also explore the power and limitations of authentication in our setting, and consider uniform consensus algorithms, which guarantee their properties also for benign faulty processes.

This paper shows how synchrony conditions can be added to the purely asynchronous model in a way that avoids any reference to message delays and computing step times, as well as system-wide constraints on execution patterns and network topology. Our Asynchronous Bounded-Cycle (ABC) model just bounds the ratio of the number of forward- and backward-oriented messages in certain ("relevant") cycles in the space-time diagram of an asynchronous execution. We show that clock synchronization and lock-step rounds can be implemented and proved correct in the ABC model, even in the presence of Byzantine failures. Furthermore, we prove that any algorithm working correctly in the partially synchronous Θ-Model also works correctly in the ABC model. In our proof, we first apply a novel method for assigning certain message delays to asynchronous executions, which is based on a variant of Farkas' theorem of linear inequalities and a non-standard cycle space of graphs. Using methods from point-set topology, we then prove that the existence of this delay assignment implies model indistinguishability for time-free safety and liveness properties. We also introduce several weaker variants of the ABC model, and relate our model to the existing partially synchronous system models, in particular, the classic models of Dwork, Lynch and Stockmayer and the query-response model by Mostefaoui, Mourgaya, and Raynal. Finally, we discuss some aspects of the ABC model's applicability in real systems, in particular, in the context of VLSI Systems-on-Chip.

No abstract available.

We provide a suite of impossibility results and lower bounds for the required number of processes and rounds for synchronous consensus under transient link failures. Our results show that consensus can be solved even in the presence of $O(n^2)$ moving omission and/or arbitrary link failures per round, provided that both the number of affected outgoing and incoming links of every process is bounded. Providing a step further toward the weakest conditions under which consensus is solvable, our findings are applicable to a variety of dynamic phenomena such as transient communication failures and end-to-end delay variations. We also prove that our model surpasses alternative link failure modeling approaches in terms of assumption coverage.

Aguilera et al. and Malkhi et al. presented two system models, which are weaker than all previously proposed models where the eventual leader election oracle Ω can be implemented, and thus, consensus can also be solved. The former model assumes unicast steps and at least one correct process with f outgoing eventually timely links, whereas the latter assumes broadcast steps and at least one correct process with f bidirectional but moving eventually timely links. Consequently, those models are incomparable. In this paper, we show that Ω can also be implemented in a system with at least one process with f outgoing moving eventually timely links, assuming either unicast or broadcast steps. It seems to be the weakest system model that allows to solve consensus via Ω-based algorithms known so far. We also provide matching lower bounds for the communication complexity of Ω in this model, which are based on an interesting “stabilization property” of infinite runs. Those results reveal a fairly high price to be paid for this further relaxation of synchrony properties.

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.

In this paper, we introduce the Asynchronous Bounded-Cycle (ABC) model, which considerably relaxes the Theta-Model proposed by Le Lann and Schmid. The ABC model just bounds the ratio of the number of forward and backward messages in certain cycles in the space-time diagram of an asynchronous execution. It hence avoids any reference to end-to-end delays, allows individual messages to have arbitrary delays, and does not involve global synchrony conditions. We show that clock synchronization and lock-step rounds can easily be implemented and proved correct in the ABC model, even in the presence of Byzantine failures. Moreover, we show that any correct Theta-algorithm also works correctly in the ABC model. Our proof is based on a novel technique for assigning message delays to asynchronous executions, which is of independent interest.

It has long been known that the consensus problem cannot be solved deterministically in completely asynchronous distributed systems, i.e., systems (1) without assumptions on communication delays and relative speed of processes and (2) without access to real-time clocks. In this paper, we define a new asynchronous system model. Instead of assuming reliable channels with finite transmission delays, stubborn channels with a finite average response time was assumed (if neither the sender nor the receiver crashes), and it is assumed that there exists some unknown physical bound on how fast an integer can be incremented. Note that there is no limit on how slow a program can be executed or how fast other statements can be executed. Also, there exists no upper or lower bound on the transmission delay of messages or the relative speed of processes. The are no additional assumptions about clocks, failure detectors, etc. that would aid in solving consensus either. It is shown that consensus can nevertheless be solved deterministically in this asynchronous system model

No abstract available.

We introduce a novel hybrid failure model, which facilitates an accurate and detailed analysis of round-based synchronous, partially synchronous and asynchronous distributed algorithms under both process and link failures. Granting every process in the system up to f/sub /spl lscr// send and receive link failures (with f/sub /spl lscr///sup a/ arbitrary faulty ones among those) in every round, without being considered faulty, we show that the well-known randomized Byzantine agreement algorithm of (Srikanth & Toueg 1987) needs just n /spl ges/ 4f/sub /spl lscr// + 2ff/sub /spl lscr///sup a/+ 3f/sub a/ + 1 processes for coping with f/sub a/ Byzantine faulty processes. The probability of disagreement after R iterations is only 2/sup -R/, which is the same as in the FLP model and thus much smaller than the lower bound 0(1/R) known for synchronous systems with lossy links. Moreover, we show that 2-stubborn links are sufficient for this algorithm. Hence, contrasting widespread belief, a perfect communications subsystem is not required for efficiently solving randomized Byzantine agreement.

This paper shows that deterministic consensus in synchronous distributed systems with link faults is possible, despite the impossibility result of Gray (1978). Instead of using randomization, we overcome this impossibility by moderately restricting the inconsistency that link faults may cause system-wide. Relying upon a novel hybrid fault model that provides different classes of faults for both nodes and links, we provide a formally verified proof that the m+1-round Byzantine agreement algorithm OMH (Lincoln and Rushby (1993)) requires n > 2f/sub l//sup s/ + f/sub l//sup r/ + f/sub l//sup ra/ + 2(f/sub a/ + f/sub s/) + f/sub o/ + f/sub m/ + m nodes for transparently masking at most f/sub l//sup s/ broadcast and f/sub l//sup r/ receive link faults (including at most f/sub l//sup ra/ arbitrary ones) per node in each round, in addition to at most f/sub a/, f/sub s/, f/sub o/, f/sub m/ arbitrary, symmetric, omission, and manifest node faults, provided that m /spl ges/ f/sub a/ + f/sub o/ + 1. Our approach to modeling link faults is justified by a number of theoretical results, which include tight lower bounds for the required number of nodes and an analysis of the assumption coverage in systems where links fail independently with some probability p.

We propose a new hybrid fault model for clock synchronization and single-round (approximate) agreement in synchronous distributed systems, which accurately captures both node and link faults. Unlike conventional "global" fault models, which rest upon the total number of faulty nodes in the system, it solely relies upon the number of faults in any two non-faulty nodes' "perceptions"-conveyed by the messages from all other nodes-of the system. This way, arbitrary node and communication faults, including receiver-caused omission and time/value faults, can be modeled properly. As an example, we show that the consistent broadcast primitive (and hence the clock synchronization algorithms) of Srikanth & Toueg (1987) can be analyzed under this model. As far as link faults are concerned, our analysis reveals that as few as 4f/sub /spl Cscr/a/+2f/sub /spl Cscr/s/+2f/sub /spl Cscr/o/+1 nodes are sufficient for tolerating at most f/sub /spl Cscr/a/, f/sub /spl Cscr/s/, and f/sub /spl Cscr/o/ asymmetric, symmetric, and omission link faults at any receiving node.

This paper shows that deterministic consensus with written messages is possible in presence of link faults and compromised signatures. Relying upon a suitable perception-based hybrid fault model that provides different categories for both node and link faults, we prove that the authenticated Byzantine agreement algorithms OMHA and ZA of Gong, Lincoln and Rushby (1995) can be made resilient to f/sub l/ link faults per node by adding 3f/sub l/ and 2f/sub l/ nodes, respectively. Both algorithms can also cope with compromised signatures if the affected nodes are considered as arbitrary faulty. Authenticated algorithms for consensus are therefore reasonably applicable even in wireless systems, where link faults and intrusions are the dominating source of errors.

We introduce our SimUTC toolkit, a fault-tolerant distributed systems simulation built upon the discrete event simulation package C++SIM. SimUTC has been developed in the course of our project SynUTC and targets distributed algorithms for high-accuracy fault-tolerant clock synchronization. This application domain requires detailed simulation models for network transmission and local clock devices, fault-injection capabilities, flexible system configuration facilities, and customized data capture and analysis tools. We explain how SimUTC addresses those issues and provide a few samples of simulation results gathered from the evaluation of the well-known fault-tolerant average clock synchronization algorithm.

Real-time and embedded computing systems pervade all areas of our lives. The characteristics of the eld and its development so far are summarised. As demands for the functionality and dependability of complex real-time systems continue to grow, many challenging problems encountered in their design and development need to be solved. Some of them are addressed in this panel, viz., synchronisation in distributed transaction processing, integration of heterogeneous systems with di erent real-time properties, and application of dynamical principles to provide fault-tolerance in real-

It has been well-known for nearly 20 years that the bistable behavior of infinite population slotted ALOHA networks causes the unpleasant effect of eventually reaching an overloaded state, where the number of backlogged stations becomes larger and larger and the useful throughput reduces to zero. The detailed analysis reveals that this statement is true for any average offered load lambda >0, regardless of the retransmission probability p. A challenging, and to the best of the authors' knowledge, not sufficiently solved problem within this context concerns the time until this destabilization occurs. This question is successfully answered based on the fact that the operation of the system may be viewed as a sequence of consecutive busy periods, each starting from backlog 0 and return to backlog 0. It turns out that the whole period of successful operation S consists of a finite sequence of busy periods of finite lengths, which is "terminated" by an infinite busy period (which never returns to backlog 0). Further analysis of this simple renewal process leads to an infinite dimensional system of linear equations, which is shown to have only one meaningful solution. A pair of upper and lower asymptotic bounds for that solution eventually provide the key to the major result, an asymptotic formula for the average number of slots up to the beginning of the infinite busy period, uniformly for p to 0 and lambda to 0.>