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 considers the collection of permanent (non-intermittent) changes made by a process, when viewed at the end of its execution. Consistency requirements for such collections of changes are specified as predicates over the atomic actions of a process. Set consistency generalizes self-cancellation, a standard consistency requirement for long-running transactions, where failed processes are responsible for undoing any partially completed work. Set consistency can also express strictly stronger requirements, such as mutual exclusion or dependency.
We show that the set consistency verification problem for processes is co-NP complete and present an algorithm for verifying set consistency by reduction to propositional validity. We have implemented this algorithm and demonstrate the value and tractability 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.
To appear in Proceedings of the IEEE/ACM 2007 International Conference on Automated Sotware Engineering (ASE '07), November 2007.
The documents referenced below are included by the contributing authors as a means to ensure timely dissemination of scholarly and technical work on a non-commercial basis. Copyright and all rights therein are maintained by the authors or other copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons downloading these documents will adhere to the terms and constraints invoked by each author's copyright.
PDF PostScript Source Code © 2007.