, Alloy solver, 2016.

, PropEr testing of generic servers, 2016.

I. Abraham, G. Chockler, I. Keidar, and D. Malkhi, Byzantine Disk Paxos: Optimal Resilience with Byzantine Shared Memory, Distributed Computing, vol.18, issue.5, 2006.

H. Abu-libdeh, L. Princehouse, and H. Weatherspoon, RACS: a case for cloud storage diversity, SoCC, 2010.

S. Adve and M. D. Hill, Weak ordering -a new definition, International Symposium on Computer Architecture, 1990.

S. V. Adve and K. Gharachorloo, Shared memory consistency models: A tutorial, IEEE Computer, vol.29, issue.12, 1996.

S. V. Adve and M. D. Hill, A unified formalization of four shared-memory models, IEEE Transactions on Parallel and Distributed Systems, vol.4, issue.6, 1993.

A. Adya, Weak consistency: A generalized theory and optimistic implementations for distributed transactions, 1999.

A. Adya, W. J. Bolosky, M. Castro, G. Cermak, R. Chaiken et al., FARSITE: federated, available, and reliable storage for an incompletely trusted environment, OSDI, 2002.

M. Ahamad, R. A. Bazzi, R. John, P. Kohli, and G. Neiger, The power of processor consistency, ACM Symposium on Parallel Algorithms and Architectures (SPAA), 1993.

M. Ahamad, G. Neiger, J. E. Burns, P. Kohli, and P. W. Hutto, Causal memory: Definitions, implementation, and programming, Distributed Computing, vol.9, issue.1, 1995.

. Aiimpacts and . Org, A history of storage cost, 2014.

A. S. Aiyer, L. Alvisi, and R. A. Bazzi, On the availability of non-strict quorum systems, DISC, 2005.

S. Almeida, J. Leitão, and L. Rodrigues, Chainreaction: a causal+ consistent datastore based on chain replication, EuroSys, 2013.

P. Alvaro, T. Condie, N. Conway, K. Elmeleegy, J. M. Hellerstein et al., Boom analytics: exploring data-centric, declarative programming for the cloud, EuroSys, 2010.

P. Alvaro, N. Conway, J. M. Hellerstein, and W. R. Marczak, Consistency analysis in bloom: a CALM and collected approach, Conference on Innovative Data Systems Research (CIDR), 2011.

P. Alvaro, A. Hutchinson, N. Conway, W. R. Marczak, and J. M. Hellerstein, Bloomunit: declarative testing for distributed programs, 2012.

P. Alvaro, P. Bailis, N. Conway, and J. M. Hellerstein, Consistency without borders, SOCC, 2013.

P. Alvaro, N. Conway, J. M. Hellerstein, and D. Maier, Blazes: Coordination analysis for distributed programs, IEEE Conference on Data Engineering (ICDE), 2014.

. Amazon, Amazon DynamoDB Pricing, 2016.

, American National Standard for Information Systems, 1992.

D. G. Andersen, J. Franklin, M. Kaminsky, A. Phanishayee, L. Tan et al., FAWN: a fast array of wimpy nodes, SOSP, 2009.

E. Anderson, X. Li, M. A. Shah, J. Tucek, and J. J. Wylie, What consistency does your key-value store actually provide?" in Hot Topics in System Dependability, ser. HotDep'10, 2010.

E. Androulaki, C. Cachin, D. Dobre, and M. Vukolic, Erasure-coded byzantine storage with separate metadata, OPODIS, 2014.

. Apache, Apache JClouds, 2016.

M. Armbrust, A. Fox, R. Griffith, A. D. Joseph, R. H. Katz et al., A view of cloud computing, Commun. ACM, vol.53, issue.4, 2010.

H. Attiya and R. Friedman, A correctness condition for high-performance multiprocessors (extended abstract), ACM Symposium on Theory of Computing, 1992.
DOI : 10.1145/129712.129778

H. Attiya and J. Welch, Sequential consistency versus linearizability, ACM Transactions on Computer Systems (TOCS), vol.12, issue.2, 1994.
DOI : 10.1145/176575.176576

H. Attiya, A. Bar-noy, and D. Dolev, Sharing memory robustly in messagepassing systems, Journal of the ACM, vol.42, issue.1, 1995.
DOI : 10.1145/93385.93441

H. Attiya, F. Ellen, and A. Morrison, Limitations of highly-available eventually-consistent data stores, PODC, 2015.

S. Babu and H. Herodotou, Massively parallel databases and mapreduce systems, Foundations and Trends in Databases, vol.5, issue.1, 2013.
DOI : 10.1561/1900000036

P. Bailis, When is "ACID" ACID? rarely, 2017.

P. Bailis and A. Ghodsi, Eventual consistency today: Limitations, extensions, and beyond, Queue, vol.11, issue.3, 2013.

P. Bailis, A. Fekete, A. Ghodsi, J. M. Hellerstein, and I. Stoica, The potential dangers of causal consistency and an explicit solution, SOCC, 2012.

P. Bailis, S. Venkataraman, M. J. Franklin, J. M. Hellerstein, and I. Stoica, Probabilistically bounded staleness for practical partial quorums, VLDB, vol.5, issue.8, 2012.

P. Bailis, A. Ghodsi, J. M. Hellerstein, and I. Stoica, Bolt-on causal consistency, ACM SIGMOD International Conference on Management of Data (SIGMOD), 2013.
DOI : 10.1145/2463676.2465279
URL : http://www.bailis.org/papers/bolton-sigmod2013.pdf

P. Bailis, A. Fekete, M. J. Franklin, A. Ghodsi, J. M. Hellerstein et al., Coordination avoidance in database systems, 2014.

P. Bailis, A. Fekete, J. M. Hellerstein, A. Ghodsi, and I. Stoica, Scalable atomic visibility with RAMP transactions, ACM International Conference on Management of Data (SIGMOD), 2014.
DOI : 10.1145/2909870
URL : http://www.bailis.org/papers/ramp-sigmod2014.pdf

