In this paper we present new general convergence results about the behaviour of the Distributed Bellman-Ford (DBF) family of routing protocols, which includes distance-vector protocols (e.g. RIP) and path-vector protocols (e.g. BGP). Our results apply to “policy-rich” protocols, by which we mean protocols that can have complex policies (e.g. conditional route transformations) that violate traditional assumptions made in the standard presentation of Bellman-Ford protocols. First, we propose a new algebraic model for abstract routing problems which has fewer primitives than previous models and can represent more expressive policy languages. The new model is also the first to allow concurrent reasoning about distance-vector and path-vector protocols. Second, we explicitly demonstrate how DBF routing protocols are instances of a larger class of asynchronous iterative algorithms, for which there already exist powerful results about convergence. These results allow us to build upon conditions previously shown by Sobrinho to be sufficient and necessary for the convergence of path-vector protocols and generalise and strengthen them in various ways: we show that, with a minor modification, they also apply to distance-vector protocols; we prove they guarantee that the final routing solution reached is unique, thereby eliminating the possibility of anomalies such as BGP wedgies; we relax the model of asynchronous communication, showing that the results still hold if routing messages can be lost, reordered, and duplicated. Thirdly, our model and our accompanying theoretical results have been fully formalised in the Agda theorem prover. The resulting library is a powerful tool for quickly prototyping and formally verifying new policy languages. As an example, we formally verify the correctness of a policy language with many of the features of BGP including communities, conditional policy, path-inflation and route filtering.

Abstract Üresin and Dubois’ paper “Parallel Asynchronous Algorithms for Discrete Data” shows how a class of synchronous iterative algorithms may be transformed into asynchronous iterative algorithms. They then prove that the correctness of the resulting asynchronous algorithm can be guaranteed by reasoning about the synchronous algorithm alone. These results have been used to prove the correctness of various distributed algorithms, including in the fields of routing, numerical analysis and peer-to-peer protocols. In this paper we demonstrate several ways in which the assumptions that underlie this theory may be relaxed. Amongst others, we (i) expand the set of schedules for which the asynchronous iterative algorithm is known to converge and (ii) weaken the conditions that users must prove to hold to guarantee convergence. Furthermore, we demonstrate that two of the auxiliary results in the original paper are incorrect, and explicitly construct a counter-example. Finally, we also relax the alternative convergence conditions proposed by Gurney based on ultrametrics. Many of these relaxations and errors were uncovered after formalising the work in the proof assistant Agda. This paper describes the Agda code and the library that has resulted from this work. It is hoped that the library will be of use to others wishing to formally verify the correctness of asynchronous iterative algorithms.

A good measure of the rate of convergence of path-vector protocols is the number of synchronous iterations required for convergence in the worst case. From an algebraic perspective, the rate of convergence depends on the expressive power of the routing algebra associated with the protocol. For example in a network of n nodes, shortest-path protocols are guaranteed to converge in O(n) iterations. In contrast the algebra underlying the Border Gateway Protocol (BGP) is in some sense too expressive and the protocol is not guaranteed to converge. There is significant interest in finding well-behaved algebras that still have enough expressive power to satisfy network operators. Recent theoretical results have shown that by constraining routing algebras to those that are "strictly increasing" we can guarantee the convergence of path-vector protocols. Currently the best theoretical worst-case upper bound for the convergence of such algebras is O(n!) iterations. However in practice it is difficult to find examples that do not converge in n iterations. In this paper we close this gap. We first present a family of network configurations that converges in Θ(n2) iterations, demonstrating that the worst case is Ω(n2) iterations. We then prove that path-vector protocols with a strictly increasing algebra are guaranteed to converge in O(n2) iterations. Together these results establish a tight Θ(n2) bound. This is another piece of the puzzle in showing that "strictly increasing" is, at least on a technical level, a reasonable constraint for practical policy-rich protocols.

