检索结果-内蒙古大学图书馆

Proceedings of the acm sigplan symposium on principles and practice of parallel programming, PPOPP 1999年 96-106页

作者： Scherer, Alex Lu, Honghui Gross, thomas Zwaenepoel, Willy ETH Zurich Zurich Switzerland

We present a system that allows OpenMP programs to execute on a network of workstations with a variable number of nodes. the ability to adapt to a variable number of nodes allows a program to take advantage of additional nodes that become available after it starts execution, or to gracefully scale down when the number of available nodes is reduced. We demonstrate that the cost of adaptation is modest;the system allows a program to adapt at a moderate rate without much performance loss. Two ideas underlie the efficiency of our design. First, we recognize that OpenMP programs exhibit convenient adaptation points during their execution, points at which the cost of adaptation can be much reduced. Second, by allowing a process a certain grace period before it must leave a node, we insure that most adaptations can occur at these adaptation points, and thus at low cost. Migration of a process, a much more expensive method for providing adaptivity, is used only as a back-up solution, when the process cannot reach an adaptation point within the grace period. Our implementation consists of an OpenMP pre-processor that generates TreadMarks distributed shared memory (DSM) programs, and a version of TreadMarks modified to adapt to a variable number of nodes. Using a DSM as the underlying substrate facilitates the data (re-)distribution necessary after an adaptation.

关键词： parallel processing systems

来源：评论

学校读者我要写书评

暂无评论

Petascale Computing with Accelerators

引用

acm sigplan NOTICES 2009年第4期44卷 241-249页

作者： Kistler, Michael Gunnels, John Brokenshire, Daniel Benton, Brad IBM Corp Austin TX 78758 USA IBM Corp Yorktown Hts NY 10598 USA

A trend is developing in high performance computing in which commodity processors are coupled to various types of computational accelerators. Such systems are commonly called hybrid systems. In this paper, we describe our experience developing an implementation of the Linpack benchmark for a petascale hybrid system, the LANL Roadrunner cluster built by IBM for Los Alamos National Laboratory. this system combines traditional x86-64 host processors with IBM PowerXCell (TM) 8i accelerator processors. the implementation of Linpack we developed was the first to achieve a performance result in excess of 1.0 PFLOPS, and made Roadrunner the #1 system on the Top500 list in June 2008. We describe the design and implementation of hybrid Linpack, including the special optimizations we developed for this hybrid architecture. We then present actual results for single node and multi-node executions. From this work, we conclude that it is possible to achieve high performance for certain applications on hybrid architectures when careful attention is given to efficient use of memory bandwidth, scheduling of data movement between the host and accelerator memories, and proper distribution of work between the host and accelerator processors.

关键词： Algorithms Performance Design Accelerators hybrid programming models

来源：评论

学校读者我要写书评

暂无评论

Backtracking-based Load Balancing

引用

acm sigplan NOTICES 2009年第4期44卷 55-64页

作者： Hiraishi, Tasuku Yasugi, Masahiro Umatani, Seiji Yuasa, Taiichi Kyoto Univ Acad Ctr Comp & Media Studies Kyoto 6068501 Japan Kyoto Univ Grad Sch Informat Kyoto 6068501 Japan

High-productivity languages for parallel computing become more important as parallel environments including multicores become more common. Cilk is such a language. It provides good load balancing for many applications including irregular ones;that is, it keeps all workers busy by creating plenty of "logical" threads and adopting the oldest-first work stealing strategy. this paper proposes a "logical thread"-free framework called Tascell, which achieves a higher performance and supports a wider range of parallel environments including clusters without loss of productivity. A Tascell worker spawns a "real" task only when requested by another idle worker. the worker performs the spawning by temporarily "backtracking" and restoring its oldest task-spawnable state. Our approach eliminates the cost of spawning/managing logical threads. It also promotes the reuse of workspaces and improves the locality of reference since it does not need to prepare a workspace for each concurrently runnable logical thread. Furthermore, Tascell enables elegant and highly-efficient backtrack search algorithms with delayed workspace copying. For instance, our 16-queens problem solver is 1.86 times faster than Cilk on a system with two dual-core processors. Our approach also enables a single program to run in both shared and distributed memory environments with reasonable efficiency and scalability.

关键词： Design Languages Performance load balancing parallel computing backtracking backtrack search

来源：评论

学校读者我要写书评

暂无评论

