TxForest: A DSL for Concurrent Filestores

TL;DR

TxForest introduces a domain-specific language that simplifies managing concurrent filestores with serializable transactions, formal verification, and an OCaml prototype for practical applications.

Contribution

It presents TxForest, a new DSL for filestores that offers a simpler API, optimistic concurrency control, formal proofs of serializability, and a practical OCaml implementation.

Findings

Formalized TxForest in a core calculus

Proved serializability of transactions

Built practical applications with OCaml prototype

Abstract

Many systems use ad hoc collections of files and directories to store persistent data. For consumers of this data, the process of properly parsing, using, and updating these filestores using conventional APIs is cumbersome and error-prone. Making matters worse, most filestores are too big to fit in memory, so applications must process the data incrementally while managing concurrent accesses by multiple users. This paper presents Transactional Forest (TxForest), which builds on earlier work on Forest to provide a simpler, more powerful API for managing filestores, including a mechanism for managing concurrent accesses using serializable transactions. Under the hood, TxForest implements an optimistic concurrency control scheme using Huet's zippers to track the data associated with filestores. We formalize TxForest in a core calculus, develop a proof of serializability, and describe our OCaml prototype, which we have used to build several practical applications.