Modular Integration of Crashsafe Caching into a Verified Virtual File System Switch
Modular Integration of Crashsafe Caching into a Verified Virtual File System Switch
复制标题
将崩溃安全缓存模块化集成到经过验证的虚拟文件系统交换机中
DOI：
10.1007/978-3-030-63461-2_12
复制
发表时间：
2020
期刊：
影响因子：
--
通讯作者：
W. Reif
中科院分区：
文献类型：
--
作者：
S. Bodenmüller;G. Schellhorn;W. Reif
在开发文件系统时，缓存是实现高性能实现的常用技术。将回写缓存集成到文件系统中不仅会影响功能正确性，还会影响文件系统的崩溃安全属性。由于部分写入数据仅存储在易失性存储器中，因此在集成回写缓存时必须特别小心，以确保运行操作期间的断电导致一致的状态。本文展示了如何非保序缓存可以添加到一个虚拟文件系统交换机（VFS），并给出了一个新的碰撞安全标准匹配的特点，这样的缓存。如果将断电分解为单个文件，则可以通过构造替代运行来解释断电，其中自该文件上次同步以来的所有写入都写入了前缀。VFS缓存已被模块化集成到Flashix中，Flashix是一种经过验证的闪存文件系统，该扩展的功能正确性和崩溃安全性已通过交互式定理证明器KIV进行验证。
When developing file systems, caching is a common technique to achieve a performant implementation. Integrating write-back caches into a file system does not only affect functional correctness but also impacts crash safety properties of the file system. As parts of written data are only stored in volatile memory, special care has to be taken when integrating write-back caches to guarantee that a power cut during running operations leads to a consistent state. This paper shows how non-order-preserving caches can be added to a virtual file system switch (VFS) and gives a novel crash-safety criterion matching the characteristics of such caches. Broken down to individual files, a power cut can be explained by constructing an alternative run, where all writes since the last synchronization of that file have written a prefix. VFS caches have been integrated modularly into Flashix, a verified file system for flash memory, and both functional correctness and crash-safety of this extension have been verified with the interactive theorem prover KIV.
登录
查看更多内容
虚拟文件系统交换机的验证
DOI：
10.1007/978-3-642-54108-7_13
发表时间：
2013
期刊：
12th IEEE International Conference on Engineering Complex Computer Systems (ICECCS 2007)
影响因子：
--
作者：
G. Ernst;G. Schellhorn;Dominik Haneberg;J. Pfähler;W. Reif
通讯作者：
W. Reif
DOI：
10.1007/s10009-014-0308-3
发表时间：
2015-11-01
影响因子：
1.5
作者：
Ernst, Gidon;Pfaehler, Joerg;Reif, Wolfgang
通讯作者：
Reif, Wolfgang
在经过验证的闪存文件系统内部：事务和垃圾收集
DOI：
10.1007/978-3-319-29613-5_5
发表时间：
2015
期刊：
影响因子：
--
作者：
G. Ernst;J. Pfähler;G. Schellhorn;W. Reif
通讯作者：
W. Reif
带有子机的 ASM 的模块化、防碰撞改进
DOI：
10.1016/j.scico.2016.04.009
发表时间：
2016
期刊：
Sci. Comput. Program.
影响因子：
--
作者：
G. Ernst;J. Pfähler;G. Schellhorn;W. Reif
通讯作者：
W. Reif
Z 和 object-Z 的细化：基础和高级应用
DOI：
10.1002/stvr.237
发表时间：
2002
期刊：
Softw. Test. Verification Reliab.
影响因子：
--
作者：
P. Stevens
通讯作者：
P. Stevens