Categories: filesystems

Filesystems

With others, I am working on formally specifying and verifying filesystems (eg SibylFS). I am also working on a verified filesystem implementation called “ImpFS”.

ImpFS

ImpFS is a new filesystem based on B-trees and persistent logs. The main “management” page (with links to all the subproject etc) is here: https://tomjridge.github.io/ocamldocs/

Some example components:

Title	Description
tjr_btree	tjr_btree is a Copy-on-Write and mutate-in-place implementation of a B-tree-like on-disk datastructure.
tjr_kv	tjr_kv is a key-value store for OCaml
mini-fs	Frontend filesystem components, including FUSE bindings, networking etc.
tjr_impfs	The ImpFS filesystem

“The ImpFS filesystem”, a talk for OCaml’20, part of ICFP’20:

A video showing the current state of ImpFS:

Recent presentations and posters

A key-value store for OCaml, presented at ML’19, colocated with ICFP’19. See “related links” below for article and slides.
I discussed ImpFS at a recent VeTSS meeting. The related poster is reproduced below.

Older work: SibylFS

SibylFS is a formal model of POSIX-like and real-world filesystems, and simultaneously a test oracle which can be used to check real-world traces of filesystem behaviour. The main page for SibylFS is here.