WEKO3
アイテム
Durable Queue Implementations Built on a Formally Defined Strand Persistency Model
https://ipsj.ixsq.nii.ac.jp/records/213899
https://ipsj.ixsq.nii.ac.jp/records/21389919a9e3c9-4a8d-415e-9981-efb6316d122b
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
IPSJ-TPRO1405006.pdf (549.9 kB)
|
Copyright (c) 2021 by the Information Processing Society of Japan
|
|
| オープンアクセス | ||
| Item type | Trans(1) | |||||||||
|---|---|---|---|---|---|---|---|---|---|---|
| 公開日 | 2021-11-25 | |||||||||
| タイトル | ||||||||||
| タイトル | Durable Queue Implementations Built on a Formally Defined Strand Persistency Model | |||||||||
| タイトル | ||||||||||
| 言語 | en | |||||||||
| タイトル | Durable Queue Implementations Built on a Formally Defined Strand Persistency Model | |||||||||
| 言語 | ||||||||||
| 言語 | eng | |||||||||
| キーワード | ||||||||||
| 主題Scheme | Other | |||||||||
| 主題 | [通常論文] non-volatile memory, persistent memory, persistency model, buffered durable linearizability | |||||||||
| 資源タイプ | ||||||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_6501 | |||||||||
| 資源タイプ | journal article | |||||||||
| 著者所属 | ||||||||||
| Waseda University | ||||||||||
| 著者所属 | ||||||||||
| Waseda University | ||||||||||
| 著者所属(英) | ||||||||||
| en | ||||||||||
| Waseda University | ||||||||||
| 著者所属(英) | ||||||||||
| en | ||||||||||
| Waseda University | ||||||||||
| 著者名 |
Jixin, Han
× Jixin, Han
× Keiji, Kimura
|
|||||||||
| 著者名(英) |
Jixin, Han
× Jixin, Han
× Keiji, Kimura
|
|||||||||
| 論文抄録 | ||||||||||
| 内容記述タイプ | Other | |||||||||
| 内容記述 | Emerging byte accessible non-volatile memory (NVM), or persistent memory (PM), 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, due to the lack of formal definition of the strand persistency model, legality and recoverability of strand persistency based programs against system crashes have been abandoned. To address this, we first propose an operational semantics of the strand persistency model to formalize the behavior of a program, memory propagation, and history generation under a concurrent environment. Then, we investigate the durability of library implementations for concurrent objects equipped with strand primitives, and propose a correctness criterion that the implementations should preserve, originated from buffered durable linearizability. Finally, as a case study, we discuss two concurrent queue implementations and show how the proposed semantics and criterion capture both the durability and linearizability of implementations. ------------------------------ This is a preprint of an article intended for publication Journal of Information Processing(JIP). This preprint should not be cited. This article should be cited as: Journal of Information Processing Vol.29(2021) (online) ------------------------------ |
|||||||||
| 論文抄録(英) | ||||||||||
| 内容記述タイプ | Other | |||||||||
| 内容記述 | Emerging byte accessible non-volatile memory (NVM), or persistent memory (PM), 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, due to the lack of formal definition of the strand persistency model, legality and recoverability of strand persistency based programs against system crashes have been abandoned. To address this, we first propose an operational semantics of the strand persistency model to formalize the behavior of a program, memory propagation, and history generation under a concurrent environment. Then, we investigate the durability of library implementations for concurrent objects equipped with strand primitives, and propose a correctness criterion that the implementations should preserve, originated from buffered durable linearizability. Finally, as a case study, we discuss two concurrent queue implementations and show how the proposed semantics and criterion capture both the durability and linearizability of implementations. ------------------------------ This is a preprint of an article intended for publication Journal of Information Processing(JIP). This preprint should not be cited. This article should be cited as: Journal of Information Processing Vol.29(2021) (online) ------------------------------ |
|||||||||
| 書誌レコードID | ||||||||||
| 収録物識別子タイプ | NCID | |||||||||
| 収録物識別子 | AA11464814 | |||||||||
| 書誌情報 |
情報処理学会論文誌プログラミング（PRO） 巻 14, 号 5, 発行日 2021-11-25 |
|||||||||
| ISSN | ||||||||||
| 収録物識別子タイプ | ISSN | |||||||||
| 収録物識別子 | 1882-7802 | |||||||||
| 出版者 | ||||||||||
| 言語 | ja | |||||||||
| 出版者 | 情報処理学会 | |||||||||