P. Bailis, S. Venkataraman, M. J. Franklin, J. M. Hellerstein, and I. Stoica, Quantifying eventual consistency with PBS, VLDB Journal, vol.23, issue.2, 2014.
DOI : 10.1145/2632792

J. Baker, C. Bond, J. C. Corbett, J. J. Furman, A. Khorlin et al., Megastore: Providing scalable, highly available storage for interactive services, Conference on Innovative Data Systems Research (CIDR), 2011.

V. Balegas, S. Duarte, C. Ferreira, R. Rodrigues, N. M. Preguiça et al., Putting consistency back into eventual consistency, EuroSys, 2015.
DOI : 10.1145/2741948.2741972
URL : https://hal.archives-ouvertes.fr/hal-01109719

C. Basescu, C. Cachin, I. Eyal, R. Haas, A. Sorniotti et al., Robust data sharing with key-value stores, IEEE/IFIP International Conference on Dependable Systems and Networks, DSN, 2012.
DOI : 10.1145/1993806.1993843

J. Bataller and J. M. Bernabéu-aubán, Synchronized DSM models, Parallel Processing, 1997.
DOI : 10.1007/bfb0002771

N. M. Belaramani, M. Dahlin, L. Gao, A. Nayate, A. Venkataramani et al., PRACTI replication, NSDI, 2006.

D. Bermbach, Benchmarking eventually consistent distributed storage systems, 2014.

D. Bermbach and J. Kuhlenkamp, Consistency in distributed storage systems -an overview of models, metrics and measurement approaches, Networked Systems (NE-TYS), 2013.

D. Bermbach and S. Tai, Eventual consistency: How soon is eventual? An evaluation of amazon s3's consistency behavior, ACM Workshop on Middleware for Service Oriented Computing, 2011.

, Benchmarking eventual consistency: Lessons learned from long-term experimental studies, IEEE International Conference on Cloud Engineering (IC2E), 2014.

P. A. Bernstein and S. Das, Rethinking eventual consistency, ACM SIGMOD International Conference on Management of Data (SIGMOD), 2013.

P. A. Bernstein, V. Hadzilacos, and N. Goodman, Concurrency Control and Recovery in Database Systems, 1987.

B. N. Bershad and M. J. Zekauskas, Midway: Shared memory parallel programming with entry consistency for distributed memory multiprocessors, Tech. Rep, 1991.

A. Bessani, R. Mendes, T. Oliveira, N. Neves, M. Correia et al., SCFS: A shared cloud-backed file system, USENIX Annual Technical Conference, USENIX ATC, 2014.

A. N. Bessani, M. Correia, B. Quaresma, F. André, and P. Sousa, DepSky: Dependable and secure storage in a cloud-of-clouds, ACM Transactions on Storage (TOS), vol.9, issue.4, 2013.

A. N. Bessani, R. Mendes, T. Oliveira, N. F. Neves, M. Correia et al., SCFS: A shared cloud-backed file system, USENIX Annual Technical Conference (ATC), 2014.

C. E. Bezerra, F. Pedone, and R. Van-renesse, Scalable state-machine replication, IEEE/IFIP International Conference on Dependable Systems and Networks, DSN, 2014.

K. Birman, A. Schiper, and P. Stephenson, Lightweight causal and atomic group multicast, ACM Transactions on Computer Systems (TOCS), vol.9, issue.3, 1991.

V. Bortnikov, G. Chockler, A. Roytman, and M. Spreitzer, Bulletin board: A scalable and robust eventually consistent shared memory over a peer-topeer overlay, Operating Systems Review, vol.44, issue.2, 2010.

K. D. Bowers, A. Juels, and A. Oprea, HAIL: a high-availability and integrity layer for cloud storage, ACM CCS, 2009.

M. Brandenburger, C. Cachin, and N. Knezevic, Don't trust the cloud, verify: integrity and consistency for cloud object stores, ACM International Systems and Storage Conference (SYSTOR), 2015.

E. A. Brewer, Pushing the CAP: Strategies for consistency and availability, IEEE Computer, vol.45, issue.2, 2012.

, Towards robust distributed systems (abstract), " in PODC, 2000.

N. Bronson, Z. Amsden, G. Cabrera, P. Chakka, P. Dimov et al., TAO: facebook's distributed data store for the social graph, USENIX Annual Technical Conference (ATC), 2013.

J. Brzezinski, C. Sobaniec, and D. Wawrzyniak, Session guarantees to achieve pram consistency of replicated shared objects, Parallel Processing and Applied Mathematics (PPAM), 2003.

, From session causality to causal consistency, Workshop on Parallel, Distributed and Network-Based Processing (PDP), 2004.

S. Burckhardt, Principles of Eventual Consistency, ser. Foundations and Trends in Programming Languages. now publishers, vol.1, 2014.

S. Burckhardt, M. Fähndrich, D. Leijen, and B. P. Wood, Cloud types for eventual consistency, Object-Oriented Programming (ECOOP), 2012.

S. Burckhardt, D. Leijen, M. Fähndrich, and M. Sagiv, Eventually consistent transactions, European Symposium on Programming (ESOP), 2012.

S. Burckhardt, A. Gotsman, H. Yang, and M. Zawirski, Replicated data types: specification, verification, optimality, ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), 2014.
URL : https://hal.archives-ouvertes.fr/hal-00934311

M. Burrows, The chubby lock service for loosely-coupled distributed systems, OSDI, 2006.

C. Cachin, A. Shelat, and A. Shraer, Efficient fork-linearizable access to untrusted shared memory, 2007.

C. Cachin, I. Keidar, and A. Shraer, Trusting the cloud, SIGACT News, vol.40, issue.2, 2009.

, Fork Sequential Consistency is Blocking, Information Processing Letters, vol.109, issue.7, 2009.

, Fail-aware untrusted storage, SIAM Journal on Computing (SICOMP), vol.40, issue.2, 2011.

C. Cachin, D. Dobre, and M. Vukolic, Separating data and control: Asynchronous BFT storage with 2t + 1 data replicas, Stabilization, Safety, and Security of Distributed Systems (SSS), 2014.