In this paper we describe an Agda-based formalization of results from Üresin & Dubois’ “Parallel Asynchronous Algorithms for Discrete Data.” That paper investigates a large class of iterative algorithms that can be transformed into asynchronous processes. In their model each node asynchronously performs partial computations and communicates results to other nodes using unreliable channels. Üresin & Dubois provide sufficient conditions on iterative algorithms that guarantee convergence to unique fixed points for the associated asynchronous iterations. Proving such sufficient conditions for an iterative algorithm is often dramatically simpler than reasoning directly about an asynchronous implementation. These results are used extensively in the literature of distributed computation, making formal verification worthwhile. Our Agda library provides users with a collection of sufficient conditions, some of which mildly relax assumptions made in the original paper. Our primary application has been in reasoning about the correctness of network routing protocols. To do so we have derived a new sufficient condition based on the ultrametric theory of Alexander Gurney. This was needed to model the complex policy-rich routing protocol that maintains global connectivity in the internet. Additionally we highlight and discuss two propositions from Üresin & Dubois, which during the course of the formalisation, turned out to be false.

We present new results in the theory of asynchronous convergence for the Distributed Bellman-Ford (DBF) family of routing protocols which includes distance-vector protocols (e.g. RIP) and path-vector protocols (e.g. BGP). We take the strictly increasing conditions of Sobrinho and make three main new contributions.

Most Internet routing protocols have one of two algorithms lurking at their core - either Dijkstra's algorithm in the case of link-state protocols or a distributed Bellman-Ford algorithm in the case of distance-vector or path-vector protocols. When computing simple shortest paths these protocols can be modified to utilize all best paths with a combination of next-hop sets and Equal Cost Multi-Path (ECMP) forwarding. We show that this picture breaks down even for simple modifications to the shortest path metric. This is illustrated with widest-shortest paths where among all shortest paths only those with greatest bandwidth are considered best. In this case Bellman-Ford and Dijkstra may compute different sets of paths and neither can compute all best paths. In addition, some paths computed by Dijkstra's algorithm cannot be implemented with next-hop forwarding. We provide a general algebraic model that helps to clarify such anomalies. This is accomplished by computing paths within the route metric rather than with specialized algorithmic extensions. Our results depend on the distinction between global and local optima that has hitherto been applied almost exclusively to more exotic routing protocols such as BGP.

Internet Service Providers (ISPs) need to balance multiple opposing objectives. On one hand, they strive to offer innovative services to obtain competitive advantages; on the other, they have to interconnect with potentially competing ISPs to achieve reachability, and coordinate with them for certain services. The complexity of balancing these objectives is reflected in the diversity of policies of the Border Gateway Protocol (BGP), the standard inter-domain routing protocol. Unforeseen interactions among the BGP policies of different ISPs can cause routing anomalies. In this work, we propose a methodology to allow ISPs to check their BGP policy configurations for guaranteed convergence to a single stable state. This requires that a set of ISPs share their configurations with each other, or with a trusted third party. Compared to previous approaches to BGP safety, we (1) allow ISPs to use a richer set of policies, (2) do not modify the BGP protocol itself, and (3) detect not only instability, but also multiple stable states. Our methodology is based on the extension of current theoretical frameworks to relax their constraints and use incomplete data. We believe that this provides a rigorous foundation for the design and implementation of safety checking tools.

Internet Service Providers (ISPs) use routing policies to implement the requirements of business contracts, manage traffic, address security concerns and increase scalability of their network. These routing policies are often a high-level expression of strategies or intentions of the ISP. They have meaning when viewed from a network-wide perspective (e.g., mark on ingress, filter on egress). However, configuring these policies for the Border Gateway Protocol (BGP) is undertaken at a low-level, on a per router basis. Unintended routing outcomes have been observed. In this work, we define a language that allows analysis of network-wide configurations at the high-level. This language aims at bridging the gap between router configurations and abstract mathematical models capable of capturing complex policies. The language can be used to verify desired properties of routing protocols and hence detect potential unintended states of BGP. The language is accompanied by a tool suite that parses router configuration languages (which by their nature are vendor-dependent) and translates them into vendor-independent representations of policies.

