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

Scalable Multicore Motion Planning Using Lock-Free Concurrency

IEEE TRANSACTIONS ON ROBOTICS 2014年第5期30卷 1123-1136页

作者： Ichnowski, Jeffrey Alterovitz, Ron Univ N Carolina Dept Comp Sci Chapel Hill NC 27599 USA

We present Parallel Rapidly Exploring Random Tree (PRRT) and Parallel RRT* (PRRT*), which are sampling-based methods for feasible and optimal motion planning designed for modern multicore CPUs. We parallelize RRT and RRT* such that all threads concurrently build a single-motion planning tree. Parallelization in this manner requires data structures, such as the nearest neighbor search tree and the motion planning tree, to be safely shared across multiple threads. Rather than relying on the traditional locks which can result in slowdowns due to lock contention, we introduce algorithms that are based on lock-free concurrency using atomic operations. We further improve scalability by using partition-based sampling (which shrinks each core's working dataset to improve cache efficiency) and parallel work-saving (in reducing the number of rewiring steps performed in PRRT*). Because PRRT and PRRT* are CPU-based, they can be directly integrated with existing libraries. In scenarios such as the Alpha Puzzle and Cubicles scenario and the Aldebaran Nao performing a two-handed task, we demonstrate that PRRT and PRRT* scale well as core counts increase, and in some cases they exhibit superlinear speedup.

关键词： concurrent algorithms motion and path planning sampling-based methods

来源：评论

学校读者我要写书评

暂无评论

Software-based contention management for efficient compare-and-swap operations

引用

CONCURRENCY AND COMPUTATION-PRACTICE & EXPERIENCE 2014年第14期26卷 2386-2404页

作者： Dice, Dave Hendler, Danny Mirsky, Ilya Ben Gurion Univ Negev IL-84105 Beer Sheva Israel Telekom Innovat Labs Berlin Germany

Many concurrent data-structure implementations - both blocking and non-blocking - use the well-known compare-and-swap (CAS) operation, supported in hardware by most modern multiprocessor architectures, for inter-thread synchronization. A key weakness of the CAS operation is its performance in the presence of memory contention. When multiple threads concurrently attempt to apply CAS operations to the same shared variable, at most a single thread will succeed in changing the shared variable's value and the CAS operations of all other threads will fail. Moreover, significant degradation in performance occurs when variables manipulated by CAS become contention 'hot spots', because failed CAS operations congest the interconnect and memory devices and slow down successful CAS operations. In this work, we study the following question: can software-based contention management improve the efficiency of hardware-provided CAS operations? In other words, can a software contention management layer, encapsulating invocations of hardware CAS instructions, improve the performance of CAS-based concurrent data structures? To address this question, we conduct what is, to the best of our knowledge, the first study on the impact of contention management algorithms on the efficiency of the CAS operation. We implemented several Java classes, that extend Java's AtomicReference class, and encapsulate calls to the native CAS instruction with simple contention management mechanisms tuned for different hardware platforms. A key property of our algorithms is the support for an almost-transparent interchange with Java's AtomicReference objects, used in implementations of concurrent data structures. We evaluate the impact of these algorithms on both a synthetic micro-benchmark and on CAS-based concurrent implementations of widely-used data structures such as stacks and queues. Our performance evaluation establishes that lightweight software-based contention management support can greatly improve

关键词： Compare-and-swap contention management concurrent algorithms

来源：评论

学校读者我要写书评

暂无评论

Lightweight Contention Management for Efficient Compare-and-Swap Operations

Lightweight Contention Management for Efficient Compare-and-...

引用

19th International Conference on Euro-Par

作者： Dice, David Hendler, Danny Mirsky, Ilya Oracle Sun Labs Redwood City CA 94065 USA Ben Gurion Univ Negev Dept Comp Sci & Telekom Innovat IL-84105 Beer Sheva Israel Ben Gurion Univ Negev Dept Comp Sci IL-84105 Beer Sheva Israel

ISBN: (纸本)9783642400476

Many concurrent data-structure implementations use the well-known compare-and-swap (CAS) operation, supported in hardware by most modern multiprocessor architectures, for inter-thread synchronization. A key weakness of the CAS operation is the degradation in its performance in the presence of memory contention. In this work we study the following question: can software-based contention management improve the efficiency of hardware-provided CAS operations? Our performance evaluation establishes that lightweight contention management support can greatly improve performance under medium and high contention levels while typically incurring only small overhead when contention is low.

关键词： Compare-and-swap contention management concurrent algorithms

来源：评论

学校读者我要写书评

暂无评论

Simple concurrent garbage collection almost without synchronization

引用

FORMAL METHODS IN SYSTEM DESIGN 2010年第2期36卷 148-166页

作者： Hesselink, Wim H. Lali, M. I. Univ Groningen Dept Math & Comp Sci NL-9700 AK Groningen Netherlands

We present two simple mark and sweep algorithms, A and B, for concurrent garbage collection by a single collector running concurrently with a number of mutators that concurrently modify shared data. Both algorithms are based on the ideas of Ben-Ari's classical algorithm for on-the-fly garbage collection with one mutator. The algorithms require the mutators to estimate the set of objects they currently hold in private variables. They differ in the grain of atomicity of this estimate and in their mutator marking requirements. For algorithm A, the only synchronization needed is at the point where the list of newly collected garbage nodes is included in the free list to again become available to the mutators. Such synchronization of access to the free list seems unavoidable. For algorithm A, the estimate can be constructed concurrently with mutator actions. Algorithm B requires that the estimate is constructed atomically. algorithms of this form have always been error-prone. We therefore provide assertional proofs of correctness, which moreover have been verified with the proof assistant PVS.

关键词： concurrent garbage collection concurrent algorithms Verification Theorem proving Memory model

来源：评论

学校读者我要写书评

暂无评论

Dynamic partial reconfiguration of CPU-s for Programmable Logic Controllers executing control programs developed in the Ladder Diagram language

引用

IFAC Proceedings Volumes 2009年第21期42卷 55-60页

作者： M. Chmiel J. Mocha D. Kania E. Hrynkiewicz Institute of Electronics Silesian University of Technology Akademicka 16 44–100 Gliwice Poland mchmiel jmocha dkania

The paper presents a method for hierarchical description of control algorithms with their partitioning into tasks that are executed sequentially and those that run concurrently. The proposed method is based entirely on components available in the Ladder Diagram (LAD) language, and can be considered as an alternative to the Sequential Function Chart (SFC) diagrams. In addition, an architecture for a reconfigurable logic controller is proposed, which is capable of executing the control program combined hardware and software tasks. For that purpose the mechanism of dynamic partial reconfiguration of programmable gate arrays (FPGA-s) is used. This makes possible to download to the programmable structure only those tasks, which are currently required by the running control algorithm. Such a hardware implementation of the controller enables effective execution of concurrent control tasks by parallel operation of the control processing units. Finally, a proposed controller architecture allows using a programmable device of a reduced size, and this makes the solution more cost-effective.

关键词： Programmable Logic Controller (PLC) Sequential Function Chart (SFC) Ladder Diagram (LAD) concurrent algorithms Reconfigurable Controller Field Programmable Gate Array (FPGA) Partial Dynamic Reconfiguration

来源：评论

学校读者我要写书评

暂无评论

Deriving linearizable fine-grained concurrent objects

引用

ACM SIGPLAN NOTICES 2008年第6期43卷 125-135页

作者： Vechev, Martin Yahav, Eran IBM Res Corp Yorktown Hts NY 10598 USA

Practical and efficient algorithms for concurrent data structures are difficult to construct and modify. algorithms in the literature are often optimized for a specific setting, making it hard to separate the algorithmic insights from implementation details. The goal of this work is to systematically construct algorithms for a concurrent data structure starting from its sequential implementation. Towards that goal, we follow a construction process that combines manual steps corresponding to high-level insights with automatic exploration of implementation details. To assist us in this process, we built a new tool called PARAGLIDER. The tool quickly explores large spaces of algorithms and uses bounded model checking to check linearizability of algorithms. Starting from a sequential implementation and assisted by the tool, we present the steps that we used to derive various highly-concurrent algorithms. Among these algorithms is a new fine-grained set data structure that provides a wait-free contains operation, and uses only the compare-and-swap ( CAS) primitive for synchronization.

关键词： algorithms verification concurrent algorithms verification synthesis model checking linearizability

来源：评论

学校读者我要写书评

暂无评论

Deriving Linearizable Fine-Grained concurrent Objects 08

Deriving Linearizable Fine-Grained Concurrent Objects

引用

ACM SIGPLAN Conference on Programming Language Design and Implementation

作者： Vechev, Martin Yahav, Eran IBM T.J. Watson Research Center Hawthorne NY USA

ISBN: (纸本)9781595938602

Practical and efficient algorithms for concurrent data structures are difficult to construct. and modify. algorithms in the literature are often optimized for a specific setting, making it hard to separate the algorithmic insights from implementation details. The goal of this work is to systematically construct algorithms for a concurrent data structure starting from its sequential implementation. Towards that goal, we follow a construction process that combines manual steps corresponding to high-level insights with automatic exploration of implementation details. To assist us in this process, we built a new tool called PARAGLIDER. The tool quickly explores large spaces of algorithms and uses bounded model checking to check linearizability of algorithms. Starting from a sequential implementation and assisted by the tool, we present the steps that we used to derive various highly-concurrent algorithms. Among these algorithms is a new fine-grained set data structure that provides a wait-free contains operation, and uses only the compare-and-swap (CAS) primitive for synchronization.

关键词： concurrent algorithms verification synthesis model checking linearizability

来源：评论

学校读者我要写书评

暂无评论

CGCExplorer: A semi-automated search procedure for provably correct concurrent collectors

引用

ACM SIGPLAN NOTICES 2007年第6期42卷 456-467页

作者： Vechev, Martin T. Yahav, Eran Bacon, David F. Rinetzky, Noam Univ Cambridge Cambridge CB2 1TN England Tel Aviv Univ Tel Aviv Israel

concurrent garbage collectors are notoriously hard to design, implement, and verify. We present a framework for the automatic exploration of a space of concurrent mark-and-sweep collectors. In our framework, the designer specifies a set of "building blocks" from which algorithms can be constructed. These blocks reflect the designer's insights about the coordination between the collector and the mutator. Given a set of building blocks, our framework automatically explores a space of algorithms, using model checking with abstraction to verify algorithms in the space. We capture the intuition behind some common mark-and-sweep algorithms using a set of building blocks. We utilize our framework to automatically explore a space of more than 1, 600, 000 algorithms built from these blocks, and derive over 100 correct fine-grained algorithms with various space, synchronization, and precision tradeoffs.

关键词： concurrent garbage collection concurrent algorithms verification synthesis

来源：评论

学校读者我要写书评

暂无评论

CGCExplorer: A semi-automated search procedure for provably correct concurrent collectors 07

CGCExplorer: A semi-automated search procedure for provably ...

引用

Conference on Programming Language Design and Implementation (PLDI)

作者： Vechev, Martin T. Yahav, Eran Bacon, David F. Rinetzky, Noam Univ Cambridge Cambridge CB2 1TN England Tel Aviv Univ Tel Aviv Israel

ISBN: (纸本)9781595936332

关键词： concurrent garbage collection concurrent algorithms verification synthesis

来源：评论

学校读者我要写书评

暂无评论

Correctness-preserving derivation of concurrent garbage collection algorithms

引用

ACM SIGPLAN NOTICES 2006年第6期41卷 341-353页

作者： Vechev, Martin T. Yahav, Eran Bacon, David F. Univ Cambridge Cambridge CB2 1TN England

Constructing correct concurrent garbage collection algorithms is notoriously hard. Numerous such algorithms have been proposed, implemented, and deployed - and yet the relationship among them in terms of speed and precision is poorly understood, and the validation of one algorithm does not carry over to others. As programs with low latency requirements written in garbage-collected languages become part of society's mission-critical infrastructure, it is imperative that we raise the level of confidence in the correctness of the underlying system, and that we understand the trade-offs inherent in our algorithmic choice. In this paper we present correctness-preserving transformations that can be applied to an initial abstract concurrent garbage collection algorithm which is simpler, more precise, and easier to prove correct than algorithms used in practice - but also more expensive and with less concurrency. We then show how both pre-existing and new algorithms can be synthesized from the abstract algorithm by a series of our transformations. We relate the algorithms formally using a new definition of precision, and informally with respect to overhead and concurrency. This provides many insights about the nature of concurrent collection, allows the direct synthesis of new and useful algorithms, reduces the burden of proof to a single simple algorithm, and lays the groundwork for the automated synthesis of correct concurrent collectors.

关键词： concurrent garbage collection concurrent algorithms verification synthesis

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：