Coordinating concurrent development in distributed environments.

摘要

The thesis addresses concurrency control in distributed environments. The motivation behind this work is that traditional database system techniques do not apply well to distributed environments because the applications can tolerate some inconsistencies in the underlying database. The correctness criteria are weaker than those employed in traditional databases because of the settings in which these environments are used. This is acceptable because environments provide active users with a consistent view of the database even when the database as a whole is inconsistent. This thesis defines on-line edit linearizability, a concurrency control criterion for distributed environments. Establishing On-line Edit Linearizability guarantees that active users always see a consistent view of the database.;As a sample implementation of on-line edit linearizability, the thesis also describes the design and implementation of two integrated environments. These environments allow concurrent editing of interdependent software modules for writing specifications using the Z notation. First, the thesis describes ZED, a single-user incremental environment for Z. ZED supports a textual view of the specification document based on a topological sort of the inheritance graph of the formal objects maintained by the system. The inheritance graph of formal objects is a derived dependency graph and is a key implementation concept in ZED. The textual view of the generated specification document closely matches the styles adopted in documenting Z specifications. The thesis then describes MultiZED, a distributed environment for Z specifications. MultiZED is based on the client-server model of distributed computing. It uses ZED as the front end editor at client machines. Clients share Z documents and objects maintained by the server. MultiZED implements on-line edit linearizability which guarantees that the document will not become inconsistent when interdependent modules are concurrently modified.