Sosp 2017 论文选读

Posted by Maxul's Sketch Notes on November 7, 2017

2017年的SOSP大会在中国上海举办。

Hyperkernel: Push-Button Verification of an OS Kernel

University of Washington

  • 针对内核的形式化验证工作，三个关键思想：对内核接口进行限制，避免无限循环和递归；对内核和用户态地址空间分开分析，简化虚拟内存的分析；使用LLVM IR中间表示作为分析对象。
  • 内核数据结构丰富，运行时不变量多，都无疑成为挑战。作者将spec编写量作为主体工作量，Z3为其节省不少工作。
  • Hyperkernel的设计借鉴了Dune、exokernel和seL4。借助虚拟化设计， 内核和用户程序使用不同页表（VMX root and non-root），所有的系统调用、定时器抢占、异常和中断都能以Hypercall的方式拦截。虚拟化模型对简化了内核中断路径验证。
  • 类似exokernel，用户对资源进行自行管理，就可以很好地和内核区分，乃至可以用数组结构来方便SMT求解，避免对内核链表和树的求解（reason）。
  • 对于用户空间的求解，其移植了用户文件系统和网络协议栈（用户态e1000和lwIp），用户态程序模拟用Dune机制实现。
  • 个人认为，该工作结合了虚拟化和形式化验证工作。

Multiprogramming a 64 kB Computer Safely and Efficiently

Stanford University

  • 单片机在硬件特性和内存资源上都比较有限。因此不支持错误隔离、虚拟内存和灵活并发等特性。
  • Tock支持微处理器上多道程序，使用Rust实现类型安全，支持SFI、内存保护等。
  • 个人解读：从标题看，该文章在内存有限的单片机上实现了进程抽象，该抽象是当前嵌入式系统所缺乏的。x86的进程地址空间隔离用MMU来实现，MCU可以用MPU来实现。
  • 该团队对TinyOS, FreeRTOS和RIOT都进行了比较论述。

Scaling a file system to many cores using an operation log

MIT CSAIL and VMware

  • 文件系统的设计中，对于多核的可扩展性和磁盘的高吞吐率而言，一直是个棘手的问题。原因和文件系统在内存子系统的缓存机制、更新设计有关。
  • ScaleFS对每个核的操作进行日志，将磁盘文件系统和内存文件系统分离，对于“高并发的数据结构”而言，避免“可交换性操作”带来的cache冲突，由此提高可扩展性，即文件系统操作不随着核数的增加导致吞吐率的下降。
  • 该设计将多核的更新记录延迟到fsync时再合并操作，为保证其正确性，使用了不少技术（如timestamping linearization points）。
  • 其实验环境为80核，吞吐率同单核单磁盘Linux ext4相当。

ffwd: delegation is (much) faster than you think

Sepideh Roghanchi, Jakob Eriksson, Nilanjana Basu (University of Illinois at Chicago)

  • 多核情况下，通常对共享内存的互斥使用锁机制，带来的影响不可小覰。
  • 本文提出的设计证明，代理（使用一个对象完成对critical section的操作）的使用效果远胜过现有任何工作（自旋锁、消息锁、RCU、STM和无锁设计）。
  • fast, fly-weight delegation (ffwd)在吞吐率和性能上都超越现有的10倍，在哈希表、二叉树、链表等数据结构上可扩展性一流。

Komodo: Using verification to disentangle secure-enclave hardware from software

Andrew Ferraiuolo (Cornell University); Andrew Baumann, Chris Hawblitzel (Microsoft Research); Bryan Parno (Carnegie Mellon University)

  • Intel SGX用硬件来保护用户态软件，使用来硬件加密技术，但不好升级。
  • 本文希望用TZ技术，实现对用户态并发的可执行体的隔离、验证，其内存加密、硬件空间隔离和验证“委托”给来一个monitor，使用形式化验证工具来验证其功能正确性。
  • 贡献：软件实现enclave；形式化模型；对原型验证并且和SGX相比性能可观；证明软件可比硬件进化更快的证据（一旦发现问题，硬件演进比软件慢很多）。

KV-Direct: High-Performance In-Memory Key-Value Store with Programmable NIC

USTC and Microsoft Research

  • 在分布式数据中心中，In-memory key-value store扮演重要角色。
  • 分布式条件下，使用NIC作为通信介质，而现代可编程的NIC可借助RDMA对内存直接访问。主存和NIC都是PCI设备。
  • 提升网卡通信速率，给内存数据库提速是本文要解决的问题。
  • 表3的bottleneck一栏很有参考价值。

NOVA-Fortis: A Fault-Tolerant Non-Volatile Main Memory File System

UC San Diego

  • 用非易失性内存做block设备实现文件系统，兼具mmap页表操纵属性和文件系统功能。
  • 贡献点：
1. 在NVMM上实现容错文件系统；
2. 实现一种原子更新算法，达到检错和修复目的；
3. mmap语义；
4. 对缺陷进行量化描述，并提出相应对策；
5. 对性能和损失进行量化。