Datalog Materialisation in Distributed RDF Stores with Dynamic Data Exchange

TL;DR

This paper introduces a scalable distributed reasoning algorithm for RDF stores that can handle arbitrary datalog rules, extending existing dynamic data exchange methods, and demonstrates its effectiveness on large datasets.

Contribution

It extends the dynamic data exchange approach to support arbitrary datalog rules in distributed RDF reasoning, maintaining inference properties and scalability.

Findings

Algorithm scales well to large RDF datasets

Supports arbitrary datalog rules in distributed reasoning

Preserves properties like nonrepetition of inferences

Abstract

Several centralised RDF systems support datalog reasoning by precomputing and storing all logically implied triples using the wellknown seminaive algorithm. Large RDF datasets often exceed the capacity of centralised RDF systems, and a common solution is to distribute the datasets in a cluster of shared-nothing servers. While numerous distributed query answering techniques are known, distributed seminaive evaluation of arbitrary datalog rules is less understood. In fact, most distributed RDF stores either support no reasoning or can handle only limited datalog fragments. In this paper we extend the dynamic data exchange approach for distributed query answering by Potter et al. [12] to a reasoning algorithm that can handle arbitrary rules while preserving important properties such as nonrepetition of inferences. We also show empirically that our algorithm scales well to very large RDF datasets

Tables

Table 1. Table 1: Comparison of Centralised and Distributed Reasoning

	Threads/Servers
	1		2		4		8
	RDFox	DMAT	RDFox	DMAT	RDFox	DMAT	RDFox	DMAT
Times (s)	86	256	56	140	35	82	16	53
Speed-up	1.0x	1.0x	1.5x	1.8x	2.5x	3.1x	5.4x	4.8x
Size	$134M\to 182M$

Equations

$$⟨x,R,z⟩\leftarrow ⟨x,R,y⟩\wedge ⟨y,R,z⟩\wedge h(y)=i,$$

$$Q=a_1^{{\bowtie }_1}\wedge \cdots \wedge a_n^{{\bowtie }_n},$$

$$\begin{array}[]{@{}r@{\;}l@{}}Q&=\langle x,R,y\rangle^{<}\wedge\langle y,S,z\rangle^{\leq}\qquad I=\{\langle a,R,b\rangle,\langle b,S,c\rangle,\langle b,S,d\rangle,\langle b,S,e\rangle\}\\ T&=\{\langle a,R,b\rangle\mapsto 1,\;\langle b,S,c\rangle\mapsto 2,\;\langle b,S,d\rangle\mapsto 3\}\\ \end{array}$$

$$b_1^{<}\wedge \cdots \wedge b_{p-1}^{<}\wedge b_{p+1}^{\le }\wedge \cdots \wedge b_n^{\le }.$$

Full text

1 Introduction

Reasoning with datalog rules over RDF data plays a key role on the Semantic Web. Datalog can capture the structure of an application domain using if-then rules, and OWL 2 RL ontologies can be translated into datalog rules. Datalog reasoning is supported in several RDF management systems such as Oracle’s database [7], GraphDB,111http://graphdb.ontotext.com/ Amazon Neptune,222http://aws.amazon.com/neptune/ VLog [17], and RDFox.333http://www.cs.ox.ac.uk/isg/tools/RDFox/ All of these system use a materialisation approach to reasoning, where all facts implied by the dataset and the rules are precomputed and stored in a preprocessing step. This is usually done using the seminaïve algorithm [2], which ensures the nonrepetition property: no rule is applied to the same facts more than once.

Many RDF management systems are centralised in that they store and process all data on a single server. To scale to workloads that cannot fit into a single server, it is common to distribute the data in a cluster of interconnected, shared-nothing servers and use a distributed query answering strategy. Abdelaziz et al. [1] present a comprehensive survey of 22 approaches to distributed query answering, and Potter et al. [12] discuss several additional systems. There is considerable variation between these approaches: some use data replication, some compute joins on dedicated server, others use distributed join algorithms, and many leverage big data frameworks such as Hadoop and Spark for data storage and query processing. In contrast, distributed datalog materialisation is less well understood, and it is more technically challenging. Freshly derived facts must be stored so that they can be taken into account in future rule applications, but without repeating derivations. Moreover, synchronisation between rule applications should be reduced to allow parallel computation.

Several theoretical frameworks developed in the 90s aim to address these questions [4, 19, 13, 15, 21]. As we discuss in more detail in Section 3, they constrain the rules so that that each server performs only certain rule applications, and they send the derived facts to all servers where these facts could participate in further rule applications. Thus, same facts can be stored on more than one server, which severely limits the scalability of such systems.

The Semantic Web community has recently developed several RDF-specific approaches. a number of them are hardwired to fixed datalog rules, such as RDFS [18, 6] or so-called ter Horst fragment [16, 5]. Focusing on a fixed set of rules considerably simplifies the technical problems. PLogSPARK [20] and SPOWL [9] handle arbitrary rules, but they do not seem to use seminaïve evaluation. Finally, several probabilistic algorithms aim to handle large datasets [11, 9], but these approaches are approximate and are thus unsuitable for many applications. Distributed SociaLite [14] is the only system we are aware of that provides seminaïve evaluation for arbitrary datalog rules. It uses a custom graph model, but the approach can readily be adapted to RDF. Moreover, its rules must explicitly encode the communication and storage strategy, which increases complexity.

In this paper we present a new technique for distributed materialisation of arbitrary datalog rules. Unlike SociaLite, we do not require any distributed processing hints in the rules. We also do not duplicate any data and thus remove an obstacle to scalability. Our approach is based on the earlier work by Potter et al. [12] on distributed query answering using dynamic data exchange, from which it inherits several important properties. First, inferences that can be made within a single server do not require any communication; coupled with careful data partitioning, this can very effectively minimise network communication. Second, rule evaluation is completely asynchronous, which promotes parallelism. This, however, introduces a complication: to ensure nonrepetition of inferences, we must be able to partially order rule derivations across the cluster, which we achieve using Lamport timestamps [8]. We discuss the motivation and the novelty in more detail in Section 3, and in Section 4 we present the approach formally.

We have implemented our approach in a new prototype system called DMAT. In Section 5 we present the results of an empirical evaluation. We compared DMAT with WebPIE [16], investigated how it scales with increasing data loads, and compared it with RDFox to understand the impact of distribution on concurrency. Our results show that DMAT outperforms WebPIE by an order of magnitude (albeit with some differences in the setting), and that it can handle well increasing data loads; moreover, DMAT’s performance is comparable to that of RDFox on a single server. Our algorithms are thus a welcome addition to the techniques for implementing truly scalable semantic systems.

2 Preliminaries

We now recapitulate the syntax and the semantics of RDF and datalog. A constant (aka RDF term) is an IRI, a blank node, or a literal. Datalog constants can be arbitrary sets, but we are limiting them to RDF terms because this work in within the context of RDF stores. A term is a constant or a variable. An atom $a$ (aka triple pattern) has the form ${a=\langle t_{s},t_{p},t_{o}\rangle}$ over terms $t_{s}$ (subject), $t_{p}$ (predicate), and $t_{o}$ (object). A fact (aka triple) is an variable-free atom. A dataset (aka RDF Graph) is a finite set of facts.

We define the set of positions as ${\Pi=\{s,p,o\}}$. Then, for ${a=\langle t_{s},t_{p},t_{o}\rangle}$ and ${\pi\in\Pi}$, we define ${a|_{\pi}=t_{\pi}}$—that is, $a|_{\pi}$ is the term that occurs in $a$ at position $\pi$. A substitution $\sigma$ is a partial function that maps finitely many variables to constants. For $\alpha$ a term or an atom, $\alpha\sigma$ is the result of replacing with $\sigma(x)$ each occurrence of a variable $x$ in $\alpha$ on which $\sigma$ is defined.

