Ensuring Consistency in Long Running Transactions

[摘要] Flow composition languages permit the construction of long-running 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 co-NP 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 thepracticality of our approach.

[发布机构] UCLA Henry Samueli School of Engineering and Applied Science

[学科分类] 计算机科学（综合）