Skip to content

Latest commit

 

History

History

fs

Verified NFS server

This proof is broken down into the following layers, organized top-down:

Layer Functionality
dir Directories and top-level NFS API.
typed Inode allocation, and hiding invariant from all lower layers.
byte Byte-based files of variable size.
block Block-based files, from gathering up blocks by Pos per inode from indirect layer.
indirect Indirect blocks accessed by abstract position Pos. Organized into a tree rooted at an inode.
inode High-level inodes with efficient in-memory access and on-disk encoding. Block allocation.
jrnl Assumed transaction-system interface.

Some interesting libraries implementing parts of the file system include:

Library Purpose
nfs spec Definitions to define the NFS specification. Also see postconditions in dir_fs.dfy.
mem_dirent In-memory, lazily read directories with in-place updates.
mem_inode In-memory inodes with in-place updates.
pos Organizes blocks in inode into a tree, determining how indirect each block is interpreted.
super Static file-system configuration and disk layout.