More Web Proxy on the site http://driver.im/

research-article

Consistency-Aware Scheduling for Weakly Consistent Programs

Authors:

Maryam Dabaghchian,

Zvonimir Rakamaric,

Burcu K. Ozkan,

Serdar TasiranAuthors Info & Claims

ACM SIGSOFT Software Engineering Notes, Volume 42, Issue 4

Pages 1 - 5

https://doi.org/10.1145/3149485.3149493

Published: 11 January 2018 Publication History

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 con ict handling. We evaluate our tool on several benchmarks. The results show that our approach is e effective in detecting buggy behaviors in weakly consistent programs.

References

[1]

M. Ahamad, G. Neiger, J. E. Burns, P. Kohli, and P. W. Hutto. Causal memory: De nitions, implementation, and programming. Distributed Computing, 9(1), 1995.

[2]

D. D. Akkoorath, A. Z. Tomsic, M. Bravo, Z. Li, T. Crain, A. Bieniusa, N. Preguica, and M. Shapiro. Cure: Strong semantics meets high availability and low latency. In ICDCS, 2016.

[3]

Antidote Reference Platform. http://github.com/SyncFree/antidote.

[4]

V. Balegas, N. Preguica, R. Rodrigues, S. Duarte, C. Ferreira, M. Najafzadeh, and M. Shapiro. Putting consistency back into eventual consistency. In EuroSys, 2015.

Digital Library

[5]

C. Baquero, P. S. Almeida, and A. Shoker. Making operation-based crdts operation-based. In PaPEC, 2014.

Digital Library

[6]

A. Bouajjani, C. Enea, R. Guerraoui, and J. Hamza. On verifying causal consistency. In POPL, 2017.

Digital Library

[7]

L. Brutschy, D. Dimitrov, P. M~ Aijller, and M. Vechev. Serializability for eventual consistency: Criterion, analysis, and applications. In POPL, 2017.

Digital Library

[8]

S. Burckhardt. Principles of Eventual Consistency. 2014.

[9]

S. Burckhardt, A. Gotsman, H. Yang, and M. Zawirski. Replicated data types: Speci cation, veri cation, optimality. In POPL, 2014.

Digital Library

[10]

A. Cerone, G. Bernardi, and A. Gotsman. A framework for transactional consistency models with atomic visibility. In CONCUR, 2015.

[11]

Commander. http://github.com/Maryam81609/commander.

[12]

M. Dabaghchian, Z. Rakamaric, B. K. Ozkan, E. Mutlu, and S. Tasiran. Consistency-aware scheduling for weakly consistent programs. Technical Report UUCS-17-002, University of Utah, 2017.

[13]

G. DeCandia, D. Hastorun, M. Jampani, G. Kakulapati, A. Lakshman, A. Pilchin, S. Sivasubramanian, P. Vosshall, and W. Vogels. Dynamo: Amazon's highly available key-value store. In SOSP, 2007.

Digital Library

[14]

M. Emmi, S. Qadeer, and Z. Rakamarić. Delay-bounded scheduling. In POPL, 2011.

Digital Library

[15]

C. J. Fidge. Timestamps in message-passing systems that preserve the partial ordering. 1987.

[16]

S. Gilbert and N. Lynch. Brewer's conjecture and the feasibility of consistent, available, partition-tolerant web services. ACM SIGACT News, 2002.

Digital Library

[17]

A. Gotsman, H. Yang, C. Ferreira, M. Najafzadeh, and M. Shapiro. 'cause I'm strong enough: Reasoning about consistency choices in distributed systems. In POPL, 2016.

Digital Library

[18]

B. H. Kim, S. Oh, and D. Lie. Consistency oracles: Towards an interactive and exible consistency model speci cation. In HotOS XVI, 2017.

Digital Library

[19]

M. Lesani, C. J. Bell, and A. Chlipala. Chapar: Certi ed causally consistent distributed key-value stores. In POPL, 2016.

Digital Library

[20]