Effective Performance Measurement and Analysis of Multithreaded Applications

引用

acm sigplan NOTICES 2009年第4期44卷 229-239页

作者： Tallent, Nathan R. Mellor-Crummey, John M. Rice Univ Houston TX 77251 USA

Understanding why the performance of a multithreaded program does not improve linearly with the number of cores in a shared-memory node populated with one or more multicore processors is a problem of growing practical importance. this paper makes three contributions to performance analysis of multithreaded programs. First, we describe how to measure and attribute parallel idleness, namely, where threads are stalled and unable to work. this technique applies broadly to programming models ranging from explicit threading (e. g., Pthreads) to higher-level models such as Cilk and OpenMP. Second, we describe how to measure and attribute parallel overhead-when a thread is performing miscellaneous work other than executing the user's computation. By employing a combination of compiler support and post-mortem analysis, we incur no measurement cost beyond normal profiling to glean this information. Using idleness and overhead metrics enables one to pinpoint areas of an application where concurrency should be increased (to reduce idleness), decreased (to reduce overhead), or where the present parallelization is hopeless (where idleness and overhead are both high). third, we describe how to measure and attribute arbitrary performance metrics for high-level multithreaded programming models, such as Cilk. this requires bridging the gap between the expression of logical concurrency in programs and its realization at run-time as it is adaptively partitioned and scheduled onto a pool of threads. We have prototyped these ideas in the context of Rice University's HPCTOOLKIT performance tools. We describe our approach, implementation, and experiences applying this approach to measure and attribute work, idleness, and overhead in executions of Cilk programs.

关键词： Performance Measurement Algorithms Performance Analysis Call Path Profiling Multithreaded programming Models HPCTOOLKIT

来源：评论

学校读者我要写书评

暂无评论

ParGeo: a library for parallel computational geometry 22

ParGeo: a library for parallel computational geometry

引用

Proceedings of the 27th acm sigplan symposium on principles and practice of parallel programming

作者： Yiqiu Wang Shangdi Yu Laxman Dhulipala Yan Gu Julian Shun MIT CSAIL UC Riverside

We present ParGeo, a multicore library for computational geometry algorithms. We describe two of the algorithms from ParGeo, convex hull and the smallest enclosing ball, and present a short evaluation of all implement...

ISBN: (纸本)9781450392044

关键词：

来源：评论

学校读者我要写书评

暂无评论

Formal Verification of Practical MPI Programs

引用

acm sigplan NOTICES 2009年第4期44卷 261-269页

作者： Vo, Anh Vakkalanka, Sarvani DeLisi, Michael Gopalakrishnan, Ganesh Kirby, Robert M. thakur, Rajeev Univ Utah Sch Comp Salt Lake City UT 84112 USA Argonne Natl Lab Div Math & Comp Sci Argonne IL 60439 USA

this paper considers the problem of formal verification of MPI programs operating under a fixed test harness for safety properties without building verification models. In our approach, we directly model-check the MPI/C source code, executing its interleavings with the help of a verification scheduler. Unfortunately, the total feasible number of interleavings is exponential, and impractical to examine even for our modest goals. Our earlier publications formalized and implemented a partial order reduction approach that avoided exploring equivalent interleavings, and presented a verification tool called ISP. this paper presents algorithmic and engineering innovations to ISP, including the use of OpenMP parallelization, that now enables it to handle practical MPI programs, including: (i) ParMETIS - a widely used hypergraph partitioner, and (ii) MADRE - a Memory Aware Data Re-distribution Engine, both developed outside our group. Over these benchmarks, ISP has automatically verified up to 14K lines of MPI/C code, producing error traces of deadlocks and assertion violations within seconds.

关键词： Verification MPI Message Passing Interface distributed programming model checking dynamic partial order reduction

来源：评论

学校读者我要写书评

暂无评论

Para-functional programming: A paradigm for programming multiprocessor systems 86

Para-functional programming: A paradigm for programming mult...

引用

13th AnnuaJ acm symposium on the principles of programming Languages, POPL 1986

作者： Hudak, Paul Smith, Lauren Yale University Department of Computer Science United States

ISBN: (纸本)089791175X