A query $Q$ is a conjunction of atoms ${a_{1}\wedge\dots\wedge a_{n}}$. Substitution $\sigma$ is an answer to $Q$ on a dataset $I$ if ${a_{i}\sigma\in I}$ holds for each ${1\leq i\leq n}$.

A datalog rule $r$ is an implication of the form ${h\leftarrow b_{1}\wedge\dots\wedge b_{n}}$, where $h$ is the head atom, all $b_{i}$ are body atoms, and each variable occurring in $h$ also occurs in some $b_{i}$. A datalog program is a finite set of rules. Let $I$ be a dataset. The result of applying $r$ to $I$ is ${r(I)=I\cup\{h\sigma\mid\sigma\text{ is an answer to }b_{1}\wedge\dots\wedge b_{n}\text{ on }I\}}$. For $P$ a program, let ${P(I)=\bigcup_{r\in P}r(I)}$; let ${P^{0}(I)=I}$; and let ${P^{i+1}(I)=P(P^{i}(I))}$ for ${i\geq 0}$. Then, ${P^{\infty}(I)=\bigcup_{i\geq 0}P^{i}(I)}$ is the materialisation of $P$ on $I$. This paper deals with the problem of computing $P^{\infty}(I)$ where $I$ is distributed across of a cluster of servers such that each fact is stored in precisely one server.

3 Motivation and Related Work

We can compute $P^{\infty}(I)$ using the definition in Section 2: we evaluate the body of each rule ${r\in P}$ as a query over $I$ and instantiate the head of $r$ for each query answer, we eliminate duplicate facts, and we repeat the process until no new facts can be derived. However, since ${P^{i}(I)\subseteq P^{i+1}(I)}$ holds for each ${i\geq 0}$, such a naïve approach repeats in each round of rule applications the work from all previous rounds. The semïnaive strategy [2] avoids this problem: when matching a rule $r$ in round $i+1$, at least one body atom of $r$ must be matched to a fact derived in round $i$. We next discuss now these ideas are implemented in the existing approaches, and then we present an overview of our approach.

3.1 Related Approaches

Several approaches to distributed reasoning partition rule applications across servers. For example, to evaluate rule ${\langle x,R,z\rangle\leftarrow\langle x,R,y\rangle\wedge\langle y,R,z\rangle}$ on $\ell$ servers, one can let each server $i$ with ${1\leq i\leq\ell}$ evaluate rule

[TABLE]

where $h(y)$ is a partition function that maps values of $y$ to integers between $1$ and $\ell$. If $h$ is uniform, then each server receives roughly the same fraction of the workload, which benefits parallelisation. However, since a triple of the form $\langle s,R,o\rangle$ can match either atom in the body of (1), each such triple must be replicated to servers $h(s)$ and $h(o)$ so they can participate in rule applications. Based on this idea, Ganguly et al. [4] show how to handle general datalog; Zhang et al. [21] study different partition functions; Seib and Lausen [13] identify programs and partition functions where no replication of derived facts is needed; Shao et al. [15] further break rules in segments; and Wolfson and Ozeri [19] replicate all facts to all servers. The primary motivation behind these approaches seems to be parallelisation of computation, which explains why the high rates of data replication were not seen as a problem. However, high replication rates are not acceptable when data distribution is used to increase a system’s capacity.

Materialisation can also be implemented without any data replication. First, one must select a triple partitioning strategy: a common approach is to assign each $\langle s,p,o\rangle$ to server $h(s)$ for a suitable hash function $h$, and another popular option is to use a distributed file system (e.g., HDFS) and thus leverage its partitioning mechanism. Then, one can evaluate the rules using a suitable distributed query algorithm and distribute the newly derived triples using the partitioning strategy. These principles were used to realise RDFS reasoning [18, 6], and they are also implicitly present in approaches implemented on top of big data frameworks such as Hadoop [16] and Spark [5, 20, 9]. However, most of these can handle only fixed rule sets, which considerably simplifies algorithm design. For example, seminaïve evaluation is not needed in the RDFS fragment since the nonrepetition of inferences can be ensured by evaluating rules in a particular order [5]. PLogSPARK [20] and SPOWL [9] handle arbitrary rules using the naïve algorithm, which can be detrimental when programs are moderately complex.

Distributed SociaLite [14] is the only system known to us that implements distributed seminaïve evaluation for general datalog. It requires users to explicitly specify the data distribution strategy and communication patterns. For example, by writing a fact $R(a,b)$ as $R[a](b)$, one specifies that the fact is to be stored on server $h(a)$ for some function $h$. Rule (1) can then be written in SociaLite as ${R[x](z)\leftarrow R[x](y)\wedge R[y](z)}$, specifying that the rule should be evaluated by sending each fact $R[a](b)$ to server $h(b)$, joining such facts with $R[b](c)$, and sending the resulting facts $R[a](c)$ to server $h(a)$. While the evaluation of some rules is parallelised, servers must synchronise after each round of rule application.

3.2 Dynamic Data Exchange for Query Answering

Before describing our approach to distributed datalog materialisation, we next recapitulate the earlier work by Potter et al. [12] on distributed query answering using dynamic data exchange, which provides the foundation for this paper.

This approach to query answering assumes that all triples are partitioned into $\ell$ mutually disjoint datasets ${I_{1},\dots,I_{\ell}}$, with $\ell$ being the number of servers. The main objectives of dynamic exchange are to reduce communication and eliminate synchronisation between servers. To achieve the former goal, each server $k$ maintains three occurrence mappings $\mu_{k,s}$, $\mu_{k,p}$, and $\mu_{k,o}$. For each resource $r$ occurring in $I_{k}$, set $\mu_{k,s}(r)$ contains all servers where $r$ occurs in the subject position, and $\mu_{k,p}(r)$ and $\mu_{k,o}(r)$ provide analogous information for the predicate and object positions. To understand how occurrences are used, consider evaluating ${Q=\langle x,R,y\rangle\wedge\langle y,R,z\rangle}$ over datasets ${I_{1}=\{\langle a,R,b\rangle,\langle b,R,c\rangle\}}$ and ${I_{2}=\{\langle b,R,d\rangle,\langle d,R,e\rangle\}}$. Both servers evaluate $Q$ using index nested loop joins. Thus, server 1 evaluates $\langle x,R,y\rangle$ over $I_{1}$, which produces a partial answer ${\sigma_{1}=\{x\mapsto a,y\mapsto b\}}$. Server 1 then evaluates ${\langle y,R,z\rangle\sigma_{1}=\langle b,R,z\rangle}$ over $I_{1}$ and thus obtains one full answer ${\sigma_{2}=\{x\mapsto a,y\mapsto b,z\mapsto c\}}$. To see whether $\langle b,R,z\rangle$ can be matched on other servers, server 1 consults its occurrence mappings for all resources in the atom. Since ${\mu_{1,s}(b)=\mu_{1,p}(R)=\{1,2\}}$, server 1 sends the partial answer $\sigma_{1}$ to server 2, telling it to continue matching the query. After receiving $\sigma_{1}$, server 2 matches atom $\langle b,R,z\rangle$ in $I_{2}$ to obtain another full answer ${\sigma_{3}=\{x\mapsto a,y\mapsto b,z\mapsto d\}}$. However, server 2 also evaluates $\langle x,R,y\rangle$ over $I_{2}$, obtaining partial answer ${\sigma_{4}=\{x\mapsto b,y\mapsto d\}}$, and it consults its occurrences to determine which servers can match ${\langle y,R,z\rangle\sigma_{4}=\langle d,R,z\rangle}$. Since ${\mu_{2,s}(d)=\{2\}}$, server 2 knows it is the only one that can match this atom, so it proceeds without any communication and computes ${\sigma_{5}=\{x\mapsto b,y\mapsto d,z\mapsto e\}}$.

