祝贺IPADS实验室两篇论文被第27届“ACM操作系统原理大会”(SOSP: ACM Symposium on Operating Systems Principles)接收

SOSP是计算机系统领域的最高水平会议，将于2019年10月27-30日在加拿大安大略省召开。本次大会共接收38篇论文，接收率仅为13.8％，能在顶级会议上从数百篇优秀的投稿中脱颖而出，命中两篇论文，是相当不容易的事情，而至此，IPADS实验室已经连续五年在计算机系统最高水平会议上发表论文。

论文细节如下： 

• Mo Zou, Haoran Ding, Dong Du, Ming Fu, Ronghui Gu and Haibo Chen. Using Concurrent Relational Logic with Helpers for Verifying the AtomFS File System. Proceedings of the 27th ACM Symposium on Operating Systems Principles (SOSP '19). Huntsville, Ontario, October 27-30, Canada, 2019.
• Mingkai Dong, Heng Bu, Jifei Yi, Benchao Dong, Haibo Chen. Performance and Protection in the ZoFS User-space NVM File System. Proceedings of the 27th ACM Symposium on Operating Systems Principles (SOSP '19). Huntsville, Ontario, Canada, October 27-30, 2019.

【AtomFS】文件系统是存储和检索永久数据的基石，然而并发文件系统的设计和实现的复杂性使得其容易存在缺陷，从而不能在所有可能的并发执行下保证一致性。形式化验证是目前已知唯一的保证系统没有编程错误的方法，已有的验证文件系统的工作（FSCQ，COGENT，Yggdrasil，CIO-FSCQ等）展示了验证文件系统的可行性，然而这些工作都无法验证在多核上运行的并发文件系统。

本工作对并发程序精化验证的相关理论成果进行扩展，在定理证明工具 Coq 中设计并实现了支持帮助机制的并发精化验证框架，成功地验证了 AtomFS ，第一个形式化验证的并发文件系统。本工作证明了 AtomFS 接口（rename, mkdir 等）在任意并发环境下的功能正确性以及原子性。测试表明，与 ext4 等成熟文件系统相比，AtomFS 具有良好的多核扩展性，在运行实际的应用程序时能取得合理的性能。该工作是 IPADS 实验室与华为 OS 内核实验室以及哥伦比亚大学合作发表的工作，同时也是 IPADS 实验室继 BridgeX [PODC '19]（基于形式化验证的分布式共识算法的关系构建和优化移植）之后，在形式化验证领域的又一工作。

【ZoFS】非易失性内存技术（NVM）的出现正改变着文件系统的设计。NVM 的可字节寻址性，让用户态可以直接访问存储设备，进而使实现用户态文件系统成为可能。然而，为了保证安全和隔离性，现有的用户态文件系统设计均对 NVM 的使用进行了诸多限制，导致NVM的高性能无法被完全发挥。用户态文件系统 ZoFS 通过设计新的抽象，将文件系统的保护和管理职责分离，减少了不必要的性能开销，从而在用户态将NVM的性能发挥到极致。

该工作是 IPADS 实验室近年来继 VPM [SoCC '16]（NVM 虚拟化）、Cocytus [FAST '16]（基于抹除码和复制的高效高可用内存键值存储）、SyncShrink [FAST '16]（针对 CoW 虚拟磁盘同步放大的优化）， SoupFS [ATC '17] （高性能内核 NVM 文件系统）、Espresso [ASPLOS '18]（JVM 中 NVM 的高效拓展）、Pisces [ATC '19]（可拓展高性能 NVM 持久化内存事务）、EROFS [ATC '19]（与华为合作研制的面向资源稀缺设备只读压缩文件系统） 之后，在探索如何高效利用新型存储技术与提升存储和文件系统性能上的系列工作之一。

                        

                                            oFS第一作者董明凯                           AtomFS第一作者邹沫                  指导老师陈海波教授

（IPADS实验室供稿）

 

 

[ 返回 ]