On semantic resolution with lemmaizing and contraction and a formal treatment of caching

Reducing redundancy in search has been a major concern for automated deduction. Subgoal-reduction strategies, such as those based on model elimination and implemented in Prolog technology theorem provers, prevent redundant search by usinglemmaizing andcaching, whereas contraction-based strategies prevent redundant search by usingcontraction rules, such assubsumption. In this work we show that lemmaizing and contraction can coexist in the framework ofsemantic resolution. On the lemmaizing side, we define two meta-level inference rules for lemmaizing in semantic resolution, one producing unit lemmas and one producing non-unit lemmas, and we prove their soundness. Rules for lemmaizing are meta-rules because they use global knowledge about the derivation, e.g. ancestry relations, in order to derive lemmas. Our meta-rules for lemmaizing generalize to semantic resolution the rules for lemmaizing in model elimination. On the contraction side, we give contraction rules for semantic strategies, and we define apurity deletion rule for first-order clauses that preserves completeness. While lemmaizing generalizes success caching of model elimination, purity deletion echoes failure caching. Thus, our approach integrates features of backward and forward reasoning. We also discuss the relevance of our work to logic programming. Supported in part by the National Science Foundation with grant CCR-94-08667 and CCR-97-01508. Supported in part by grant NSC 86-2213-E-002-047 and NSC 87-2213-E-002-029 of the National Science Council of the Republic of China. Maria Paola Bonacina, Ph.D.: She is on the faculty of the Department of Computer Science of the University of Iowa. She received a laurea (1986) and a doctorate in informatics from the Universita degli Studi di Milano, and a Ph.D. in computer science from the State University of New York at Stony Brook (1992). She was awarded fellowships by the Universita degli Studi di Milano, the European Union and the General Electric Foundation. The unifying theme of her research is automated theorem proving. Her research areas include distributed automated deduction, the theory of search and strategy analysis, completion-based theorem proving, category theory for computer science, term rewriting systems, logic programming, and manyvalued logic. Jieh Hsiang, Ph.D.: He is a Professor of Computer Science at the National Taiwan University and is also the Director of the Center of Excellence for Research in Computer Systems of the National Taiwan University. Professor Hsiang is known for work in term rewriting systems and automated deduction. His other research interests include logic programming, programming logics, computer viruses, and intelligent agents. Recently he has also become interested in the digitization of Taiwanese and Chinese historical records and heritage. Professor Hsiang received a B.S. degree in mathematics from National Taiwan University in 1976 and a Ph.D. degree in computer science from the University of Illinois at Urbana-Champaign in 1982. Before returning to Taiwan in 1993, he was a Professor of Computer Science at the State University of New York st Stony Brook.     

On the Modelling of Search in Theorem Proving- Towards a Theory of Strategy Analysis

We present a model for representing search in theorem proving. This model captures the notion ofcontraction, which has been central in some of the recent developments in theorem proving. We outline an approach to measuring the complexity of search which can be applied to analyze and evaluate the behaviour of theorem-proving strategies. Using our framework, we compare contraction-based strategies of different contraction power and show how they affect the evolution of the respective search spaces during the derivation.     

A model and a first analysis of distributed‐search contraction‐based strategies

While various approaches to parallel theorem proving have been proposed, their usefulness is evaluated only empirically. This research is a contribution towards the goal of machine‐independent analysis of theorem‐proving strategies. This paper considers clausal contraction‐based strategies and their parallelization by distributed search, with subdivision of the search space and propagation of clauses by message‐passing (e.g., à la Clause‐Diffusion). A model for the representation of the parallel searches produced by such strategies is presented, and the bounded‐search‐spaces approach to the measurement of search complexity in infinite search spaces is extended to distributed search. This involves capturing both its advantages, e.g., the subdivision of work, and disadvantages, e.g., the cost of communication, in terms of search space. These tools are applied to compare the evolution of the search space of a contraction‐based strategy with that of its parallelization in the above sense. This revised version was published online in June 2006 with corrections to the Cover Date.     

Towards a unified model of search in theorem-proving: subgoal-reduction strategies

This paper advances the design of a unified model for the representation of search in first-order clausal theorem-proving, by extending to tableau-based subgoal-reduction strategies (e.g., model-elimination tableaux), the marked search-graph model, already introduced for ordering-based strategies, those that use (ordered) resolution, paramodulation/superposition, simplification, and subsumption. The resulting analytic marked search-graphs subsume AND–OR graphs, and allow us to represent those dynamic components, such as backtracking and instantiation of rigid variables, that have long been an obstacle to modelling subgoal-reduction strategies properly. The second part of the paper develops for analytic marked search-graphs the bounded search spaces approach to the analysis of infinite search spaces. We analyze how tableau inferences and backtracking affect the bounded search spaces during a derivation. Then, we apply this analysis to measure the effects of regularity and lemmatization by folding-up on search complexity, by comparing the bounded search spaces of strategies with and without these features. We conclude with a discussion comparing the marked search-graphs for tableaux, linear resolution, and ordering-based strategies, showing how this search model applies across these classes of strategies.     

Evaluation of parallelization strategies for an incremental Delaunay triangulator in e3