This strategy has several important benefits. First, all answers that can be produced within a single server, such as $\sigma_{5}$ in our example, are produced without any communication. Second, the location of every resource is explicitly recorded, rather than computed using a fixed rule (e.g., a hash function). We use this to partition a graph based on its structural properties and thus collocate highly interconnected resources. Combined with the first property, this can significantly reduce network communication. Third, the system is completely asynchronous: when server 1 sends $\sigma_{1}$ to server 2, it does not need to to wait for server 2 to finish; and server 2 can process $\sigma_{1}$ whenever it wishes. This eliminates the need for synchronisation between servers, which is beneficial for parallelisation.

3.3 Our Contribution

In this paper we extend the dynamic data exchange framework to datalog materialisation. We draw inspiration from the work by Motik et al. [10] on parallelising datalog materialisation in centralised, shared memory systems. Intuitively, their algorithm considers each triple in the dataset, identifies each rule and body atom that can be matched to the triple, and evaluates the rest of the rule as a query. This approach is amenable to parallelisation since distinct processors can simultaneously process distinct triples; since the number of triples is generally very large, the likelihood of workload skew between processors is very low.

Our distributed materialisation algorithm is based on the same general principle: each server matches the rules to locally stored triples, but the resulting queries are evaluated using dynamic data exchange. This approach requires no synchronisation between servers, and it reduces communication in the same way as described in Section 3.2. We thus expect our approach to exhibit the same good properties as the approach to query answering by Potter et al. [12].

The lack of synchronisation between servers introduces a technical complication. Remember that, to avoid repeating derivations, at least one body atom in a rule must be matched to a fact derived in the previous round of rule application. However, due to asynchronous rule application, there is no global notion of a rule application round (unlike, say, SociaLite). A naïve solution would be to associate each fact with a timestamp recording when the fact has derived, so the order of fact derivation could then be recovered by comparing timestamps. However, this would require maintaining a high coherence of server clocks in the cluster, which is unrealistic in practice. Instead, we use Lamport timestsamps [8], which provide a cheap way of determining a partial order of events across a cluster. We describe this technique in more detail in Section 4.

Another complication is due to the fact that the occurrence mappings stored in the servers may need to be updated due to the derivation of new triples. For completeness, it is critical that all servers are updated before such triples are used in rule applications. Our solution to this problem is fully asynchronous, which again benefits parallelisation.

Finally, since no central coordinator keeps track of the state of the computation of different servers, detecting when the system as a whole can terminate is not straightforward. We solve this problem using a well-known termination detection algorithm based on token passing [3].

4 Distributed Materialisation Algorithm

We now present our distributed materialisation algorithm and prove it to be correct. We present the algorithm in steps. In Section 4.1 we discuss data structures that the servers use to store their triples and implement Lamport timestamps. In Section 4.2 we discuss the occurrence mappings. In Section 4.3 we discuss the communication infrastructure and the message types used. In Section 4.4 we present the algorithm’s pseudocode. In Section 4.5 we discuss how to detect termination. Finally, in Section 4.6 we argue about the algorithm’s correctness.

4.1 Adding Lamport Timestamps to Triples

As already mentioned, to avoid repeating derivations, our algorithm uses Lamport timestamps [8], which is a technique for establishing a causal order of events in a distributed system. If all servers in the system could share a global clock, we could trivially associate each event with a global timestamp, which would allow us to recover the ‘happens-before’ relationship between events by comparing timestamps. However, maintaining a precise global clock in a distributed system is technically very challenging, and Lamport timestamps provide a much simpler solution. In particular, each event is annotated an integer timestamp in a way that guarantees the following property ($\ast$):

if there is any way for an event $A$ to possibly influence an event $B$, then the timestamp of $A$ is strictly smaller then the timestamp of $B$.

To achieve this, each server maintains a local integer clock that is incremented each time an event of interest occurs, which clearly ensures ($\ast$) if $A$ and $B$ occur within one server. Now assume that $A$ occurs in server $s_{1}$ and $B$ occurs in $s_{2}$; clearly, $A$ can influence $B$ only if $s_{1}$ sends a message to $s_{2}$, and $s_{2}$ processes this message before event $B$ takes place. To ensure that holds ($\ast$) in such a case, server $s_{1}$ includes its current clock value into the message it sends to $s_{2}$; moreover, when processing this message, server $s_{2}$ updates its local clock to the maximum of the message clock and the local clock, and then increments the local clock. Thus, when $B$ happens after receiving the message, it is guaranteed to have a timestamp that is larger than the timestamp of $A$.

To map this idea to datalog materialisation, a derivation of a fact corresponds to the notion of an event, and using a fact to derive another fact corresponds to the ‘influences’ notion. Thus, we associates facts with integer timestamps.

More precisely, each server $k$ in the cluster maintains an integer $C_{k}$ called the local clock, a set $I_{k}$ of the derived triples, and a partial function ${T_{k}:I_{k}\rightarrow\mathbb{N}}$ that associates triples with natural numbers. Function $T_{k}$ is partial because timestamps are not assigned to facts upon derivation, but during timestamp synchronisation. Before the algorithm is started, $C_{k}$ must be initialised to zero, and all input facts (i.e., the facts given by the user) partitioned to server $k$ should be loaded into $I_{k}$ and assigned a timestamp of zero.

To capture formally how timestamps are used during query evaluation, we introduce the notion of an annotated query as a conjunction of the form

[TABLE]

where each $a_{i}$ is an atom and each $\bowtie_{i}$ is symbol $<$ or symbol $\leq$; each $a_{i}^{\bowtie_{i}}$ is called an annotated atom. An annotated query requires a timestamp to be evaluated. More precisely, a substitution $\sigma$ is an answer to $Q$ on $I_{k}$ and $T_{k}$ w.r.t. a timestamp $\tau$ if (i) $\sigma$ is an answer to the ‘ordinary’ query ${a_{1}\wedge\dots\wedge a_{n}}$ on $I_{k}$, and (ii) for each ${1\leq i\leq n}$, the value of $T_{k}$ is defined for $a_{i}\sigma$ and it satisfies ${T_{k}(a_{i}\sigma)\bowtie\tau}$. For example, let $Q$, $I$, and $T$ be as follows, and let ${\tau=2}$:

[TABLE]

Then, ${\sigma_{1}=\{x\mapsto a,y\mapsto b,z\mapsto c\}}$ is an answer to $Q$ on $I$ and $T$ w.r.t. $\tau$, whereas ${\sigma_{2}=\{x\mapsto a,y\mapsto b,z\mapsto d\}}$ and ${\sigma_{3}=\{x\mapsto a,y\mapsto b,z\mapsto e\}}$ are not. $\sigma_{2}$ is excluded because $T(\langle b,S,d\rangle)\geq 2$ and $\sigma_{3}$ is excluded because the timestamp of $\langle b,S,e\rangle$ is undefined.

To incorporate this notion into our algorithm, we assume that each server can evaluate a single annotated atom. Specifically, given an annotated $a^{\bowtie}$, a timestamp $\tau$, and a substitution $\sigma$, server $k$ can call ${\textsc{Evaluate}(a^{\bowtie},\tau,I_{k},T_{k},\sigma)}$. The call returns each substitution $\rho$ defined over the variables in $a$ and $\sigma$ such that ${\sigma\subseteq\rho}$ holds, ${a\rho\in I_{k}}$ holds, and $T_{k}$ is defied on $a\rho$ and it satisfies ${T(a\rho)\bowtie\tau}$. In other words, Evaluate matches $a^{\bowtie}$ in $I_{k}$ and $T_{k}$ w.r.t. $\tau$ and it returns each extension of $\sigma$ that agrees with $a^{\bowtie}$. For efficiency, server $k$ should index the facts in $I_{k}$; any RDF indexing scheme can be used, and one can modify index lookup to simply skip over facts whose timestamps do not match $\tau$.

