Modular rollback through control logging: a pair of twin functional pearls

Abstract

We present a technique, based on the use of first-class control operators, enabling programs to maintain and invoke rollback logs for sequences of reversible effects. Our technique is modular, in that it provides complete separation between some library of effectful operations, and a client, "driver" program which invokes and rolls back sequences of these operations. In particular, the checkpoint mechanism, which is entirely encapsulated within the effect library, logs not only the library's effects, but also the client's control state. Thus, logging and rollback can be almost completely transparent to the client code.