Database of Case Studies Achieved Using CADP

Performance Evaluation of Concurrent Data Structures

Organisation: RWTH Aachen (Germany)
Chinese Academy of Science, Beijing (China)

Method: LNT

Tools used: CADP (Construction and Analysis of Distributed Processes)
MAMA

Domain: Concurrent Programming.

Period: 2016

Size: up to 378 million states

Description: The speed-ups obtained by concurrent programming heavily rely on exploiting highly-concurrent data structures. This case-study analyses the performance of several lock-based (either fine-grained or coarse-grained) and lock-free concurrent data structures, namely stacks (Treiber stack and its variant with hazard pointers), queues (Michael-Scott two-lock queue, its lock-free variant, and an improvement of this lock-free variant) and lists (coarse-grained and fine-grained synchronisation list, lazy list, and optimistic list). It uses a model-based approach, namely probabilistic model checking, to yield worst-case and best-case bounds on performance metrics, such as expected time and probabilities to finish a certain number of operations within a deadline.

The starting point of the approach is to model each concurrent data structure at hand, together with the threads that perform read and write operations on it, using the language LNT. The number of read and write operations is bounded by composing the model of the data structure in parallel with a monitor process, to keep the state space finite. The underlying LTS (Labelled Transition System) can then be generated and minimised for branching bisimulation using the CADP toolbox, and can be used both to check for functional correctess and performance evaluation. This case-study focuses on performance evaluation.

The approach assumes that the delays between read and write operations are random by nature and governed by negative exponential distributions. These random delays are inserted in the LTS by renaming the read and write actions to Markovian delays with different rates, using the label renaming operation available in CADP. CADP is then used to yield a (continuous-time) Markov automaton, which has random delay transitions and is non-deterministic due to concurrency. The Markov automaton is then analysed using recently developed algorithms implemented in the MAMA toolset. These algorithms allow for determining the expected time until a certain state is reached and the probability to reach a state within a given deadline if the Markov automaton is deterministic. Otherwise, in the general case, the analysis provides bounds for these expected time and probability, which represent the best-case and worst-case scenarios.

Conclusions: This case-study uses the CADP toolbox intensively to generate LTS from LNT models and to minimise them for branching bisimulation, whereas the subsequent steps are performed using both a script that transforms this generated LTS into a Markov automaton and the MAMA toolset for analysing the Markov automaton. CADP generates and minimises models up to 378 million states. The approach allows all transitions of LTS except delay transitions to be hidden, giving rise to LTS reductions of up to 99.9 %. The bisimulation reduction times for large state spaces are about 50% of the generation times.

The conducted experiments are conclusive: They show that (as expected) lock-based data structures have a rather deterministic performance, whereas lock-free and fine-grained lock-based have more varying performance. In addition, fine-grained lists may yield a lower throughput as many unsuccessful operations are carried out under intense race conditions. The followed approach would not have been possible using probabilistic model checkers such as PRISM/MRMC as they do not support non-deterministic continuous-time stochastic models. An additional benefit is that the written LNT models can also be used to check the functional correctness of the data structures.

Publications: [Wu-Yang-Katoen-16] Hao Wu, Xiaoxiao Yang, and Joost-Pieter Katoen. "Performance Evaluation of Concurrent Data Structures". Proceedings of the Symposium on Dependable Software Engineering (SETTA'16), Beijing, China. Lecture Notes in Computer Science vol. 9984, pages 38-49. Springer, 2016.
Available on-line at: https://link.springer.com/chapter/10.1007/978-3-319-47677-3_3
or http://www-i2.informatik.rwth-aachen.de/pub/index.php?type=download&pub_id=1322
Contact:
Hao Wu
Software Modelling and Verification Group
RWTH Aachen University
Ahornstrasse 55
D-52074 Aachen
GERMANY
Email: Hao.Wu@cs.rwth-aachen.de
Further remarks: This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Last modified: Fri Jul 20 17:55:17 2018.

Back to the CADP case studies page