Finally, we describe how rule matching is mapped to answering annotated queries. Let $P$ be a datalog program to be materialised. Given a fact $f$, function ${\textsc{MatchRules}(f,P)}$ considers each rule ${h\leftarrow b_{1}\wedge\dots\wedge b_{n}\in P}$ and each body atom $b_{p}$ with ${1\leq p\leq n}$, and, for each substitution $\sigma$ over the variables of $b_{p}$ where ${f=b_{p}\sigma}$, it returns ${(\sigma,b_{p},Q,h)}$ where $Q$ is the annotated query

[TABLE]

Intuitively, MatchRules identifies each rule and each pivot body atom $b_{p}$ that can be matched to $f$ via substitution $\sigma$. This $\sigma$ will be extended to all body atoms of the rule by matching all remaining atoms in nested loops using function Evaluate. The annotations in (3) specify how to match the remaining atoms without repetition: facts matched to atoms before (resp. after) the pivot must have timestamps strictly smaller (resp. smaller or equal) than the timestamp of $f$. As is usual in query evaluation, the atoms of (3) may need to be reordered to obtain an efficient query plan. This can be achieved using any known technique, and further discussion of this issue is out of scope of this paper.

4.2 Occurrence Mappings

To decide whether rule matching may need to proceed on other servers, each server $k$ must store indexes $\mu_{k,s}$, $\mu_{k,p}$, and $\mu_{k,o}$ called occurrence mappings that map resources to sets of server IDs. To ensure scalability, $\mu_{k,s}$, $\mu_{k,p}$, and $\mu_{k,o}$ need not be defined on all resources: if, say, $\mu_{k,s}$ is not defined on resource $r$, we will assume that $r$ can occur on any server. However, these mappings will need to be correct during algorithm’s execution: if server $I_{k}$ contains a resource $r$ (in any position), and if $r$ occurs on some other server $j$ in position $\pi$, then $\mu_{k,\pi}$ must be defined on $r$ and it must contain $j$. Moreover, all servers will have to know the locations of all resources occurring in the heads of the rules in $P$.

Storing only partial occurrences at each server introduces a complication: when a server processes a partial match $\sigma$ received from another server, its local occurrence mappings may not cover some of the resources in $\sigma$. Potter et al. [12] solve this by accompanying each partial match $\sigma$ with a vector ${\boldsymbol{\lambda}=\lambda_{s},\lambda_{p},\lambda_{o}}$ of partial occurrences. Whenever a server extends $\sigma$ by matching an atom, it also records in $\boldsymbol{\lambda}$ its local occurrences for each resource added to $\sigma$ so that this information can be propagated to subsequent servers.

Occurrence mappings are initialised on each server $k$ for each resource that initially occurs in $I_{k}$, but they may need to be updated as fresh triples are derived. To ensure that the occurrences correctly reflect the distribution of resources at all times, occurrence mappings of all servers must be updated before a triple can be added to the set of derived triples of the target server.

Our algorithm must decide where to store each freshly derived triple. It is common practice in distributed RDF systems to store all triples with the same subject on the same server. This is beneficial since it allows subject–subject joins—the most common type of join in practice—to be answered without any communication. We follow this well-established practice and ensure that the derived triples are grouped by subject. Consequently, we require that $\mu_{k,s}(r)$, whenever it is defined, contains exactly one server. Thus, to decide where to store a derived triple, the server from the subject’s occurrences is used, and, if the subject occurrences are unavailable, then a predetermined server is used.

4.3 Communication Infrastructure and Message Types

We assume that the servers can communicate asynchronously by passing messages. That is, each server can call ${\textsc{Send}(m,d)}$ to send a message $m$ to a destination server $d$. This function can return immediately, and the receiver can processes the message later. Also, our core algorithm is correct as long as each sent message is processed eventually, regardless of whether the messages are processed in the order in which they are sent between servers. We next describe the two types of message used in our algorithm. The approach used to detect termination can introduce other message types and might place constraints on the order of message delivery; we discuss this in more detail in Section 4.5.

Message $\mathsf{PAR}[i,\sigma,Q,h,\tau,\boldsymbol{\lambda}]$ informs a server that $\sigma$ is a partial match obtained by matching some fact with timestamp $\tau$ to the body of a rule with head atom $h$; moreover, the remaining atoms to be matched are given by an annotated query $Q$ starting from the atom with index $i$. The partial occurrences for all resources mentioned in $\sigma$ are recorded in $\boldsymbol{\lambda}$.

Message $\mathsf{FCT}[f,D,k_{h},\tau,\boldsymbol{\lambda}]$ says that $f$ is a freshly derived fact that should be stored at server $k_{h}$. Set $D$ contains servers whose occurrences must be updated due to the addition of $f$. Timestamp $\tau$ corresponds to the time at which the message was sent. Finally, $\boldsymbol{\lambda}$ are the partial occurrences for the resources in $f$.

Potter et al. [12] already observed $\mathsf{PAR}$ messages correspond to partial join results so a large number of such messages can be produced during query evaluation; moreover, to facilitate asynchronous processing, the received $\mathsf{PAR}$ messages may need to be buffered on the received server, which can easily require excessive space. They also presented a flow control mechanism that can be used to restrict memory consumption at each server without jeopardising completeness. This solution is directly applicable to our problem as well, so we do not discuss it any further.

4.4 The Algorithm

With these definitions in mind, Algorithms 1 and 2 comprise our approach to distributed datalog materialisation. Before starting, each server $k$ loads its subset of the input RDF graph into $I_{k}$, sets the timestamp of each fact in $I_{k}$ to zero, initialises $C_{k}$ to zero, and receives the copy of the program $P$ to be materialised. The server then starts an arbitrary number of server threads, each executing the ServerThread function. Each thread repeatedly processes either an unprocessed fact $f$ in $I_{k}$ or an unprocessed message $m$; if both are available, they can be processed in arbitrary order. Otherwise, the termination condition is processed as we discuss later in Section 4.5.

Function Synchronise updates the local clock $C_{k}$ with a timestamp $\tau$. This must be done in a critical section (i.e., two threads should not execute it simultaneously). The local clock is updated if ${C_{k}\leq\tau}$ holds; moreover, all facts in $I_{k}$ without a timestamp are are timestamped with $C_{k}$ since they are derived before the event corresponding to $\tau$. Assigning timestamps to facts in this way reduces the need for synchronising access to $C_{k}$ between threads.

Function ProcessFact kickstarts the matching of the rules to fact $f$. After synchronising the clock with the timestamp of $f$, it simply calls MatchRules to identify all rules where one atom matches to $f$, and forwards each match FinishMatch to finish matching the pivot atom.

A $\mathsf{PAR}$ message is processed by matching atom $a_{i}^{\bowtie_{i}}$ of the annotated query in $I_{k}$ and $T_{k}$ w.r.t. $\tau$, and forwarding each match to FinishMatch.

