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

Research output: Contribution to book/Conference proceedings/Anthology/ReportConference contributionContributedpeer-review

Abstract

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.

Details

Original languageEnglish
Title of host publicationNASA Formal Methods
EditorsGuillaume Brat, Neha Rungta, Arnaud Venet
PublisherSpringer, Berlin [u. a.]
Pages307-321
Number of pages15
ISBN (print)978-3-642-38087-7
Publication statusPublished - 2013
Peer-reviewedYes

Publication series

SeriesLecture Notes in Computer Science, Volume 7871
ISSN0302-9743

Conference

Title5th NASA Formal Methods Symposium
Abbreviated titleNFM 2013
Conference number5
Duration14 - 16 May 2013
Degree of recognitionInternational event
CityMoffett Field
CountryUnited States of America

External IDs

Scopus 84883339819
ORCID /0000-0002-5321-9343/work/142236751
ORCID /0000-0003-1724-2586/work/165453610

Keywords

Keywords

  • probabilistic, quantitative, probabilistic-write/copy select

Library keywords