A Probabilistic Quantitative Analysis of Probabilistic-Write/Copy-Select

Christel BaierChristel Baier, Benjamin EngelBenjamin Engel, Sascha KlüppelholzSascha Klüppelholz, Steffen MärckerSteffen Märcker, Hendrik TewsHendrik Tews, Marcus VölpMarcus Völp

DOI Link

Christel Baier, Benjamin Engel, Sascha Klüppelholz, Steffen Märcker, Hendrik Tews, Marcus Völp
A Probabilistic Quantitative Analysis of Probabilistic-Write/Copy-Select
Proc. of the 5th NASA Formal Methods Symposium (NFM), volume 7871 of Lecture Notes in Computer Science, 307--321, 2013. Springer

Details
Bibtex

KurzfassungAbstract
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.
Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science

The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-642-38088-4_21.

@inproceedings{BEKMTV2013,
  author    = {Christel Baier and Benjamin Engel and Sascha Kl{\"{u}}ppelholz
               and Steffen M{\"{a}}rcker and Hendrik Tews and Marcus V{\"{o}}lp},
  title     = {A Probabilistic Quantitative Analysis of
               Probabilistic-Write/Copy-Select},
  booktitle = {Proc. of the 5th {NASA} Formal Methods Symposium (NFM)},
  series    = {Lecture Notes in Computer Science},
  volume    = {7871},
  publisher = {Springer},
  year      = {2013},
  pages     = {307--321},
  doi       = {10.1007/978-3-642-38088-4_21}
}