Joint work with Vincent Danos and Jean Krivine
A distributed transaction is a computation where several agents agree on a common action. Such agents normally do not have a global view of the state space and therefore must come to agreement by local (typically one-to-one) interactions. When modelling such behaviour, it is normally straightforward to guarantee soundness – a transaction occurs only if the individual agents satisfy the correct local requirements. Completeness is often much more difficult; indeed, the existence of a possible computation leading to the required global state does not guarantee that such a state will be reached. For instance, the agents may deadlock while racing to obtain the necessary shared resources. Completeness is normally achieved by including explicit backtracking mechanisms in the model.
We shall discuss how to model distributed transactions in such models by avoiding ad-hoc implementations of backtracking. The solution is described at a general categorical level, meaning that it can be exploited in process calculi, Petri nets and graph transformation systems alike. The main underlying structure is a factorisation system which allows a computation to be broken up into an irreversible component followed by a reversible component. The construction is proved to be correct by exhibiting a certain equivalence of categories. In the concrete case of Petri nets, the construction can be visualised nicely by utilising string diagrams.