Proving the Correctness of NVM Recovery under Strand Persistency Model

• Item type: Trans(1)
• 公開日: 2021-09-30
• タイトル: Proving the Correctness of NVM Recovery under Strand Persistency Model
• タイトル / 言語: en
• タイトル: Proving the Correctness of NVM Recovery under Strand Persistency Model
• 言語: eng
• キーワード / 主題Scheme: Other
• キーワード / 主題: [発表概要, Unrefereed Presentatin Abstract]
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_6501
• 資源タイプ: journal article
• 著者所属: Waseda University
• 著者所属: Waseda University
• 著者所属(英): en
• 著者所属(英): Waseda University
• 著者所属(英): en
• 著者所属(英): Waseda University
• 著者名: Jixin, Han; Keiji, Kimura
• 著者名(英): Jixin, Han; Keiji, Kimura
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: Emerging byte accessible non-volatile memory (NVM) technologies can promise durability like existing file systems even at an unexpected crash, as well as the competitive performance with DRAM. Similar to the memory consistency problems, appropriate order of memory access operations and cache eviction operations, or persistent operations, must be considered to guarantee both program recoverability and performance with the underlying persistency model. Several persistency models have been proposed in the literature. The strand persistency model, which potentially shows higher performance than the epoch persistency model, has more relaxed rules to exploit more parallelism. However, no formal proof that ensures the correctness of the recovery from a crash has been shown. To close this gap, we use buffered durable linearizability as our correctness criterion as an extension of the traditional linearizability. We first propose an operational semantics of the strand persistency model to formalize the generation of a history and buffered durable linearizability under a concurrent environment. Then, we validate the correctness of the implementation of a target concurrent and durable data structure by proving any history generated from it meets such the central correctness condition. Such a criterion is served as a specification that guarantees the recoverability of concurrent shared objects to a legal state in the case of failure. We show the feasibility of the proposed technique by applying it to a durable queue as a case study.
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: Emerging byte accessible non-volatile memory (NVM) technologies can promise durability like existing file systems even at an unexpected crash, as well as the competitive performance with DRAM. Similar to the memory consistency problems, appropriate order of memory access operations and cache eviction operations, or persistent operations, must be considered to guarantee both program recoverability and performance with the underlying persistency model. Several persistency models have been proposed in the literature. The strand persistency model, which potentially shows higher performance than the epoch persistency model, has more relaxed rules to exploit more parallelism. However, no formal proof that ensures the correctness of the recovery from a crash has been shown. To close this gap, we use buffered durable linearizability as our correctness criterion as an extension of the traditional linearizability. We first propose an operational semantics of the strand persistency model to formalize the generation of a history and buffered durable linearizability under a concurrent environment. Then, we validate the correctness of the implementation of a target concurrent and durable data structure by proving any history generated from it meets such the central correctness condition. Such a criterion is served as a specification that guarantees the recoverability of concurrent shared objects to a legal state in the case of failure. We show the feasibility of the proposed technique by applying it to a durable queue as a case study.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AA11464814
• 書誌情報: 情報処理学会論文誌プログラミング（PRO）; 巻 14, 号 4, p. 5-5, 発行日 2021-09-30
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 1882-7802
• 出版者 / 言語: ja
• 出版者: 情報処理学会