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

32nd ACM Symposium on Parallelism in algorithms and Architectures (SPAA)

作者： Sheffi, Gali Petrank, Erez Technion Dept Comp Sci Haifa Israel

ISBN: (纸本)9781450369350

Hardware and software faults increasingly surface in today's computing environment and vast theoretical and practical research efforts are devoted to ameliorate the effects of malfunctionality in the computing process. Most research to date, however, has focused on how to discover and handle faulty data. In this paper we formalize and study faulty functionality in a modern multicore shared-memory environment. Functional faults have been previously studied in the architecture community. However, they have never been formally defined and lower/upper bounds were not previously proven. We present a model of functional faults, and study avenues that allow tolerating functional faults while maintaining the correctness of the entire computation. We exemplify this model by constructing a robust consensus protocol from functionally-faulty compare-and-swap objects. We then show a (tight) impossibility result for the same construction, when the number of faults exceeds a certain threshold. Interestingly, for some fault types, more functional faults can be tolerated than the analogue data faults, beating an impossibility result for data faults and demonstrating the difference between the two models.

关键词： concurrent algorithms shared memory lowerbounds fault-tolerance hardware faults software faults

来源：评论

学校读者我要写书评

暂无评论

Auto-active Verification of Distributed Systems and Specification Refinements with Why3-do

引用

Science of Computer Programming 2025年

作者： Cláudio Belo Lourenço Jorge Sousa Pinto Huawei Central Software Institute Edinburgh United Kingdom HASLab/INESC TEC & Universidade do Minho Portugal

In this paper, we introduce a novel approach for rigorously verifying safety properties of state machine specifications. Our method leverages an auto-active verifier and centers around the use of action functions annotated with contracts. These contracts facilitate inductive invariant checking, ensuring correctness during system execution. Our approach is further supported by the Why3-do library, which extends the Why3 tool's capabilities to verify concurrent and distributed algorithms using state machines. Two distinctive features of Why3-do are: (i) it supports specification refinement through refinement mappings, enabling hierarchical reasoning about distributed algorithms; and (ii) it can be easily extended to make verifying specific classes of systems more convenient. In particular, the library contains models allowing for message-passing algorithms to be described with programmed handlers , assuming different network semantics. A gallery of examples, all verified with Why3 using SMT solvers as proof tools, is also described in the paper. It contains several auto-actively verified concurrent and distributed algorithms, including the Paxos consensus algorithm.

关键词： Deductive Verification Auto-active Verification State Machine Specifications Specification Refinement Refinement Mappings Distributed algorithms concurrent algorithms Paxos Consensus

来源：评论

学校读者我要写书评

暂无评论

Functional Faults 20

Functional Faults

引用

25th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP)

作者： Sheffi, Gali Petrank, Erez Technion Dept Comp Sci Haifa Israel

ISBN: (纸本)9781450368186

Hardware and software faults increasingly surface in today's computing environment and vast theoretical and practical research efforts are being devoted to overcoming the effects of malfunctionality in the computing process. Most research to date, however, has focused on how to discover and handle faulty data. We initiate a formal study of faulty functionality in a modern multicore shared-memory environment. We introduce a model of functional faults, and study avenues that allow tolerating functional faults while maintaining the correctness of the entire computation. We demonstrate the generality of this model by constructing a robust consensus protocol from functionally-faulty compare-and-swap objects. Additionally, We formally prove (tight) impossibility result for the same constructions.

关键词： concurrent algorithms shared memory lower-bounds fault-tolerance hardware faults software faults

来源：评论

学校读者我要写书评

暂无评论

concurrent use of write-once memory

引用

JOURNAL OF PARALLEL AND DISTRIBUTED COMPUTING 2018年 113卷 250-260页

作者： Aspnes, James Censor-Hillel, Keren Yaakobi, Eitan Yale Univ Dept Comp Sci POB 2158 New Haven CT 06520 USA Technion Dept Comp Sci Haifa Israel

We consider the problem of implementing general shared-memory objects on top of write-once bits, which can be changed from 0 to 1 but not back again. In a sequential setting, write-once memory (WOM) codes have been developed that allow simulating memory that support multiple writes, even of large values, setting an average of 1 + o(1) write-once bits per write. We show that similar space efficiencies can be obtained in a concurrent setting, though at the cost of high time complexity and fixed bound on the number of write operations. As an alternative, we give an implementation that permits unboundedly many writes and has much better amortized time complexity, but at the cost of unbounded space complexity. Whether one can obtain both low time complexity and low space complexity in the same implementation remains open. (C) 2017 Elsevier Inc. All rights reserved.

