Making constraint solvers more usable: overconstraint problem

The richness and expressive power of geometric constraints causes unintended ambiguities and inconsistencies during their solution or realization. For example, geometric constraint problems may turn out to be overconstrained requiring the user to delete one or more of the input constraints, and the solutions must then be dynamically updated. Without proper guidance by the constraint solver, the user must have profound insight into the mathematical nature of constraint systems and understand the internals of the solver algorithm. But a general user is most likely unfamiliar with those problems, so that the required interaction with the constraint solver may well be beyond the user's ability. In this paper, we present strategies and techniques to empower the user to deal effectively with the overconstraint problem while not requiring him or her to become an expert in the mathematics of constraint solving.We formulate this problem as a series of formal requirements that gel with other essentials of constraint solvers. We then give algorithmic solutions that are both general and efficient (running time typically linear in the number of relevant constraints).     

Simple linear string constraints

Modern web applications often suffer from command injection attacks. Even when equipped with sanitization code, many systems can be penetrated due to software bugs. It is desirable to automatically discover such vulnerabilities, given the bytecode of a web application. One approach would be symbolically executing the target system and constructing constraints for matching path conditions and attack patterns. Solving these constraints yields an attack signature, based on which, the attack process can be replayed. Constraint solving is the key to symbolic execution. For web applications, string constraints receive most of the attention because web applications are essentially text processing programs. We present simple linear string equation (SISE), a decidable fragment of the general string constraint system. SISE models a collection of regular replacement operations (such as the greedy, reluctant, declarative, and finite replacement), which are frequently used by text processing programs. Various automata techniques are proposed for simulating procedural semantics such as left-most matching. By composing atomic transducers of a SISE, we show that a recursive algorithm can be used to compute the solution pool, which contains the value range of each variable in concrete solutions. Then a concrete variable solution can be synthesized from a solution pool. To accelerate solver performance, a symbolic representation of finite state transducer is developed. This allows the constraint solver to support a 16-bit Unicode alphabet in practice. The algorithm is implemented in a Java constraint solver called SUSHI. We compare the applicability and performance of SUSHI with Kaluza, a bounded string solver.     

On-Line Symbolic Constraint Embedding for Simulation of Hybrid Dynamical Systems

In this paper we present a simulator designed to handle multibody systems with changing constraints, wherein the equations of motion for each of its constraint configurations are formulated in minimal ODE form with constraints embedded before they are passed to an ODE solver. The constraint-embedded equations are formulated symbolically according to a re-combination of terms of the unconstrained equations, and this symbolic process is undertaken on-line by the simulator. Constraint-embedding undertaken on-the-fly enables the simulation of systems with an ODE solver for which constraints are not known prior to simulation start or for which the enumeration of all constraint conditions would be unwieldy because of their complexity or number. Issues of drift associated with DAE solvers that usually require stabilization are sidestepped with the constraint-embedding approach. We apply nomenclature developed for hybrid dynamical systems to describe the system with changing constraints and to distinguish the roles of the forward dynamics solver, a collision detector, and an impact resolver. We have prototyped the simulator in MATLAB and demonstrate the design using three representative examples.     

Solving piecewise polynomial constraint systems with decomposition and a subdivision-based solver

Piecewise polynomial constraint systems are common in numerous problems in computational geometry, such as constraint programming, modeling, and kinematics. We propose a framework that is capable of decomposing, and efficiently solving a wide variety of complex piecewise polynomial constraint systems, that include both zero constraints and inequality constraints, with zero-dimensional or univariate solution spaces. Our framework combines a subdivision-based polynomial solver with a decomposition algorithm in order to handle large and complex systems. We demonstrate the capabilities of our framework on several types of problems and show its performance improvement over a state-of-the-art solver.     

Acquiring Both Constraint and Solution Preferences in Interactive Constraint Systems