A $\mathsf{FCT}$ message informs server $k$ that fact $f$ will be added to the set $I_{k_{h}}$ of facts derived at server $k_{h}$. Set $D$ lists all remaining servers that need to be informed of the addition, and partial occurrences $\boldsymbol{\lambda}$ are guaranteed to correctly reflect the occurrences of each resource in $f$. Server $k$ updates its $\mu_{k,\pi}(r)$ by appending $\lambda_{\pi}(r)$ (line 19). Since servers can simultaneously process $\mathsf{FCT}$ messages, server $k$ adds to $D$ all servers that might have been added to $\mu_{k,\pi}(r)$ since the point when $\lambda_{\pi}(r)$ had been constructed (line 18), and it also updates $\lambda_{\pi}(r)$ (line 19). Finally, the server adds $f$ to $I_{k}$ if $k$ is the last server (line 20), and otherwise it forwards the message to another server $d$ form $D$.

Function FinishMatch finishes matching atom $a_{\mathit{last}}$ by (i) extending $\boldsymbol{\lambda}$ with the occurrences of all resources that might be relevant for the remaining body atoms or the rule head, and (ii) either matching the next body atom or deriving the rule head. For the former task, the algorithm identifies in line 30 each variable $x$ in the matched atom that either occurs in the rule head or in a remaining atom, and for each $\pi$ it adds the occurrences of $x\sigma$ to $\lambda_{\pi}$. Now if $Q$ has been matched completely (line 31), the server also ensures that the partial occurrences are correctly defined for the resources occurring in the rule head (lines 32–33), it identifies the server $k_{h}$ that should receive the derived fact as described in Section 4.2, it identifies the set $D$ of the destination servers whose occurrences need to be updated, and it sends the $\mathsf{FCT}$ message to one server from $D$. Otherwise, atom $a_{i+i}\sigma$ must be matched next. To determine the set $D$ of servers that could possibly match this atom, server $k$ intersects the occurrences of each resource from $a_{i+i}\sigma$ (line 44) and sends a $\mathsf{PAR}$ message to all servers in $D$.

4.5 Termination Detection

Since no server has complete information about the progress of any other server, detecting termination is nontrivial; however, we can reuse an existing solution.

When messages between each pair of servers are guaranteed to be delivered in order in which they are sent (as is the case in our implementation), one can use Dijkstra’s token ring algorithm [3], which we summarise next. All servers in the cluster are numbered from $1$ to $\ell$ and are arranged in a ring (i.e., server 1 comes after server $\ell$). Each server can be black or white, and the servers will pass between them a token that can also be black or white. Initially, all servers are white and server 1 has a white token. The algorithm proceeds as follows.

• •

When server 1 has the token and it becomes idle (i.e., it has no pending work or messages), it sends a white token to the next server in the ring.

• •

When a server other than 1 has the token and it becomes idle, the server changes the token’s colour to black if the server is itself black (and it leaves the token’s colour unchanged otherwise); the server forwards the token to the next server in the ring; and the server changes its colour to white.

• •

A server $i$ turns black whenever it sends a message to a server ${j<i}$.

• •

All servers can terminate when server 1 receives a white token.

The Dijkstra–Scholten algorithm extends this approach to the case when the order of message delivery cannot be guaranteed.

4.6 Correctness

We next prove that our algorithm is correct and that it exhibits the nonrepetition property. We present here only an outline of the correctness argument, and we give the full proof in the supplementary material.

Let us fix a run of Algorithms 1 and 2 on some input. First, we show that Lamport timestamps capture the causality of fact derivation in this run. To this end, we introduce four event types relating to an arbitrary fact $f$. Event $\mathsf{add}_{k}(f)$ occurs when $f$ is assigned a timestamp on server $k$ in line 26. Event $\mathsf{process}_{k}(f)$ occurs when server $k$ starts processing a new fact in line 8. Event $\mathsf{PAR}_{k}(f,i)$ occurs when server $k$ completes line 12 for a $\mathsf{PAR}$ message with index $i$ originating from a call to MatchRules on fact $f$. Finally, event $\mathsf{FCT}_{k}(f)$ occurs when server $k$ completes line 16 for a $\mathsf{FCT}$ message for fact $f$. We write ${e_{1}\rightsquigarrow e_{2}}$ if event $e_{1}$ occurs chronologically before event $e_{2}$; this relation is clearly transitive and irreflexive. Furthermore, each fact is stored and assigned a timestamp on just one server, so we define $T(f)$ as $T_{k}(f)$ for the unique server $k$ that satisfies ${f\in I_{k}}$. Lemma 1 then essentially says that the happens-before relationship between facts and events on facts agrees with the timestamps assigned to the facts.

Lemma 1 ()

In each run of the algorithm, for each server $k$, and all facts $f_{1}$ and $f_{2}$, we have ${T(f_{1})<T(f_{2})}$ whenever one of the following holds:

• •

${\mathsf{PAR}_{k}(f_{1},i)\rightsquigarrow\mathsf{add}_{k}(f_{2})}$* for some $i$,*

• •

${\mathsf{process}_{k}(f_{1})\rightsquigarrow\mathsf{FCT}_{k}(f_{2})}$, or

• •

${\mathsf{PAR}_{k}(f_{1},i)\rightsquigarrow\mathsf{FCT}_{k}(f_{2})}$* for some $i$.*

Next, we show that then the occurrence mappings $\mu_{k,\pi}$ on each relevant server $k$ are updated whenever a triple is added to some $I_{j}$. This condition is formally captured in Lemma 2, and it ensures that partial answers are sent to all relevant servers that can possibly match an atom in a query. Note that the implication in Lemma 2 is the only relevant direction: if $\mu_{k,\pi}(r)$ contains irrelevant servers, we can have redundant $\mathsf{PAR}$ messages, but this does not harm correctness.

Lemma 2 ()

At any point in the algorithm’s run, for all servers $k$ and $j$, each position ${\pi\in\Pi}$, and each resource $r$ such that $r$ occurs in $I_{j}$ at position $\pi$ and $\mu_{k,\pi}$ is defined on $r$, property ${j\in\mu_{k,\pi}(r)}$ holds.

Using Lemmas 1 and 2, we prove our main claim.

Theorem 4.1 ()

For ${I_{1},\dots,I_{\ell}}$ the sets obtained by applying Algorithms 1 and 2 to an input set of facts $I$ and program $P$, we have ${P^{\infty}(I)=I_{1}\cup\dots\cup I_{\ell}}$. Moreover, the algorithm exhibits the nonrepetition property.

5 Evaluation

To evaluate the practical applicability of our approach, we have implemented a prototype distributed datalog reasoned that we call DMAT. We have reused a well-known centralised RDF system to store and index triples in RAM, on top of which we have implemented a mechanism for associating triples with timestamps. To implement the Evaluate function, we use the system’s interface for answering individual atoms and then simply filter out the answers whose timestamp does not match the given one. For simplicity, DMAT currently uses only one thread per server, but we plan to remove this limitation in future. We have published444http://krr-nas.cs.ox.ac.uk/2019/distributed-materialisation/ the executable and test files used, with the exception of the datasets, which can be recreated using the LUBM generator.

We have evaluated our system’s performance in three different ways, each aimed at analysing a specific aspect of the problem. First, to establish a baseline for the performance of DMAT, as well as to see whether distributing the data can speed up the computation, we compared DMAT with RDFox [10]—a state-of-the-art, centralised, RAM-based reasoner—on a relatively small dataset. Second, to compare the performance of our approach with the state-of-the-art for distributed reasoning, we compared DMAT with WebPIE [16]—a distributed RDF reasoner based on MapReduce. Third, we studied the scalability of our approach by proportionally increasing the input data and the number of servers.

Few truly large RDF datasets are publicly available, so the evaluation of distributed reasoning is commonly based on the well-known LUBM555http://swat.cse.lehigh.edu/projects/lubm/ benchmark (e.g., [16, 9, 20]). Following this practice, LUBM datasets of sizes ranging from 134 M to 6.5 G triples provided the input data for our system. We also used the lower bound program was obtained by extracting the OWL 2 RL portion of the LUBM ontology and translating it into datalog.

