Multiprocessor equipment is cheap and ubiquitous now, but users of description logic (DL) reasoners have to face the awkward fact that the major tableau-based DL reasoners can make use only one of the available processors. Recently, researchers have started investigating how concurrent computing can play a role in tableau-based DL reasoning with the intention of fully exploiting the processing resources of multiprocessor computers. The published research mostly focuses on utilizing disjunctive branches, the or-part of tableau expansion trees. We investigated the possibility and the role of concurrently processing conjunctive branches, the and-part of tableau expansion trees. In this work, we present an algorithm to process conjunctive branches in parallel and address the key implementation aspects of the algorithm. A research prototype to execute this algorithm has been developed and empirically evaluated. The experimental results are presented and analyzed. We found that parallelizing the processing of conjunctive branches of tableau expansion trees is auspicious and can partly evolve into a scalable solution for DL reasoning.
Multiprocessor computers are almost everywhere now, such as high-performance computing servers, personal computers, laptops, tablets, phones, watches, etc. In many computing areas it is investigated how to better use the power of multiprocessor computers, and concurrent computing is an important option. Unfortunately, few such advances have been achieved for tableau-based Description Logic (DL) reasoning, which is the dominant method adopted by the major DL reasoning systems. None of the major DL reasoning systems can utilize the available processing capacity of multiprocessor computers properly. To be more precise, any of them can only use one processor at a time, no matter how many processors are available on the computer where it is running.
At the same time, DL reasoners are processing more complex ontologies. With the fast development of the Internet, DL reasoning can be considered in the age of big data. In the semantic web area, both huge but often simple as well as more and more complicated ontologies are emerging. Even for specialized or highly optimized DL systems it is not easy to reason about these ontologies. So, people are investigating innovative methods to improve reasoning performance. Concurrent reasoning solutions may improve performance for dealing with massive or complicated ontologies.
The wide availability of multiprocessor computing facilities makes concurrent DL
reasoning feasible. Several approaches have been reported for concurrent reasoning
in some non-shared or shared memory context [
It is well-known that an expansion tree is an and-or tree in tableau-based DL reasoning. Disjunctive branches compose the or part of a completion tree, conjunctive branches do the and part, and generally the two types of branches interlace with one another. Almost all of the few shared-memory parallelized tableau-based DL reasoning investigations focus on exploiting disjunctive branches in expansion trees.
In the remaining sections, the role of conjunctive branches in tableau expansion trees is addressed, a parallelized tableau-based algorithm which processes conjunctive branches simultaneously is presented, the key points of the algorithm’s implementation are discussed, experiments and evaluations on the program are shown and are analyzed, and some related investigations are also mentioned. 2
The concept pDr1:C1 [ Dr2:C2q \ pC3 [ C3q must have the disjunctive branches Dr1:C1[Dr2:C2 or C3[ C3 clash-free only if it is satisfiable. In this case, C3[ C3 K, so the satisfiability of pDr1:C1 [ Dr2:C2q \ pC3 [ C3q is determined by whether Dr1:C1 [ Dr2:C2 is satisfiable. That is to say, if the concept pDr1:C1 [ Dr2:C2q \ pC3 [
C3q is satisfiable, both the conjunctive branches Dr1:C1 and Dr2:C2 must be clashfree. The algorithm has to explore all conjunctive branches unless an unsatisfiability result is entailed.
Testing satisfiability is an essential function in tableau-based DL reasoning, and its goal is to search for a model by expanding concepts descriptions to completion trees, which consist of disjunctive and conjunctive branches. Testing satisfiability is generally used by other DL reasoning services. As we know an important functionality of modern DL systems is classification, which calculates all subsumption relationships entailed by a terminology: (1) With respect to T , C D is proven if CI DI holds for every model I of T . This is calculated by testing the satisfiability of the concept C [ D with respect to T . The subsumption computation is reducible to testing satisfiability in such a way. It is obvious that C D is the most common case, and thus the majority of such subsumption tests find models. That is to say, in order to gain better performance, a tableau-based DL reasoning algorithm should find models as fast as possible. In a tableau expansion view, such a model is a disjunctive branch with a bundle of conjunctive branches, both clashfree. Considering that such a disjunctive branch exists quite often, faster processing of conjunctive branches in that disjunctive branch should improve reasoning performance. Although research on parallelizing the processing of disjunctive branches is known, parallelizing the processing of conjunctive branches has not been researched so far, but it should play a role in improving the performance of tableau-based DL reasoning. 3
As mentioned in Section 1, many approaches are known that pursue new methods to increase the performance of reasoners, and concurrent computing is an option. In tableaubased DL reasoning, disjunctive and conjunctive branches have always been sequentially processed as of now, although there exists the potential benefit of parallelization.
The search for a model in a disjunctive branch is independent of other disjunctive
branches. The satisfiability of a concept is sufficiently supported by any model found
among disjunctive branches. With a sequential algorithm, if two disjunctive branches
are generated at some point, the second branch is only calculated if the first branch is not
clash-free. With a parallel algorithm, multiple disjunctive branches are processed at the
same time, and the search terminates when one of them is proven as clash-free. Some
research has already been reported on the topic of parallelizing tableau calculation on
disjunctive branches [
Computation on a conjunctive branch impacts its siblings in a different way than for disjunctive branches. A model is found by a tableau algorithm if and only if all involved conjunctive branch siblings are clash-free. With a sequential algorithm, all conjunctive branches on a disjunctive branch must be explored so that a clash-free and -tree can be built. Parallelizing computation on conjunctive branches in a satisfiable context should theoretically improve performance. Given the fact that most satisfiability tests introduced by classification, a key functionality of a DL reasoning system, return positive results, parallelizing conjunctive branches in tableau-based reasoning should play an important role. However, conjunctive branch parallelization has not been researched as much yet.
Parallelizing the processing of conjunctive branches is necessary to maximally utilize parallel computers. As we discussed in Section 2, the majority of computations of tableau-based DL reasoning find clash-free completion trees, each of which can be considered as a disjunctive branch containing a number of conjunctive branches. According to our experience, subsumption tests in classification are often easily satisfiable. Such a satisfiable disjunctive branch is usually the first one being tested. So, a parallel scheme in that case hardly improves reasoning performance. On the other hand, all conjunctive branches of a clash-free disjunctive branch must be explored and determined as clash-free. Therefore, parallelizing the exploration of potentially clash-free conjunctive branches can improve reasoning performance. Research on parallelizing the processing of conjunctive branches in tableau-based DL reasoning may even play a more important role than on disjunctive branches. 4
In this section we present a parallel tableau-based DL algorithm. When we use the word parallel in the following, a modern shared-memory multi-thread architecture should always be taken into account.
Concurrent algorithms have much more technical features than sequential ones. Some solutions require very tricky techniques. For example, in a sequential context, a DL tableau algorithm terminates the search in a disjunctive branch when a clash is found in a conjunctive branch. Such a termination task needs more complex mechanics in a parallel context. A termination test in a multiple threads context not only needs to check its own state but also the state of its siblings, i.e., it must monitor contradiction detection for all its siblings as the prerequisite for ensuring both soundness and performance.
The efficient managing of resources is an important tradeoff in designing concurrent algorithms, especially in a shared-memory context. A common pitfall in developing shared-memory parallel algorithms consist of taking unlimited threading for granted, as usually happens in recursive algorithms. A compensation for this flaw is the use of shared data to control resources allocated to a parallel program. However, shared data as well as communication between threads always reduce a parallel program’s performance.
Our scheme for controlling continuation resources is using a thread pool, which is normally configured with a fixed size. The members of the pool are reusable, which largely reduces system overhead. The most notable shared data consists of an increasing number of sibling conjunctive branches, and we use a concurrent queue to buffer them. Every threaded reasoning continuation picks a conjunctive branch out of the shared queue and processes it. Also, every continuation has to monitor and report its finding, as mentioned before.
The parallelization of processing conjunctive branches is addressed by Algorithms 1 and 2. It consists of two parts: Algorithm 1 as the control (master) and Algorithm 2 as the continuation (slave). Algorithm 1 first applies tableau expansion rules that are neither a D-rule nor a @-rule. The function clashed? returns true if all disjunctive branches (i.e., stages in Deslog [25]) are not clash-free, otherwise it returns false and cuts away clashed stages. If all disjunctive branches are not clash-free in this phase, the computation terminates. Otherwise, the model-search is continued on the generated disjunctive branches, which are provisionally clash-free. That is to say, the generating rule produces conjunctive branches which are kept in a buffer. Then the aforementioned thread pool schedules computation continuations on the conjunctive branch buffer. The computation continuation executed by the pooled thread is addressed by Algorithm 2, which is executed by multiple threads simultaneously.
We implemented Algorithms 1 and 2 with our parallelized tableau-based DL reasoning framework Deslog [25]. The underground parallel mechanics of Deslog is supported by the java.concurrent package. All working threads processing continuations are activated and pooled in the bootstrap phase. In each subsumption test run, every thread monitors a volatile flag that indicates whether a clash has been detected by its siblings and modifies the flag if it finds a clash (Line 2 and 3, Algorithm 2). If a clash has been detected, all threads and the flag are reset.
A performance bottleneck may result from the low level Java concurrency components. For example, we use a concurrent linked queue to buffer immediate conjunctive branches, and the buffer is accessed by a number of threads concurrently. Also, we use volatile flags as shared states with the intention of notifying state modification as fast as possible, and the maintenance of the volatile variables may require extra processor resources in a shared-memory parallel computing environment. We can design and construct the high level part of the program, but can hardly control the low level facilities on which the program depends. 5
Algorithm 1 is expected to improve the performance of tableau-based DL reasoning in such a way that conjunctive branches are processed simultaneously. A higher performance improvement is expected from reasoning about problems where more conjunctive expansion branches are involved. We designed a series of synthesized tests to prove this assumption.
The test cases consist of a set of Web Ontology Language (OWL) benchmarks developed on the basis of the tea ontology1. Their size (and complexity) can be scaled by a general concept inclusion (GCI) axiom pattern as follows: | ƒ i 0 CI
i | §
DR2i:pC2i \ C2i 1q;
I ; RiI
I
I ; i P N; | P N; i ⁄ | (2)
We defined a set of factors to measure the algorithm’s performance. Performance improvement is directly reflected by thread number and speedup. With the same thread number, reasoning performance varies with the number of involved conjunctive branches. So, our program records the number of involved conjunctive branches, , in every satisfiability test. N , the total number of the tests in a set of computations, of which every one processes conjunctive branches, is calculated after each run. We discovered that 1 http://code.google.com/p/deslog/downloads/detail?name=tea.tar.gz Algorithm 1: parallelize-tracesptree, rule-queue-without-D@, worker-queueq the most frequently occurring number of the involved conjunctive branches impacts the final reasoning performance and is the order of the conjunctive branches involved in a run. We take the mean of the values to calculate this order, which is noted as , where at most k conjunctive branches are involved in a satisfiability test: For example, we get shown in Table 1.
4977 , with respect to the sample data
We conducted several experiments to evaluate Algorithm 1. According to our
knowledge, the hardware environment can have quite an impact on the performance of a
parallel program in a shared-memory context [
The reasoning performance of Algorithm 1 is illustrated by the results shown in Figures 2-8. When 2:09, i.e., each test processes only 2 conjunctive branches, parallelizing the processing of conjunctive expansion does not contribute to a performance improvement. It seems that the overhead introduced by threading outclasses the benefits. However, according to our experiments performance improvements can be gained when ¥ 3:09. Better performance improvements come from greater values. k
N 0 k 0
N ; k P N; 0 ⁄ 8 (3)
2 p u seepd 1 0 1 2 3 4 5 6 7 8 thre9ads 10 11 12 13 14 15 16 17
Fig.4.Thespeedupwhen| 4and 5:08.
3 eedup 2 p s 1 0 1 2 3 4 5 6 7 8 thre9ads 10 11 12 13 14 15 16 17
Fig.5.Thespeedupwhen| 7and 7:13. epud sep 5 1 0 pu 6 ed seapn 4 i edm 2 1 0 1 2 3 4 5 6 7 8 10 11 12 13 14 15 16
17
The scalability of parallelizing the processing of conjunctive branches is summarized in Figure 9 by illustrating the speedup trend, which is based on the median speedup values from our 9-thread tests (Figure 2-8), given the observed values.
Besides synthesized test cases, we also tested a real-world ontology, fly anatomy. Figure 10 shows the result for fly anatomy. The maximum speedup value is around the value of , which is in this test case 2:91, and we see that the peak value of the speedup is greater than 2 and that there exists a linear speedup increase before reaching the peak value. This test result shows a stable scalability to some degree.
We amend Equation 3 to a more general form as indicated by Equation 4, in order to illustrate the program’s impacts on real-world ontologies: k
N q k q
N q ; 0 ⁄ q ⁄ k; k P N; 0 ⁄ 8 (4) Here, q is a lower bound of a sample space. Namely, tests with conjunctive branches less than q are bypassed. With Equation 4, we can focus on the tests with greater q value, e.g. q 3. Figure 11 shows the speedups gained by testing some ontologies, with q 4.
Scalability is the most interesting point in this research. Optimistically, we expect to
gain linear or even super-linear scalability.2 In the circumstances of expecting minimal
overheads, we anticipate the ratio, between speed-up and the number of thread, e ¥ 1
in accordance with e ns ; n ⁄ ; n ⁄ p, where s is speedup, n is thread number,
and p is the total number of processors. However, e ⁄ 1 is the most normal case in
practice. According to our tests, e 0:8398 is the greatest value, which occurs when
2 A super-linear speedup is controversial but sometimes observed, and we accept it as the result
of the combined effectiveness of hardware, software, and algorithms [
9 threads 10 11 12 13 14 15 16 17 s 12:5971, n 15, 29:06, and p 16 (see Figure 8). It is obvious that a certain system overhead cannot be avoided and must hinder the program from reaching the normal peak value. Furthermore, most tableau-based satisfiability tests for classification find models, as mentioned above, and parallelizing the processing of conjunctive branches is useful in the case of satisfiable tests. However, negative tests entailing unsatisfiability predominantly exist in classification, too. If a number of clashes can be detected before processing a bundle of conjunctive branches, this parallel algorithm can hardly contribute to a performance gain. 6
In the past, tableau-based DL reasoning techniques have been investigated extensively.
In [24] a tableau algorithm was proposed to reason about ALC. After that, tableau
algorithms have been presented along with the growing expressivity of DL languages
[
Generic tableau algorithms generally run with a low performance, so a number of
optimization techniques have been developed for real-world reasoners. Without some of
these optimization techniques, a tableau-based DL reasoning system remains unusable.
Examples of important optimization techniques are dependency-directed backjumping,
lazy unfolding, axiom absorption, etc [
For the purpose of exploiting multiprocessor computers’ power to deal with
increasingly complex ontologies, researchers have started looking for scalable solutions,
among which concurrent computing plays a role. A variety of concurrency-oriented DL
reasoning research has been presented recently. [
Cheap multiprocessor computing resources are ubiquitous now. How these powerful computers can be used adequately is an important topic in computing areas, and some research, such as graphics processing, has progressed a lot. Unfortunately, DL reasoning just started its journey in this direction, and any full-scale DL/OWL reasoner can only use one single processor at a time no matter how many are available. At the same time, ontologies processed by DL reasoning systems are becoming bigger and more complex because of the fast development of the semantic web technology. A possible solution is the integration of concurrent computing, or more specifically, concurrent reasoning, which should make full use of the availability of multiprocessor computing resources and may improve performance in a scalable way. Our research proved that such scalability is possible.
We have shown that the computing performance of tableau-based DL reasoning can be improved by parallelizing the processing of conjunctive branches of expansion trees. All of the investigations that explore parallelized tableau-based DL reasoning make an effort to exploit simultaneous processing of disjunctive branches in tableau expansion trees. On the other hand, our research is the first one to seriously investigate the parallel processing of conjunctive branches in tableau expansion trees. We addressed the role of conjunctive branches in tableau expansion trees and noticeable points of parallelizing the processing of conjunctive branches. We presented a parallel algorithm that simultaneously calculates conjunctive branches. We discussed the key characteristics of implementing the algorithm. We evaluated the program, and the essential effectiveness of the algorithm was shown by synthesized tests. We analyzed the scalability of the algorithm based on our proposed metric.
In the future, more efficient memory management techniques may be explored. At present, we implemented the algorithm with Java. When processing complex ontologies, which generally need relatively large memory sizes, Java’s memory management, e.g., garbage collection, has a high impact on reasoning performance. Such influence is generally negative and could be avoided by using C++ for implementation. Moreover, thread scheduling used by the present implementation heavily depends on the Java concurrency package. More elaborate designs may improve performance further. 21. Mutharaju, R., Maier, F., Hitzler, P.: A MapReduce algorithm for EL+. In: Proceedings of the 2010 International Workshop on Description Logics. p. 456 (2010) 22. Nagashima, U., Hyugaji, S., Sekiguchi, S., Sato, M., Hosoya, H.: An experience with superlinear speedup achieved by parallel computing on a workstation cluster: Parallel calculation of density of states of large scale cyclic polyacenes. Parallel computing 21(9), 1491–1504 (1995) 23. Quinn, M.J., Deo, N.: An upper bound for the speedup of parallel best-bound branch-andbound algorithms. BIT Numerical Mathematics 26(1), 35–43 (1986) 24. Schmidt-Schauß, M., Smolka, G.: Attributive concept descriptions with complements. Artificial Intelligence 1(48), 1–26 (1991) 25. Wu, K., Haarslev, V.: A parallel reasoner for the description logic ALC. In: Proceedings of the 2012 International Workshop on Description Logics (2012)