A parallel execution model of logic programs

A parallel-execution model that can concurrently exploit AND and OR parallelism in logic programs is presented. This model employs a combination of techniques in an approach to executing logic problems in parallel, making tradeoffs among number of processes, degree of parallelism, and combination bandwidth. For interpreting a nondeterministic logic program, this model (1) performs frame inheritance for newly created goals, (2) creates data-dependency graphs (DDGs) that represent relationships among the goals, and (3) constructs appropriate process structures based on the DDGs. (1) The use of frame inheritance serves to increase modularity. In contrast to most previous parallel models that have a large single process structure, frame inheritance facilitates the dynamic construction of multiple independent process structures, and thus permits further manipulation of each process structure. (2) The dynamic determination of data dependency serves to reduce computational complexity. In comparison to models that exploit brute-force parallelism and models that have fixed execution sequences, this model can reduce the number of unification and/or merging steps substantially. In comparison to models that exploit only AND parallelism, this model can selectively exploit demand-driven computation, according to the binding of the query and optional annotations. (3) The construction of appropriate process structures serves to reduce communication complexity. Unlike other methods that map DDGs directly onto process structures, this model can significantly reduce the number of data sent to a process and/or the number of communication channels connected to a process     

An extended Petri net model for normal logic programs

This paper presents an application of the concepts of siphons (deadlocks) and inhibitor arcs in Petri net theory to logic programs with negations. More specifically, an extended Petri net is used to model function-free normal logic programs. In this model, because of the presence of inhibitor arcs, the arbitrary applications of firing rule may cause a contradictory situation. We suggest two directions to avoid contradictions: greedy and secure applications of firing rule. We choose the secure application and show that this is a direct translation of the well-founded semantics in the net model. Furthermore, we show that the greatest unfounded set corresponds to the greatest siphon in Petri net theory when we delete the transitions disabled by the secure application of firing rule, and that the property of siphon simplifies the computation of well-founded semantics for logic programs. We also propose the reduced-Petri-net method by which we can reduce an extended Petri net to a Petri net without inhibitor arcs and compute the well-founded model by iterative applications of this transformation using conventional application of firing rule     

DIALOG — A dataflow model for parallel execution of logic programs

The paper presents a dataflow execution model, DIALOG, for logic programs which operates on an intermediate virtual machine. The virtual machine is granulated at clause argument level to exploit argument parallelism through unification. The model utilises a new variable binding scheme that eliminates dereference operations for accessing variables, and therefore supports OR-parallelism in the highly distributed dataflow environment. The model has been implemented in Occam. A conventional dataflow architecture in support of the model has been simulated as a testbed for the evaluation. The simulation indicates some encouraging results and suggests future improvements.     

A practical framework for theabstract interpretation of logic programs

There are numerous papers concerned with the compile-time derivation of certain run-time properties of logic programs, e.g. mode inferencing, type checking, type synthesis, and properties relevant for and-parallel execution. Most approaches have little in common, they are developed in an ad hoc way, and their correctness is not always obvious. We develop a general framework which is suited to develop complex applications and to prove their correctness. All states which are possible at run time can be represented by an infinite set of proof trees (and trees, SLD derivations). The core idea of our approach is to represent this infinite set of and trees by a finite abstract and-or graph. We present a generic abstract interpretation procedure for the construction of such an abstract and-or graph and formulate conditions which allow us to construct a correct one in finite time.     

A Petri net model for probabilistic logic

In this article we investigate the use of Petri nets for the representation of possible worlds in probabilistic logic. We propose a method to generate possible worlds based upon the reachability tree of the Petri net model. The number of columns in the matrix of possible worlds grows exponentially with the problem size. Nilsson [Proceedings of 1976 National Computer Conference and Readings in Artificial Intelligence, Morgan Kaufmann, Los Altos, CA, 1981, pp. 192-199] suggested a method to generate only those columns of the possible world matrix that are likely to be important for the solution. We provide Petri net models for the method suggested by Nilsson and show that they lead to intuitive and simple computational methods. © 1996 John Wiley & Sons, Inc.     

A survey of parallel execution strategies for transitive closure and logic programs