We conducted all tests with DMAT on the Amazon Elastic Compute Cloud (EC2). We used the $r4.8xlarge$ servers, each equipped with a 2.3 GHz Intel Broadwell processors and 244 GB RAM; such a large amount of RAM was needed since the underlying storage mechanism in our system is RAM-based. An additional, identical server stored the dictionary (i.e., a data structure mapping resources to integers): this server did not participate in materialisation, but was used only to distribute the program and the data to the cluster. Finally, the EC2 instances offer 10 Gbps network performance, according to the manifest published by Amazon666https://aws.amazon.com/ec2/instance-types/. In all tests apart from the ones with WebPIE, we partitioned the dataset by using the graph partitioning approach by Potter et al. [12]: this data partitioning approach aims to place strongly connected resources on the same server and thus reduce communication overhead. For the tests with WebPIE, due to memory constraints of the partitioning software, we partitioned triples by subject hashing. For each test, we loaded the input triples and the program into all servers, and computed the materialisation while recording the wall-clock time. Apart from reporting this time, we also report the reasoning throughput measured in thousands of triples derived per second and worker (ktps/w). We next discuss the results of our experiments.

Comparison with RDFox.

First, we ran RDFox and DMAT on a fixed dataset while increasing the number of threads for RDFox and the numbers of servers for DMAT. Since RDFox requires the materialised dataset to fit into RAM of a single server, we used a small input dataset of just 134 M triples. The results, shown in Table 3, provide us with two insights. First, the comparison on one thread establishes a baseline for the DMAT’s performance. In particular, DMAT is slower than RDFox, which is not surprising: RDFox is a mature and tuned system, whereas DMAT is just a prototype. However, DMAT is still competitive with RDFox, suggesting that our approach is free of any overheads that might make it uncompetitive. Second, the comparison on multiple threads shows how effective our approach is at achieving concurrency. RDFox was specifically designed with that goal in mind in a shared-memory setting. However, as one can see from our results, DMAT also parallelises computation well: in some cases the speedup is larger than in the case of RDFox. This seems to be the case mainly because data partitioning allows each server to handle an isolated portion of the graph, which can reduce the need for synchronisation.

Comparison with WebPIE.

Next, we compared DMAT with WebPIE to see how our approach compares with the state of the art in distributed materialisation. To keep the experimentation effort manageable, we did not rerun WebPIE ourselves; rather, we considered the same input dataset sizes as Urbani et al. [16] and reused their published results. The setting of these experiments thus does not quite match our setting: (i) WebPIE handles only the ter Horst fragment of OWL and thus cannot handle all axioms in the OWL 2 RL subset of the LUBM ontology; (ii) experiments with WebPIE were run on physical (rather than virtualised) servers with only 24 GB of RAM each; and (iii) WebPie used 64 workers, while DMAT used just 12 servers. Nevertheless, as one can see from Table 3, despite using more than five times fewer servers, DMAT is faster by an order of magnitude. Hadoop is a disk-based system so lower performance is to be expected to some extent, but this may not be the only reason: triples in DMAT are partitioned by subject so, unlike WebPIE, DMAT does not perform any communication on subject–subject joins.

Scalability Experiments.

Finally, to investigate the scalability of DMAT, we measured how the system’s performance changes when the input data and the number of servers increase proportionally. The results are shown in Table 3. As one can see, increasing the size of the input does introduce an overhead for each server. Our analysis suggests that this is mainly because handling a larger dataset requires sending more messages, and communication seems to be the main source of overhead in the system. This, in turn, leads to a moderate reduction in throughout. Nevertheless, the system still exhibits very high inferences rates and clearly scales to very large inputs.

6 Conclusion

In this paper we have presented a novel approach to datalog reasoning in distributed RDF systems. Our work extends the distributed query answering algorithm by Potter et al. [12], from which it inherits several benefits. First, the servers in our system are asynchronous, which is beneficial for concurrency. Second, dynamic data exchange is effective at reducing network communication, particularly when input data is partitioned so that related triples are co-located. Finally, we have shown empirically that our prototype implementation is an order of magnitude faster than WebPIE [17], and that it scales to increasing data loads. In the near future we intend to conduct tests on a broader range of datasets and rule sets, as well as direct comparisons with other in-memory distributed systems that perform tasks similar to DMAT.

We see several interesting avenues for our future work. First, better approaches to partitioning the input data are needed: hash partitioning does not guarantee that joins other than subject–subject ones are processed on one server, and graph partitioning cannot handle large input graphs. Second, supporting more advanced features of datalog, such as stratified negation and aggregation is also needed in many practical applications.

Acknowledgments

This work was supported by the SIRIUS Centre for Scalable Access in the Oil and Gas Domain, and the EPSRC project AnaLOG.

Appendix 0.A Proofs

See 1

Proof

Consider an arbitrary run of Algorithms 1 and 2, arbitrary server $k$, and arbitrary facts $f_{1}$ and $f_{2}$.

Assume that ${\mathsf{PAR}_{k}(f_{1})\rightsquigarrow\mathsf{add}_{k}(f_{2})}$ holds. Then, after the call to Synchronise in line 12, the local clock of server $k$ has a value that is strictly larger than $T(f_{1})$. Thus, when $f_{2}$ is assigned a timestamp, ${T(f_{2})>T(f_{1}})$ holds.

If ${\mathsf{process}_{k}(f_{1})\rightsquigarrow\mathsf{FCT}_{k}(f_{2})}$ (resp. ${\mathsf{PAR}_{k}(f_{1})\rightsquigarrow\mathsf{FCT}_{k}(f_{2})}$) holds, then after the call to Synchronise in line 8 (resp. 12), the local clock of server $k$ has a value that is strictly larger than $T(f_{1})$. Server $k$ reads this value into the $\mathsf{FCT}$ message for $f_{2}$ in line 41 or line 23. Before $f_{2}$ is added on some destination server, this server calls Synchronise in line 16, which ensures $T(f_{2})>T(f_{1})$. ∎

See 2

Proof

Fix $r$ in the domain of $\mu_{k,\pi}$, we want to show that $j\in\mu_{k,\pi}(r)\rightsquigarrow r\in voc_{\pi}(I_{j})$. If the initial state of $voc_{\pi}(I_{j})$ includes $r$, then there is nothing to prove because the occurrence mappings are initialized consistent.

Now let $\mathsf{addOcc}_{k}(r,\pi,j)$ denote the point at line 19 where $j$ is added to the image of $\mu_{k,\pi}(r)$. Let $f_{k,r}$ denote the first fact added to $I_{k}$ with $r$ as an argument and $\pi_{k}$ the position of $r$ in $f_{k,r}$. Let $f_{j,r}$ be the analogous for $I_{j}$. Let $D(f)$ denote the set of update servers compiled for fact $f$ in FinishMatch.

Assume $k\neq j$ and that $\mathsf{add}_{k}(f_{k,r})\rightsquigarrow\mathsf{add}_{j}(f_{j,r})$ and $f_{j,r}\not\in I_{0}$. We know that the set $D(f_{j,r})\cap D(f_{k,r})$ is not empty because of Lemma 3. Let $l$ be an element of the intersection. Both $\mathsf{FCT}_{l}(f_{k,r})$ and $\mathsf{FCT}_{l}(f_{j,r})$ will occur on server $l$. If $\mathsf{addOcc}_{l}(r,\pi_{k},k)\rightsquigarrow\mathsf{addOcc}_{l}(r,\pi_{j},j)$, $k$ is be added to $D(f_{j,r})$ at line 19, if it was not an initial member of $D(f_{j,r})$. In either case, or in the case that $l=k$, $f_{j,r}$ updates server $k$ before being added to $I_{k}$, hence $\mathsf{addOcc}_{k}(r,\pi_{j},j)\rightsquigarrow\mathsf{add}_{j}(f_{j,r})$. If instead $\mathsf{addOcc}_{l}(r,\pi_{j},j)\rightsquigarrow\mathsf{addOcc}_{l}(r,\pi_{k},k)$, $j$ is added to $D(f_{k,r})$, and we can still conclude $\mathsf{addOcc}_{k}(r,\pi_{j},j)\rightsquigarrow\mathsf{add}_{k}(f_{k,r})\rightsquigarrow\mathsf{add}_{j}(f_{j,r})$ because of our initial assumption. If we assume $\mathsf{add}_{j}(f_{j,r})\rightsquigarrow\mathsf{add}_{k}(f_{k,r})$ then the symmetrical argument applies.