Routing stability and correctness in the Internet have long been a concern. Despite this, few theoretical frameworks have been proposed to check BGP configurations for convergence and safety. The most popular approach is based on the Stable Paths Problem (SPP) model. Unfortunately, SPP requires enumeration of all possible control-plane paths, which is infeasible in large networks. In this work, we study how to apply algebraic frameworks to the BGP configuration checking problem. We propose an extension of the Stratified Shortest Path Problem (SSPP) model that has a similar expressive power to SPP, but enables more efficient checking of configuration correctness. Our approach remains valid when BGP policies are applied to iBGP sessions - a case which is often overlooked by previous work, although common in today's Internet. While this paper focuses mainly on iBGP problems, our methodology can be extended to eBGP if operators are willing to share their local-preference configurations.

Internet routers can obtain distinct routes to the same destination from multiple routing protocols. A mechanism called administrative distance (AD) has evolved to implement route selection in such cases. AD simply imposes a preference ranking among routing protocols. A related mechanism called route redistribution (RR) is used to increase connectivity by injecting routes from one protocol into another. Recent research has shown that the current design of RR with AD mechanisms can give rise to routing and forwarding anomalies that are difficult to debug. We present a new algebraic model that captures not only RR with AD, but also sub-protocol interactions that exist within protocols such as OSPF and IS-IS. Compared with previous work, our model provides a clearer view of the issues and trade-offs involved.

There are several situations in which it would be advantageous to allow route preferences to be dependent on which neighbor is to receive the route. This idea could be realised in many possible ways and could interact differently with other elements of route choice, such as filtering: not all of these will have the property that a unique routing solution can always be found. We develop an algebraic model of route selection to aid in the analysis of neighbor-specific preferences in multipath routing. Using this model, we are able to identify a set of such routing schemes in which convergence is guaranteed.

Implementing BGP route processing in an event-driven manner appears to be advantageous in terms of scalability. However, the inter-domain routing system as a whole would be overwhelmed without some type of rate limiting on BGP update streams. At first glace, an event-driven, pipelined route processing model does not seem to fit well with the traditional timer-based way of implementing BGP rate-limiting. In this paper we present a lazy event-driven BGP route processing pipeline that easily accommodates rate limiting.

Routing protocols often keep track of multiple route metrics, where some metrics are more important than others. Route selection is then based on lexicographic comparison: the most important attribute of each route is considered first, and if this does not give enough information to decide which route is better, the next attribute is considered; and so on. We investigate protocols that find globally optimal paths and protocols that find only locally optimal paths. In each case we characterize exactly when lexicographic products can be used to define well-behaved routing protocols. We apply our results to protocols that can partition a network into distinct administrative regions, such as OSPF areas and BGP autonomous systems. We show that in some cases this type of local autonomy is fully compatible with global optimality.

Internet round-trip-times (RTTs) exhibit widespread and persistent Triangle Inequality Violations (TIVs). It has been shown that TIVs are a natural consequence of the Internet's routing structure and they degrade the embedding accuracy of any Internet coordinate systems based on RTTs. In this paper, we simulate a coordinate system in a hypothetical overlay environment where RTTs are measured with respect to overlay forwarding that has eliminated all the TIVs. The resulting coordinate system is much more accurate and the embedding accuracy is predictable and stable (under simulated node churn) than the existing techniques based on RTTs along paths chosen by native IP forwarding. We believe that this work helps to illustrate the detrimental effects of TIVs on Internet coordinate systems, and it suggests that high quality coordinate systems in the global Internet may be possible only with overlay forwarding.

