|
| What is CADP? |
|---|
|
Home Page
Tools Overview Current Status Recent Changes |
| Installation |
|
How to obtain CADP?
Usage Statistics |
| Documentation |
|
FAQ
Tutorials Publications Manual Pages Demo Examples Wikipedia |
| CADP Community |
|
Newsletters
Education & Training Case Studies Research Tools |
| CADP Resources |
|
VLSAT Benchmarks
VLTS Benchmarks Other Resources |
| About CADP |
| Contributors |
| 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: [email protected] |
| Further remarks: | This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies |
Back to the CADP case studies page