Modular Rollback through Control Logging

摘要

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. This separation of concerns manifests itself nicely when we must implement software with sophisticated error handling. We illustrate with two examples that exploit the architecture to disentangle some core parsing task from its error management. The parser code is completely separate from the error-correction code, although the two components are deeply intertwined at run time.