One of the most important pragmatic advantages of functional languages is that concurrency in a program is implicit-there is no need for special constructs to express parallelism as is required in most conventional languages. Furthermore, it is fairly easy for compilers to automatically determine the concurrency as a step toward decomposing a program for execution on a suitable parallel architecture. Yet it is often the case that one knows precisely the optimal decomposition for execution on a particular machine, and one can never expect a compiler to determine such optimal mappings in all cases. this paper is concerned with ways to allow the programmer to explicitly express this mapping of program to machine, by using annotations that, given a few minor constraints, cannot alter the functional semantics of the program. We show through several deeded examples the expressiveness and conciseness of the resulting " para-functional programming methodology, using an experimental language called ParAlfl based on our ideas. We also give a formal denotational description of the mapping semantics using a notion of execution trees.

关键词： Functional programming

来源：评论

学校读者我要写书评

暂无评论

How to build programmable multi-core chips 09

How to build programmable multi-core chips

引用

Proceedings of the 14th acm sigplan symposium on principles and practice of parallel programming

作者： Jack B. Dennis Massachusetts Institute of Technology Cambridge MA USA

ISBN: (纸本)9781605583976

the arrival of multi-core chips has heightened interest in the discipline of parallel programming, a topic that has received much attention for many years. Computer architects have much to learn from sound principles for structuring software and expressing parallel computation. this talk will cover principles for the design of computer systems to support composable parallel software - the idea that any parallel program is usable, without change, as a component of larger parallel programs. By following these principles, a revolution in the ease of building robust and high-performance parallel software can be achieved. the principles suggest interesting directions for computer architecture; the tools to experiment with new architecture concepts are ready and waiting for the savvy and ambitious researcher

关键词： parallel algorithms design performance

来源：评论

学校读者我要写书评

暂无评论

Engineering formal metatheory

引用

acm sigplan NOTICES 2008年第1期43卷 3-15页

作者： Aydemir, Brian Chargueraud, Arthur Pierce, Benjamin C. Pollack, Randy Weirich, Stephanie Univ Penn Philadelphia PA 19104 USA Univ Edinburgh Edinburgh EH8 9YL Midlothian Scotland

Machine-checked proofs of properties of programming languages have become a critical need, both for increased confidence in large and complex designs and as a foundation for technologies such as proof-carrying code. However, constructing these proofs remains a black art, involving many choices in the formulation of definitions and theorems that make a huge cumulative difference in the difficulty of carrying out large formal developments. the representation and manipulation of terms with variable binding is a key issue. We propose a novel style for formalizing metatheory, combining locally nameless representation of terms and cofinite quantification of free variable names in inductive definitions of relations on terms (typing, reduction,...). the key technical insight is that our use of cofinite quantification obviates the need for reasoning about equivariance (the fact that free names can be renamed in derivations);in particular, the structural induction principles of relations defined using cofinite quantification are strong enough for metatheoretic reasoning, and need not be explicitly strengthened. Strong inversion principles follow (automatically, in Coq) from the induction principles. Although many of the underlying ingredients of our technique have been used before, their combination here yields a significant improvement over other methodologies using first-order representations, leading to developments that are faithful to informal practice, yet require no external tool support and little infrastructure within the proof assistant. We have carried out several large developments in this style using the Coq proof assistant and have made them publicly available. Our developments include type soundness for System F-< : and core ML (with references, exceptions, datatypes, recursion, and patterns) and subject reduction for the Calculus of Constructions. Not only do these developments demonstrate the comprehensiveness of our approach;they have also been optimized for

关键词： design documentation languages theory verification binding Coq locally nameless

来源：评论

学校读者我要写书评

暂无评论

Automatic differentiation of parallel loops with formal methods 22

Automatic differentiation of parallel loops with formal meth...

引用

Proceedings of the 27th acm sigplan symposium on principles and practice of parallel programming

作者： Jan Hückelheim Laurent Hascoët Argonne National Laboratory Inria Sophia Antipolis

ISBN: (纸本)9781450392044

the accompanying poster to this short paper presents a combination of reverse mode AD and formal methods to enable efficient differentiation of (or backpropagation through) shared-memory parallel code. Compared to the state of the art, our approach can more often avoid the need for atomic updates or private data copies during the parallel derivative computation, even in the presence of unstructured or data-dependent data access patterns. this is achieved by gathering information about the memory access patterns from the input program, which is assumed to be correctly parallelized. this information is then used to build a model of assertions in a theorem prover, which can be used to check the safety of shared memory accesses during the parallel derivative computation.

关键词： OpenMP

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：