Abstract

Modern geo-replicated data stores provide high availability by relaxing the underlying consistency requirements. Programs layered over such data stores are called weakly consistent programs. Due to the reduced consistency requirements, they exhibit highly nondeterministic behaviors, some of which might violate program invariants. Therefore, implementing correct weakly consistent programs and reasoning about them is challenging. In this paper, we present a systematic scheduling approach that is aware of the underlying consistency model. Our approach dynamically explores all possible program behaviors allowed by the used data store consistency model, and it evaluates program invariants during the exploration. We implement the approach in a prototype model checker for Antidote, which is a causally consistent key-value data store with convergent conflict handling. We evaluate our tool on several benchmarks. The results show that our approach is effective in detecting buggy behaviors in weakly consistent programs.

Citation

BibTeX

@article{2017_jpf_dr,
  title = {Consistency-Aware Scheduling for Weakly Consistent Programs},
  author = {Maryam Dabaghchian and Zvonimir Rakamaric},
  journal = {ACM SIGSOFT Software Engineering Notes},
  volume = {42},
  publisher = {ACM},
  pages = {1--5},
  doi = {10.1145/3149485.3149493},
  number = {4},
  month = {oct},
  note = {Proceedings of the 2017 Java Pathfinder Workshop (JPF)},
  year = {2017}
}

Acknowledgements

This research is supported in part by European FP7 project 609 551 SyncFree (2013-2016).