An important feature of database technology of the nineties is the use of parallelism for speeding up the execution of complex queries. This technology is being tested in several experimental database architectures and a few commercial systems for conventional select-project-join queries. In particular, hash-based fragmentation is used to distribute data to disks under the control of different processors in order to perform selections and joins in parallel. With the development of new query languages, and in particular with the definition of transitive closure queries and of more general logic programming queries, the new dimension of recursion has been added to query processing. Recursive queries are complex; at the same time, their regular structure is particularly suited for parallel execution, and parallelism may give a high efficiency gain. We survey the approaches to parallel execution of recursive queries that have been presented in the recent literature. We observe that research on parallel execution of recursive queries is separated into two distinct subareas, one focused on the transitive closure of Relational Algebra expressions, the other one focused on optimization of more general Datalog queries. Though the subareas seem radically different because of the approach and formalism used, they have many common features. This is not surprising, because most typical Datalog queries can be solved by means of the transitive closure of simple algebraic expressions. We first analyze the relationship between the transitive closure of expressions in Relational Algebra and Datalog programs. We then review sequential methods for evaluating transitive closure, distinguishing iterative and direct methods. We address the parallelization of these methods, by discussing various forms of parallelization. Data fragmentation plays an important role in obtaining parallel execution; we describe hash-based and semantic fragmentation. Finally, we consider Datalog queries, and present general methods for parallel rule execution; we recognize the similarities between these methods and the methods reviewed previously, when the former are applied to linear Datalog queries. We also provide a quantitative analysis that shows the impact of the initial data distribution on the performance of methods. Recommended by: Patrick Valduriez     

Abstract interpretation of logic programs using magic transformations

In dataflow analysis of logic programs, information must be propagated according to the control strategy of the language under consideration. However, for languages with top-down control flow, naive top-down dataflow analyses may have problems guaranteeing completeness and/or termination. What is required in the dataflow analysis is a bottom-up fixpoint computation, guided by the (possibly top-down) control strategy of the language. This paper describes the application of the magic templates algorithm, originally devised as a technique for efficient bottom-up computation of logic programs, to dataflow analysis of logic programs. It turns out that a direct application of the magic templates algorithm can result in an undesirable loss in precision, because connections between “calling patterns” and the corresponding “success patterns” may be lost. We show how the original magic templates algorithm can be modified to avoid this problem, and prove that the resulting analysis algorithm is at least as precise as any other abstract interpretation that uses the same abstract domain and abstract operations.     

Deriving linear size relations for logic programs by abstract interpretation

We propose an automatic method for derivinglinear size relations, which specify, with respect to some given norm, linear relationships between the sizes of the arguments of atoms in the least Herbrand model of a definite Horn clause program. The method is presented as an application of abstract interpretation. Its abstract domain consists of affine subspaces or linear varieties, and operations on elements of the domain are expressed in terms of operations from linear algebra. The main application of the technique is situated in automatic termination analysis. Others are complexity and granularity analysis and the specialisation of constraints in constraint logic languages.     

Binding environments for parallel logic programs in non-shared memory multiprocessors

A method known asclosed environments can be used to represent variable bindings for OR-parellel logic programs without relying on a shared memory or common address space. The representation is based on a procedure that trans-forms stack frames after unification, taking into account problems with common unbound ancestors and shared instances of complex terms. Closed environments were developed for the AND/OR Process Model, but may be applicable to other OR-parallel models.     

A wide instruction word architecture for parallel execution of logic programs coded in BSL

This paper begins by describing BSL, a new logic programming language fundamentally different from Prolog. BSL is a nondeterministic Algol-class language whose programs have a natural translation to first order logic; executing a BSL program without free variables amounts to proving the corresponding first order sentence. A new approach is proposed for parallel execution of logic programs coded in BSL, that relies on advanced compilation techniques for extracting fine grain parallelism from sequential code. We describe a new “Very Long Instruction Word” (VLIW) architecture for parallel execution of BSL programs. The architecture, now being designed at the IBM Thomas J. Watson Research Center, avoids the synchronization and communication delays (normally associated with parallel execution of logic programs on multiprocessors), by determining data dependences between operations at compile time, and by coupling the processing elements very tightly, via a single central shared register file. A simulator for the architecture has been implemented and some simulation results are reported in the paper, which are encouraging.     

An abstract interpretation scheme for identifying inherent parallelism in logic programs

We describe a new scheme for the abstract interpretation of logic programs. The scheme was developed to identify and integrate different forms of inherent parallelism in logic programs at compile time. The scheme has four components: generalization, abstract unification, summarization and concretization, algorithms for which are discussed. The abstract domain for interpretation consists of type expressions which are used as program modes. The generated mode information has been applied to identify different classes of procedures exhibiting different forms of inherent parallelism. The mode information has also been applied for detection of guards and producer-consumer relationship. The advantages and limitations of our resulting scheme are discussed.     

Continuation-based control in the implementation of parallel logic programs

Continuations are used to define the flow of messages between low level tasks in a parallel logic programming language. A combination of compiler and runtime operations reduces message traffic by up to 50% when success continuations are passed as parameters in messages that start new processes. Continuations are also the key to fast task switching, a critical operation in this fine grain parallel system. Data from sample programs shows the effectiveness of continuations in reducing message traffic and the speed with which task switches are performed on a typical host architecture.Supported by NSF Grant CCR-8707177 and grants from Motorola, Inc, and Hewlett-Packard Corp.     