We have shown that, for $k\neq j$, $\mathsf{addOcc}_{k}(r,\pi_{j},j)\rightsquigarrow\mathsf{add}_{j}(f_{j,r})$, which is equivalent to the thesis. When $k=j$, then it is true by construction that $\mathsf{addOcc}_{k}(r,\pi_{k},k)\rightsquigarrow\mathsf{add}_{k}(f_{k,r})$ and we conclude. ∎

Lemma 3 ()

Let $a,b\in P^{\infty}(I)$ have a common resource $r$, then $D_{r}(a)\cap D_{r}(b)\neq\emptyset$, where $D_{r}(x)$ is the update set created for the $\mathsf{FCT}$ message of $x$.

Proof

The proof is by induction over $P^{i}(I)$. It is true by definition for $i=0$ because the condition in Lemma 2 has to apply to the initial configuration. For the inductive step, suppose the property is true for all facts in $P^{i-1}(I)$ and let $a,b\in P^{i}(I)$ share a resource $r$. We can find two chains $a_{0},a_{1},\cdots,a_{n}=a$ and $b_{0},b_{1},\cdots,b_{m}=b$ such that for each $i$ and $x\in\{a,b\}$ $x_{i}$ participates in the derivation of $x_{i+1}$, it has $r$ among its arguments, and $D_{r}(x_{i})\subseteq D_{r}(x_{i+1})$ (we select the branch of the derivation tree that corresponds to the first matchings of the resource $r$ so that the partial mappings are passed between $x_{i}$ and $x_{i+1}$). At each stage $D_{r}(a_{i})\cap D_{r}(b_{i})\subset D_{r}(a_{i+1})\cap D_{r}(b_{i+1})$, therefore the property holds.

See 4.1

Proof (Soundness)

The proof is by induction on the construction of sets $I_{i}$. The argument is straightforward so we just present a sketch: when ${(\sigma,a,Q,h)}$ is returned on some server $k$ in line 9, substitution $\sigma$ satisfies ${a\sigma\in I_{k}}$; moreover, as matching of $Q$ progresses, each substitution $\sigma^{\prime}$ returned in line line 13 satisfies ${a_{i}\sigma^{\prime}\in I_{k^{\prime}}}$; consequently, each substitution $\sigma$ in line 41 is an answer to the annotated query $Q$. Thus, each such $\sigma$ matches all body atoms of the rule corresponding to ${(\sigma,a,Q,h)}$ in $P^{\infty}(I)$, and so we clearly have ${h\sigma\in P^{\infty}(I)}$. ∎

Proof (Completeness)

Let $P$ be a program, let $I$ be an input dataset, and let ${I_{1},\dots,I_{\ell}}$ be the datasets computes after Algorithms 1 and 2 finish on some partition of $I$ to $\ell$ servers. Our claim follows from the following property:

($\ast$) for each $i$ and each fact ${f\in P^{i}(I)}$, a server $k$ exists were ${f\in I_{k}}$ holds.

The proof is by induction on $i$. The base case holds trivially, so we assume that ($\ast$) holds for some ${i\geq 0}$ and show that it also holds for ${i+1}$. To this end, we consider an arbitrary fact ${f\in P^{i+1}(I)\setminus P^{i}(I)}$. This fact is derived by a rule ${h\leftarrow b_{0}\wedge\dots\wedge b_{n}\in P}$ and substitution $\sigma$ such that ${h\sigma=f}$ and ${b_{j}\sigma\in P^{i}(I)}$ for ${0\leq j\leq n}$. Now choose $p$ as the smallest integer between [math] and $n$ such that ${T(b_{p^{\prime}})\leq T(b_{p}\sigma)}$ holds for each ${0\leq p^{\prime}\leq n}$. Now let ${a_{0},\dots,a_{n}}$ be the body atoms of the rule rearranged so that ${a_{0}=b_{p}}$ is the pivot atom, and the remaining atoms correspond to the annotated query ${Q=a_{1}^{\bowtie_{1}}\wedge\dots\wedge a_{n}^{\bowtie_{n}}}$ returned by ${\textsc{MatchRules}(b_{p}\sigma,P)}$ in line 9 on fact $b_{p}\sigma$. Finally, for each ${0\leq j\leq n}$, let $\sigma_{j}$ be the substitution $\sigma$ restricted to all variables occurring in atoms ${a_{0},\dots,a_{j}}$ and let ${\tau_{j}=T(a_{j}\sigma)}$; moreover, ($\ast$) holds for $i$ by the induction assumption, so there exists a server $k_{j}$ such that ${a_{j}\sigma\in I_{k_{j}}}$ holds. We next prove the following:

($\lozenge$) for each ${0\leq j\leq n}$, function ${\textsc{FinishMatch}(j,\sigma_{j},a_{j},Q,h,\tau_{0},\boldsymbol{\lambda}_{j})}$ is called for some $\boldsymbol{\lambda}_{j}$.

Property ($\lozenge$) implies our claim because in lines 31–41 the algorithm then constructs a $\mathsf{FCT}$ message for $h\sigma$ and dispatches it to some server $k_{h}$, so $h\sigma$ is eventually added to $I_{k_{h}}$ in line 20, as required for ($\ast$).

We next prove ($\lozenge$) by induction on ${0\leq j\leq n}$. For the base case, ${a_{0}\sigma\in I_{k_{0}}}$ ensures that $\textsc{ProcessFact}(a_{0}\sigma)$ is called on server $k_{0}$, so ${\textsc{MatchRules}(a_{0}\sigma,P)}$ returns ${(\sigma_{0},a_{0},Q,h)}$, and ${\textsc{FinishMatch}(0,\sigma_{0},a_{0},Q,h,\tau_{0},\boldsymbol{\emptyset})}$ is called in line 10. For the induction step, we assume that ($\lozenge$) holds for some ${0\leq j<n}$, and we show that it holds for ${j+1}$ as well. To this end, we consider several cases.

Assume that event ${\mathsf{PAR}_{k_{j+1}}(a_{0}\sigma,j+1)}$ occurs at some point during the algorithm’s run. Server $k_{j+1}$ then executes line 13 for $a_{j+1}^{\bowtie_{j+1}}$. Note that ${a_{j+1}\sigma\in I_{k_{j+1}}}$ holds by induction assumption. We next show that server $k_{j+1}$ contains $a_{j+1}\sigma$ at the point in time when line 13 is executed. We have the following possibilities.

• •

If event $\textsf{add}_{k_{j_{1}}}(a_{j+1}\sigma)$ never happens, then server $k_{j+1}$ contains fact $a_{j+1}\sigma$ since the algorithm’s start.

• •

If ${\textsf{add}_{k_{j_{1}}}(a_{j+1}\sigma)\rightsquigarrow\mathsf{PAR}_{k_{j+1}}(a_{0}\sigma,j+1)}$ holds, then server $k_{j+1}$ clearly contains fact $a_{j+1}\sigma$ at this point in time.

