scholarly journals Verifying correctness of persistent concurrent data structures: a sound and complete method

2021 ◽  
Author(s):  
John Derrick ◽  
Simon Doherty ◽  
Brijesh Dongol ◽  
Gerhard Schellhorn ◽  
Heike Wehrheim
Keyword(s):  
Data Structures ◽  
Formal Proof ◽  
Sequential Data ◽  
Proof Technique ◽  
Concurrent Data Structures ◽  
Automated Translation ◽  
Correctness Criterion ◽  
Persistent Memory ◽  
Non Volatile Memory ◽  
Translation Procedure

AbstractNon-volatile memory (NVM), aka persistent memory, is a new memory paradigm that preserves its contents even after power loss. The expected ubiquity of NVM has stimulated interest in the design of persistent concurrent data structures, together with associated notions of correctness. In this paper, we present a formal proof technique for durable linearizability, which is a correctness criterion that extends linearizability to handle crashes and recovery in the context ofNVM.Our proofs are based on refinement of Input/Output automata (IOA) representations of concurrent data structures. To this end, we develop a generic procedure for transforming any standard sequential data structure into a durable specification and prove that this transformation is both sound and complete. Since the durable specification only exhibits durably linearizable behaviours, it serves as the abstract specification in our refinement proof. We exemplify our technique on a recently proposed persistentmemory queue that builds on Michael and Scott’s lock-free queue. To support the proofs, we describe an automated translation procedure from code to IOA and a thread-local proof technique for verifying correctness of invariants.

scholarly journals An Implementation of The Scalable and Correct Time-Stamped Stack

2019 ◽  
Author(s):  
Henry Jetmundsen ◽  
Patrick Thompson ◽  
Matthew Villegas ◽  
Justin Zabel
Keyword(s):  
Experimental Data ◽  
Data Structures ◽  
Software Transactional Memory ◽  
Proof Technique ◽  
Comparative Performance ◽  
New Approach ◽  
Concurrent Data Structures ◽  
Weak Ordering ◽  
Time Stamps ◽  
Generic Proof

Many concurrent data structures impose real time ordering over their elements. This is needed only if the insertions modifying the data structure ran sequentially. A new approach using time stamps was proposed to avoid unneeded ordering. Our implementation is based on that time-stamped (TS) stack. Concurrent insertions can be left unordered and then ordered as necessary at removal. Because of this weak ordering, using linearizability to establish correctness is not possible. The original paper presents a new approach to proving correctness for the TS stack. This proof technique is a new, generic proof for correctness on concurrent data structures. In this paper, we highlight our general approach to re-implementing the Time-Stamped stack, discuss our modifications made to to the stack, give an overview of our implementation of a stack using software transactional memory, and analyze comparative performance graphs based on our experimental data.

Octopus + : An RDMA-Enabled Distributed Persistent Memory File System

2021 ◽  
Vol 17 (3) ◽  
pp. 1-25
Author(s):  
Bohong Zhu ◽  
Youmin Chen ◽  
Qing Wang ◽  
Youyou Lu ◽  
Jiwu Shu
Keyword(s):  
High Speed ◽  
High Performance ◽  
File System ◽  
Direct Memory Access ◽  
File Systems ◽  
Distributed File Systems ◽  
Persistent Memory ◽  
Memory Modules ◽  
Non Volatile Memory ◽  
Volatile Memory

Non-volatile memory and remote direct memory access (RDMA) provide extremely high performance in storage and network hardware. However, existing distributed file systems strictly isolate file system and network layers, and the heavy layered software designs leave high-speed hardware under-exploited. In this article, we propose an RDMA-enabled distributed persistent memory file system, Octopus + , to redesign file system internal mechanisms by closely coupling non-volatile memory and RDMA features. For data operations, Octopus + directly accesses a shared persistent memory pool to reduce memory copying overhead, and actively fetches and pushes data all in clients to rebalance the load between the server and network. For metadata operations, Octopus + introduces self-identified remote procedure calls for immediate notification between file systems and networking, and an efficient distributed transaction mechanism for consistency. Octopus + is enabled with replication feature to provide better availability. Evaluations on Intel Optane DC Persistent Memory Modules show that Octopus + achieves nearly the raw bandwidth for large I/Os and orders of magnitude better performance than existing distributed file systems.

NVLSM: A Persistent Memory Key-Value Store Using Log-Structured Merge Tree with Accumulative Compaction

2021 ◽  
Vol 17 (3) ◽  
pp. 1-26
Author(s):  
Baoquan Zhang ◽  
David H. C. Du
Keyword(s):  
Computer Systems ◽  
Memory Storage ◽  
Low Latency ◽  
Latency Data ◽  
Persistent Memory ◽  
Write Amplification ◽  
Non Volatile Memory ◽  
Data Persistence ◽  
Average Latency ◽  
Volatile Memory

Computer systems utilizing byte-addressable Non-Volatile Memory ( NVM ) as memory/storage can provide low-latency data persistence. The widely used key-value stores using Log-Structured Merge Tree ( LSM-Tree ) are still beneficial for NVM systems in aspects of the space and write efficiency. However, the significant write amplification introduced by the leveled compaction of LSM-Tree degrades the write performance of the key-value store and shortens the lifetime of the NVM devices. The existing studies propose new compaction methods to reduce write amplification. Unfortunately, they result in a relatively large read amplification. In this article, we propose NVLSM, a key-value store for NVM systems using LSM-Tree with new accumulative compaction. By fully utilizing the byte-addressability of NVM, accumulative compaction uses pointers to accumulate data into multiple floors in a logically sorted run to reduce the number of compactions required. We have also proposed a cascading searching scheme for reads among the multiple floors to reduce read amplification. Therefore, NVLSM reduces write amplification with small increases in read amplification. We compare NVLSM with key-value stores using LSM-Tree with two other compaction methods: leveled compaction and fragmented compaction. Our evaluations show that NVLSM reduces write amplification by up to 67% compared with LSM-Tree using leveled compaction without significantly increasing the read amplification. In write-intensive workloads, NVLSM reduces the average latency by 15.73%–41.2% compared to other key-value stores.

Sign in / Sign up

Export Citation Format

Share Document