关键词： concurrent algorithms Write-once memory Space complexity

来源：评论

学校读者我要写书评

暂无评论

Read-Uncommitted Transactions for Smart Contract Performance 39

Read-Uncommitted Transactions for Smart Contract Performance

引用

39th IEEE International Conference on Distributed Computing Systems (ICDCS)

作者： Cook, Victor Painter, Zachary Peterson, Christina Dechev, Damian Univ Cent Florida Comp Sci Dept Orlando FL 32816 USA

ISBN: (纸本)9781728125190

Smart contract transactions demonstrate issues of performance and correctness that application programmers must work around. Although the blockchain consensus mechanism approaches ACID compliance, use cases that rely on frequent state changes are impractical due to the block publishing interval of O(10(1)) seconds. The effective isolation level is READ COMMITTED, only revealing state transitions at the end of the block interval. Values read may be stale and not match program order, causing many transactions to fail when a block is committed. This paper perceives the blockchain as a transactional data structure, using this analogy in the development of a new algorithm, Hash-Mark-Set (HMS), that improves transaction throughput by providing a READ-UNCOMMITTED view of state variables. HMS creates a directed acyclic graph (DAG) from the pending transaction pool. The transaction order derived from the DAG is used to provide a READ-UNCOMMITTED view of the data for new transactions, which enter the DAG as they are received. An implementation of HMS is provided, interoperable with Ethereum and ready for use in smart contracts. Over a wide range of transaction mixes, HMS is demonstrated to improve throughput. A side product of the implementation is a new technique, Runtime Argument Augmentation (RAA), that allows smart contracts to communicate with external data services before submitting a transaction. RAA has use cases beyond HMS and can serve as a lightweight replacement for blockchain oracles.

关键词： Blockchain Smart contracts concurrent algorithms Transaction throughput

来源：评论

学校读者我要写书评

暂无评论

Boosting concurrency in Parallel State Machine Replication 19

Boosting concurrency in Parallel State Machine Replication

引用

20th ACM/IFIP/USENIX International Middleware Conference

作者： Escobar, Ian Aragon Dotti, Fernando Luis Alchieri, Eduardo Pedone, Fernando Pontificia Univ Catolica Rio Grande do Sul Porto Alegre RS Brazil Univ Brasilia Brasilia DF Brazil Univ Svizzera Italiana USI Lugano Switzerland

ISBN: (纸本)9781450370097

State machine replication (SMR) is a well-known approach to implementing fault-tolerant services, providing high availability and strong consistency. To boost the performance of SMR, some proposals execute independent commands concurrently, while dependent commands execute sequentially in the total delivery order. The most general approach to handling command dependencies resorts to a directed acyclic graph (DAG), where nodes represent commands and edges represent dependencies. In this paper we show that due to the command arrival and multithreaded execution rates of SMR, a highly concurrent implementation of a DAG is needed. We show that a typical coarse-grained DAG implementation, where the whole graph is a critical section, results in a bottleneck in the replica. We propose two improvements to the coarse-grained DAG approach: fine-grained algorithms, using lock-coupling, and lock-free algorithms. Our fine-grain algorithms lock individual vertices in the DAG. The lock-free algorithms use nonblocking synchronization, with atomic operations, and lazy synchronization to postpone physical removal of nodes. All algorithms were integrated in a parallel SMR prototype. Experimental evaluation revealed that the fine-grained algorithms are also subject to a bottleneck. The lock-free implementation, however, sports linear speedup with the number of working threads, in some cases scaling up to 64 threads.

关键词： State Machine Replication concurrent algorithms Fault Tolerance

来源：评论

学校读者我要写书评

暂无评论

Efficient Compute at the Edge: Optimizing Energy Aware Data Structures for Emerging Edge Hardware 16

Efficient Compute at the Edge: Optimizing Energy Aware Data ...

引用

International Conference on High Performance Computing and Simulation (HPCS)

作者： Khan, Amin M. Umar, Ibrahim Phuong Hoai Ha UiT Arctic Univ Norway Dept Comp Sci Tromso Norway

ISBN: (纸本)9781538678794

