Analysis of Polka Contention Manager for use in Multicore Hard Real-Time Systems
Adrien Quillet, Audrey Queudet, Didier Lime · 2020
Transactional memory (TM) draws the attention of both academic and development groups; indeed this concept offers an alternative to lock-based approaches, easing programmers' work. Despite the large amount of investigations around this topic, the question of the correctness of most TM implementations remains open. More specifically, the lack of upper bounds on the execution time of transactions prevents the use of TM in real-time systems. To address this issue, we introduce new realistic assumptions relative to real-time systems, which allow to ensure wait-freedom guarantees progress (i.e. all transactions progress) when Polka contention manager is considered. In that context, through a thorough formalization of the system, we prove upper bounds both on the number of abortions and on the execution time of transactions.