Change search
ReferencesLink to record
Permanent link

Direct link
Model checking transaction properties for concurrent real-time transactions in UPPAAL
Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
2016 (English)Independent thesis Advanced level (degree of Master (One Year)), 15 credits / 22,5 HE creditsStudent thesis
Abstract [en]

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. 

Place, publisher, year, edition, pages
2016. , 36 p.
Keyword [en]
Real-time transaction management, MVCC, model-checking, timeliness, isolation
National Category
Embedded Systems
URN: urn:nbn:se:mdh:diva-31782OAI: diva2:934461
Subject / course
Computer Science
2016-06-02, 11:45 (English)
Available from: 2016-06-15 Created: 2016-06-08 Last updated: 2016-06-15Bibliographically approved

Open Access in DiVA

fulltext(1143 kB)12 downloads
File information
File name FULLTEXT01.pdfFile size 1143 kBChecksum SHA-512
Type fulltextMimetype application/pdf

By organisation
Embedded Systems
Embedded Systems

Search outside of DiVA

GoogleGoogle Scholar
Total: 12 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Total: 17 hits
ReferencesLink to record
Permanent link

Direct link