Ensuring Consistency in Long Running Transactions UCLA Computer Science Dept. Technical Report TR-070011
Jeffrey Fischer Rupak Majumdar · 2007
Flow composition languages permit the construction of longrunning transactions from collections of independent, atomic services. Due to environmental limitations, such transactions usually cannot be made to conform to standard ACID semantics. We propose set consistency, a powerful, yet intuitive, notion of consistency for long-running transactions. Set consistency specifications are written as predicates over the atomic actions of a process and require that the set of atomic actions executed along any system trace must satisfy the set consistency requirement. Set consistency generalizes cancellation semantics, a standard consistency requirement for long-running transactions, where failed processes are responsible for undoing any partially completed work, and can express strictly stronger requirements such as mutual exclusion or dependency. We believe that such predicates are both intuitive for developers and useful for representing real world constraints. We formalize a core calculus for representing long-running transactions, providing sequential and parallel composition, as well as exception-handling and compensation actions, within the language. We show that the set consistency verification problem for processes in our core language against consistency requirements given as boolean predicates is coNP complete and present an algorithm for verifying set consistency by reduction to propositional satisfiability. We have implemented this algorithm and demonstrate the value of our approach on three real-world case studies. In each case the consistency requirements can be verified within a second, demonstrating the practicality of our approach.