• •

If ${\mathsf{PAR}_{k_{j+1}}(a_{0}\sigma,j+1)\rightsquigarrow\textsf{add}_{k_{j_{1}}}(a_{j+1}\sigma)}$ were to hold, then Lemma 1 implies ${T(a_{0}\sigma)<T(a_{j+1}\sigma)}$, contradicting our assumption that ${T(a_{j+1}\sigma)\leq T(a_{0}\sigma)}$.

Moreover, if ${T(a_{j+1}\sigma)=T(a_{0}\sigma)}$, since ${a_{0}=b_{p}}$ was chosen so that $p$ is the least index of a body atom matched to a fact with timestamp $T(a_{0}\sigma)$, the shape of $Q$ from (3) ensures that ${\bowtie_{j+1}=\;\leq}$. Consequently, the call to Evaluate in line 13 on server $k_{j+1}$ returns $\sigma_{j+1}$, so the call in line 14 ensures ($\lozenge$).

Now assume that event ${\mathsf{PAR}_{k_{j+1}}(a_{0}\sigma,j+1)}$ never occurs during the algorithm’s run—that is, server $k_{j}$ never forwards a $\mathsf{PAR}$ message to server $k_{j+1}$. Then, for some ${\pi\in\Pi}$ and ${r=a_{j+1}\sigma_{j}|_{\pi}}$, we have ${k_{j+1}\not\in\lambda_{\pi}(r)}$ at the point in time when line 44 is executed on server $k_{j}$, ensuring that $k_{j+1}$ is removed from $D$. However, this $\lambda_{\pi}(r)$ is populated in line 30 when resource $r$ is matched on some server $k_{s}$ with ${0\leq s\leq j}$, so at that point in time we have ${k_{j+1}\not\in\mu_{k_{s},\pi}(r)}$. Now if event $\textsf{add}_{k_{j+1}}(a_{j+1}\sigma)$ never happened, then server $k_{j+1}$ would contain $a_{j+1}\sigma$ when the algorithm starts; but then, since $\mu_{k_{s},\pi}$ is defined on $r$, Lemma 2 implies ${k_{j+1}\not\in\mu_{k_{s},\pi}(r)}$, which is a contradiction. Consequently, event $\textsf{add}_{k_{j+1}}(a_{j+1}\sigma)$ occurs on server $k_{j+1}$.

Moreover, let ${\alpha=\mathsf{process}_{k_{s}}(a_{0}\sigma)}$ if ${s=0}$, and let ${\alpha=\mathsf{PAR}_{k_{s}}(a_{0}\sigma,j)}$ if ${s>0}$. Function FinishMatch is called on server $k_{s}$ by the induction assumption for ($\lozenge$), so event $\alpha$ occurs on server $k_{s}$.

Now note that the set $I_{k_{j+1}}\cap\{f\mid f|_{\pi}=r\}$ is not empty and let $f_{r,\pi}$ be the first fact in the in the set that is added to $k_{j+1}$ and consider the set the set $D$ constructed in line 35 for $f_{r,\pi}$ (from here on update set). By definition,the partial occurrences for resource $r$ at position $\pi$ in the $\mathsf{FCT}$ message for $f_{r,\pi}$ cannot contain $k_{j+1}$, therefore the occurrences of $r$ are added to $D$. Let $D_{r}$ be the contribution of $r$ to $D$; it cannot be empty because $f_{r,\pi}$ was derived at some server and it is either the case that $D_{r}$ contains $k_{s}$ or not.

First, assume $k_{s}\in D_{r}$, then event $\mathsf{FCT}_{k_{s}}(f_{r,\pi})$ occurs on server $k_{s}$. This event updates occurrences for $r$ on $k_{s}$, so for ${k_{j+1}\not\in\mu_{k_{s},\pi}(r)}$ to hold, ${\alpha\rightsquigarrow\mathsf{FCT}_{k_{s}}(a_{j+1}\sigma)}$ must hold. But then, regardless of how $\alpha$ is defined, Lemma 1 implies $T(a_{0}\sigma)<T(a_{j+1}\sigma)$, which contradicts our assumption that ${T(a_{j+1}\sigma)\leq T(a_{0}\sigma)}$ holds.

Otherwise, we know that the presence of the resource $r$ in $I_{k_{s}}$ had not yet been fully notified when the the partial mappings for the argument $r$ of $f_{r,\pi}$ were created. Let $f^{\prime}_{r}$ be the first added fact to $I_{k_{s}}$ that contains $r$ in any position, and its update set $D^{\prime}$. We apply Lemma 3 on $f_{r,\pi}$ and $f^{\prime}_{r}$ to find an element in $k^{\prime}\in D_{r}\cap D^{\prime}_{r}$ where both $\mathsf{FCT}_{k^{\prime}}(f_{r,\pi})$ and $\mathsf{FCT}_{k^{\prime}}(f^{\prime}_{r})$ occur. If $\mathsf{FCT}_{k^{\prime}}(f_{r,\pi})\rightsquigarrow\mathsf{FCT}_{k^{\prime}}(f^{\prime}_{r})$, then $k_{j+1}$ is added to $\mu_{k^{\prime},\pi}$ at line 19 when the first message is processed, and then to $\lambda_{\pi}$ at line 19 when the second message is processed. This event is then followed by $\mathsf{FCT}_{k_{s}}(f^{\prime}_{r})$ and we proceed as done with $\mathsf{FCT}_{k_{s}}(f_{r,\pi})$ above to derive $T(a_{0}\sigma)<T(f^{\prime}_{r})$ from Lemma 1. But $f^{\prime}_{r}$ is the first appearance of $r$ in server $k_{s}$, hence $T(a_{0}\sigma)<T(a_{s}\sigma)$ which contradicts our assumption that $T(a_{s}\sigma)<T(a_{0}\sigma)$ holds.

If $\mathsf{FCT}_{k^{\prime}}(f^{\prime}_{r})\rightsquigarrow\mathsf{FCT}_{k^{\prime}}(f_{r,\pi})$, then $k_{s}$ is added to $\mu_{k^{\prime},\pi}$ at line 19 when the first message is processed, and then to $D$ at line 18 when the second message is processed, so $\mathsf{FCT}_{k_{s}}(f_{r,\pi})$ eventually happens and we conclude like above.

In summary, we proved that ${\mathsf{PAR}_{k_{j+1}}(a_{0}\sigma,j+1)}$ occurs on server $k_{j+1}$ and this concludes the theorem. ∎

Proof (Nonrepetition of Derivations)

Assume that processFact considers two facts $f_{1}$ and $f_{2}$, both of which matched the same rule and produce the same substitution $\sigma$. Let $b_{1}$ and $Q_{1}$ be the pivot atom and the annotated query returned in line 9 when $f_{1}$ is processed, and let $b_{2}$ and $Q_{2}$ be defined analogously. Thus, ${b_{1}\sigma=f_{1}}$ and ${b_{2}\sigma=f_{2}}$. Since each fact is processed only once, atoms $b_{1}$ and $b_{2}$ are distinct. Now w.l.o.g. let us assume that $b_{1}$ occurs before $b_{2}$ in the body of the rule; thus, the atom corresponding to $b_{2}$ in $Q_{1}$ is annotated with $\leq$, and the atom corresponding to $b_{1}$ in $Q_{2}$ is annotated with $<$. But then, $f_{2}$ is not matched by $Q_{1}$ if ${T(f_{1})<T(f_{2})}$ holds, and $f_{1}$ is not matched by $Q_{2}$ if ${T(f_{1})\geq T(f_{2})}$ holds, which contradicts our assumption that the algorithm repeats inferences. ∎