B. Calder, J. Wang, A. Ogus, N. Nilakantan, A. Skjolsvold et al., Windows azure storage: a highly available cloud storage service with strong consistency, SOSP, 2011.

I. Cano, S. Aiyar, and A. Krishnamurthy, Characterizing private clouds: A large-scale empirical analysis of enterprise clusters, SoCC, 2016.

A. Cerone, G. Bernardi, and A. Gotsman, A framework for transactional consistency models with atomic visibility, Conference on Concurrency Theory, 2015.

A. Cerone, A. Gotsman, and H. Yang, Algebraic laws for weak consistency, CONCUR, 2017.

H. Chihoub, S. Ibrahim, G. Antoniu, and M. S. Pérez-hernández, Harmony: Towards automated self-adaptive consistency in cloud storage, IEEE International Conference on Cluster Computing (CLUSTER), 2012.
URL : https://hal.archives-ouvertes.fr/hal-00734050

, Consistency in the cloud: When money does matter!" in Symposium on Cluster, Cloud, and Grid Computing (CCGrid), 2013.

G. Chockler, D. Dobre, and A. Shraer, Brief announcement: Consistency and complexity tradeoffs for highly-available multi-cloud store, DISC, 2013.

B. Chun, P. Maniatis, S. Shenker, and J. Kubiatowicz, Attested appendonly memory: making adversaries stick to their word, SOSP, 2007.

K. Claessen and J. Hughes, Quickcheck: a lightweight tool for random testing of haskell programs, ACM SIGPLAN ICFP, 2000.

. Cloudera, Observers -making ZooKeeper scale even further, 2009.

. Cloudspaces, CloudSpaces EU FP7 project, 2015.

B. A. Coan, B. M. Oki, and E. K. Kolodner, Limitations on database availability when networks partition, ACM Symposium on Principles of Distributed Computing, 1986.

. Consul, Consul -distributed service discovery and configuration, 2016.

, Consul -consensus protocol, 2016.

N. Conway, W. R. Marczak, P. Alvaro, J. M. Hellerstein, and D. Maier, Logic and lattices for distributed programming, SOCC, 2012.

B. F. Cooper, R. Ramakrishnan, U. Srivastava, A. Silberstein, P. Bohannon et al., Pnuts: Yahoo!'s hosted data serving platform, VLDB, vol.1, 2008.

B. F. Cooper, A. Silberstein, E. Tam, R. Ramakrishnan, and R. Sears, Benchmarking cloud serving systems with ycsb, SoCC, 2010.

J. C. Corbett, J. Dean, M. Epstein, A. Fikes, C. Frost et al., Spanner: Google's globally distributed database, ACM Transactions on Computer Systems (TOCS), vol.31, issue.3, 2013.

M. Correia, N. F. Neves, and P. Veríssimo, How to tolerate half less one Byzantine nodes in practical distributed systems, SRDS, 2004.

M. Correia, D. G. Ferro, F. P. Junqueira, and M. Serafini, Practical hardening of crash-tolerant systems, USENIX Annual Technical Conference, 2012.

S. B. Davidson, H. Garcia-molina, and D. Skeen, Consistency in partitioned networks, ACM Computing Surveys, vol.17, issue.3, 1985.

G. Decandia, D. Hastorun, M. Jampani, G. Kakulapati, A. Lakshman et al., Dynamo: amazon's highly available key-value store, SOSP, 2007.

P. Deutsch, The eight fallacies of distributed computing, 1994.

D. Dobre, P. Viotti, and M. Vukoli?, Hybris: Robust hybrid cloud storage, SOCC, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01610463

I. Drago, M. Mellia, M. M. Munafò, A. Sperotto, R. Sadre et al., Inside dropbox: understanding personal cloud storage services, ACM SIGCOMM Internet Measurement Conference, IMC '12, 2012.

I. Drago, E. Bocchi, M. Mellia, H. Slatman, and A. Pras, Benchmarking personal cloud storage, ACM SIGCOMM Internet Measurement Conference, IMC 2013, 2013.
URL : https://hal.archives-ouvertes.fr/hal-01346257

J. Du, C. Iorgulescu, A. Roy, and W. Zwaenepoel, Gentlerain: Cheap and scalable causal consistency with physical clocks, SOCC, 2014.

J. Du, D. Sciascia, S. Elnikety, W. Zwaenepoel, and F. Pedone, Clock-rsm: Low-latency inter-datacenter state machine replication using loosely synchronized physical clocks, IEEE/IFIP International Conference on Dependable Systems and Networks, DSN, 2014.

M. Dubois, C. Scheurich, and F. A. Briggs, Memory access buffering in multiprocessors, International Symposium on Computer Architecture (ISCA), 1986.

C. Dwork, N. Lynch, and L. Stockmeyer, Consensus in the presence of partial synchrony, J. ACM, vol.35, issue.2, 1988.

D. Dziuma, P. Fatourou, and E. Kanellou, Consistency for transactional memory computing, Bulletin of the EATCS, vol.113, 2014.
DOI : 10.1007/978-3-319-14720-8_1

. Eurecom, Hybris -robust hybrid cloud storage library, 2016.

H. Fan, S. Chatterjee, and W. M. Golab, Watca: The waterloo consistency analyzer, IEEE International Conference on Data Engineering (ICDE), 2016.
DOI : 10.1109/icde.2016.7498354

R. Fan and N. Lynch, Efficient Replication of Large Data Objects, DISC, 2003.
DOI : 10.1007/978-3-540-39989-6_6

A. Fekete, D. Gupta, V. Luchangco, N. A. Lynch, and A. A. Shvartsman, Eventuallyserializable data services, PODC, 1996.

A. J. Feldman, W. P. Zeller, M. J. Freedman, and E. W. Felten, SPORC: group collaboration using untrusted cloud resources, OSDI, 2010.

M. J. Fischer, N. A. Lynch, and M. Paterson, Impossibility of distributed consensus with one faulty process, Journal of the ACM, vol.32, issue.2, 1985.
DOI : 10.1145/3149.214121

