[TOC]
tjr_btree is a B-tree library written for OCaml, and based on code extracted from an Isabelle formalization.
Library structure:
System structure:
Type dependencies:
- The Isabelle code can be found here.
- Online OCamldoc documentation can be found here.
- Introductory examples, including a simple on-disk key-value store, can be found in the examples directory.
- To install, try the Dockerfile (
docker build .) and then to build locally, strip the "RUN" prefix from the relevant Dockerfile lines and use opam pin.
This code implements a B-tree. The implementation can be copy-on-write, or mutate-in-place.
The B-tree supports the usual operations: find, insert, delete.
In addition, there is an insert_many operation for inserting
multiple key-value pairs at once. This operation is more efficient
than repeatedly inserting. It is typically used when higher-level
operations are cached and then flushed all at once.
The routines are fully parameterized (e.g., by key and value type, key order, store type etc). It is easy to have many B-trees using the same store, even operating concurrently (although individual B-trees must be updated sequentially at the moment).
The core is implemented in small-step operational style, with each disk access corresponding to a separate step. Thus, it should be feasible to introduce very fine-grained concurrency by interleaving individual steps of each operation (where multiple operations execute on different B-trees).
The core code is written in Isabelle/HOL and exported to OCaml (although it could easily be implemented in any language because the routines are very "concrete"). This repository contains the OCaml wrapper round the core OCaml code extracted from Isabelle.
The easiest way to install is via opam, pinning the github repos. See the Dockerfile.
In your code, use:
open Tjr_btree
open Tjr_btree.Btree_intf
open Tjr_btree_examples
After installing, you can run the examples by typing:
make runThe output should look something like:
From opam, there are no dependencies except what is required by the following libraries.
| Dependency | Comment |
|---|---|
| isa_btree | Base OCaml defns extracted from Isabelle |
| Dependency | Comment |
|---|---|
| bin_prot, ppx_bin_prot | marshalling via bin_prot, for testing |
| extunix? | fsync |
All sync-ed states are persistent on disk (imagine that blocks are written once and then never mutated), so operations such as "snapshot" are almost trivial (assuming copy-on-write). FIXME clarify
ImpFS is a project to build an advanced high-performance filesystem. tjr_btree is one of the core libraries used by ImpFS.
FIXME to do