Constraints are useful to model many real-life problems. Soft constraints are even more useful, since they allow for the use of preferences, which are very convenient in many real-life problems. In fact, most problems cannot be precisely defined by using hard constraints only.However, soft constraint solvers usually can only take as input preferences over constraints, or variables, or tuples of domain values. On the other hand, it is sometimes easier for a user to state preferences over entire solutions of the problem.In this paper, we define an interactive framework where it is possible to state preferences both over constraints and over solutions, and we propose a way to build a system with such features by pairing a soft constraint solver and a learning module, which learns preferences over constraints from preferences over solutions. We also describe a working system which fits our framework, and uses a fuzzy constraint solver and a suitable learning module to search a catalog for the best products that match the user's requirements.     

Enforcement of entailment constraints in distributed service-based business processes

ContextA distributed business process is executed in a distributed computing environment. The service-oriented architecture (SOA) paradigm is a popular option for the integration of software services and execution of distributed business processes. Entailment constraints, such as mutual exclusion and binding constraints, are important means to control process execution. Mutually exclusive tasks result from the division of powerful rights and responsibilities to prevent fraud and abuse. In contrast, binding constraints define that a subject who performed one task must also perform the corresponding bound task(s).ObjectiveWe aim to provide a model-driven approach for the specification and enforcement of task-based entailment constraints in distributed service-based business processes.MethodBased on a generic metamodel, we define a domain-specific language (DSL) that maps the different modeling-level artifacts to the implementation-level. The DSL integrates elements from role-based access control (RBAC) with the tasks that are performed in a business process. Process definitions are annotated using the DSL, and our software platform uses automated model transformations to produce executable WS-BPEL specifications which enforce the entailment constraints. We evaluate the impact of constraint enforcement on runtime performance for five selected service-based processes from existing literature.ResultsOur evaluation demonstrates that the approach correctly enforces task-based entailment constraints at runtime. The performance experiments illustrate that the runtime enforcement operates with an overhead that scales well up to the order of several ten thousand logged invocations. Using our DSL annotations, the user-defined process definition remains declarative and clean of security enforcement code.ConclusionOur approach decouples the concerns of (non-technical) domain experts from technical details of entailment constraint enforcement. The developed framework integrates seamlessly with WS-BPEL and the Web services technology stack. Our prototype implementation shows the feasibility of the approach, and the evaluation points to future work and further performance optimizations.     

Automatic Implication Checking for CHR Constraints

Constraint Handling Rules (CHRs) are a high-level rule-based programming language commonly used to define constraint solvers. We present a method for automatic implication checking between constraints of CHR solvers. Supporting implication is important for implementing extensible solvers and reification, and for building hierarchical CHR constraint solvers. Our method does not copy the entire constraint store, but performs the check in place using a trailing mechanism. The necessary code enhancements can be done by automatic program transformation based on the rules of the solver. We extend our method to work for hierarchically organized modular CHR solvers. We show the soundness of our method and its completeness for a restricted class of canonical solver as well as for specific existing non-canonical CHR solvers. We evaluate our trailing method experimentally by comparing with the copy approach: runtime is almost halved.     

A Relational Positioning Methodology for Robot Task Specification and Execution

This paper presents a relational positioning methodology that allows to restrict totally or partially the movements of an object by specifying its allowed positions in terms of a set of intuitive geometric constraints. In order to derive these positions, a geometric constraint solver must be used. To this end, positioning mobile with respect to fixed (PMF), a geometric constraint solver for the relational positioning of rigid objects in free space is introduced. The solver exploits the fact that, in a set of geometric constraints, the rotational component can often be separated from the translational one and solved independently. PMF may be used as an interface for specifying offline-programmed robot tasks, as well as for assisting the execution of teleoperated tasks requiring constrained movements. Examples describing both the solver's operation and typical applications are discussed.     

Algorithmic Power from Declarative Use of Redundant Constraints