The paper deals with the parallelization of Delaunay triangulation, a widely used space partitioning technique. Two parallel implementations of a three-dimensional incremental construction algorithm are presented. The first is based on the decomposition of the spatial domain, while the second relies on the master-slaves approach. Both parallelization strategies are evaluated, stressing practical issues rather than theoretical complexity. We report on the exploitation of two different parallel environments: a tightly coupled distributed memory MIMD architecture and a network of workstations co-operating under the Linda environment Then, a third hybrid solution is proposed, specifically addressed to the exploitation of higher parallelism. It combines the other two solutions by grouping the processing nodes of the multicomputer into clusters and by exploiting parallelism at two different levels.     

Employing nested OpenMP for the parallelization of multi-zone computational fluid dynamics applications

In this paper we describe the parallelization of the multi-zone code versions of the NAS Parallel Benchmarks employing multi-level OpenMP parallelism. For our study, we use the NanosCompiler that supports nesting of OpenMP directives and provides clauses to control the grouping of threads, load balancing, and synchronization. We report the benchmark results, compare the timings with those of different hybrid parallelization paradigms (MPI+OpenMP and MLP) and discuss OpenMP implementation issues that affect the performance of multi-level parallel applications.     

Performance characteristics of the multi-zone NAS parallel benchmarks

We describe a new suite of computational benchmarks that models applications featuring multiple levels of parallelism. Such parallelism is often available in realistic flow computations on systems of meshes, but had not previously been captured in benchmarks. The new suite, named NPB (NAS parallel benchmarks) multi-zone, is derived from the NPB suite, and involves solving the application benchmarks LU, BT and SP on collections of loosely coupled discretization meshes. The solutions on the meshes are updated independently, but after each time step they exchange boundary value information. This strategy provides relatively easily exploitable coarse-grain parallelism between meshes. Three reference implementations are available: one serial, one hybrid using the message passing interface (MPI) and OpenMP, and another hybrid using a shared memory multi-level programming model (SMP+OpenMP). We examine the effectiveness of hybrid parallelization paradigms in these implementations on four different parallel computers. We also use an empirical formula to investigate the performance characteristics of the hybrid parallel codes.     

A taxonomy of parallel strategies for deduction

This paper presents a taxonomy of parallel theorem-proving methods based on the control of search (e.g., master–slaves versus peer processes), the granularity of parallelism (e.g., fine, medium and coarse grain) and the nature of the method (e.g., ordering-based versus subgoal-reduction). We analyze how the different approaches to parallelization affect the control of search: while fine and medium–grain methods, as well as master-slaves methods, generally do not modify the sequential search plan, parallel-search methods may combine sequential search plans (multi-search) or extend the search plan with the capability of subdividing the search space (distributed search). Precisely because the search plan is modified, the latter methods may produce radically different searches than their sequential base, as exemplified by the first distributed proof of the Robbins theorem generated by the Modified Clause-Diffusion prover Peers-mcd. An overview of the state of the field and directions for future research conclude the paper. This revised version was published online in June 2006 with corrections to the Cover Date.     

A fast poisson solver for distributed memory multiprocessors

We present a parallel algorithm for distributed memory multiprocessors, which is based on generalized marching (GM), one of the fastest methods in the class of fast Poisson solvers. The GM algorithm is not suited for any but very coarse-grain parallel processing. The main difficulty with parallelization is that the number of independent processes and the amount of work in each process change exponentially and in inverse proportion of each other. To improve parallelism, the matrices involved in GM are diagonalized performing multiple FFTs. In this way, independent processes extending across all the algorithm are obtained. The parallel GM has been tested on an Ncube/10 and a Symult S2010, running the Express communication system. A performance evaluation has been carried out using a scaled efficiency model and some classical parameters.     

Integrating Parallelization Strategies for Linkage Analysis

We describe a second parallel implementation of the ILINK program from the LINKAGE package that improves on our previous implementation. To improve running time we integrated the strategy of parallel estimation of the gradient at a candidate recombination fraction vector with a previously implemented strategy for evaluating in parallel the likelihood at one vector. We also integrated an adaptive loadbalancing strategy in conjunction with our previous static loadbalancing strategy. We implemented a strategy for partitioning input pedigrees, but this slowed down the program; we give some evidence for what the problems are. To best exploit parallelism at all levels of the program and to take advantage of both coarse-grain and fine-grain parallelism it is necessary to combine multiple algorithmic strategies.     

On logic programs that do not fail

This paper investigates the advantages of reasoning on logic programs and queries that have only successful derivations. We consider an extension of the logic programming paradigm that combines guarded clauses and delay declarations. The main contribution of this paper consists of some general conditions for a class of programs and queries which imply that successful derivations only are present. A few practical instances of the method are studied, and their applicability demonstrated. The general conditions are derived extending proof methods originally developed for Prolog's programs. From the point of view of parallelism, the method is able to reason about termination (with success) of pipeline parallel executions of programs. In particular, we show some examples of parallelization of terminating Prolog programs. Moreover, from the point of view of nondeterminism, don't care nondeterminism can be safely adopted for the class of programs that have only successfull derivations.     

