Categories: filesystems

Filesystems

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

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.

Current work

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
tjr_minifs	Compositional file system components, including FUSE bindings, networking etc.
tjr_impfs	The ImpFS high-performance verified filesystem

These components, and many others, are available from github:

https://github.com/tomjridge/isa_btree/ - Isabelle definitions of the B-tree routines
https://github.com/tomjridge/tjr_btree/ - OCaml B-tree library (wrapper for isa_btree)
https://github.com/tomjridge/tjr_mem_queue/ - In-memory message queue
https://github.com/tomjridge/tjr_lru_cache/ - LRU cache
https://github.com/tomjridge/tjr_pcache/ - A persistent (on-disk) cache
https://github.com/tomjridge/tjr_kv/ - A key/value store
https://github.com/tomjridge/path_resolution/ - Formal model of path resolution
https://github.com/tomjridge/mini-fs/ - Various filesystem routines, FUSE bindings, in-memory filesystem, network filesystem client/server implementation etc
ImpFS - to be released shortly!

Note that these components in turn require other libraries (which are also available from GitHub).

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.