We use the term policy-based routing to refer collec- tively to the Stable Paths Problem, Sobrinho's Routing Algebras, and to classical Path Algebras (semi-rings used to generalise minimum-weight routing). These theories all contain sufficient conditions that ensure the existence of solutions (stable routings) for labelled graphs. We attempt to provide a unified theory from which all of these seemingly disparate sufficient conditions can be derived. Our theory is based purely on abstract relations and their properties and not on the syntactic or axiomatic details of the policy-based theories.

The separation of intradomain and interdomain routing has been a key feature of the Internet's routing architecture from the early days of the ARPAnet. However, the appropriate "division of labor" between the two protocols becomes unclear when an Autonomous System (AS) has interdomain routes to a destination prefix through multiple border routers---a situation that is extremely common today because neighboring domains often connect in several locations. We believe that the current mechanism of early-exit or hot-potato routing---where each router in an AS directs traffic to the "closest" border router based on the intradomain path costs---is convoluted, restrictive, and sometimes quite disruptive. In this paper, we propose a flexible mechanism for routers to select the egress point for each destination prefix, allowing network administrators to satisfy diverse goals, such as traffic engineering and robustness to equipment failures. We present one example optimization problem that uses integer-programming techniques to tune our mechanism to improve network robustness. Experiments with topology and routing data from two backbone networks demonstrate that our solution is both simple (for the routers) and expressive (for the network administrators).

There is a shortage of routing protocols that meet the needs of network engineers. This has led to BGP being pressed into service as an IGP, despite its lack of convergence guarantees. The development, standardization, and deployment of routing protocols, or even minor changes to existing protocols, are very difficult tasks. We present an approach called Metarouting that defines routing protocols using a high-level and declarative language. Once an interpreter for a metarouting language is implemented on a router, a network operator would have the freedom to implement and use any routing protocol definable in the language. We enforce a clean separation of protocol mechanisms (link-state, path-vector, adjacency maintenance, and so on) from routing policy (how routes are described and compared). The Routing Algebra framework of Sobrinho [25] is used as the theoretical basis for routing policy languages. We define the Routing Algebra Meta-Language (RAML) that allows for the construction of a large family of routing algebras and has the key property that correctness conditions --- guarantees of convergence with respect to the chosen mechanisms --- can be derived automatically for each expression defining a new routing algebra.

Hot-potato routing is a mechanism employed when there are multiple (equally good) interdomain routes available for a given destination. In this scenario, the Border Gateway Protocol (BGP) selects the interdomain route associated with the closest egress point based upon intradomain path costs. Consequently, intradomain routing changes can impact interdomain routing and cause abrupt swings of external routes, which we call hot-potato disruptions. Recent work has shown that hot-potato disruptions can have a substantial impact on large ISP backbones and thereby jeopardize the network robustness. As a result, there is a need for guidelines and tools to assist in the design of networks that minimize hot-potato disruptions. However, developing these tools is challenging due to the complex and subtle nature of the interactions between exterior and interior routing. In this paper, we address these challenges using an analytic model of hot-potato routing that incorporates metrics to evaluate network sensitivity to hot-potato disruptions. We then present a methodology for computing these metrics using measurements of real ISP networks. We demonstrate the utility of our model by analyzing the sensitivity of a large AS in a tier~1 ISP network.

IP forwarding anomalies, triggered by equipment failures, implementation bugs, or configuration errors, can significantly disrupt and degrade network service. Robust and reliable detection of such anomalies is essential to rapid problem diagnosis, problem mitigation, and repair. We propose a simple, robust method that integrates routing and traffic data streams to reliably detect forwarding anomalies. The overall method is scalable, automated and self-training. We find this technique effectively identifies forwarding anomalies, while avoiding the high false alarms rate that would otherwise result if either stream were used unilaterally.