Efficient support for fine-grain parallelism on shared-memory machines

A coarse-grain parallel program typically has one thread (task) per processor, whereas a fine-grain program has one thread for each independent unit of work. Although there are several advantages to fine-grain parallelism, conventional wisdom is that coarse-grain parallelism is more efficient. This paper illustrates the advantages of fine-grain parallelism and presents an efficient implementation for shared-memory machines. The approach has been implemented in a portable software package called Filaments, which employs a unique combination of techniques to achieve efficiency. The performance of the fine-grain programs discussed in this paper is always within 13% of a hand-coded coarse-grain program and is usually within 5%. © 1998 John Wiley & Sons, Ltd.     

Automatic compile-time parallelization of logic programs for restricted,goal level,independent and parallelism

A framework for the automatic parallelization of (constraint) logic programs is proposed and proved correct. Intuitively, the parallelization process replaces conjunctions of literals with parallel expressions. Such expressions trigger at run-time the exploitation of restricted, goal-level, independent and parallelism. The parallelization process performs two steps. The first one builds a conditional dependency graph (which can be simplified using compile-time analysis information), while the second transforms the resulting graph into linear conditional expressions, the parallel expressions of the &-Prolog language. Several heuristic algorithms for the latter (“annotation”) process are proposed and proved correct. Algorithms are also given which determine if there is any loss of parallelism in the linearization process with respect to a proposed notion of maximal parallelism. Finally, a system is presented which implements the proposed approach. The performance of the different annotation algorithms is compared experimentally in this system by studying the time spent in parallelization and the effectiveness of the results in terms of speedups.     

OpenGR: A directive-based grid programming environment

A new grid programming environment for remote procedure call (RPC) based master–worker type task parallelization is presented. The environment is realized through the use of a set of compiler directives, called OpenGR, and is implemented in the present study based on the Omni OpenMP compiler system and Ninf-G grid-enabled RPC system as a parallel execution mechanism. Using OpenGR directives, existing sequential applications can be readily adapted to the grid environment as master–worker parallel programs using the RPC architecture. The combination of OpenGR and OpenMP directives also allows for the hybrid parallelization of sequential programs, supporting both synchronous and asynchronous parallelism.     

A parallel algorithm with enhancements via partial objective value cuts for cluster-based wireless sensor network design

In this paper, we develop a parallel algorithm for the solution of an integrated topology control and routing problem in Wireless Sensor Networks (WSNs). After presenting a mixed-integer linear optimization formulation for the problem, for its solution, we develop an effective parallel algorithm in a Master–Worker model that incorporates three parallelization strategies, namely low-level parallelism, domain decomposition, and multiple search (both cooperative and independent) in a single Master–Worker framework.     

Benchmark evaluation of the IBM SP2 for parallel signal processing

This paper evaluates the IBM SP2 architecture, the AIX parallel programming environment, and the IBM message-passing library (MPL) through STAP (Space-Time Adaptive Processing) benchmark experiments. Only coarse-grain parallelism was exploited on the SP2 due to its high communication overhead. A new parallelization scheme is developed for programming message passing multicomputers. Parallel STAP benchmark structures are illustrated with domain decomposition, efficient mapping of partitioned programs, and optimization of collective communication operations. We measure the SP2 performance in terms of execution time, Gflop/s rate, speedup over a single SP2 node, and overall system utilization. With 256 nodes, the Maul SP2 demonstrated the best performance of 23 Gflop/s in executing the High-Order Post-Doppler program, corresponding to a 34% system utilization. We have conducted a scalability analysis to reveal the performance growth rate as a function of machine size and STAP problem size. Important lessons learned from these parallel processing benchmark experiments are discussed in the context of real-time, adaptive, radar signal processing on massively parallel processors (MPP)     

EIGENVECTORS-BASED PARALLELISATION OF NESTED LOOPS WITH AFFINE DEPENDENCES

Abstract

This paper presents a method for parallelising nested loops with affine dependences. The data dependences of a program are represented exactly using a dependence matrix rather than an imprecise dependence abstraction. By a careful analysis of the eigenvectors and eigenvalues of the dependence matrix, we detect the parallelism inherent in the program, partition the iteration space of the program into sequential and parallel regions, and generate parallel code to execute these regions. For a class of programs considered in the paper, the proposed method can expose more coarse-grain and fine-grain parallelism than a hyperplane-based loop transformation.     

ParC—An Extension of C for Shared Memory Parallel Processing

ParC is an extension of the C programming language with block-oriented parallel constructs that allow the programmer to express fine-grain parallelism in a shared-memory model. It is suitable for the expression of parallel shared-memory algorithms, and also conducive for the parallelization of sequential C programs. In addition, performance enhancing transformations can be applied within the language, without resorting to low-level programming. The language includes closed constructs to create parallelism, as well as instructions to cause the termination of parallel activities and to enforce synchronization. The parallel constructs are used to define the scope of shared variables, and also to delimit the sets of activities that are influenced by termination or synchronization instructions. The semantics of parallelism are discussed, especially relating to the discrepancy between the limited number of physical processors and the potentially much larger number of parallel activities in a program.