The advent of exascale computing, with the unparalleled rise in the scale of data in Internet of Things (IoT), high performance computing (HPC), and big data domains, both at the center and the edge of the system, requires optimal exploitation of energy-efficient computing hardware dedicated for edge processing. Emerging hardware for data processing at the edge must take advantage of advanced concurrent data locality-aware algorithms and data structures in order to provide better throughput and energy efficiency. Their design must be performance portable for their implementation to perform equally well on the edge hardware as well as other high performance computing, embedded and accelerator platforms. concurrent search trees are one such widely used back-end for many important big data systems, databases, and file systems. We analyze DeltaTree, a concurrent energy-efficient and locality-aware data structure based on relaxed cache-oblivious model and van Emde Boas trees, on Intel's specialized computing platform Movidius Myriad 2, designed for machine vision and computing capabilities at the edge. We compare the throughput and energy efficiency of DeltaTree with B-link tree, a highly concurrent B+tree, on Movidius Myriad 2, along with a high performance computing platform (Intel Xeon), an ARM embedded platform, and an accelerator platform (Intel Xeon Phi). The results show that DeltaTree is performance portable, providing better energy-efficiency and throughput than B-link tree on these platforms for most workloads. For Movidius Myriad 2 in particular, DeltaTree performs really well with its throughput and efficiency up to 4x better than B-link tree.

关键词： edge computing energy efficient algorithms concurrent algorithms data locality binary search trees

来源：评论

学校读者我要写书评

暂无评论

BQ: A Lock-Free Queue with Batching 18

BQ: A Lock-Free Queue with Batching

引用

30th ACM Symposium on Parallelism in algorithms and Architectures (SPAA)

作者： Milman, Gal Kogan, Alex Lev, Yossi Luchangco, Victor Petrank, Erez Technion Haifa Israel Oracle Labs Redwood Shores CA USA

ISBN: (纸本)9781450357999

concurrent data structures provide fundamental building blocks for concurrent programming. Standard concurrent data structures may be extended by allowing a sequence of operations to be submitted as a batch for later execution. A sequence of such operations can then be executed more efficiently than the standard execution of one operation at a time. In this paper we develop a novel algorithmic extension to the prevalent FIFO queue data structure that exploits such batching scenarios. An implementation in C++ on a multicore demonstrates a significant performance improvement of up to 16x (depending on batch lengths), compared to previous queue implementations.

关键词： concurrent algorithms concurrent Data Structures Lock-Freedom Linearizability FIFO Queue

来源：评论

学校读者我要写书评

暂无评论

An Efficient Implementation of Boolean Grobner Basis Computation 3rd

引用

3rd Latin American High-Performance Computing Conference (CARLA)

作者： Castro Campos, Rodrigo Alexander Sagols Troncoso, Feliu Davino Zaragoza Martinez, Francisco Javier Univ Autonoma Metropolitana Azcapotzalco Optimizac Mexico City DF Mexico Inst Politecn Nacl Ctr Invest & Estudios Avanzados Dept Matemat Mexico City DF Mexico Univ Autonoma Metropolitana Azcapotzalco Dept Sistemas Mexico City DF Mexico

ISBN: (纸本)9783319579726;9783319579719

The computation of boolean Grobner bases has become an increasingly popular technique for solving systems of boolean equations that appear in cryptography. This technique has been used to solve some cryptosystems for the first time. In this paper, we describe a new concurrent algorithm for boolean Grobner basis computation that is capable of solving the first HFE challenge. We also discuss implementation details, including optimal runtime parameters that depend on the CPU architecture. Our implementation is available as open source software.

关键词： Grobner basis Boolean ideals concurrent algorithms

来源：评论

学校读者我要写书评

暂无评论

Effect of portable fine-grained locality on energy efficiency and performance in concurrent search trees 16

Effect of portable fine-grained locality on energy efficienc...

引用

21st ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP)

作者： Umar, Ibrahim Anshus, Otto J. Ha, Phuong H. UiT Arctic Univ Norway Dept Comp Sci Tromso Norway

ISBN: (纸本)9781450340922

Recent research has suggested that improving fine-grained datalocality is one of the main approaches to improving energy efficiency and performance. However, no previous research has investigated the effect of the approach on these metrices in the case of concurrent data structures. This paper investigates how fine-grained data locality influences energy efficiency and performance in concurrent search trees, a crucial data structure that is widely used in several important systems. We conduct a set of experiments on three lock-based concurrent search trees: DeltaTree, a portable fine-grained localityaware concurrent search tree;CBTree, a coarse-grained localityaware B+ tree;and BST-TK, a locality-oblivious concurrent search tree. We run the experiments on a commodity x86 platform and an embedded ARM platform. The experimental results show that DeltaTree has 13-25% better energy efficiency and 10-22% more operations/second on the x86 and ARM platforms, respectively. The results confirm that portable fine-grained locality can improve energy efficiency and performance in concurrent search trees.

关键词： Performance evaluation power analysis concurrent algorithms energy efficient computing systems data locality multi-core processors memory systems

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：