Despite the architectural separation between intradomain and interdomain routing in the Internet, intradomain protocols do influence the path-selection process in the Border Gateway Protocol (BGP). When choosing between multiple equally-good BGP routes, a router selects the one with the closest egress point, based on the intradomain path cost. Under such hot-potato routing, an intradomain event can trigger BGP routing changes. To characterize the influence of hot-potato routing, we conduct controlled experiments with a commercial router. Then, we propose a technique for associating BGP routing changes with events visible in the intradomain protocol, and apply our algorithm to AT&T's backbone network. We show that (i) hot-potato routing can be a significant source of BGP updates, (ii) BGP updates can lag 60 seconds or more behind the intradomain event, (iii) the number of BGP path changes triggered by hot-potato routing has a nearly uniform distribution across destination prefixes, and (iv) the fraction of BGP messages triggered by intradomain changes varies significantly across time and router locations. We show that hot-potato routing changes lead to longer delays in forwarding-plane convergence, shifts in the flow of traffic to neighboring domains, extra externally-visible BGP update messages, and inaccuracies in Internet performance measurements.

The desire to better understand global BGP dynamics has motivated several studies using active measurement techniques, which inject announcements and withdrawals of prefixes from the global routing domain. From these one can measure quantities such as the BGP convergence time. Previously, the route injection infrastructure of such experiments has either been temporary in nature, or its use has been restricted to the experimenters. The routing research community would benefit from a permanent and public infrastructure for such active probes. We use the term BGP Beacon to refer to a publicly documented prefix having global visibility and a published schedule for announcements and withdrawals. A BGP Beacon is to be used for the ongoing study of BGP dynamics, and so should be supportedwith a long-term commitment. We describe several BGP Beacons thathave been set up at various points in the Internet. We then describe techniques for processing BGP updates when a BGP Beacon is observed from a BGP monitoring point such as Oregon's Route Views. Finally, we illustrate the use of BGP Beacons in the analysis of convergence delays, route flap damping, and update inter-arrival times.

The term virtual private network (VPN) encompasses a wide array of diverse technologies and network architectures. All VPNs should provide users with the isolation and security associated with private networks, but at lower costs made possible by implementing these networks over some type of shared infrastructure. Provider provisioned VPN allow enterprises to outsource their private backbone networks to service providers. For this reason, we will also refer to them as virtual private routed networks (VPRNs). This contrasts with other VPN technologies that require customers to manage their own point-to-point connections (leased lines or tunnels) and associated network administration. One type of VPRN currently being deployed is described in RFC 2547, which uses BGP to propagate routing information for all VPNs implemented within a provider's backbone, and a tunneling technology, such as MPLS, to isolate traffic. This technology requires fairly complex configurations within the backbone, and so poses challenges to providers supporting a large number of VPN customers. We present a formal analysis of several configuration and implementation concerns for VPRNs of the RFC 2547 variety. In particular, we focus on integrity constraints that must be maintained by providers in order to ensure that intraVPRN connectivity is achieved, and that disjoint VPRNs are isolated from each other.

BGP is unique among IP-routing protocols in that routing is determined using semantically rich routing policies. However this expressiveness has come with hidden risks. The interaction of locally defined routing policies can lead to unexpected global routing anomalies, which can be very difficult to identify and correct in the decentralized and competitive Internet environment. These risks increase as the complexity of local policies increase. which is precisely the current trend. BGP policy languages have evolved in a rather organic fashion with little effort to avoid policy-interaction problems. We believe that researchers should start to consider how to design policy languages for path-vector protocols in order to avoid routing anomalies while obtaining desirable protocol properties. We take a few steps in this direction by identifying the important dimensions of this design space and characterizing some of the inherent design trade-offs. We do this in a general way that is not constrained by the details of BGP.

