[Haskell-cafe] Announcing Halfs, a Haskell Filesystem
ijones at syntaxpolice.org
Wed Apr 12 18:43:54 EDT 2006
Halfs is a filesystem implemented in the functional programming
language Haskell. Halfs can be mounted and used like any other Linux
filesystem, or used as a library. Halfs is a fork (and a port) of the
filesystem developed by Galois Connections.
We've created a virtual machine to make using Halfs extremely easy.
You don't need an extra partition or a thumb drive, or even Linux
(Windows and Mac OS can emulate the virtual machine). For the
impatient, go to the quick start:
The Halfs web page is here:
In the course of developing a web server for an embedded operating
system, Galois Connections had need of a filesystem which was small
enough to alter to our needs and written in a high-level language so
that we could show certain high assurance properties about its
behavior. Since we had already ported the Haskell runtime to this
operating system, Haskell was the obvious language of choice. Halfs is
a port of our filesystem to Linux, with some modifications.
High assurance development is a methodology for creating software
systems that meet rigorously-defined specifications with a high degree
of confidence. That methodology comprises tools and practices. Its
goal is to produce such systems reliably and effectively, with an
ordinary degree of developer effort.
Haskell is particularly well-suited to high assurance development. It
is a high-level, fully-expressive, pure, functional language, with a
powerful type system. One of the obligations of high assurance
development is the demonstration of strong correspondence between
high-level executable models and the eventual implementation. Haskell
supports this directly: it can describe systems all the way from
high-level executable models through to system implementations. The
fact that Haskell is pure comes from its mathematical basis, and means
that, by default, a function does not interfere with other
functions. The type system is an automatic and scalable proof engine
that can encode and enforce desirable properties. Together, these
features allow the correctness of complex systems to be established,
making Haskell ideal for high assurance development.
The question was whether Haskell is well suited as the implementation
language for a filesystem, which involves fixed sized buffers, lots of
IO, and binary data structures. Though correctness is much more
important to us than performance, we hoped that a Haskell filesystem
would have acceptable performance, and that writing such low-level
code would not be awkward or error-prone.
We have developed a filesystem, Halfs, which aims to answer the above
questions. One may mount a Halfs filesystem in Linux using the FUSE
(Filesystem in Userspace) kernel module. We have created two new
monads, FSRead and FSWrite which restrict the IO monad to reading and
writing operations respectively. For performance, Halfs uses efficient
mutable arrays for block IO, as well as caching for blocks and inodes.
More information about the Haskell-Cafe