R. Friedman, R. Vitenberg, and G. Chockler, On the composability of consistency conditions, Information Processing Letters, vol.86, issue.4, 2003.

A. Ganesan, R. Alagappan, A. C. Arpaci-dusseau, and R. H. Arpaci-dusseau, Redundancy does not imply fault tolerance: Analysis of distributed storage reactions to single errors and corruptions, USENIX Conference on File and Storage Technologies, 2017.

A. Ganesan, R. Alagappan, A. C. Arpaci-dusseau, and R. H. Arpaci-dusseau, Redundancy does not imply fault tolerance: Analysis of distributed storage reactions to single errors and corruptions, FAST, 2017.
DOI : 10.1145/3125497
URL : http://dl.acm.org/ft_gateway.cfm?id=3125497&type=pdf

G. R. Gao and V. Sarkar, Location consistency-a new memory model and cache consistency protocol, IEEE Transactions on Computers, vol.49, issue.8, 2000.
DOI : 10.1109/12.868026

K. Gharachorloo, D. Lenoski, J. Laudon, P. B. Gibbons, A. Gupta et al., Memory consistency and event ordering in scalable shared-memory multiprocessors, International Symposium on Computer Architecture, 1990.
DOI : 10.1109/isca.1990.134503

S. Ghemawat, H. Gobioff, and S. Leung, The google file system, SOSP, 2003.
DOI : 10.1145/1165389.945450

P. B. Gibbons and E. Korach, Testing shared memories, SIAM J. Comput, vol.26, issue.4, 1997.
DOI : 10.1137/s0097539794279614

G. A. Gibson, D. Nagle, K. Amiri, J. Butler, F. W. Chang et al., A cost-effective, high-bandwidth storage architecture, International Conference on Architectural Support for Programming Languages and Operating Systems, 1998.
DOI : 10.1145/291006.291029

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

L. Glendenning, I. Beschastnikh, A. Krishnamurthy, and T. E. Anderson, Scalable consistency in scatter, SOSP, 2011.
DOI : 10.1145/2043556.2043559

W. M. Golab, X. Li, and M. A. Shah, Analyzing consistency properties for fun and profit, 2011.
DOI : 10.1145/1993806.1993834

W. M. Golab, M. R. Rahman, A. Auyoung, K. Keeton, and I. Gupta, Clientcentric benchmarking of eventual consistency for cloud storage systems, IEEE Conference on Distributed Computing Systems (ICDCS), 2014.
DOI : 10.1145/2523616.2525935

J. R. Goodman, Cache consistency and sequential consistency, SCI Commitee, issue.61, 1989.

A. Gotsman, H. Yang, C. Ferreira, M. Najafzadeh, and M. Shapiro, Cause I'm strong enough: Reasoning about consistency choices in distributed systems, ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), 2016.
DOI : 10.1145/2914770.2837625
URL : https://hal.archives-ouvertes.fr/hal-01243192

J. Gray and A. Reuter, Transaction Processing: Concepts and Techniques, 1993.

R. Guerraoui and M. Vukolic, How fast can a very robust read be, PODC, 2006.
DOI : 10.1145/1146381.1146419

H. S. Gunawi, M. Hao, R. O. Suminto, A. Laksono, A. D. Satria et al., Why does the cloud stop computing?: Lessons from hundreds of service outages, SoCC, 2016.

V. Hadzilacos and S. Toueg, A modular approach to fault-tolerant broadcasts and related problems, 1994.

R. Halalai, P. Sutra, E. Riviere, and P. Felber, Zoofence: Principled service partitioning and application to the zookeeper coordination service, IEEE International Symposium on Reliable Distributed Systems, 2014.
DOI : 10.1109/srds.2014.41

J. Hamilton, The cost of latency, 2009.

R. Hamlet, Random testing, Encyclopedia of Software Engineering, 1994.

S. Han, H. Shen, T. Kim, A. Krishnamurthy, T. E. Anderson et al., Metasync: File synchronization across multiple untrusted storage services, USENIX Annual Technical Conference (ATC), 2015.

T. Harris, J. R. Larus, and R. Rajwar, Transactional Memory, 2010.

P. Helland, Life beyond distributed transactions: an apostate's opinion, Conference on Innovative Data Systems Research (CIDR), 2007.

M. Herlihy, Wait-Free Synchronization, ACM Trans. Program. Lang. Syst, vol.13, issue.1, 1991.

M. Herlihy and N. Shavit, The art of multiprocessor programming, 2008.
DOI : 10.1145/1146381.1146382

M. Herlihy and J. M. Wing, Linearizability: A correctness condition for concurrent objects, ACM Transactions on Programming Languages and Systems (TOPLAS), vol.12, issue.3, 1990.
DOI : 10.1145/78969.78972
URL : http://www.cs.uoregon.edu/classes/06W/cis607atom/readings/herlihy-linearizability.pdf

M. P. Herlihy and J. M. Wing, Linearizability: A Correctness Condition for Concurrent Objects, ACM Trans. Program. Lang. Syst, vol.12, issue.3, 1990.
DOI : 10.1145/78969.78972
URL : http://www.cs.uoregon.edu/classes/06W/cis607atom/readings/herlihy-linearizability.pdf

A. Horn and D. Kroening, Faster linearizability checking via p-compositionality, IFIP International Conference on Formal Techniques for Distributed Objects, Components, and Systems, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01767332

J. Hughes, B. C. Pierce, T. Arts, and U. Norell, Mysteries of dropbox: Propertybased testing of a distributed synchronization service, IEEE International Conference on Software Testing, Verification and Validation, 2016.

P. Hunt, M. Konar, F. P. Junqueira, and B. Reed, Zookeeper: wait-free coordination for internet-scale systems, USENIX Annual Technical Conference, USENIX ATC, 2010.

P. W. Hutto and M. Ahamad, Slow memory: Weakening consistency to enchance concurrency in distributed shared memories, International Conference on Distributed Computing Systems (ICDCS), 1990.
DOI : 10.1109/icdcs.1990.89297

