AbstractsComputer Science

As a technique to ensure absence of undesired interference in transactional computations, Concurrency Control (CC) guarantees logical data consistency via providing transaction isolation, thus contributing to their dependability. However, single-version CC, which requires that a transaction system always works on the current version of a data item, may introduce unpredictable delays for real-time transactions because of unbounded blocking time which may cause deadline misses. Compared to single-version CC (current value of a data item is available but the historical values are overwritten and not accessible) mechanism, multi-version Concurrency Control (MVCC, historical values of a data item are maintained in a version list and accessible) mechanisms have several advantages. The benefit of multiple versions for concurrency control is helping the scheduler avoid rejecting operations, which could improve the concurrency for real-time transaction systems. Because transactions are less likely to be blocked using MVCC, timeliness could be improved. Transaction isolation levels, out of which the serializable one is the highest, control the degree of interference-freedom of concurrent transactions. Instead of serializable isolation, some MVCC mechanisms are known to achieve a relaxed level of isolation. In order to select an appropriate MVCC mechanism that guarantees both timeliness and an acceptable level of isolation for a given transaction set, trade-off analysis between isolation and timeliness is necessary. However, even though approaches have been proposed to analyze timeliness and isolation together, they only focus on lock-based single-version concurrency control algorithms, not on MVCC. In this thesis, we focus on modeling multi-version based real-time transaction system as a network of timed automata, and verify the consistency of the tradeoff transaction timeliness and isolation in UPPAAL. We propose a modular modeling approach to model real-time multi-version transaction systems by reusing and extending set of basic blocks. The proposed approach not only reduces the modeling efforts, but also enables easy adjustment for adapting current MVCC mechanism to another. Assuming a given transaction set, we model three MVCC algorithms including multi-version Timestamp Ordering, a variant of multi-version Two-Phase locking and a Two-Version Priority Ceiling Protocol, and verify both timeliness and isolation level. The verification results show that Two-Version Priority Ceiling Protocol outperforms the other two MVCC algorithms with the given transaction set.