The multi exit discriminator (MED) attribute of the border gateway protocol (BGP) is widely used to implement "cold potato routing" between autonomous systems. However, the use of MED in practice has led to BGP persistent oscillation. The MED oscillation problem has been described with example configurations and complicated, step-by-step evaluation of dynamic route computations performed at multiple routers. Our work presents the first rigorous analysis of the MED oscillation problem. We employ the stable paths problem (SPP) formalism that allows a static analysis of the interaction of routing policies. We give a formal definition of MED induced routing anomalies (MIRA) and show that, in general, they can span multiple autonomous systems. However, if we assume that the BGP configurations between autonomous systems follows a common model based on customer/provider and peer/peer relationships, then we show that the scope of any MIRA is always contained within a single autonomous system. Contrary to widely held assumptions, we show that a MIRA can occur even in a fully meshed IBGP configuration. We also show that a stable BGP routing may actually violate the stated semantics of the MED attribute.

The Border Gateway Protocol (BGP) has two distinct modes of operation. External BGP (EBGP) exchanges reachability information between autonomous systems, while Internal BGP (IBGP) exchanges external reachability information within an autonomous system. We study several routing anomalies that are unique to IBGP because, unlike EBGP, forwarding paths and signaling paths are not always symmetric. In particular, we focus on anomalies that can cause the protocol to diverge, and those that can cause a router's chosen forwarding path to an egress point to be deflected by another router on that path. Deflections can greatly complicate the debugging of routing problems, and in the worst case multiple deflections can combine to form persistent forwarding loops. We define a correct IBGP configuration to be one that is anomaly free for every possible set of routes sent by neighboring autonomous systems. We show that determination of IBGP configuration correctness is NP-hard. However, we give simple sufficient conditions on network configurations that guarantee correctness.

Dynamic routing protocols such as RIP and OSPF essentially implement distributed algorithms for solving the shortest paths problem. The border gateway protocol (BGP) is currently the only interdomain routing protocol deployed in the Internet. BGP does not solve a shortest paths problem since any interdomain protocol is required to allow policy-based metrics to override distance-based metrics and enable autonomous systems to independently define their routing policies with little or no global coordination. It is then natural to ask if BGP can be viewed as a distributed algorithm for solving some fundamental problem. We introduce the stable paths problem and show that BGP can be viewed as a distributed algorithm for solving this problem. Unlike a shortest path tree, such a solution does not represent a global optimum, but rather an equilibrium point in which each node is assigned its local optimum. We study the stable paths problem using a derived structure called a dispute wheel, representing conflicting routing policies at various nodes. We show that if no dispute wheel can be constructed, then there exists a unique solution for the stable paths problem. We define the simple path vector protocol (SPVP), a distributed algorithm for solving the stable paths problem. SPVP is intended to capture the dynamic behavior of BGP at an abstract level. If SPVP converges, then the resulting state corresponds to a stable paths solution. If there is no solution, then SPVP always diverges. In fact, SPVP can even diverge when a solution exists. We show that SPVP will converge to the unique solution of an instance of the stable paths problem if no dispute wheel exists.

The border gateway protocol (BGP) is the routing protocol used to maintain connectivity between autonomous systems in the Internet. Empirical measurements have shown that there can be considerable delay in BGP convergence after routing changes. One contributing factor in this delay is a BGP-specific timer used to limit the rate at which routing messages are transmitted. We use the SSFNet simulator to explore the relationship between convergence time and the configuration of this timer. For each simple network topology simulated, we observe that there is an optimal value for the rate-limiting timer that minimizes convergence time.

The Internet consists of a large number of autonomous systems (ASes) that exchange routing information using the border gateway protocol (BGP). Each AS applies local policies for selecting routes and propagating routes to others, with important implications for the reliability and stability of the global system. In and of itself, BGP does not ensure that every pair of hosts can communicate. In addition, routing policies are not guaranteed be safe, and may cause protocol divergence. Backup routing is often used to increase the reliability of the network under link and router failures, at the possible expense of safety. This paper presents a general model for backup routing that increases network reliability while allowing each AS to apply local routing policies that are consistent with the commercial relationships it has with its neighbors. In addition, our model is inherently safe in the sense that the global system remains safe under any combination of link and router failures. Our model and the proof of inherent safety are cast in terms of the stable paths problem, a static formalism that captures the semantics of interdomain routing policies. Then, we describe how to realize our model in BGP with locally-implementable routing policies. To simplify the specification of local policies, we propose a new BGP attribute that conveys the avoidance level of a route. We also describe how to realize these policies without modification to BGP by using the BGP community attribute.