L. Iftode, C. Dubnicki, E. W. Felten, and K. Li, Improving release-consistent shared virtual memory using automatic update, IEEE International Symposium on High-Performance Computer Architecture (HPCA), 1996.
DOI : 10.1109/hpca.1996.501170

L. Iftode, J. P. Singh, and K. Li, Scope consistency: A bridge between release consistency and entry consistency, ACM Symposium on Parallel Algorithms and Architectures (SPAA), 1996.

P. R. Johnson and R. H. Thomas, Maintenance of duplicate databases, vol.677, 1975.

E. Junqué-de-fortuny, D. Martens, and F. Provost, Predictive modeling with big data: is bigger really better?, Big Data, vol.1, issue.4, 2013.

F. P. Junqueira, I. Kelly, and B. Reed, Durability with bookkeeper, Operating Systems Review, vol.47, issue.1, 2013.

R. Kapitza, J. Behl, C. Cachin, T. Distler, S. Kuhnle et al., CheapBFT: resource-efficient Byzantine fault tolerance, EuroSys, 2012.

P. J. Keleher, A. L. Cox, and W. Zwaenepoel, Lazy release consistency for software distributed shared memory, International Symposium on Computer Architecture, 1992.

K. Kingsbury, Jepsen -distributed systems safety analysis, 2016.

M. Komorowski, Trends in the cost of computing, 2015.

R. Kotla, L. Alvisi, and M. Dahlin, Safestore: A durable and practical storage system, USENIX Annual Technical Conference, USENIX ATC, 2007.

T. Kraska, M. Hentschel, G. Alonso, and D. Kossmann, Consistency rationing in the cloud: Pay only when it matters, VLDB, vol.2, issue.1, 2009.

S. Krishnamurthy, W. H. Sanders, and M. Cukier, An adaptive framework for tunable consistency and timeliness using replication, Dependable Systems and Networks (DSN), 2002.

R. Ladin, B. Liskov, L. Shrira, and S. Ghemawat, Providing high availability using lazy replication, ACM Transactions on Computer Systems (TOCS), vol.10, issue.4, 1992.

A. Lakshman and P. Malik, Cassandra: a decentralized structured storage system, Operating Systems Review, vol.44, issue.2, 2010.

S. Lakshmanan, M. Ahamad, and H. Venkateswaran, A secure and highly available distributed store for meeting diverse data storage needs, Dependable Systems and Networks (DSN), 2001.

L. Lamport, Paxos made simple, SIGACT News, vol.32, issue.4, 2001.

, Time, clocks, and the ordering of events in a distributed system, Communications of the ACM (CACM), vol.21, issue.7, 1978.

, How to make a multiprocessor computer that correctly executes multiprocess programs, IEEE Transactions on Computers, vol.28, issue.9, 1979.

, Specifying concurrent program modules, ACM Transactions on Programming Languages and Systems (TOPLAS), vol.5, issue.2, 1983.

, On interprocess communication. part i: Basic formalism, Distributed Computing, vol.1, issue.2, 1986.

, On interprocess communication. part ii: Algorithms, Distributed Computing, vol.1, issue.2, 1986.

L. Lamport, R. E. Shostak, and M. C. Pease, The byzantine generals problem, ACM Transactions on Programming Languages and Systems (TOPLAS), vol.4, issue.3, 1982.

G. T. Laycock, The theory and practice of specification based software testing, 1993.

C. Lee, S. J. Park, A. Kejriwal, S. Matsushita, and J. K. Ousterhout, Implementing linearizability at large scale and low latency, SOSP, 2015.

M. Lesani, C. J. Bell, and A. Chlipala, Chapar: certified causally consistent distributed key-value stores, ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), 2016.

A. Li, X. Yang, S. Kandula, and M. Zhang, Cloudcmp: comparing public cloud providers, ACM SIGCOMM IMC, 2010.

C. Li, D. Porto, A. Clement, J. Gehrke, N. Preguiça et al., Making geo-replicated systems fast as possible, consistent when necessary, OSDI, 2012.

C. Li, J. Leitão, A. Clement, N. M. Preguiça, R. Rodrigues et al., Automating the choice of consistency levels in replicated systems, USENIX Annual Technical Conference (ATC), 2014.

J. Li, E. Michael, N. K. Sharma, A. Szekeres, and D. R. Ports, Just say NO to paxos overhead: Replacing consensus with network ordering, OSDI, 2016.

J. Li and D. Mazières, Beyond one-third faulty replicas in byzantine fault tolerant systems, NSDI, 2007.

J. Li, M. N. Krohn, D. Mazières, and D. Shasha, Secure untrusted data repository (sundr), OSDI, 2004.

R. J. Lipton and J. S. Sandberg, Pram: A scalable shared memory, 1988.

S. Liu, P. Viotti, C. Cachin, V. Quéma, and M. Vukolic, XFT: practical fault tolerance beyond crashes, USENIX Symposium on Operating Systems Design and Implementation, OSDI, 2016.

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, SOSP, 2011.

, Stronger semantics for low-latency geo-replicated storage, NSDI, 2013.

B. T. Loo, T. Condie, M. N. Garofalakis, D. E. Gay, J. M. Hellerstein et al., Declarative networking: language, execution and optimization, ACM SIGMOD International Conference on Management of Data, 2006.

P. G. Lopez, S. Toda, C. Cotes, M. Sanchez-artigas, and J. Lenton, Stacksync: Bringing elasticity to dropbox-like file synchronization, ACM/IFIP/USENIX Middleware, 2014.

H. Lu, K. Veeraraghavan, P. Ajoux, J. Hunt, Y. J. Song et al., Existential consistency: measuring and understanding consistency at facebook, SOSP, 2015.

N. A. Lynch and A. A. Shvartsman, RAMBO: A Reconfigurable Atomic Memory Service for Dynamic Networks, DISC, 2002.

N. A. Lynch and M. R. Tuttle, An introduction to input/output automata, CWI Quarterly, vol.2, 1989.

P. Mahajan, S. T. Setty, S. Lee, A. Clement, L. Alvisi et al., Depot: Cloud storage with minimal trust, OSDI, 2010.

