Categories: filesystems
Filesystems
With others, I am working on formally specifying and verifying filesystems.
SibylFS
So far, we have constructed a filesystem test oracle called SibylFS. The main page for SibylFS is here
ImpFS
We are working on a verified filesystem implementation, including a CoW B-tree library.
A recent poster talking about the different components is:
Many of these components 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)
- OCaml B-tree library (wrapper for
- 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
Note that these components in turn require other libraries (which are also available from GitHub).
A very simple set of commands to build many of these components (not
path_resolution or mini-fs) is:
https://github.com/tomjridge/tjr_imp_build_script
A collection of all ocamldoc documentation is: https://tomjridge.github.io/tjr_imp_build_script/