Towards Model Checking Library for Persistent Data Structures

Persistent concurrent data structures, which allow concurrent access and store critical data into byte-addressable non-volatile memory (NVM) to keep them beyond system crashes, are attractive. However, they are complicated and hard to be confident in the correctness of them because 1) cache and regi...

Full description

Saved in:
Bibliographic Details
Main Authors: Iiboshi, Hiroyuki, Ugawa, Tomoharu
Format: Conference Proceeding
Language:English
Subjects:
Computer crashes
Data models
Data structures
Libraries
Load modeling
Model checking
non volatile memory
Nonvolatile memory
persistent data structure
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Persistent concurrent data structures, which allow concurrent access and store critical data into byte-addressable non-volatile memory (NVM) to keep them beyond system crashes, are attractive. However, they are complicated and hard to be confident in the correctness of them because 1) cache and registers are expected to remain volatile, and 2) cache flush instructions are reordered with load and store instructions in accordance with the memory model of the system. This paper provides a design of a model checking library, named MMLib-NVM, which is useful to verify persistent concurrent data structures that run on hardware with a weak memory model and non-volatile memory. The library is for the SPIN model checker. MMLib-NVM allows the users to develop models of their data structures without considering the memory model and behaviour of NVM, besides explicit memory barriers and cache flush instructions. We implemented a prototype of MMLib-NVM and investigated a property derived from durable linearisability of a persistent lock-free queue, the durable queue, of Friedman et al. against the sequential consistency and total store ordering memory models by model checking using MMLib-NVM.
ISSN:2575-257X
DOI:10.1109/NVMSA.2018.00032