P. Mahajan, L. Alvisi, and M. Dahlin, Consistency, availability, and convergence, 2011.

P. Mahajan, S. T. Setty, S. Lee, A. Clement, L. Alvisi et al., Depot: Cloud storage with minimal trust, ACM Trans. Comput. Syst, vol.29, issue.4, 2011.

D. Malkhi and M. K. Reiter, Secure and scalable replication in phalanx, Symposium on Reliable Distributed Systems (SRDS), 1998.

, Byzantine quorum systems, Distributed Computing, vol.11, issue.4, 1998.

D. Mazières and D. Shasha, Building Secure File Systems out of Byzantine Storage, PODC, 2002.

. Memcached, Memcached, 2016.

J. Misra, Axioms for memory access in asynchronous hardware systems, ACM Transactions on Programming Languages and Systems (TOPLAS), vol.8, issue.1, 1986.

I. Moraru, D. G. Andersen, and M. Kaminsky, There is more consensus in egalitarian parliaments, SOSP, 2013.

D. Mosberger, Memory consistency models, Operating Systems Review, vol.27, issue.1, 1993.

M. Najafzadeh, A. Gotsman, H. Yang, C. Ferreira, and M. Shapiro, The CISE tool: proving weakly-consistent applications correct, Workshop on the Principles and Practice of Consistency for Distributed Data, PaPoC@EuroSys, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01350636

D. Ongaro and J. K. Ousterhout, In search of an understandable consensus algorithm, USENIX Annual Technical Conference, USENIX ATC, 2014.

A. Oprea and M. K. Reiter, On consistency of encrypted files, DISC, 2006.

M. T. Özsu and P. Valduriez, Principles of Distributed Database Systems, 2011.

S. Patil, M. Polte, K. Ren, W. Tantisiriroj, L. Xiao et al., YCSB++: benchmarking and performance debugging advanced features in scalable table stores, SOCC, 2011.

M. Pease, R. Shostak, and L. Lamport, Reaching Agreement in the Presence of Faults, J. ACM, vol.27, issue.2, 1980.

D. Perkins, N. Agrawal, A. Aranya, C. Yu, Y. Go et al., Simba: tunable end-to-end data consistency for mobile apps, EuroSys, 2015.

K. Petersen, M. Spreitzer, D. B. Terry, M. Theimer, and A. J. Demers, Flexible update propagation for weakly consistent replication, SOSP, 1997.

J. S. Plank, S. Simmerman, and C. D. Schuman, Jerasure: A library in C/C++ facilitating erasure coding for storage applications -Version 1.2, 2008.

M. R. Rahman, W. M. Golab, A. Auyoung, K. Keeton, and J. J. Wylie, Toward a principled framework for benchmarking consistency, Computing Research Repository, 2012.

J. Rao, E. J. Shekita, and S. Tata, Using paxos to build a scalable, consistent, and highly available datastore, VLDB, vol.4, issue.4, 2011.

M. Raynal and A. Schiper, A suite of definitions for consistency criteria in distributed shared memories, Annales des Télécommunications, vol.52, issue.11-12, 1997.

B. Reed and F. P. Junqueira, A simple totally ordered broadcast protocol, Workshop on Large-Scale Distributed Systems and Middleware (LADIS), 2008.

P. L. Reiher, J. S. Heidemann, D. Ratner, G. Skinner, and G. J. Popek, Resolving file conflicts in the ficus file system, USENIX Summer 1994 Technical Conference, 1994.

R. Rodrigues and B. Liskov, High availability in dhts: Erasure coding vs. replication, IPTPS, 2005.

H. Roh, M. Jeon, J. Kim, and J. Lee, Replicated abstract data types: Building blocks for collaborative applications, Journal of Parallel and Distributed Computing, vol.71, issue.3, 2011.

Y. Saito and M. Shapiro, Optimistic replication, ACM Computing Surveys, vol.37, issue.1, 2005.
URL : https://hal.archives-ouvertes.fr/inria-00444768

N. Santos, L. Veiga, and P. Ferreira, Vector-field consistency for ad-hoc gaming, ACM/IFIP/USENIX Middleware Conference, 2007.

M. Serafini, D. Dobre, M. Majuntke, P. Bokor, and N. Suri, Eventually Linearizable Shared Objects, 2010.

M. Shapiro, N. M. Preguiça, C. Baquero, and M. Zawirski, Convergent and commutative replicated data types, Bulletin of the EATCS, vol.104, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00932833

, Conflict-free replicated data types, Stabilization, Safety, and Security of Distributed Systems (SSS), 2011.

A. Shraer, C. Cachin, A. Cidon, I. Keidar, Y. Michalevsky et al., Venus: verification for untrusted cloud storage, ACM Cloud Computing Security Workshop (CCSW), 2010.

B. H. Sigelman, L. A. Barroso, M. Burrows, P. Stephenson, M. Plakal et al., Dapper, a large-scale distributed systems tracing infrastructure, 2010.

A. Singh, P. Fonseca, P. Kuznetsov, R. Rodrigues, and P. Maniatis, Zeno: Eventually consistent byzantine-fault tolerance, NSDI, 2009.

A. Singla, U. Ramachandran, and J. K. Hodgins, Temporal notions of synchronization and consistency in beehive, ACM Symposium on Parallel Algorithms and Architectures (SPAA), 1997.

K. C. Sivaramakrishnan, G. Kaki, and S. Jagannathan, Declarative programming over eventually consistent data stores, ACM SIGPLAN Conference on Programming Language Design and Implementation, 2015.

. Softlayer, IBM SoftLayer, 2016.

E. Stefanov, M. Van-dijk, E. Shi, C. W. Fletcher, L. Ren et al., Path ORAM: an extremely simple oblivious RAM protocol, ACM SIGSAC Conference on Computer and Communications Security, 2013.

R. C. Steinke and G. J. Nutt, A unified theory of shared memory consistency, Journal of the ACM, vol.51, issue.5, 2004.

M. Stonebraker, The case for shared nothing, IEEE Database Eng. Bull, vol.9, issue.1, 1986.

