- title
- A Probabilistic Quantitative Analysis of Probabilistic-Write/Copy-Select
- Please use the following URL when quoting:
- https://nbn-resolving.org/urn:nbn:de:bsz:14-qucosa-129917
- original_z0
- NASA Formal Methods Lecture Notes in Computer Science, Volume 7871, 2013, pp 307-321, ISSN: 0302-9743
- publication_date
- 2013
- Abstract (EN)
- Probabilistic-Write/Copy-Select (PWCS) is a novel synchronization scheme suggested by Nicholas Mc Guire which avoids expensive atomic operations for synchronizing access to shared objects. Instead, PWCS makes inconsistencies detectable and recoverable. It builds on the assumption that, for typical workloads, the probability for data races is very small. Mc Guire describes PWCS for multiple readers but only one writer of a shared data structure. In this paper, we report on the formal analysis of the PWCS protocol using a continuous-time Markov chain model and probabilistic model checking techniques. Besides the original PWCS protocol, we also considered a variant with multiple writers. The results were obtained by the model checker PRISM and served to identify scenarios in which the use of the PWCS protocol is justified by guarantees on the probability of data races. Moreover, the analysis showed several other quantitative properties of the PWCS protocol.
- otherVersion0
- DOI: 10.1007/978-3-642-38088-4_21
- Abstract und Metadaten zum Beitrag, der im Konferenzband NASA Formal Methods Lecture Notes in Computer Science, 2013, bei Springer erschienen ist. The final publication is available at link.springer.com
Link: http://dx.doi.org/10.1007/978-3-642-38088-4_21 - Keywords (DE)
- Probabilistisches Modell, Synchronisation, Sonderforschungsbereich 912, Hochadaptive Energieeffiziente Systeme
- Keywords (EN)
- Probabilistic model checking, synchronization, Collaborative Research Centre 912, Highly Adaptive Energy-Efficient Computing
- Classification (DDC)
- 004
- Classification (RVK)
- ST 230
- university_publisher
- Technische Universität Dresden, Dresden
- URN Qucosa
- urn:nbn:de:bsz:14-qucosa-129917
- Qucosa date of publication
- 03.12.2013
- Document type
- in_proceeding
- Document language
- English
- licence