An IP routing protocol is safe if it is guaranteed to converge in the absence of network topology changes. BGP, currently the only interdomain routing protocol employed on the Internet, is not safe in this sense. It may seem that the source of BGP's potential divergence is inherent in the requirements for any interdomain routing protocol-policy-based metrics must be allowed to override distance-based metrics, and each autonomous system must be allowed to independently define its routing policies with little or no global coordination. In this paper we present a simple path vector protocol (SPVP) that captures the underlying semantics of BGP by abstracting away all nonessential details. We then add a dynamically computed attribute to SPVP routing messages, called the route history. Protocol oscillations caused by policy conflicts produce routes whose histories contain cycles. These cycles identify the policy conflicts and the autonomous systems involved. SPVP is made safe by automatically suppressing routes whose histories contain cycles. We discuss how this safe SPVP can be used in the design of a safe BGP.

The border gateway protocol, BGP, is currently the only interdomain routing protocol employed on the Internet. As required of any interdomain protocol, BGP allows policy-based metrics to override distance-based metrics and enables each autonomous system to independently define its routing policies with little or no global coordination. Varadhan et al. (1996) have shown that there are collections of routing policies that together are not safe in the sense that they can cause BGP to diverge. That is, an unsafe collection of routing policies can result in some autonomous systems exchanging BGP routing messages indefinitely, without ever converging to a set of stable routes. In this paper we present sufficient conditions on routing policies that guarantee BGP safety. We use a new formalism, called the simple path vector protocol (SPVP), that is designed to capture the underlying semantics of any path vector protocol such as BGP. We identify a certain circular set of relationships between routing policies at various autonomous systems that we call a dispute cycle. We show that systems with no dispute cycles are guaranteed to be safe. While these include systems whose policies are consistent with shortest paths under some link metric, the class of systems with no dispute cycles is strictly larger.

The Border Gateway Protocol (BGP) is the de facto inter-domain routing protocol used to exchange reachability information between Autonomous Systems in the global Internet. BGP is a path-vector protocol that allows each Autonomous System to override distance-based metrics with policy-based metrics when choosing best routes. Varadhan et al. [18] have shown that it is possible for a group of Autonomous Systems to independently define BGP policies that together lead to BGP protocol oscillations that never converge on a stable routing. One approach to addressing this problem is based on static analysis of routing policies to determine if they are safe. We explore the worst-case complexity for convergence-oriented static analysis of BGP routing policies. We present an abstract model of BGP and use it to define several global sanity conditions on routing policies that are related to BGP convergence/divergence. For each condition we show that the complexity of statically checking it is either NP-complete or NP-hard.

Previous approaches to supporting hypothetical queries have been “eager”: some representation of the hypothetical state (or the corresponding delta) is materialized, and query evaluation is filtered through that representation. This paper develops a framework for evaluating hypothetical queries using a “lazy” approach, or using a hybrid of eager and lazy approaches.

Qian and Wiederhold (1991) presented an algorithm for the incremental recomputation of relational algebra expressions that was claimed to preserve a certain minimality condition. This condition guarantees that the incremental change sets do not contain any unnecessary tuples; so, redundant computations are not performed. We show that, in fact, their algorithm violates this condition. We present an improved algorithm that does preserve this notion of minimality.