H. Sutter, The free lunch is over: a fundamental turn toward concurrency in software, 2005.

. Syncany, Secure file synchronization software for arbitrary storage backends, 2016.

A. S. Tanenbaum and M. Van-steen, Distributed systems -principles and paradigms (2. ed.). Pearson Education, 2007.

D. Terry, Replicated data consistency explained through baseball, Communications of the ACM (CACM), vol.56, issue.12, 2013.

D. B. Terry, A. J. Demers, K. Petersen, M. Spreitzer, M. Theimer et al., Session guarantees for weakly consistent replicated data, Parallel and Distributed Information Systems (PDIS), 1994.

D. B. Terry, M. Theimer, K. Petersen, A. J. Demers, M. Spreitzer et al., Managing update conflicts in bayou, a weakly connected replicated storage system, SOSP, 1995.

D. B. Terry, V. Prabhakaran, R. Kotla, M. Balakrishnan, M. K. Aguilera et al., Consistency-based service level agreements for cloud storage, SOSP, 2013.

E. Torlak, M. Vaziri, and J. Dolby, Memsat: checking axiomatic specifications of memory models, ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), 2010.

F. J. Torres-rojas and E. Meneses, Convergence through a weak consistency model: Timed causal consistency, CLEI electronic journal, vol.8, issue.2, 2005.

F. J. Torres-rojas, M. Ahamad, and M. Raynal, Timed consistency for shared distributed objects, PODC, 1999.

. Twitter, Distributed systems tracing with zipkin, 2012.

G. S. Veronese, M. Correia, A. N. Bessani, L. C. Lung, and P. Veríssimo, Efficient byzantine fault-tolerance, IEEE Trans. Computers, vol.62, issue.1, 2013.

. Vmware, The Snowden Leak: A Windfall for Hybrid Cloud?, 2013.

W. Vogels, Eventually consistent, vol.6, 2008.

M. Vukoli?, The Byzantine empire in the intercloud, SIGACT News, vol.41, issue.3, 2010.

H. Wada, A. Fekete, L. Zhao, K. Lee, and A. Liu, Data consistency properties and the trade-offs in commercial cloud storage: the consumers' perspective, Conference on Innovative Data Systems Research (CIDR), 2011.

Y. Wang, L. Alvisi, and M. Dahlin, Gnothi: separating data and metadata for efficient and available storage replication, USENIX Annual Technical Conference, USENIX ATC, 2012.

H. Weatherspoon and J. Kubiatowicz, Erasure coding vs. replication: A quantitative comparison, IPTPS, 2002.

S. A. Weil, S. A. Brandt, E. L. Miller, D. D. Long, and C. Maltzahn, Ceph: A scalable, high-performance distributed file system, OSDI, 2006.

J. R. Wilcox, D. Woos, P. Panchekha, Z. Tatlock, X. Wang et al., Verdi: a framework for implementing and formally verifying distributed systems, ACM SIGPLAN PLDI, 2015.

J. M. Wing and C. Gong, Testing and verifying concurrent objects, J. Parallel Distrib. Comput, vol.17, issue.1-2, 1993.

Z. Wu, M. Butkiewicz, D. Perkins, E. Katz-bassett, and H. V. Madhyastha, Spanstore: cost-effective geo-replicated storage spanning multiple cloud services, SOSP, 2013.

C. Xie, C. Su, C. Littley, L. Alvisi, M. Kapritsos et al., High-performance ACID via modular concurrency control, SOSP, 2015.

Y. Yang, G. Gopalakrishnan, G. Lindstrom, and K. Slind, Nemos: A framework for axiomatic and executable specifications of memory consistency models, International Parallel and Distributed Processing Symposium (IPDPS), 2004.

J. Yin, J. Martin, A. Venkataramani, L. Alvisi, and M. Dahlin, Separating agreement from execution for byzantine fault tolerant services, SOSP, 2003.

H. Yu and A. Vahdat, Design and evaluation of a conit-based continuous consistency model for replicated services, ACM Transactions on Computer Systems (TOCS), vol.20, issue.3, 2002.

D. Yuan, Y. Luo, X. Zhuang, G. R. Rodrigues, X. Zhao et al., Simple testing can prevent most critical failures: An analysis of production failures in distributed data-intensive systems, OSDI, 2014.

, High-performance theorem prover, Z3, 2016.

M. Zawirski, N. Preguiça, S. Duarte, A. Bieniusa, V. Balegas et al., Write fast, read in the past: Causal consistency for client-side applications, ACM/IFIP/USENIX Middleware Conference, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01248194

H. Zeineddine and W. Bazzi, Rationing data updates with consistency considerations in distributed systems, IEEE International Conference on Networks, ICON, 2011.

K. Zellag and B. Kemme, Consistency anomalies in multi-tier architectures: automatic detection and prevention, VLDB Journal, vol.23, issue.1, 2014.

A. Zeller and R. Hildebrandt, Simplifying and isolating failure-inducing input, IEEE Trans. Software Eng, vol.28, issue.2, 2002.

H. Zhang, M. Dong, and H. Chen, Efficient and available in-memory kv-store with hybrid erasure coding and replication, USENIX Conference on File and Storage Technologies, 2016.

I. Zhang, N. K. Sharma, A. Szekeres, A. Krishnamurthy, and D. R. Ports, Building consistent transactions with inconsistent replication, SOSP, 2015.

, It follows trivially from RVal(F) > SeqRVal(F)

, n: cloud stores, exposing key-value API as in Alg. 2 30: Client state variables: 31: ts ? TS , initially (0, ?) 32: cloudList ? {Ci × . . . × Ci} ? {?}, initially ? 33: operation put (k, v) 34: (ts, ?, ?, ?) ? RM DS.read(k, f alse) 35: if ts = ? then ts ? (0, cid) 36: ts ? (ts.sn + 1, cid) 37: cloudList ? ? 38: trigger timer 39: forall f + 1 selected clouds Ci do 40: Ci.put(k|ts, v) 41: wait until |cloudList| = f + 1 or timer expires 42: if |cloudList| < f + 1 then 43: forall f secondary clouds Ci do 44: Ci.put(k|ts, v) 45: wait until |cloudList| = f + 1 46: RM DS.condUpdate(k, ts, cloudList, H(v), size(v)) 47: trigger garbage collection // see Section 3.3.4 48: return ok 49: upon put(k|ts, v) completes at cloud Ci 50: cloudList ? cloudList ? {Ci} 51: operation get (k) // worst-case, Section 3.3.5 code only 52: (ts, cloudList, hash, size) ? RM DS.read(k, true) 53: if ts = ? or cloudList = ? then return ? 54: forall Ci ? cloudList do 55: Ci.get(k|ts) 56: upon get(k|ts) returns data from cloud Ci 57: if H(data) = hash then return data 58: else Ci.get(k|ts) 59: upon received notify(k, ts ? ) from RMDS such that ts ? > ts 60: cancel all pending get 61: return get (k) 62: operation list () 63: mdList ? RM DS.list() 64: forall md ? mdList do 65: if md.cloudList = ? then 66: mdList ? mdList \ {md} 67: return mdList 68: operation delete (k) 69: (ts, cloudList, ?, ?) ? RM DS.read(k, f alse) 70: if ts = ? or cloudList = ? then return ok 71: ts ? (ts.sn + 1, cid) 72: RM DS, Proposition B.4. SequentialConsistency > Causality Proof. First, we proceed to show that (SingleOrder ? PRAM) ? CausalArbitration. By SingleOrder and PRAM we have that vis ? ar and so ? vis. Thus, hb = (so ? vis) + ? Types: 25: TS = (N0 × N0) ? {?}, vol.26

D. Lemma, Let o and o ? be two get or put operations with timestamps ts(o) and ts(o ? ), respectively, such that o precedes o ? . Then ts(o) ? ts(o ? ), and if o ? is a, vol.2

, RM DS denotes calls to RMDS within operation o (and similarly for o ? ), the following

, Alg. 3, precedes (all possible calls to) o ? .RM DS.read() at line 52, Alg. 3 (resp., line 34, Alg. 3). By linearizability of RMDS (and RMDS functionality in Alg. 1) and definition of operation timestamps, it follows that ts(o ? ) ? ts(o). Moreover, if o ? is a put, then ts(o ? ) > ts(o) because ts(o ? ) is obtained from incrementing the timestamp ts returned by o ? .RM DS, vol.46

, at line 52 (resp. 34) follow the latest call of o.RM DS.read() in line 52, by Alg. 1 and by linearizability of RMDS, it follows that ts(o ? ) ? ts(o), then since all possible calls to o ? .RM DS.read(, vol.2

D. Lemma, Unique puts). If o and o ? are two put operations, then ts(o) ? = ts(o ? ), vol.2

. Proof, By lines 34-36, Alg. 3, RMDS functionality (Alg. 1) and the fact that a given client does not invoke concurrent operations on the same key

D. Lemma, Let rd be a get(k) operation returning value v ? = ?. Then there exists a single put operation wr of the form put(k, v) such that ts, vol.2

, rd receives v in response to get(k|ts(rd)) from some cloud C i . Suppose for the purpose of contradiction that v is never written by a put. Then, by the collision resistance of H(), the check at line 57 does not pass and rd does not return v. Therefore, we conclude that some operation wr issues put (k|ts(rd)) to C i in line 40. Hence, ts(wr) = ts(rd). Finally, Since rd returns v and has a timestamp ts(rd)

D. Theorem, Every execution ex of Algorithm 3 satisfies linearizability, vol.2

D. , Alternative proof of Hybris linearizability In this section, we prove the linearizability of the Hybris protocol ( § D.1) using the axiomatic framework we

, If o is a put, then ts(o) is the value of client's variable ts when its assignment completes at line 36, Alg. 3. Else, if o is a get, then ts(o) equals the value of ts when client executes line 57, Alg. 3 (i.e., when get returns). Without loss of generality, Preliminaries We define the timestamp of operation o, denoted ts(o), as follows

, Let st be an equivalence relation on H that groups pairs of operations having the same timestamp

, Let o and o ? be two get or put operations with timestamps ts(o) and ts(o ? ), respectively, such that o rb ? ? o ? . Then there exists a partial order tso ? ar \ st induced by timestamps such that: if o ? is a put then o tso ? ? o ?

, RM DS denotes calls to RMDS within operation o (and similarly for o ? ), the following

, Alg. 3, precedes (all possible calls to) o ? .RM DS.read() at line 52, Alg. 3 (resp., line 34, Alg. 3). By linearizability of RMDS (and RMDS functionality in Alg. 1) and definition of operation timestamps, it follows that ts(o ? ) ? ts(o). Moreover, if o ? is a put, then o tso ? ? o ? , because ts(o ? ) is obtained from incrementing the timestamp ts returned by o ? .RM DS, vol.46

, at line 52 (resp. 34) follow the latest call of o.RM DS.read() in line 52, by Alg. 1 and by linearizability of RMDS, it follows that ts(o ? ) ? ts(o). If o ? is a put, then since all possible calls to o ? .RM DS.read(, vol.2

, No two operations ordered by the returns-before partial order have strictly decreasing timestamps. Formally: ?a, b ? H : a rb ? ? b ? b tso ? ? a ? rb ? st ? tso

D. Lemma, Unique timestamps of puts). If o and o ? are two put operations, then

. Proof, By lines 34-36, Alg. 3, RMDS functionality (Alg. 1) and the fact that a given client does

D. Lemma, Let rd be a get(k) operation returning value v ? = ?. Then, there exists a single put operation wr of the form put(k, v) such that rd ? st wr, vol.3

, De plus, grâce à l'approche axiomatique que nous avons adoptée, nous avons mis en place

, En outre, nous établissons la correspondance entre ces sémantiques et les implémentations de prototypes et de systèmes décrit dans la littérature de recherche (Annexe C). Enfin, dans l'Annexe B, nous fournissons des preuves de relations de force entre les modèles sémantiques