Interval constraints can be used to solve problems in numerical analysis. In this paper we show that one can improve the performance of such an interval constraint program by the declarative use of constraints that are redundant in the sense of not needed to define the problem. The first example shows that computation of an unstable recurrence relation can be improved. The second example concerns a solver of nonlinear equations. It shows that, by adding as redundant constraints instances of Taylor's theorem, one can obtain convergence that appears to be quadratic.     

An integrated runtime and compile-time approach for parallelizingstructured and block structured applications

In compiling applications for distributed memory machines, runtime analysis is required when data to be communicated cannot be determined at compile-time. One such class of applications requiring runtime analysis is block structured codes. These codes employ multiple structured meshes, which may be nested (for multigrid codes) and/or irregularly coupled (called multiblock or irregularly coupled regular mesh problems). In this paper, we present runtime and compile-time analysis for compiling such applications on distributed memory parallel machines in an efficient and machine-independent fashion. We have designed and implemented a runtime library which supports the runtime analysis required. The library is currently implemented on several different systems. We have also developed compiler analysis for determining data access patterns at compile time and inserting calls to the appropriate runtime routines. Our methods can be used by compilers for HPF-like parallel programming languages in compiling codes in which data distribution, loop bounds and/or strides are unknown at compile-time. To demonstrate the efficacy of our approach, we have implemented our compiler analysis in the Fortran 90D/HPF compiler developed at Syracuse University. We have experimented with a multi-bloc Navier-Stokes solver template and a multigrid code. Our experimental results show that our primitives have low runtime communication overheads and the compiler parallelized codes perform within 20% of the codes parallelized by manually inserting calls to the runtime library     

对象族拓扑约束求解的研究

针对当前对象族模型在求解拓扑约束时存在的缺陷,提出一种求解拓扑约束的新方法,这种方法在求解拓扑约束时,把拓扑约束映射为布尔约束满足问题,通过用SAT求解器求解布尔约束来求解拓扑约束。实践证明,该方法不仅直接关联与拓扑约束指定的特征的语义,而且当模型中存在大量相交的特征时也是可行的,提高了拓扑约束求解的效率。     

Dynamic Dispatching of Cyclic Real-Time Tasks with Relative Timing Constraints

In some hard real-time systems, relative timing constraints may be imposed on task executions, in addition to the release time and deadline constraints. Relative timing constraints such as separation or relative deadline constraints may be given between start or finish times of tasks (Gerber et al., 1995; Han and Lin, 1989; Han et al., 1992; Han and Lin, 1992; Han et al., 1996).One approach in real-time scheduling is to find a total order on a set of N tasks in a scheduling window, and cyclically use this order at run time to execute tasks. However, in the presence of relative timing constraints, if the task execution times are nondeterministic with defined lower and upper bounds, it is not always possible to statically assign task start times at pre-runtime for a given task ordering (Gerber et al., 1995).We develop a technique called dynamic cyclic dispatching as an extension of a parametric dispatching mechanism in (Gerber et al., 1995). An ordered set of N tasks is assumed to be given in a scheduling window and this schedule(ordering) is cyclically repeated at runtime in consecutive scheduling windows. Relative timing constraints between tasks may be defined across scheduling window boundaries as well as within one scheduling window. A task set is defined to be dispatchable if there exists any way in which the tasks can be dispatched with all their timing constraints satisfied. An off-line algorithm is presented to check the dispatchability of a task set and to obtain parametric lower and upper bound functions for task start times if the task set is dispatchable. These parametric bound functions are evaluated at runtime to obtain a valid time interval during which a task can be started. The complexity of this off-line component is shown to be O(n ² N ³) where n is the number of tasks in a scheduling window that have relative timing constraints with tasks in the next scheduling window. An online algorithm can evaluate these bounds in O(N) time.Unlike static approaches which assign fixed start times to tasks in the scheduling window, our approach allows us to flexibly manage the slack times at runtime without sacrificing the dispatchability of tasks. Also, a wider class of relative timing constraints can be imposed to the task set compared to the traditional approaches.     