W. Lloyd, M. J. Freedman, M. Kaminsky, and D. G. Andersen. Don't settle for eventual: Scalable causal consistency for wide-area storage with cops. In SOSP, 2011.

Digital Library

[21]

M. Najafzadeh, A. Gotsman, H. Yang, C. Ferreira, and M. Shapiro. The cise tool: Proving weakly-consistent applications correct. In PaPoC, 2016.

Digital Library

[22]

C. H. Papadimitriou. The serializability of concurrent database updates. JACM, 1979.

Digital Library

[23]

Riak - A Key-Value Store. http://basho.com/products/riak-overview.

[24]

M. Shapiro, N. M. Preguiğa, C. Baquero, and M. Zawirski. Con ict-free replicated data types. In SSS, 2011.

Digital Library

[25]

SyncFree Project. https://syncfree.lip6.fr.

[26]

D. B. Terry, M. M. Theimer, K. Petersen, A. J. Demers, M. J. Spreitzer, and C. H. Hauser. Managing update con icts in bayou, a weakly connected replicated storage system. In SOSP, 1995.

Digital Library

[27]

P. Zeller. Testing properties of weakly consistent programs with repliss. In PaPoC, 2017.

Digital Library

[28]

P. Zeller and A. Poetzsch-He ter. Towards a proof framework for information systems with weak consistency. In SEFM, 2016.

Cited By

Al‐Mahfoudh MStutsman RGopalakrishnan G(2023)Efficient linearizability checking for actor‐based systemsSoftware: Practice and Experience10.1002/spe.325153:11(2163-2199)Online publication date: 22-Aug-2023
https://doi.org/10.1002/spe.3251
Ozkan B(2020)Verifying Weakly Consistent Transactional Programs Using Symbolic ExecutionNetworked Systems10.1007/978-3-030-67087-0_17(261-278)Online publication date: 3-Jun-2020
https://dl.acm.org/doi/10.1007/978-3-030-67087-0_17

Consistency-Aware Scheduling for Weakly Consistent Programs
1. Software and its engineering
  1. Software organization and properties
    1. Software system structures

Recommendations

Verifying Weakly Consistent Transactional Programs Using Symbolic Execution
Networked Systems
Abstract
We present a method for verifying whether all executions of a set of transactions satisfy a given invariant when run on weakly consistent systems. Existing approaches check that all executions under weak consistency are equivalent to some serial ...
Towards Weakly Consistent Local Storage Systems
SoCC '16: Proceedings of the Seventh ACM Symposium on Cloud Computing

Heterogeneity is a fact of life for modern storage servers. For example, a server may spread terabytes of data across many different storage media, ranging from magnetic disks, DRAM, NAND-based solid state drives (SSDs), as well as hybrid drives that ...
Implementing sequentially consistent programs on processor consistent platforms

Designers of distributed algorithms typically assume strong memory consistency guarantees, but system implementations provide weaker guarantees for better performance and scalability. This motivates the study of how to implement programs designed for ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGSOFT Software Engineering Notes

ACM SIGSOFT Software Engineering Notes Volume 42, Issue 4

October 2017

98 pages

ISSN:0163-5948

DOI:10.1145/3149485

Editor:
John Georgas
Northern Arizona University, USA

Issue’s Table of Contents

Copyright © 2018 Authors.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 11 January 2018

Published in SIGSOFT Volume 42, Issue 4

Check for updates

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
95
Total Downloads

Downloads (Last 12 months)3
Downloads (Last 6 weeks)0

Reflects downloads up to 17 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Al‐Mahfoudh MStutsman RGopalakrishnan G(2023)Efficient linearizability checking for actor‐based systemsSoftware: Practice and Experience10.1002/spe.325153:11(2163-2199)Online publication date: 22-Aug-2023
https://doi.org/10.1002/spe.3251
Ozkan B(2020)Verifying Weakly Consistent Transactional Programs Using Symbolic ExecutionNetworked Systems10.1007/978-3-030-67087-0_17(261-278)Online publication date: 3-Jun-2020
https://dl.acm.org/doi/10.1007/978-3-030-67087-0_17

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents