Greg Neverov: Software Transactional Memory for F#

Greg Neverov (of active patterns fame) has placed an implementation of Software Transactional Memory for F# up on hubFS. Here's the description:

I have written a library for using software transactional memory in F#. The library exposes memory transactions as a monad using F#’s new computation expression feature. It can be downloaded here.

Software transactional memory (STM) is an approach to concurrent programming that avoids the use of traditional, error-prone locks to control access to shared memory. Instead of using locks a programmer specifies sections of code that will make atomic changes to shared memory.

The design and implementation of this F# library is blatantly copied from the paper Composable Memory Transactions. I am enormously grateful to the authors of this paper whose clear and precise explanation made the implementation of this complicated piece of software almost trivial.

The low-level STM machinery is implemented in the file stm.cs. It is written in C# mainly because I was working off existing code I’d written some time ago, but there’s no reason why it could not be written in F#. It is all managed code and internally uses monitors for synchronization. It currently uses a very coarse grained lock meaning that only one transaction can commit at once and every waiting thread is resumed when a transaction completes, but this can be improved with more work. The implementation follows the description in the paper.

The F# monadic interface is in the file stm.fs. It imports definitions from the C# assembly and defines the monad type Stm<'a> with corresponding builder class to enable computation expression syntax. An issue with the implementation of STM systems is how to access the transaction log to make reads and writes during a transaction. Two common approachs are to use thread-local storage which is slow, or implicitly pass the transaction log as an extra parameter to every function, which requires code generation. The advantage of using computation expressions (or monadic do notation) is that the transaction log is explicitly passed between functions by the programmer’s code, thereby avoiding compiler modification, but also avoiding the need for the programmer to manually manage the transaction log parameter passing scheme as well.

Fantastic stuff Greg!