Tackling Complexity in High Performance Computing Applications

We present a software framework that supports the specification of user-definable configuration options in HPC applications independently of the application code itself. Such options include model parameter values, the selection of numerical algorithm, target platform etc. and additional constraints that prevent invalid combinations of options from being made. Such constraints, which are capable of describing complex cross-domain dependencies, are often crucial to the correct functioning of the application and are typically either completely absent from the code or a hard to recover from it. The framework uses a combination of functional workflows and constraint solvers. Application workflows are built from a combination of functional components: higher-order co-ordination forms and first-order data processing components which can be either concrete or abstract, i.e. without a specified implementation at the outset. A repository provides alternative implementations for these abstract components. A constraint solver, written in Prolog, guides a user in making valid choices of parameters, implementations, machines etc. for any given context. Partial designs can be stored and shared providing a systematic means of handling application use and maintenance. We describe our methodology and illustrate its application in two classes of application: a data intensive commercial video transcoding example and a numerically intensive incompressible Navier–Stokes solver.     

Lessons learned from programmers' experiences with one‐way constraints

One‐way constraints have been incorporated in many graphical user interface toolkits because they are simple to learn, easy to write, and can express many types of useful graphical relationships. This paper is an evaluative paper that examines users' experience with one‐way constraints in two user interface development toolkits, Garnet and Amulet, over a 15‐year time span. The lessons gained from this examination can help guide the design of future constraint systems. The most important lessons are that (1) constraints should be allowed to contain arbitrary code that is written in the underlying toolkit language and does not require any annotations, such as parameter declarations, (2) constraints are difficult to debug and better debugging tools are needed, and (3) programmers will readily use one‐way constraints to specify the graphical layout of an application, but must be carefully and time‐consumingly trained to use them for other purposes. Copyright © 2005 John Wiley & Sons, Ltd.     

Usability levels for sparse linear algebra components

Sparse matrix computations are ubiquitous in high‐performance computing applications and often are their most computationally intensive part. In particular, efficient solution of large‐scale linear systems may drastically improve the overall application performance. Thus, the choice and implementation of the linear system solver are of paramount importance. It is difficult, however, to navigate through a multitude of available solver packages and to tune their performance to the problem at hand, mainly because of the plethora of interfaces, each requiring application adaptations to match the specifics of solver packages. For example, different ways of setting parameters and a variety of sparse matrix formats hinder smooth interactions of sparse matrix computations with user applications. In this paper, interfaces designed for components that encapsulate sparse matrix computations are discussed in the light of their matching with application usability requirements. Consequently, we distinguish three levels of interfaces, high, medium, and low, corresponding to the degree of user involvement in the linear system solution process and in sparse matrix manipulations. We demonstrate when each interface design choice is applicable and how it may be used to further users' scientific goals. Component computational overheads caused by various design choices are also examined, ranging from low level, for matrix manipulation components, to high level, in which a single component contains the entire linear system solver. Published in 2007 by John Wiley & Sons, Ltd.     

Ultraviolet: A Constraint Satisfaction Algorithm for Interactive Graphics

Ultraviolet is a constraint satisfaction algorithm intended for use in interactive graphical applications. It is capable of solving constraints over arbitrary domains using local propagation, and inequality constraints and simultaneous linear equations over the reals. To support this, Ultraviolet is a hybrid algorithm that allows different subsolvers to be used for different parts of the constraint graph, depending on graph topology and kind of constraints. In addition, Ultraviolet and its subsolvers support plan compilation, producing efficient compiled code that can be evaluated repeatedly to resatisfy a given collection of constraints for different input values.     

An efficient distributed randomized algorithm for solving large dense symmetric indefinite linear systems

