Using semantic correctness in multidatabases to achieve local autonomy, distribute coordination, and maintain global integrity

A multidatabase poses the following four, often contradictory, requirements . First, local databases require both design autonomy to accommodate the di verse legacy nature of the local databases, and execution autonomy to ensur e that local transactions are not unduly blocked by global transactions. Se cond, management of global transactions must be distributed to avoid bottle necks and to tolerate failure in the global database. Third, both local and global integrity constraints must be maintained. Finally, concurrent proce ssing of transactions requires that execution histories be correct, an obje ctive traditionally achieved with serializability. Although alternate forms of correctness have been proposed, none of the solutions advanced to date has simultaneously achieved all four requirements. We propose a transaction processing model that uses a semantics-based notion of correctness to achi eve all four requirements simultaneously for applications that satisfy a ce rtain set of properties. The support required for global transactions forms a separate layer at each site that respects both design autonomy and execu tion autonomy. Global transactions are managed at each site via a successor set mechanism so that site and communication failures do not impede transa ctions at operating sites. Semantic correctness encompasses three propertie s: ensuring that local and global integrity constraints are maintained, tha t transactions output consistent data and that all partially executed trans actions can complete. A fourth property ensures that the successor set desc ription is a valid refinement of the specification. These four properties m ust be proved for applications executed by our model. We show how model che cking can automate, in part, the verification of the properties. (C) 2000 E lsevier Science Inc. All rights reserved.