Article Free Access Share on Verifiable properties of database transactions Authors: Michael Benedikt Bell Laboratories, 600 Mountain Avenue, Murray Hill NJ Bell Laboratories, 600 Mountain Avenue, Murray Hill NJView Profile , Timothy Griffin Bell Laboratories, 600 Mountain Avenue, Murray Hill NJ Bell Laboratories, 600 Mountain Avenue, Murray Hill NJView Profile , Leonid Libkin Bell Laboratories, 600 Mountain Avenue, Murray Hill NJ Bell Laboratories, 600 Mountain Avenue, Murray Hill NJView Profile Authors Info & Claims PODS '96: Proceedings of the fifteenth ACM SIGACT-SIGMOD-SIGART symposium on Principles of database systemsJune 1996 Pages 117–127https://doi.org/10.1145/237661.237692Published:03 June 1996Publication History 18citation320DownloadsMetricsTotal Citations18Total Downloads320Last 12 Months16Last 6 weeks1 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF

Materialized views and view maintenance are important for data warehouses, retailing, banking, and billing applications. We consider two related view maintenance problems: 1) how to maintain views after the base tables have already been modified, and 2) how to minimize the time for which the view is inaccessible during maintenance.Typically, a view is maintained immediately, as a part of the transaction that updates the base tables. Immediate maintenance imposes a significant overhead on update transactions that cannot be tolerated in many applications. In contrast, deferred maintenance allows a view to become inconsistent with its definition. A refresh operation is used to reestablish consistency. We present new algorithms to incrementally refresh a view during deferred maintenance. Our algorithms avoid a state bug that has artificially limited techniques previously used for deferred maintenance.Incremental deferred view maintenance requires auxiliary tables that contain information recorded since the last view refresh. We present three scenarios for the use of auxiliary tables and show how these impact per-transaction overhead and view refresh time. Each scenario is described by an invariant that is required to hold in all database states. We then show that, with the proper choice of auxiliary tables, it is possible to lower both per-transaction overhead and view refresh time.

We study the problem of efficient maintenance of materialized views that may contain duplicates. This problem is particularly important when queries against such views involve aggregate functions, which need duplicates to produce correct results. Unlike most work on the view maintenance problem that is based on an algorithmic approach, our approach is algebraic and based on equational reasoning. This approach has a number of advantages: it is robust and easily extendible to new language constructs, it produces output that can be used by query optimizers, and it simplifies correctness proofs.We use a natural extension of the relational algebra operations to bags (multisets) as our basic language. We present an algorithm that propagates changes from base relations to materialized views. This algorithm is based on reasoning about equivalence of bag-valued expressions. We prove that it is correct and preserves a certain notion of minimality that ensures that no unnecessary tuples are computed. Although it is generally only a heuristic that computing changes to the view rather than recomputing the view from scratch is more efficient, we prove results saying that under normal circumstances one should expect, the change propagation algorithm to be significantly faster and more space efficient than complete recomputing of the view. We also show that our approach interacts nicely with aggregate functions, allowing their correct evaluation on views that change.

The programming language Scheme contains the control construct call/cc that allows access to the current continuation (the current control context). This, in effect, provides Scheme with first-class labels and jumps. We show that the well-known formulae-as-types correspondence, which relates a constructive proof of a formula α to a program of type α, can be extended to a typed Idealized Scheme. What is surprising about this correspondence is that it relates classical proofs to typed programs. The existence of computationally interesting “classical programs” —programs of type α, where α holds classically, but not constructively — is illustrated by the definition of conjunctively, disjunctive, and existential types using standard classical definitions. We also prove that all evaluations of typed terms in Idealized Scheme are finite.

In the course of developing a mathematical theory or proof it is a common practice to introduce new notation to represent notation that is previously understood. The author presents a formal account that is intended to model the practice of introducing and using notational (abbreviate) definitions. The aim of this work is a pragmatic one: to provide a framework useful in the design and implementation of secure proof system interfaces which accommodate, as much as possible, conventional mathematical practice. A typed lambda -calculus is used to represent expressions of a given object language. A Delta -equation is introduced to model conventional definition equations.>