Randomized algorithms are gaining ground in high-performance computing applications as they have the potential to outperform deterministic methods, while still providing accurate results. We propose a randomized solver for distributed multicore architectures to efficiently solve large dense symmetric indefinite linear systems that are encountered, for instance, in parameter estimation problems or electromagnetism simulations. The contribution of this paper is to propose efficient kernels for applying random butterfly transformations and a new distributed implementation combined with a runtime (PaRSEC) that automatically adjusts data structures, data mappings, and the scheduling as systems scale up. Both the parallel distributed solver and the supporting runtime environment are innovative. To our knowledge, the randomization approach associated with this solver has never been used in public domain software for symmetric indefinite systems. The underlying runtime framework allows seamless data mapping and task scheduling, mapping its capabilities to the underlying hardware features of heterogeneous distributed architectures. The performance of our software is similar to that obtained for symmetric positive definite systems, but requires only half the execution time and half the amount of data storage of a general dense solver.     

Timing constraint specification and analysis

Real‐time programmers have to deal with the problem of relating timing constraints associated with source code to sequences of machine instructions. This paper describes an environment to assist users in the specification and analysis of timing constraints. A timing analyzer predicts the best and worst case bounds for these constrained portions of code. A user interface for this timing analyzer was developed to depict whether these constraints were violated or met. A user is allowed to specify timing constraints within the source code of a C program. The user interface also provides three different methods for interactively selecting portions of programs. After each selection the corresponding bounded times, source code lines, and machine instructions are automatically displayed. Users are prevented from only selecting portions of the program for which timing bounds cannot be obtained. In addition, a technique is presented that allows the timing analysis to scale efficiently with complex functions and loops. The result is a user‐friendly environment that supports the user specification and analysis of timing constraints at a high (source code) level and retains the accuracy of low (machine code) level analysis. Copyright © 1999 John Wiley & Sons, Ltd.     

Design and initial performance of a high-level unstructured mesh framework on heterogeneous parallel systems

OP2 is a high-level domain specific library framework for the solution of unstructured mesh-based applications. It utilizes source-to-source translation and compilation so that a single application code written using the OP2 API can be transformed into multiple parallel implementations for execution on a range of back-end hardware platforms. In this paper we present the design and performance of OP2’s recent developments facilitating code generation and execution on distributed memory heterogeneous systems. OP2 targets the solution of numerical problems based on static unstructured meshes. We discuss the main design issues in parallelizing this class of applications. These include handling data dependencies in accessing indirectly referenced data and design considerations in generating code for execution on a cluster of multi-threaded CPUs and GPUs. Two representative CFD applications, written using the OP2 framework, are utilized to provide a contrasting benchmarking and performance analysis study on a number of heterogeneous systems including a large scale Cray XE6 system and a large GPU cluster. A range of performance metrics are benchmarked including runtime, scalability, achieved compute and bandwidth performance, runtime bottlenecks and systems energy consumption. We demonstrate that an application written once at a high-level using OP2 is easily portable across a wide range of contrasting platforms and is capable of achieving near-optimal performance without the intervention of the domain application programmer.     

Constraint hierarchies

Constraints allow programmers and users to state declaratively a relation that should be maintained, rather than requiring them to write procedures to maintain the relation themselves. They are thus useful in such applications as programming languages, user interface toolkits, and simulation packages. In many situations, it is desirable to be able to state bothrequired andpreferential constraints. The required constraints must hold. Since the other constraints are merely preferences, the system should try to satisfy them if possible, but no error condition arises if it cannot. Aconstraint hierarchy consists of a set of constraints, each labeled as either required or preferred at some strength. An arbitrary number of different strengths is allowed. In the discussion of a theory of constraint hierarchies, we present alternate ways of selecting among competing possible solutions, and prove a number of propositions about the relations among these alternatives. We then outline algorithms for satisfying constraint hierarchies, and ways in which we have used constraint hierarchies in a number of programming languages and systems.