Satisfiability Modulo Theories on arithmetic theories have significant applications in many important domains. Previous efforts have been mainly devoted to improving the techniques and heuristics in sequential SMT sol...
详细信息
ISBN:
(纸本)9783031656262;9783031656279
Satisfiability Modulo Theories on arithmetic theories have significant applications in many important domains. Previous efforts have been mainly devoted to improving the techniques and heuristics in sequential SMT solvers. With the development of computing resources, a promising direction to boost performance is parallel and even distributed SMT solving. We explore this potential in a divide-and-conquer view and propose a novel dynamic parallel framework with variable-level partitioning. To the best of our knowledge, this is the first attempt to perform variable-level partitioning for arithmetic theories. Moreover, we enhance the interval constraint propagation algorithm, coordinate it with Boolean propagation, and integrate it into our variable-level partitioning strategy. Our partitioning algorithm effectively capitalizes on propagation information, enabling efficient formula simplification and search space pruning. We apply our method to three state-of-the-art SMT solvers, namely CVC5, OpenSMT2, and Z3, resulting in efficient parallel SMT solvers. Experiments are carried out on benchmarks of linear and nonlinear arithmetic over both real and integer variables, and our variable-level partitioning method shows substantial improvements over previous partitioning strategies and is particularly good at non-linear theories.
This book constitutes the thoroughly refereed post-conference proceedings of the 18th international Workshop on Job Scheduling Strategies for parallelprocessing, JSSPP 2014, held in Phoenix, AZ, USA, in May 2014. The...
详细信息
ISBN:
(数字)9783319157894
ISBN:
(纸本)9783319157887
This book constitutes the thoroughly refereed post-conference proceedings of the 18th international Workshop on Job Scheduling Strategies for parallelprocessing, JSSPP 2014, held in Phoenix, AZ, USA, in May 2014. The 9 revised full papers presented were carefully reviewed and selected from 24 submissions. The papers cover the following topics: single-core parallelism; moving to distributed-memory, larger-scale systems, scheduling fairness; and parallel job scheduling.
The quality of the mesh is one of the most critical aspects for solving partial differential equations (PDEs) in applications of Computational Fluid Dynamics. Many geometry criteria have been proposed and are widely u...
详细信息
ISBN:
(数字)9781728142487
ISBN:
(纸本)9781728142487
The quality of the mesh is one of the most critical aspects for solving partial differential equations (PDEs) in applications of Computational Fluid Dynamics. Many geometry criteria have been proposed and are widely used in business pre-processing software like ICEM CFD, PointWise, Gambit. However, these traditional geometry criteria fail to recognize some quality features that seriously affect the accuracy of numerical calculations, such as density and distribution of mesh elements. These quality features are usually evaluated based on engineering experience, which heavily increases the pre-processing cost and requires extensive engineering experience. In this paper, we introduce a deep learning model to solve the mentioned issues by offline learning. The proposed model is small and fast and can be embedded in pre-processing software. Experiment results show that the derived model is capable of performing the quality evaluating task and achieve an accuracy of 93.8%.
The proceedings contain 53 papers from the High Performance Computing for Computational Science - VECPAR 2004 - 6th internationalconference. The topics discussed include: large scale simulations;development and integ...
详细信息
The proceedings contain 53 papers from the High Performance Computing for Computational Science - VECPAR 2004 - 6th internationalconference. The topics discussed include: large scale simulations;development and integration of parallel multidisciplinary computational software for modeling a modern manufacturing process;a survey of high-quality computational libraries and their impact in science and engineering applications;a performance prediction model for tomographic reconstruction in structural biology;a high performance system for processing queries on distributed geospatial data sets;parallel implementation of information retrieval clustering models;and scaling up the preventive replication of autonomous databases in cluster systems.
This 4-Volume-Set, CCIS 0251 - CCIS 0254, constitutes the refereed proceedings of the internationalconference on Informatics Engineering and Information Science, ICIEIS 2011, held in Kuala Lumpur, Malaysia, in Novemb...
ISBN:
(数字)9783642254833
ISBN:
(纸本)9783642254826
This 4-Volume-Set, CCIS 0251 - CCIS 0254, constitutes the refereed proceedings of the internationalconference on Informatics Engineering and Information Science, ICIEIS 2011, held in Kuala Lumpur, Malaysia, in November 2011. The 210 revised full papers presented together with invited papers in the 4 volumes were carefully reviewed and selected from numerous submissions. The papers are organized in topical sections on e-learning, information security, software engineering, image processing, algorithms, artificial intelligence and soft computing, e-commerce, data mining, neural networks, social networks, grid computing, biometric technologies, networks, distributed and parallel computing, wireless networks, information and data management, web applications and software systems, multimedia, ad hoc networks, mobile computing, as well as miscellaneous topics in digital information and communications.
The proceedings contain 88 papers. The topics discussed include: clock synchronization in cell BE traces;supporting parameter sweep applications with synthesized grid services;a P2P approach to resource discovery in o...
详细信息
ISBN:
(纸本)3540854509
The proceedings contain 88 papers. The topics discussed include: clock synchronization in cell BE traces;supporting parameter sweep applications with synthesized grid services;a P2P approach to resource discovery in on-line monitoring of grid workflows;transparent mobile middleware integration for java and .NET development environments;providing non-stop service for message-passing based parallelapplications with RADIC;on-line performance modeling for MPI applications;MPC: a unified parallel runtime for clusters of NUMA machines;directory-based metadata optimizations for small files in PVFS;Caspian: a tunable performance model for multi-core systems;performance model for parallel mathematical libraries based on historical knowledgebase;a performance model of dense matrix operations on many-core architectures;empirical analysis of a large-scale hierarchical storage system;and to snoop or not to snoop: evaluation of fine-grain and coarse-grain snoop filtering techniques.
Instruction-grain lifeguards monitor the events of a running application at the level of individual instructions in order to identify and help mitigate application bugs and security exploits. Because such lifeguards i...
详细信息
ISBN:
(纸本)9781605588391
Instruction-grain lifeguards monitor the events of a running application at the level of individual instructions in order to identify and help mitigate application bugs and security exploits. Because such lifeguards impose a 10-100X slowdown on existing platforms, previous studies have proposed hardware designs to accelerate lifeguard processing. However, these accelerators are either tailored to a specific class of lifeguards or suitable only for monitoring single-threaded programs. We present ParaLog, the first design of a system enabling fast online parallel monitoring of multithreaded parallelapplications. ParaLog supports a broad class of software-defined lifeguards. We show how three existing accelerators can be enhanced to support online multithreaded monitoring, dramatically reducing lifeguard overheads. We identify and solve several challenges in monitoring parallelapplications and/or parallelizing these accelerators, including (i) enforcing inter-thread data dependences, (ii) dealing with inter-thread effects that are not reflected in coherence traffic, (iii) dealing with unmonitored operating system activity, and (iv) ensuring lifeguards can access shared metadata with negligible synchronization overheads. We present our system design for both Sequentially Consistent and Total Store Ordering processors. We implement and evaluate our design on a 16 core simulated CMP, using benchmarks from SPLASH-2 and PARSEC and two lifeguards: a data-flow tracking lifeguard and a memory-access checker lifeguard. Our results show that (i) our parallel accelerators improve performance by 2-9X and 1.13-3.4X for our two lifeguards, respectively, (ii) we are 5-126X faster than the time-slicing approach required by existing techniques, and (iii) our average overheads for applications with eight threads are 51% and 28% for the two lifeguards, respectively.
The use of semantic knowledge in its various forms has become an important aspect in managing data in database and information systems. In the form of integrity constraints, it has been used intensively in query optim...
详细信息
The proceedings contain 117 papers. The special focus in this conference is on Grid Computing, Resource Management, Scheduling techniques for Cluster, Grid Computing Systems and distributed Computing. The topics inclu...
ISBN:
(纸本)3540220569
The proceedings contain 117 papers. The special focus in this conference is on Grid Computing, Resource Management, Scheduling techniques for Cluster, Grid Computing Systems and distributed Computing. The topics include: Advanced simulation technique for modeling multiphase fluid flow in porous media;a smart agent-based grid computing platform;publishing and executing parallel legacy code using an OGSI grid service;the prove trace visualisation tool as a grid service;privacy protection in ubiquitous computing based on privacy label and information flow;application-oriented scheduling in the knowledge grid;a monitoring and prediction tool for time-constraint grid application;optimal server allocation in reconfigurable clusters with multiple job types;design and evaluation of an agent-based communication model for a parallel file system;task allocation for minimizing programs completion time in multicomputer systems;adaptive interval-based caching management scheme for cluster video server;data discovery mechanism for a large peer-to-peer based scientific data grid environment;running data mining applications on the grid;application of block design to a load balancing algorithm on distributed networks;maintenance strategy for efficient communication at data warehouse;a framework for orthogonal data and control parallelism exploitation;unified development solution for cluster and grid computing and its application in chemistry;a modified parallel computation model based on cluster;a parallel volume splatting algorithm based on pc-clusters and numerical revelation and analysis of critical ignition conditions for branch chain reactions by Hamiltonian systematization methods of kinetic models.
The outcome of a business process (e.g., duration, cost, success rate) depends significantly on how well the assigned resources perform at their respective tasks. Currently, this assignment is typically based on a sta...
详细信息
ISBN:
(纸本)9783642253690
The outcome of a business process (e.g., duration, cost, success rate) depends significantly on how well the assigned resources perform at their respective tasks. Currently, this assignment is typically based on a static resource query that specifies the minimum requirements (e.g., role) a resource has to meet. This approach has the major downside that any resource whatsoever that meets the requirements can be retrieved, possibly selecting resources that do not perform well on the task. To address this challenge, we present and evaluate in this paper a model-based approach that uses data integration and mining techniques for selecting resources based on their likely performance for the task or sub-process at hand.
暂无评论