A type system for logic programs

A theory for a type system for logic programs is developed which addressesthe question of well-typing, type inference, and compile-time and run-time type checking. A type is a recursively enumerable set of ground atoms, which is tuple-distributive. The association of a type to a program is intended to mean that only ground atoms that are elements of the type may be derived from the program. A declarative definition of well-typed programs is formulated, based on an intuitive approach related to the fixpoint semantics of logic programs. Whether a program is well typed is undecidable in general. We define a restricted class of types, called regular types, for which type checking is decidable. Regular unary logic programs are proposed as a specification language for regular types. An algorithm for type-checking a logic program with respect to a regular type definition is described, and its complexity is analyzed. Finally, the practicality of the type system is discussed, and some examples are shown. The type system has been implemented in FCP for FCP and is incorporated in the Logix system.     

An execution model for exploiting AND-parallelism in logic programs

This paper presents a parallel execution model for exploiting AND-parallelism in Horn Clause logic programs. The model is based upon the generator-consumer approach, and can be implemented efficiently with small run-time overhead. Other related models that have been proposed to minimize the run-time overhead are unable to exploit the full parallelism inherent in the generator-consumer approach. Furthermore, our model performs backtracking more intelligently than these models. We also present two implementation schemes to realize our model: one has a coordinator to control the activities of processes solving different literals in the same clause; and the other achieves synchronization by letting processes pass messages to each other in a distributed fashion. Trade-offs between these two schemes are then discussed. This work was supported by Army Research Office grant #DAAG29-84-K-0060 to the Artificial Intelligence Laboratory at the University of Texas at Austin.     

A vertex centric parallel algorithm for linear temporal logic model checking in Pregel

Linear Temporal Logic (LTL) Model Checking is a very important and popular technique for the automatic verification of safety-critical hardware and software systems, aiming at ensuring their quality. However, it is well known that LTL model checking suffers from the state explosion problem, often leading to insurmountable scalability problems when applying it to real-world systems. While there has been work on distributed algorithms for explicit on-the-fly LTL model checking, these are not sufficiently scalable and capable of tolerating faults during computation, significantly limiting their usefulness in huge cluster environments. Moreover, implementing these algorithms is generally viewed as a very challenging, error-prone task. In this paper, we instead rely on Pregel, a simple yet powerful model for distributed computation on large graphs. Pregel has from the start been designed for efficient, scalable and fault tolerant operation on clusters of thousands of computers, including large cloud setups. To harness Pregel’s power, we propose a new vertex centric distributed algorithm for explicit LTL model checking of concurrent systems. Experimental results illustrate feasibility and scalability of the proposed algorithm. Compared with other distributed algorithms, our algorithm is more scalable, reliable and efficient.     

A characterization of answer sets for logic programs

Checking if a program has an answer set, and if so, compute its answer sets are just some of the important problems in answer set logic programming. Solving these problems using Gelfond and Lifschitz's original definition of answer sets is not an easy task. Alternative characterizations of answer sets for nested logic pro- grams by Erdem and Lifschitz, Lee and Lifschitz, and You et al. are based on the completion semantics and various notions of tightness. However, the notion of tightness is a local notion in the sense that for different answer sets there are, in general, different level mappings capturing their tightness. This makes it hard to be used in the design of algorithms for computing answer sets. This paper proposes a characterization of answer sets based on sets of generating rules. From this char- acterization new algorithms are derived for computing answer sets and for per- forming some other reasoning tasks. As an application of the characterization a sufficient and necessary condition for the equivalence between answer set seman- tics and completion semantics has been proven, and a basic theorem is shown on computing answer sets for nested logic programs based on an extended notion of loop formulas. These results on tightness and loop formulas are more general than that in You and Lin's work.     

High-level Petri net model of logic program with negation

The formalism of nonmonotonic reasoning has been integrated into logic programming to define semantics for logic program with negation. Because a Petri net provides a uniform model for both the logic of knowledge and the control of inference, the class of high-level Petri nets called predicate/transition nets (PrT-nets) has been employed to study production rule based expert systems and Horn clause logic programs. We show that a PrT-net can implement the nonmonotonicity associated with a logic program with negation as well as the monotonicity of Horn clause logic program. In particular, we define a semantics for a normal logic program and implement it with PrT-net. We demonstrate that in the presence of inconsistency in a normal logic program, the semantics still works well by deducing meaningful answers. The variations and potential applications of the PrT-net are also addressed