Specifying a Realistic File System

Specifying a Realistic File System
复制标题

指定实际的文件系统

DOI：
--
复制
发表时间：
2015
期刊：
MARS
影响因子：
--
通讯作者：
Toby C. Murray
Toby C. Murray
中科院分区：
--
文献类型：
--
作者：
Sidney Amani;Toby C. Murray

文献摘要

被引文献

相似文献

我们介绍了BilbyFS的正确性规范中最有趣的元素，这是一个高性能的Linux闪存文件系统。BilbyFS规范支持异步写入，这一特性已被多个文件系统验证项目忽略，并已用于验证BilbyFS的fsync()C实现的正确性。它利用非决定论的简洁性，浅层嵌入到高阶逻辑中。
We present the most interesting elements of the correctness specification of BilbyFs, a performant Linux flash file system. The BilbyFs specification supports asynchronous writes, a feature that has been overlooked by several file system verification projects, and has been used to verify the correctness of BilbyFs’s fsync() C implementation. It makes use of nondeterminism to be concise and is shallowly-embedded in higher-order logic.