to the underlying network. In the presence of insertions and deletions to base tuples, our original incremental view maintenance implementation utilizes the count algorithm13 that ensures only tuples that are no longer derivable are deleted. This has subsequently been improved18 via the use of a compact form of data provenance encoded using binary decision diagrams shipped with each derived tuple.

In general, updates could occur very frequently, at a period that is shorter than the expected time for a typical query to reach a fixpoint. In that case, query results can never fully reflect the state of the network. We focus our analysis instead on a bursty model. In this weaker, but still fairly realistic model, updates are allowed to happen during query processing. However, we make the assumption that after a burst of updates, the network eventually quiesces (does not change) for a time long enough to allow all the queries in the system to reach a fixpoint. Unlike the continuous model, the bursty model is amenable to simpler analysis; our results on that model provide some intuition as to the behavior in the continuous update model as well.

We have proven20 that in the presence of reliable, in-order delivery of messages, link-restricted NDlog rules under the bursty model achieve a variant of the typical distributed systems notion of eventual consistency, where the eventual state of the quiescent system corresponds to what would be achieved by rerunning the queries from scratch in that state.

4. use cases

In the past 3 years, since the introduction of declarative networking and the release of P2, several applications have been developed. We describe two of the original use cases that motivated our work and drove several of our language and system designs: safe extensible routers and overlay network development. We will briefly mention new applications in Section 5.

4. 1. Declarative routing

The Internet’s core routing infrastructure, while arguably robust and efficient, has proven to be difficult to evolve to accommodate the needs of new applications. Prior research on this problem has included new hard-coded routing protocols on the one hand, and fully extensible Active Networks31 on the other. Declarative routing21 explores a new point in this design space that aims to strike a better balance between the extensibility and robustness of a routing infrastructure.

With declarative routing, a routing protocol is implemented by writing a simple query in NDlog, which is then executed in a distributed fashion at the nodes that receive the query. Declarative routing can be viewed as a restrictive instantiation of Active Networks for the control plane, which aims to balance the concerns of expressiveness, performance and security, properties which are needed for an extensible routing infrastructure to succeed.

Security is a key concern with any extensible system particularly when it relates to nontermination and the consumption of resources. NDlog is amenable to static analysis due to its connections to Datalog. In terms of query execution, pure Datalog (without any negation, aggregation, or

function symbols) has polynomial time and space com-plexities in the size of the input. This property provides a natural bound on the resource consumption. However, many extensions of Datalog (including NDlog) augment the core language in various ways, invalidating its polynomial complexity.

Fortunately, static analysis tests have been developed to check for the termination of an augmented Datalog query on a given input. 15 In a nutshell, these tests identify recursive definitions in the query rules, and check whether these definitions terminate. Examples of recursive definitions that terminate are ones that evaluate monotonically increasing (decreasing) predicates whose values are upper (lower) bounded. Moreover, the declarative framework is amenable to other verification techniques, including theorem proving, 32 model checking, 25 and runtime verification. 28

NDlog can express a variety of well-known routing protocols (e.g., distance vector, path vector, dynamic source routing, link state, multicast) in a compact and clean fashion, typically in a handful of lines of program code. Moreover, higher-level routing concepts (e.g., QoS constraints) can be achieved via simple modifications to these queries. Finally, writing the queries in NDlog illustrates surprising relationships between protocols. For example, we have shown that distance vector and dynamic source routing protocols differ only in a simple, traditional query optimization decision: the order in which a query’s predicates are evaluated.

To limit query computation to the relevant portion of the network, we use a query rewrite technique, called magic sets rewriting. 4 Rather than reviewing the Magic Sets optimization here, we illustrate its use in an example. Consider the situation where instead of computing all-pairs shortest paths, we are only in computing the shortest paths from a selected group of source nodes (magicSrc) to selected destination nodes (magicDst). By modifying rules sp1–sp4 from the path-vector program, the following computes only paths limited to sources/destinations in the magicSrc/ magicDst tables, respectively.

sp1-sd pathDst(@Dest,Src,Path,Cost) :- magicSrc(@Src),
link(@Src,Dest,Cost), Path=f_init(Src,Dst).
sp2-sd pathDst(@Dst,Src,Path,Cost) :-
pathDst(@Nxt,Src,Path1,Cost1), link(@Nxt,Dest,Cost2),
Cost=Cost1+Cost2, Path=f_concatPath(Path1,Dest).
sp3-sd spCost(@Dest,Src,min<Cost>) :- magicDst(@Dest),
pathDst(@Dest,Src,Path,Cost).
sp4-sd shortestPath(@Dest,Src,Path,Cost) :-
spCost(@Dest,Src,Cost), pathDst(@Dest,Src,Path,Cost).

Query shortestPath(@Src,Dest,Path,Cost).

Our evaluation results21 based on running declarative routing protocols on the PlanetLab26 global testbed and in a local cluster show that when all nodes issue the same query, the query execution has similar scalability properties as the traditional distance vector and path-vector protocols. For example, the convergence latency for the path-vector program is proportional to the network diameter, and converges in the same time as the path-vector protocol. Second,