The formal definitions we use in this paper are based on those given in~[24, 15].  Biswas and Enea~[13] shows that checking whether an execution is \ccc{} is polynomial time while checking whether it is \pcc{} or \sic{} is NP-complete.

%In this paper we tackle trace-based robustness problem. In the literature, the decidability and complexity of trace-based
The robustness problem we study in this paper has been investigated in the context of weak memory models, but only relative to sequential consistency, against Release/Aquire (RA), TSO and Power~[35, 16, 14, 28]. Checking robustness against \ccc{}  and \sic{} relative to \serc{} has been investigated in~[9, 10].
%All of these work study the robustness between a weak consistency model (e.g., RA, TSO, or \ccc{}) and the strong semantics model, i.e., sequential consistency and serialisability.
%On the other hand,
In this work, we study the robustness problem between two weak consistency models, which poses different non-trivial challenges.
In particular, previous work proposed reductions to reachability under sequential consistency (or \serc{}) that relied on a concept of minimal robustness violations (w.r.t. an operational semantics), which does not apply in our case.
% an important technique that was commonly used in previous work which consists of using borderline violations
%cannot be applied here. Since, these violations defined such that removing the last action in the violation results in serialisable execution which is not valid in our case.
%However, we have reduced the robustness against \ccc{} relative to \pcc{} to the robustness against \ccc{} relative to \serc{} which allowed us to use the results that were proved in [12, 10].
%Note that our reduction from \pcc{} to \serc{} is similar in spirit to the one shown in [43], however,
%in our case execution traces include the store order dependency relation in order to construct the happens before relation.
The relationship between \pcc{} and \serc{} is similar in spirit to the one given by Biswas and Enea~[13] in the context of checking whether an execution is \pcc{}. However, that relationship was proven in the context of a ``weaker'' notion of trace (containing only program order and read-from), and it does not extend to our notion of trace. For instance, that result does not imply preserving $$ dependencies which is crucial in our case.

Some works describe various over- or under-approximate analyses for checking robustness relative to \serc{}. The works in~[12, 17, 18, 25, 39] propose static analysis techniques based on computing an abstraction of the set of computations, which is used for proving robustness.
In particular, [18, 39] encode program executions under the weak consistency model
using FOL formulas to describe the dependency relations between actions in the executions.
These approaches may return false alarms due to the abstractions they consider in their encoding.
Note that in this paper, we prove a strengthening of the results of [12] with regard to the shape of happens before cycles allowed under \pcc{}.

An alternative to {\em trace-based} robustness, is {\em state-based} robustness which requires that a program is robust if the sets of reachable states under two semantics coincide.
While state-robustness is the necessary and sufficient concept for preserving state-invariants, its verification, which amounts in computing the set of reachable states under the weak semantics models is in general a hard problem.
The decidability and the complexity of this problem has been investigated in the context of relaxed memory models such as TSO and Power, and it has been shown that it is either decidable but highly complex (non-primitive recursive), or undecidable [5, 6].
Automatic procedures for approximate reachability/invariant checking have been proposed using either abstractions or bounded analyses, e.g., [7, 4, 27, 1]. Proof methods have also been developed for verifying invariants in the context of weakly consistent models such as [36, 31, 40, 3]. These methods, however, do not provide decision procedures.
%   \section{Conclusion}
\label{sec:conclusion}
We have proposed a reduction of the problem of checking robustness between weak consistency models to reachability that increases the size of the program only linearly, and therefore, we showed that checking robustness is in principle as hard as checking reachability.
Then, we gave a pragmatic technique for proving robustness based on the notion of non-mover relations that can be constructed automatically using SMT solvers. We tested our techniques on realistic programs that model the most intricate parts of distributed applications that are obtained from the standard OLTP Benchmark and open source Github projects.

\bibliographystyle{splncs04}
\begin{thebibliography}{10}
\providecommand{\url}[1]{\texttt{#1}}
\providecommand{\urlprefix}{URL }
\providecommand{\doi}[1]{https://doi.org/#1}

[1]
Abdulla, P.A., Atig, M.F., Bouajjani, A., Ngo, T.P.: Context-bounded analysis
for {POWER}. In: Legay, A., Margaria, T. (eds.) Tools and Algorithms for the
Construction and Analysis of Systems - 23rd International Conference, {TACAS}
2017, Held as Part of the European Joint Conferences on Theory and Practice
of Software, {ETAPS} 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings,
Part {II}. Lecture Notes in Computer Science, vol. 10206, pp. 56--74 (2017).
\doi{10.1007/978-3-662-54580-5\_4},
\url{https://doi.org/10.1007/978-3-662-54580-5\_4}

[2]
Adya, A.: Weak consistency: A generalized theory and optimistic implementations
for distributed transactions. Ph.D. thesis (1999)

[3]
Alglave, J., Cousot, P.: Ogre and pythia: an invariance proof method for weak
consistency models. In: Castagna, G., Gordon, A.D. (eds.) Proceedings of the
44th {ACM} {SIGPLAN} Symposium on Principles of Programming Languages, {POPL}
2017, Paris, France, January 18-20, 2017. pp. 3--18. {ACM} (2017),
\url{http://dl.acm.org/citation.cfm?id=3009883}

[4]
Alglave, J., Kroening, D., Tautschnig, M.: Partial orders for efficient bounded
model checking of concurrent software. In: Sharygina, N., Veith, H. (eds.)
Computer Aided Verification - 25th International Conference, {CAV} 2013,
Saint Petersburg, Russia, July 13-19, 2013. Proceedings. Lecture Notes in
Computer Science, vol.~8044, pp. 141--157. Springer (2013).
\doi{10.1007/978-3-642-39799-8\_9},
\url{https://doi.org/10.1007/978-3-642-39799-8\_9}

[5]
Atig, M.F., Bouajjani, A., Burckhardt, S., Musuvathi, M.: On the verification
problem for weak memory models. In: Hermenegildo, M.V., Palsberg, J. (eds.)
Proceedings of the 37th {ACM} {SIGPLAN-SIGACT} Symposium on Principles of
Programming Languages, {POPL} 2010, Madrid, Spain, January 17-23, 2010. pp.
7--18. {ACM} (2010). \doi{10.1145/1706299.1706303},
\url{https://doi.org/10.1145/1706299.1706303}

[6]
Atig, M.F., Bouajjani, A., Burckhardt, S., Musuvathi, M.: What's decidable
about weak memory models? In: Seidl, H. (ed.) Programming Languages and
Systems - 21st European Symposium on Programming, {ESOP} 2012, Held as Part
of the European Joint Conferences on Theory and Practice of Software, {ETAPS}
2012, Tallinn, Estonia, March 24 - April 1, 2012. Proceedings. Lecture Notes
in Computer Science, vol.~7211, pp. 26--46. Springer (2012).
\doi{10.1007/978-3-642-28869-2\_2},
\url{https://doi.org/10.1007/978-3-642-28869-2\_2}

[7]
Atig, M.F., Bouajjani, A., Parlato, G.: Getting rid of store-buffers in {TSO}
analysis. In: Gopalakrishnan, G., Qadeer, S. (eds.) Computer Aided
Verification - 23rd International Conference, {CAV} 2011, Snowbird, UT, USA,
July 14-20, 2011. Proceedings. Lecture Notes in Computer Science, vol.~6806,
pp. 99--115. Springer (2011). \doi{10.1007/978-3-642-22110-1\_9},
\url{https://doi.org/10.1007/978-3-642-22110-1\_9}

[8]
Barnett, M., Chang, B.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: {A}
modular reusable verifier for object-oriented programs. In: de~Boer, F.S.,
Bonsangue, M.M., Graf, S., de~Roever, W.P. (eds.) Formal Methods for
Components and Objects, 4th International Symposium, {FMCO} 2005, Amsterdam,
The Netherlands, November 1-4, 2005, Revised Lectures. Lecture Notes in
Computer Science, vol.~4111, pp. 364--387. Springer (2005).
\doi{10.1007/11804192\_17}, \url{https://doi.org/10.1007/11804192\_17}

[9]
Beillahi, S.M., Bouajjani, A., Enea, C.: Checking robustness against snapshot
isolation. In: Dillig, I., Tasiran, S. (eds.) Computer Aided Verification -
31st International Conference, {CAV} 2019, New York City, NY, USA, July
15-18, 2019, Proceedings, Part {II}. Lecture Notes in Computer Science, vol.
11562, pp. 286--304. Springer (2019). \doi{10.1007/978-3-030-25543-5\_17},
\url{https://doi.org/10.1007/978-3-030-25543-5\_17}

[10]
Beillahi, S.M., Bouajjani, A., Enea, C.: Robustness against transactional
causal consistency. In: Fokkink, W.J., van Glabbeek, R. (eds.) 30th
International Conference on Concurrency Theory, {CONCUR} 2019, August 27-30,
2019, Amsterdam, the Netherlands. LIPIcs, vol.~140, pp. 30:1--30:18. Schloss
Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik (2019).
\doi{10.4230/LIPIcs.CONCUR.2019.30},
\url{https://doi.org/10.4230/LIPIcs.CONCUR.2019.30}

[11]
Berenson, H., Bernstein, P.A., Gray, J., Melton, J., O'Neil, E.J., O'Neil,
P.E.: A critique of {ANSI} {SQL} isolation levels. In: Carey, M.J.,
Schneider, D.A. (eds.) Proceedings of the 1995 {ACM} {SIGMOD} International
Conference on Management of Data, San Jose, California, USA, May 22-25, 1995.
pp. 1--10. {ACM} Press (1995). \doi{10.1145/223784.223785},
\url{https://doi.org/10.1145/223784.223785}

[12]
Bernardi, G., Gotsman, A.: Robustness against consistency models with atomic
visibility. In: Desharnais, J., Jagadeesan, R. (eds.) 27th International
Conference on Concurrency Theory, {CONCUR} 2016, August 23-26, 2016,
Qu{\'{e}}bec City, Canada. LIPIcs, vol.~59, pp. 7:1--7:15. Schloss Dagstuhl -
Leibniz-Zentrum f{\"{u}}r Informatik (2016).
\doi{10.4230/LIPIcs.CONCUR.2016.7},
\url{https://doi.org/10.4230/LIPIcs.CONCUR.2016.7}

[13]
Biswas, R., Enea, C.: On the complexity of checking transactional consistency.
Proc. {ACM} Program. Lang.  \textbf{3}({OOPSLA}),  165:1--165:28 (2019).
\doi{10.1145/3360591}, \url{https://doi.org/10.1145/3360591}

[14]
Bouajjani, A., Derevenetc, E., Meyer, R.: Checking and enforcing robustness
against {TSO}. In: Felleisen, M., Gardner, P. (eds.) Programming Languages
and Systems - 22nd European Symposium on Programming, {ESOP} 2013, Held as
Part of the European Joint Conferences on Theory and Practice of Software,
{ETAPS} 2013, Rome, Italy, March 16-24, 2013. Proceedings. Lecture Notes in
Computer Science, vol.~7792, pp. 533--553. Springer (2013).
\doi{10.1007/978-3-642-37036-6\_29},
\url{https://doi.org/10.1007/978-3-642-37036-6\_29}

[15]
Bouajjani, A., Enea, C., Guerraoui, R., Hamza, J.: On verifying causal
consistency. In: Castagna, G., Gordon, A.D. (eds.) Proceedings of the 44th
{ACM} {SIGPLAN} Symposium on Principles of Programming Languages, {POPL}
2017, Paris, France, January 18-20, 2017. pp. 626--638. {ACM} (2017),
\url{http://dl.acm.org/citation.cfm?id=3009888}

[16]
Bouajjani, A., Meyer, R., M{\"{o}}hlmann, E.: Deciding robustness against total
store ordering. In: Aceto, L., Henzinger, M., Sgall, J. (eds.) Automata,
Languages and Programming - 38th International Colloquium, {ICALP} 2011,
Zurich, Switzerland, July 4-8, 2011, Proceedings, Part {II}. Lecture Notes in
Computer Science, vol.~6756, pp. 428--440. Springer (2011).
\doi{10.1007/978-3-642-22012-8\_34},
\url{https://doi.org/10.1007/978-3-642-22012-8\_34}

[17]
Brutschy, L., Dimitrov, D., M{\"{u}}ller, P., Vechev, M.T.: Serializability for
eventual consistency: criterion, analysis, and applications. In: Castagna,
G., Gordon, A.D. (eds.) Proceedings of the 44th {ACM} {SIGPLAN} Symposium on
Principles of Programming Languages, {POPL} 2017, Paris, France, January
18-20, 2017. pp. 458--472. {ACM} (2017),
\url{http://dl.acm.org/citation.cfm?id=3009895}

[18]
Brutschy, L., Dimitrov, D., M{\"{u}}ller, P., Vechev, M.T.: Static
serializability analysis for causal consistency. In: Foster, J.S., Grossman,
D. (eds.) Proceedings of the 39th {ACM} {SIGPLAN} Conference on Programming
Language Design and Implementation, {PLDI} 2018, Philadelphia, PA, USA, June
18-22, 2018. pp. 90--104. {ACM} (2018). \doi{10.1145/3192366.3192415},
\url{https://doi.org/10.1145/3192366.3192415}

[19]
Burckhardt, S.: Principles of eventual consistency. Found. Trends Program.
Lang.  \textbf{1}(1-2),  1--150 (2014). \doi{10.1561/2500000011},
\url{https://doi.org/10.1561/2500000011}

[20]
Burckhardt, S., Gotsman, A., Yang, H., Zawirski, M.: Replicated data types:
specification, verification, optimality. In: Jagannathan, S., Sewell, P.
(eds.) The 41st Annual {ACM} {SIGPLAN-SIGACT} Symposium on Principles of
Programming Languages, {POPL} '14, San Diego, CA, USA, January 20-21, 2014.
pp. 271--284. {ACM} (2014). \doi{10.1145/2535838.2535848},
\url{https://doi.org/10.1145/2535838.2535848}

[21]
Burckhardt, S., Leijen, D., Protzenko, J., F{\"{a}}hndrich, M.: Global sequence
protocol: {A} robust abstraction for replicated shared state. In: Boyland,
J.T. (ed.) 29th European Conference on Object-Oriented Programming, {ECOOP}
2015, July 5-10, 2015, Prague, Czech Republic. LIPIcs, vol.~37, pp. 568--590.
Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik (2015).
\doi{10.4230/LIPIcs.ECOOP.2015.568},
\url{https://doi.org/10.4230/LIPIcs.ECOOP.2015.568}

[22]
Cahill, M.J., R{\"{o}}hm, U., Fekete, A.D.: Serializable isolation for snapshot
databases. {ACM} Trans. Database Syst.  \textbf{34}(4),  20:1--20:42 (2009).
\doi{10.1145/1620585.1620587}, \url{https://doi.org/10.1145/1620585.1620587}

[23]
Cassandra-lock: \url{https://github.com/dekses/cassandra-lock}

[24]
Cerone, A., Bernardi, G., Gotsman, A.: A framework for transactional
consistency models with atomic visibility. In: Aceto, L., de~Frutos{-}Escrig,
D. (eds.) 26th International Conference on Concurrency Theory, {CONCUR} 2015,
Madrid, Spain, September 1.4, 2015. LIPIcs, vol.~42, pp. 58--71. Schloss
Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik (2015).
\doi{10.4230/LIPIcs.CONCUR.2015.58},
\url{https://doi.org/10.4230/LIPIcs.CONCUR.2015.58}

[25]
Cerone, A., Gotsman, A.: Analysing snapshot isolation. J. {ACM}
\textbf{65}(2),  11:1--11:41 (2018). \doi{10.1145/3152396},
\url{https://doi.org/10.1145/3152396}

[26]
Cerone, A., Gotsman, A., Yang, H.: Algebraic laws for weak consistency. In:
Meyer, R., Nestmann, U. (eds.) 28th International Conference on Concurrency
Theory, {CONCUR} 2017, September 5-8, 2017, Berlin, Germany. LIPIcs, vol.~85,
pp. 26:1--26:18. Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik
(2017). \doi{10.4230/LIPIcs.CONCUR.2017.26},
\url{https://doi.org/10.4230/LIPIcs.CONCUR.2017.26}

[27]
Dan, A.M., Meshman, Y., Vechev, M.T., Yahav, E.: Effective abstractions for
verification under relaxed memory models. Comput. Lang. Syst. Struct.
\textbf{47},  62--76 (2017). \doi{10.1016/j.cl.2016.02.003},
\url{https://doi.org/10.1016/j.cl.2016.02.003}

[28]
Derevenetc, E., Meyer, R.: Robustness against power is pspace-complete. In:
Esparza, J., Fraigniaud, P., Husfeldt, T., Koutsoupias, E. (eds.) Automata,
Languages, and Programming - 41st International Colloquium, {ICALP} 2014,
Copenhagen, Denmark, July 8-11, 2014, Proceedings, Part {II}. Lecture Notes
in Computer Science, vol.~8573, pp. 158--170. Springer (2014).
\doi{10.1007/978-3-662-43951-7\_14},
\url{https://doi.org/10.1007/978-3-662-43951-7\_14}

[29]
Difallah, D.E., Pavlo, A., Curino, C., Cudr{\'{e}}{-}Mauroux, P.: Oltp-bench:
An extensible testbed for benchmarking relational databases. Proc. {VLDB}
Endow.  \textbf{7}(4),  277--288 (2013). \doi{10.14778/2732240.2732246},
\url{http://www.vldb.org/pvldb/vol7/p277-difallah.pdf}

[30]
Experiments: \url{https://github.com/relative-robustness/artifact}

[31]
Gotsman, A., Yang, H., Ferreira, C., Najafzadeh, M., Shapiro, M.: 'cause i'm
strong enough: reasoning about consistency choices in distributed systems.
In: Bod{\'{\i}}k, R., Majumdar, R. (eds.) Proceedings of the 43rd Annual
{ACM} {SIGPLAN-SIGACT} Symposium on Principles of Programming Languages,
{POPL} 2016, St. Petersburg, FL, USA, January 20 - 22, 2016. pp. 371--384.
{ACM} (2016). \doi{10.1145/2837614.2837625},
\url{https://doi.org/10.1145/2837614.2837625}

[32]
Hawblitzel, C., Petrank, E., Qadeer, S., Tasiran, S.: Automated and modular
refinement reasoning for concurrent programs. In: Kroening, D., Pasareanu,
C.S. (eds.) Computer Aided Verification - 27th International Conference,
{CAV} 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part {II}.
Lecture Notes in Computer Science, vol.~9207, pp. 449--465. Springer (2015).
\doi{10.1007/978-3-319-21668-3\_26},
\url{https://doi.org/10.1007/978-3-319-21668-3\_26}

[33]
Holt, B., Bornholt, J., Zhang, I., Ports, D.R.K., Oskin, M., Ceze, L.:
Disciplined inconsistency with consistency types. In: Aguilera, M.K., Cooper,
B., Diao, Y. (eds.) Proceedings of the Seventh {ACM} Symposium on Cloud
Computing, Santa Clara, CA, USA, October 5-7, 2016. pp. 279--293. {ACM}
(2016). \doi{10.1145/2987550.2987559},
\url{https://doi.org/10.1145/2987550.2987559}

[34]
Kozen, D.: Lower bounds for natural proof systems. In: 18th Annual Symposium on
Foundations of Computer Science, Providence, Rhode Island, USA, 31 October -
1 November 1977. pp. 254--266. {IEEE} Computer Society (1977).
\doi{10.1109/SFCS.1977.16}, \url{https://doi.org/10.1109/SFCS.1977.16}

[35]
Lahav, O., Margalit, R.: Robustness against release/acquire semantics. In:
McKinley, K.S., Fisher, K. (eds.) Proceedings of the 40th {ACM} {SIGPLAN}
Conference on Programming Language Design and Implementation, {PLDI} 2019,
Phoenix, AZ, USA, June 22-26, 2019. pp. 126--141. {ACM} (2019).
\doi{10.1145/3314221.3314604}, \url{https://doi.org/10.1145/3314221.3314604}

[36]
Lahav, O., Vafeiadis, V.: Owicki-gries reasoning for weak memory models. In:
Halld{\'{o}}rsson, M.M., Iwama, K., Kobayashi, N., Speckmann, B. (eds.)
Automata, Languages, and Programming - 42nd International Colloquium, {ICALP}
2015, Kyoto, Japan, July 6-10, 2015, Proceedings, Part {II}. Lecture Notes in
Computer Science, vol.~9135, pp. 311--323. Springer (2015).
\doi{10.1007/978-3-662-47666-6\_25},
\url{https://doi.org/10.1007/978-3-662-47666-6\_25}

[37]
Lamport, L.: Time, clocks, and the ordering of events in a distributed system.
Commun. {ACM}  \textbf{21}(7),  558--565 (1978). \doi{10.1145/359545.359563},
\url{https://doi.org/10.1145/359545.359563}

[38]
Lipton, R.J.: Reduction: {A} method of proving properties of parallel programs.
Commun. {ACM}  \textbf{18}(12),  717--721 (1975).
\doi{10.1145/361227.361234}, \url{https://doi.org/10.1145/361227.361234}

[39]
Nagar, K., Jagannathan, S.: Automated detection of serializability violations
under weak consistency. In: Schewe, S., Zhang, L. (eds.) 29th International
Conference on Concurrency Theory, {CONCUR} 2018, September 4-7, 2018,
Beijing, China. LIPIcs, vol.~118, pp. 41:1--41:18. Schloss Dagstuhl -
Leibniz-Zentrum f{\"{u}}r Informatik (2018).
\doi{10.4230/LIPIcs.CONCUR.2018.41},
\url{https://doi.org/10.4230/LIPIcs.CONCUR.2018.41}

[40]
Najafzadeh, M., Gotsman, A., Yang, H., Ferreira, C., Shapiro, M.: The {CISE}
tool: proving weakly-consistent applications correct. In: Alvaro, P.,
Bessani, A. (eds.) Proceedings of the 2nd Workshop on the Principles and
Practice of Consistency for Distributed Data, PaPoC@EuroSys 2016, London,
United Kingdom, April 18, 2016. pp. 2:1--2:3. {ACM} (2016).
\doi{10.1145/2911151.2911160}, \url{https://doi.org/10.1145/2911151.2911160}

[41]
Papadimitriou, C.H.: The serializability of concurrent database updates. J.
{ACM}  \textbf{26}(4),  631--653 (1979). \doi{10.1145/322154.322158},
\url{https://doi.org/10.1145/322154.322158}

[42]
Perrin, M., Most{\'{e}}faoui, A., Jard, C.: Causal consistency: beyond memory.
In: Asenjo, R., Harris, T. (eds.) Proceedings of the 21st {ACM} {SIGPLAN}
Symposium on Principles and Practice of Parallel Programming, PPoPP 2016,
Barcelona, Spain, March 12-16, 2016. pp. 26:1--26:12. {ACM} (2016).
\doi{10.1145/2851141.2851170}, \url{https://doi.org/10.1145/2851141.2851170}

[43]
Raad, A., Lahav, O., Vafeiadis, V.: On the semantics of snapshot isolation. In:
Enea, C., Piskac, R. (eds.) Verification, Model Checking, and Abstract
Interpretation - 20th International Conference, {VMCAI} 2019, Cascais,
Portugal, January 13-15, 2019, Proceedings. Lecture Notes in Computer
Science, vol. 11388, pp. 1--23. Springer (2019).
\doi{10.1007/978-3-030-11245-5\_1},
\url{https://doi.org/10.1007/978-3-030-11245-5\_1}

[44]
Rackoff, C.: The covering and boundedness problems for vector addition systems.
Theor. Comput. Sci.  \textbf{6},  223--231 (1978).
\doi{10.1016/0304-3975(78)90036-1},
\url{https://doi.org/10.1016/0304-3975(78)90036-1}

[45]
Shapiro, M., Ardekani, M.S., Petri, G.: Consistency in 3d. In: Desharnais, J.,
Jagadeesan, R. (eds.) 27th International Conference on Concurrency Theory,
{CONCUR} 2016, August 23-26, 2016, Qu{\'{e}}bec City, Canada. LIPIcs,
vol.~59, pp. 3:1--3:14. Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r
Informatik (2016). \doi{10.4230/LIPIcs.CONCUR.2016.3},
\url{https://doi.org/10.4230/LIPIcs.CONCUR.2016.3}

[46]
Shasha, D.E., Snir, M.: Efficient and correct execution of parallel programs
that share memory. {ACM} Trans. Program. Lang. Syst.  \textbf{10}(2),
282--312 (1988). \doi{10.1145/42190.42277},
\url{https://doi.org/10.1145/42190.42277}

[47]
Trade: \url{https://github.com/Haiyan2/Trade}

[48]
Twitter: \url{https://github.com/edmundophie/cassandra-twitter}

\end{thebibliography}

%%%%% To display Open Access text and logo, Please add below text and copy the cc_by_4-0.eps in the manuscript package %%%

\vfill

{\small\medskip\noindent{\bf Open Access} This chapter is licensed under the terms of the Creative Commons\break Attribution 4.0 International License (\url{http://creativecommons.org/licenses/by/4.0/}), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.}

{\small \spaceskip .28em plus .1em minus .1em The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material.~If material is not included in the chapter's Creative Commons license and your intended\break use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.}

\medskip\noindent\includegraphics{cc.pdf}

%% Appendix
\appendix
\newpage
%!TEX root = draft.tex
\section{Proofs for Section \ref{sec:CCPCrobustness}}
\label{sec:CCPCrobustnessProofs}

\begin{proof}[Proof of Lemma \ref{lem:Transform}]
We start with the case $\textsf{X} = \ccc$.  We first show that $\atrace_\pcinstr$ satisfies $\axpoco$ and $\axcoarb$. For $\axpoco$, let $\atr_{1}' \in \{\atrrd{\atr_{1}},\atrwr{\atr_{1}}\}$ and $\atr_{2}' \in \{\atrrd{\atr_{2}},\atrwr{\atr_{2}}\}$, such that $(\atr_{1}',\atr_{2}') \in (\po_\pcinstr\cup\rfo_\pcinstr)^{+}$. By the definition of $\viso_\pcinstr$, we have that either $(\atr_{1}'=\atrrd{\atr_{1}},\atr_{2}'=\atrwr{\atr_{2}}) \in \po_\pcinstr$ and $\atr_1 = \atr_2$ or $(\atr_{1},\atr_2) \in (\po\cup\rfo)^{+}$, which implies that $(\atr_{1},\atr_2) \in \viso$. In both cases we obtain that $(\atr_{1}',\atr_{2}') \in \viso_\pcinstr$. The axiom $\axpoco$ can be proved in a similar way.
%        \item $\axcoarb$: the same proof steps as in $\axpoco$.
%    \end{itemize}

Next, we show that $\atrace_\pcinstr$ satisfies the property $\axretval$.  Let $\atr$ be a transaction in $\atrace$ that contains a read event $\readact(\atr,\anaddr,\aval)$.
Let $\atr_0$ be the transaction in $\atrace$ such that
$$\atr_0 = Max_{\arbo}(\{\atr' \in \atrace\ |\ (\atr',\atr) \in \viso \wedge \exists\ \writeact(\atr',\anaddr,\cdot)\in\amap(\atr')\}).$$
The read value $\aval$ must have been written by $\atr_0$ since $\atrace$ satisfies $\axretval$. Thus, the read $\readact(\atr,\anaddr,\aval)$ in $\atrrd{\atr}$ of $\atrace_\pcinstr$ must return the value written by $\atrwr{\atr_0}$.
From the definitions of $\viso_\pcinstr$ and $\arbo_\pcinstr$, we get
$$\atrwr{\atr_1}\in\{\atrwr{\atr'} \in \atrace_\pcinstr\ |\ (\atrwr{\atr'},\atrrd{\atr}) \in \viso_\pcinstr \wedge \exists\ \writeact(\atrwr{\atr'},\anaddr,\cdot)\in\amap(\atrwr{\atr'})\}$$
$$\atr_1 \in \{\atr' \in \atrace\ |\ (\atr',\atr) \in \viso \wedge \exists\ \writeact(\atr',\anaddr,\cdot)\in\amap(\atr')\}$$
because $(\atrwr{\atr_{1}},\atrrd{\atr_{2}}) \in \viso_\pcinstr$ implies $(\atr_{1},\atr_{2}) \in \viso$. Since $(\atrwr{\atr_{1}},\atrwr{\atr_{2}}) \in \arbo_\pcinstr$ implies $(\atr_{1},\atr_{2}) \in \arbo$, we also obtain that
$$\atrwr{\atr_0} = Max_{\arbo_\pcinstr}(\{\atrwr{\atr'} \in \atrace_\pcinstr\ |\ (\atrwr{\atr'},\atrrd{\atr}) \in \viso_\pcinstr \wedge \exists\ \writeact(\atrwr{\atr'},\anaddr,\cdot)\in\amap(\atrwr{\atr'})\})$$
and since the read $\readact(\atr,\anaddr,\aval)$ in $\atrrd{\atr}$ of $\atrace_\pcinstr$ returns the value written by $\atrwr{\atr_0}$, $\atrace_\pcinstr$ satisfies $\axretval$.

For the case $\textsf{X} = \pcc$, we show that $\atrace_\pcinstr$ satisfies the property $\axprefix$ (the other axioms are proved as in the case of $\ccc$).
% In the previous case we already showed that $\axpoco$ and $\axcoarb$ hold.
%     Now we will show that $\atrace_\pcinstr$ satisfies the property $\axprefix$.
Suppose we have $(\atr_{1}',\atr_{2}') \in \arbo_\pcinstr$ and $(\atr_{2}',\atr_{3}') \in \viso_\pcinstr$ where $\atr_{1}' \in \{\atrrd{\atr_{1}},\atrwr{\atr_{1}}\}$, $\atr_{2}' \in \{\atrrd{\atr_{2}},\atrwr{\atr_{2}}\}$, and $\atr_{3}' \in \{\atrrd{\atr_{3}},\atrwr{\atr_{3}}\}$. The are five cases to be discussed:
\begin{enumerate} %[label=\alph*]
\item $(\atr_{1}'=\atrrd{\atr_{1}},\atr_{2}'=\atrwr{\atr_{2}}) \in \po_\pcinstr$ and $\atr_1 = \atr_2$ and $(\atr_{2},\atr_{3}) \in \viso$,
\item $(\atr_{1},\atr_{2}) \in \arbo$ and $(\atr_{2},\atr_{3}) \in \viso$,
\item $(\atr_{1},\atr_{2}) \in \arbo$ and $(\atr_{2}'=\atrrd{\atr_{2}},\atr_{3}'=\atrwr{\atr_{3}}) \in \po_\pcinstr$ and $\atr_2 =  \atr_3$,
\item $(\atr_{1}'=\atrrd{\atr_{1}},\atr_{2}'=\atrwr{\atr_{2}}) \in \po_\pcinstr$ and $\atr_1 = \atr_2$ and $(\atr_{2},\atr_{3}) \in \arbo$ and $\atr_{3}'= \atrwr{\atr_{3}}$,
\item $(\atr_{1},\atr_{2}) \in \arbo$ and $(\atr_{2},\atr_{3}) \in \arbo$ and $\atr_{3}'= \atrwr{\atr_{3}}$.
\end{enumerate}
Cases (a) and (b) imply that $(\atr_{1},\atr_{3}) \in \viso$ since $\arbo;\viso \subset \arbo$, which implies that $(\atr_{1}',\atr_{3}') \in \viso_\pcinstr$. Cases (c), (d), and (e) imply that $(\atr_{1},\atr_{3}) \in \arbo$ and $\atr_{3}'= \atrwr{\atr_{3}}$ then
we get that $(\atrwr{\atr_{1}},\atrwr{\atr_{3}}) \in \viso_\pcinstr$ and $\atr_{3}'= \atrwr{\atr_{3}}$ which means that
$(\atr_{1}',\atr_{3}') \in \viso_\pcinstr$.

Note that the rule $(\atrwr{\atr_{1}},\atrwr{\atr_{2}}) \in \viso_\pcinstr$ if $(\atr_{1},\atr_{2}) \in \arbo$ cannot change the fact that $$\atrwr{\atr_1}\in\{\atrwr{\atr'} \in \atrace_\pcinstr\ |\ (\atrwr{\atr'},\atrrd{\atr}) \in \viso_\pcinstr \wedge \exists\ \writeact(\atrwr{\atr'},\anaddr,\cdot)\in\amap(\atrwr{\atr'})\}$$ iff $$\atr_1 \in \{\atr' \in \atrace\ |\ (\atr',\atr) \in \viso \wedge \exists\ \writeact(\atr',\anaddr,\cdot)\in\amap(\atr')\}$$ Thus, the proof of $\axretval$ follows as in the previous case.

For the case $\textsf{X} = \sic$, we show that $\atrace_\pcinstr$ satisfies $\axconflict$. If $(\atrwr{\atr_{1}},\atrwr{\atr_{2}}) \in \sto_\pcinstr$, then $(\atr_{1},\atr_{2}) \in \sto \subset \viso$, which implies that $(\atrwr{\atr_{1}},\atrrd{\atr_{2}}) \in \viso_\pcinstr$. Therefore, $(\atrwr{\atr_{1}},\atrwr{\atr_{2}}) \in \viso_\pcinstr$, which concludes the proof. The axiom $\axretval$ can be proved as in the previous cases.
%Thus, the property $\axconflict$ holds. Also, we prove in the same way as the previous two cases that $\atrace_\pcinstr$ satisfies the property $\axretval$.
\end{proof}

\begin{proof}[Proof of Lemma \ref{lem:cycles}]
($\Rightarrow$) Let $\atrace$ be a trace under \ccc{}. From $\axpoco$ and $\axcoarb$ we get that $\arbo_{0}^{+} \subset \arbo$, and $\arbo_{0}^{+}$ is acyclic because $\arbo$ is total order.  Assume by contradiction that $\viso_{0}^{+};\cfo$ is cyclic which implies that $\viso;\cfo$ is cyclic since $\viso_{0}^{+} \subset \viso$, which means that there exist $\atr_1$ and $\atr_2$ such that $(\atr_1, \atr_2) \in \viso$ and $(\atr_2, \atr_1) \in \cfo$.
$(\atr_2, \atr_1) \in \cfo$ implies that there exists $\atr_3$ such that $(\atr_3, \atr_1) \in \sto$ and $(\atr_3, \atr_2) \in \rfo$.
Based on the definition of $\axretval$, $\atr_3$ has two possible instances:
\begin{itemize}
\item $\atr_3$ corresponds to the "fictional" transaction that wrote the initial values which cannot be the case when $(\atr_1, \atr_2) \in \viso$ and $\atr_1$ writes to the same variable that $\atr_2$ reads from,
\item $\atr_3$ is the last transaction that occurs before $\atr_2$ that writes the value read by $\atr_2$, which means that
$(\atr_1,\atr_3) \in \arbo$ which contradicts the fact that $(\atr_3, \atr_1) \in \sto$ since $\sto \subset \arbo$.
\end{itemize}

($\Leftarrow$) Let $\atrace$ be a trace such that $\arbo_{0}^{+}$ and $\viso_{0}^{+};\cfo$ are acyclic. Then, we define the relations $\viso$ and $\arbo$ such that $\viso = \viso_{0}^{+}$ and $\arbo$ is any total order that includes $\arbo_{0}^{+}$. Then, we obtain that $(\viso \cup \sto)^{+} \subset \arbo$ and $\viso;\cfo$ is acyclic. Thus, $\atrace$ satisfies the properties $\axpoco$ and $\axcoarb$. Next, we will show that $\atrace$ satisfies $\axretval$.
Let $\atr$ be a transaction in $\atrace$ that contains a read event $\readact(\atr,\anaddr,\aval)$.
Let $\atr_0$ be transaction in $\atrace$ such that $$\atr_0 = Max_{\arbo}(\{\atr' \in \atrace\ |\ (\atr',\atr) \in \viso \wedge \exists\ \writeact(\atr',\anaddr,\cdot)\in\amap(\atr')\})$$ then the read must return a value written by $\atr_0$.
Assume by contradiction that there exists some other transaction $\atr_1 \neq \atr_0$ such that $(\atr_1,\atr) \in \rfo$.
Then, we get that $(\atr_1,\atr_0) \in \arbo$ and both write to $\anaddr$, therefore, $(\atr_1,\atr_0) \in \sto$ since $\sto \subset \arbo$. Combining $(\atr_1,\atr) \in \rfo$ and $(\atr_1,\atr_0) \in \sto$ we obtain $(\atr,\atr_0) \in \cfo$ and since
$(\atr_0,\atr) \in \viso$ then we obtain that $(\atr,\atr) \in \viso;\cfo$ which contradicts the fact that $\viso;\cfo$ is acyclic.
Therefore, the read value was written by $\atr_0$ and $\atrace$ satisfies $\axretval$.
%%(2): The only-if direction: similar to (1) since $\ccc{} \subset \pcc$, we have that $\arbo_{0}^{+}$ is acyclic. We assume by contradiction that $\arbo_{0}^{+}?;\viso_{0};\cfo$ is cyclic. The property $\axprefix$ implies that $\sto;\viso \subset \viso$ since $\sto \subset \arbo$ and since $\viso_{0}^{+} \subset \viso$ then  $\arbo_{0}^{+}?;\viso_{0} \subset \viso$.  Thus, $\viso;\cfo$ is cyclic which results in a contradiction as in (1).
%%(2): The if direction: we define the relations $\viso$ and $\arbo$ such that $\arbo_{0}^{+}\subset \arbo$ and  $\viso = \arbo ; \viso_{0} \cup \viso_{0}$ which imply that $\viso_{0}^{+} \subset \viso$ and $\arbo;\viso \subset \viso$.  Thus, $\atrace$ satisfies the properties $\axpoco$, $\axcoarb$, and $\axprefix$. Using the same proof steps as in (1) we can show that $\atrace$ satisfies $\axretval$.
%%(3): The only-if direction: similar to above we have that $\arbo_{0}^{+}$ is acyclic.  We assume by contradiction that $\arbo_{0}^{+};\cfo$ is cyclic. Combining the properties $\axconflict$ and $\axpoco$ implies that $\arbo_{0}^{+} \subset \viso$. Thus, $\viso;\cfo$ is cyclic which results in a contradiction as in (1).
%%(3): The if direction: we can define the relations $\viso$ and $\arbo$ such that $\viso = \arbo_{0}^{+}$ and $\arbo_{0}^{+}\subset \arbo$ which imply the properties $\axpoco$, $\axcoarb$, and $\axconflict$. Using the same proof steps as in (1) we can show that $\atrace$ satisfies $\axretval$.
\end{proof}

\begin{proof}[Proof of Lemma~\ref{lem:CcCc}]
The only-if direction follows from Lemma \ref{lem:Transform}. For the if direction: consider a trace $\atrace_\pcinstr$ which is \ccc{}. We prove by contradiction that $\atrace$ must be \ccc{} as well.
Assume that $\atrace$ is not \ccc{} then it must contain a cycle in either $\arbo_{0}^{+}$ or $\viso_{0}^{+};\cfo$ (based on Lemma \ref{lem:cycles}). In the rest of the proof when we mention a cycle we implicitly refer to a cycle in either $\arbo_{0}^{+}$ or $\viso_{0}^{+};\cfo$.

Splitting every transaction $\atr \in \atrace$ in a trace to a pair of transactions $\atrrd{\atr}$ and $\atrwr{\atr}$ that occur in this order might not maintain a cycle of $\atrace$. However, we prove that this is not possible and our splitting conserves the cycle.
Assume we have a vertex $\atr$ as part of the cycle. We show that $\atr$ can be split into two transactions
$\atrrd{\atr}$ and $\atrwr{\atr}$ while maintaining the cycle.
Note that $\atr$ is part of a cycle iff either
\begin{enumerate}
\item  $(\atr_{1},\atr) \in \arbo_{0}$ and $(\atr,\atr_{2})\in \arbo_{0}$ or
\item  $(\atr_{1},\atr) \in \viso_{0}$ and $(\atr,\atr_{2})\in \viso_{0}$ or
\item  $(\atr_{1},\atr) \in \viso_{0}$ and $(\atr,\atr_{2})\in \cfo$ or
\item $(\atr_{1},\atr) \in \cfo$ and $(\atr,\atr_{2})\in \viso_{0}$
\end{enumerate}
where $\atr_{1}$ and $\atr_{2}$ might refer to the same transaction.
Thus, by splitting $\atr$ to $\atrrd{\atr}$ and $\atrwr{\atr}$, the above four cases imply that:
\begin{enumerate}
\item if $(\atr_{1},\atr) \in \viso_{0}$ and $(\atr,\atr_{2})\in \arbo_{0}$ then
$(\atr_{1}',\atrrd{\atr}) \in (\po_\pcinstr \cup \rfo_\pcinstr)$ and $(\atrwr{\atr},\atr_{2}')\in (\po_\pcinstr \cup \rfo_\pcinstr \cup \sto_\pcinstr)$ where $\atr_{1}' \in \{\atrrd{\atr_{1}},\atrwr{\atr_{1}}\}$ and $\atr_{2}' \in \{\atrrd{\atr_{2}},\atrwr{\atr_{2}}\}$. This maintains the vertices $\atr_{1}'$ and $\atr_{2}'$ connected in the cycle formed by the dependency relations of $\atrace_\pcinstr$ since $(\atrrd{\atr},\atrwr{\atr}) \in \po_\pcinstr$;
\item if $(\atr_{1},\atr) \in \sto$ and $(\atr,\atr_{2})\in \arbo_{0}$ then
$(\atr_{1}',\atrwr{\atr}) \in \sto_\pcinstr$ and $(\atrwr{\atr},\atr_{2}')\in (\po_\pcinstr \cup \rfo_\pcinstr \cup \sto_\pcinstr)$ which maintains the vertices $\atr_{1}'$ and $\atr_{2}'$ connected in the cycle formed by the dependency relations of $\atrace_\pcinstr$;
\item $(\atr_{1},\atr) \in \viso_{0}$ and $(\atr_{2},\atr) \in \cfo$ then $(\atr_{1}',\atrrd{\atr}) \in (\po_\pcinstr \cup \rfo_\pcinstr)$ and $(\atrrd{\atr},\atr_{2}')\in \cfo_\pcinstr$ maintains the vertices $\atr_{1}'$ and $\atr_{2}'$ connected in the cycle formed by the dependency relations of $\atrace_\pcinstr$;
\item $(\atr_{1},\atr) \in \cfo$ and $(\atr_{2},\atr) \in \viso_{0}$ then $(\atr_{1}',\atrwr{\atr}) \in \cfo_\pcinstr$ and $(\atrwr{\atr},\atr_{2}')\in (\po_\pcinstr \cup \rfo_\pcinstr)$ which maintains the vertices $\atr_{1}'$ and $\atr_{2}'$ connected in the cycle formed by the dependency relations of $\atrace_\pcinstr$ as well.
\end{enumerate}
Therefore, doing the splitting creates a cycle in either $(\po_\pcinstr \cup \rfo_\pcinstr \cup \sto_\pcinstr)^{+}$ or $(\po_\pcinstr \cup \rfo_\pcinstr)^{+};\cfo_\pcinstr$ which implies that $\atrace_\pcinstr$ is not \ccc{}, a contradiction.
\end{proof}

\begin{proof}[Proof of Lemma \ref{lem:PcSer}]
($\Leftarrow$) Assume that $\atrace_\pcinstr$ is \serc{}. We will show that $\atrace$ is \pcc{}.
Notice that if $(\atr_{1},\atr_{2}) \in \viso_{0}^{+}$ then $(\atrwr{\atr_{1}},\atrrd{\atr_{2}}) \in \arbo_\pcinstr$
which implies that $(\atr_{1},\atr_{2}) \in \viso$. Similarly, if $(\atr_{1},\atr_{2}) \in \arbo_{0}^{+}$ then $(\atrwr{\atr_{1}},\atrwr{\atr_{2}}) \in \arbo_\pcinstr$ or $(\atrwr{\atr_{1}},\atrrd{\atr_{2}}) \in \arbo_\pcinstr$ which implies that $(\atrwr{\atr_{1}},\atrwr{\atr_{2}}) \in \arbo_\pcinstr$ which in both cases implies that $(\atr_{1},\atr_{2}) \in \arbo$. Thus, $\atrace$ satisfies the properties $\axpoco$ and $\axcoarb$.

Now assume that $(\atr_{1},\atr_{2})\in \arbo$ and $(\atr_{2},\atr_{3})\in \viso$. We show that $(\atr_{1},\atr_{3})\in \viso$.
The assumption implies that $(\atrwr{\atr_{1}},\atrwr{\atr_{2}}) \in \arbo_\pcinstr$ and
$(\atrwr{\atr_{2}},\atrrd{\atr_{3}}) \in \arbo_\pcinstr$, which means that $(\atrwr{\atr_{1}},\atrrd{\atr_{3}}) \in \arbo_\pcinstr$. Therefore, $(\atr_{1},\atr_{3}) \in \viso$ and $\atrace$ satisfies the property $\axconflict$.

Concerning $\axretval$, let $\atr$ be a transaction in $\atrace$ that contains a read event $\readact(\atr,\anaddr,\aval)$.
Let $\atr_0$ be transaction in $\atrace$ such that
$$\atr_0 = Max_{\arbo}(\{\atr' \in \atrace\ |\ (\atr',\atr) \in \viso \wedge \exists\ \writeact(\atr',\anaddr,\cdot)\in\amap(\atr')\}).$$
We show that the read must return a value written by $\atr_0$.
The definitions of $\viso$ and $\arbo$ imply that
$$\atrwr{\atr_1}\in\{\atrwr{\atr'} \in \atrace_\pcinstr\ |\ (\atrwr{\atr'},\atrrd{\atr}) \in \arbo_\pcinstr \wedge \exists\ \writeact(\atrwr{\atr'},\anaddr,\cdot)\in\amap(\atrwr{\atr'})\}$$
$$\atr_1 \in \{\atr' \in \atrace\ |\ (\atr',\atr) \in \viso \wedge \exists\ \writeact(\atr',\anaddr,\cdot)\in\amap(\atr')\}$$
because $(\atrwr{\atr_{1}},\atrrd{\atr_{2}}) \in \arbo_\pcinstr$ implies $(\atr_{1},\atr_{2}) \in \viso$.
Then, we obtain that
$$\atrwr{\atr_0} = Max_{\arbo_\pcinstr}(\{\atrwr{\atr'} \in \atrace_\pcinstr\ |\ (\atrwr{\atr'},\atrrd{\atr}) \in \arbo_\pcinstr \wedge \exists\ \writeact(\atrwr{\atr'},\anaddr,\cdot)\in\amap(\atrwr{\atr'})\})$$
and since $\atrace_\pcinstr$ is \serc{} we know that the read must return the value written by $\atrwr{\atr_0}$. Thus, the read returns the value written by $\atr_0$, which implies that $\atrace$ satisfies $\axretval$ holds. Therefore, $\atrace$ is \pcc{}.

($\Rightarrow$) Assume that $\atrace$ is \pcc{}. We show that $\atrace_\pcinstr$ is \serc{}.
Since $\atrace_\pcinstr$ is the result of splitting transactions, a cycle in its dependency relations can only originate from a cycle in $\atrace$. Therefore, it is sufficient to show that any happens-before cycle in $\atrace$ is broken in $\atrace_\pcinstr$.
From Lemma \ref{lem:pccycles}, we have that $\atrace$ either does not admit a happens-before cycle or any (simple) happens-before cycle in $\atrace$ must have either two successive $\cfo$ dependencies or a $\sto$ dependency followed by a $\cfo$ dependency.
If $\atrace$ does not admit a happens-before cycle then it is \serc{}, and $\atrace_\pcinstr$  is trivially \serc{} (since splitting transactions cannot introduce new cycles).

\scalebox{0.67}
\begin{tikzpicture}
\node[shape=rectangle ,draw=none,font=\large] (A0) at (0,0)  [] {$\atr_1$ };
\node[shape=rectangle ,draw=none,font=\large] (A1) at (2,0)  [] {$\atr_2$};
\node[shape=rectangle ,draw=none,font=\large] (B1) at (4,0)  [] {$\atr_3$};
\node[shape=rectangle ,draw=none,font=\large] (B2) at (5,0)  [] {$\Longrightarrow$};
%\node[shape=rectangle ,draw=none,font=\large] (C0) at (8,0)  [] {$\cdots$ };
\node[shape=rectangle ,draw=none,font=\large] (C1) at (6,0)  [] {$\atrrd{\atr_{1}}$};
\node[shape=rectangle ,draw=none,font=\large] (D1) at (8,0)  [] {$\atrwr{\atr_{1}}$};
\node[shape=rectangle ,draw=none,font=\large] (D2) at (10,0)  [] {$\atrrd{\atr_{2}}$};
\node[shape=rectangle ,draw=none,font=\large] (D0) at (12,0)  [] {$\atrwr{\atr_{2}}$};
\node[shape=rectangle ,draw=none,font=\large] (E0) at (14,0)  [] {$\atrrd{\atr_{3}}$ };
\node[shape=rectangle ,draw=none,font=\large] (E1) at (16,0)  [] {$\atrwr{\atr_{3}}$};

\begin{scope}[ every edge/.style={draw=black,very thick}]
\path [->] (A0) edge[] node [above,font=\small] {$\sto \cup \cfo$}  (A1);
\path [->] (A1) edge[] node [above,font=\small] {$\cfo$}  (B1);
\path [->] (B1) edge[bend left] node [above,font=\small] {$\hbo$}  (A0);

\path [->] (C1) edge[] node [above,font=\small] {$\po_\pcinstr$}  (D1);
\path [->] (D1) edge[bend left] node [below,font=\small] {$\sto_\pcinstr$}  (D0);
\path [->] (C1) edge[bend right] node [above,font=\small] {$\cfo_\pcinstr$}  (D0);
\path [->] (D2) edge[] node [above,font=\small] {$\po_\pcinstr$}  (D0);

\path [->] (D2) edge[bend right] node [above,font=\small] {$\cfo_\pcinstr$}  (E1);
\path [->] (E0) edge[] node [above,font=\small] {$\po_\pcinstr$}  (E1);
\end{scope}
\end{tikzpicture}}

Otherwise, if $\atrace$ admits a happens-before cycle like above, then $\atrace$ must contain three transactions $\atr_{1}$, $\atr_{2}$, and $\atr_{3}$ such that $(\atr_{1},\atr_{2}) \in \sto \cup \cfo$, $(\atr_{2},\atr_{3}) \in \cfo$, and $(\atr_{3},\atr_{1}) \in \hbo$ (like in the picture above).
Then, by splitting transactions we obtain that $(\atrwr{\atr_{1}},\atrwr{\atr_{2}}) \in \sto_\pcinstr$ or $(\atrrd{\atr_{1}},\atrwr{\atr_{2}}) \in \cfo_\pcinstr$, and $(\atrrd{\atr_{2}},\atrwr{\atr_{3}}) \in \cfo_\pcinstr$.
Since, we have $(\atrrd{\atr_{2}},\atrwr{\atr_{2}}) \in \po_\pcinstr$ (and not $(\atrwr{\atr_{2}},\atrrd{\atr_{2}}) \in \po_\pcinstr$), this cannot lead to a cycle in $\atrace_\pcinstr$, which concludes the proof that $\atrace_\pcinstr$ is \serc{}
%Thus, in all cases $\atrace_\pcinstr$ doesn't contain cycles. Therefore, $\atrace_\pcinstr$ is \serc{}.
\end{proof}

%!TEX root = draft.tex
\section{Proofs for Section~\ref{sec:robustness}}
\label{sec:robustnessProofs}

\begin{proof}[Proof of Lemma~\ref{lem:pcsicycles}]
%Since $\atrace$ is \pcc{}, there exists a causal order $\viso$ and an arbitration order $\arbo$, such that $\viso\subseteq \arbo$ and $\axpc$ hold.
Let $\arbo_{1}$ be a total order that includes $\arbo_{0}^{+}$ and $\arbo_{0}^{+};\cfo;\arbo_{0}^{*}$ ($\arbo_{0}^*$ is the reflexive closure of $\arbo_{0}$). This is well defined because there exists no cycle between tuples in these two relations. Indeed, if $(\atr_{1},\atr_{2}) \in \arbo_{0}^{+}$ and there exist $\atr_{3}$ and $\atr_{4}$ such that $(\atr_{2}, \atr_{3}) \in \arbo_{0}^{+}$, $(\atr_{3},  \atr_{4}) \in \cfo$, and $(\atr_{4}, \atr_{1}) \in \arbo_{0}^{*}$, then we have a cycle in  $\arbo_{0}^{+};\cfo$ that does not contain two successive $\cfo$ dependencies, which contradicts the hypothesis. Also, for every pair of transactions $(\atr_{1},\atr_{2})$ there cannot exist $\atr_{3}$ and $\atr_{4}$ such that
$$(\atr_{2}, \atr_{3}) \in \arbo_{0}^{+},\ (\atr_{3},  \atr_{4}) \in \cfo\mbox{ and }(\atr_{4}, \atr_{1}) \in \arbo_{0}^{*}$$ and
$\atr_{3}'$ and $\atr_{4}'$ such that $$(\atr_{1}, \atr_{3}') \in \arbo_{0}^{+},\ (\atr_{3}',  \atr_{4}') \in \cfo\mbox{ and }(\atr_{4}', \atr_{2}) \in \arbo_{0}^{*}$$
This will imply a cycle in $\arbo_{0}^{+};\cfo;\arbo_{0}^{+};\cfo$ which again contradicts the hypothesis.
%if $(\atr_{1},\atr_{2}) \not\in \arbo_{0}^{+}$ and there exist $\atr_{3}$ and $\atr_{4}$ such that $(\atr_{2}, \atr_{3}) \in \arbo_{0}^{+}$, $(\atr_{3},  \atr_{4}) \in \cfo$, and $(\atr_{4}, \atr_{1}) \in \arbo_{0}^{*}$ ($\arbo_{0}^*$ denotes the reflexive closure of $\arbo_{0}$), then $(\atr_{2},\atr_{1}) \in \arbo_{1}$.
% and $\arbo_{1}$ is transitive\footnote{Note that .}.
Also, let $\viso_{1}$ be the smallest transitive relation that includes $\arbo_{0}^{+}$ and $\arbo_{1};\arbo_{0}^{+}$. We show that $\viso_{1}$ and $\arbo_{1}$ are causal and arbitration orders of $\atrace$ that satisfy all the axioms of \sic{}.

$\axpoco$ and $\axcoarb$ hold trivially. Since $\sto \subseteq \viso_{1}$, $\axconflict$ holds as well.
%We show first that $\arbo_{1}$ is a well defined total order. Note that because $\axcoarb$, $\arbo_{0}^{+} \subset \arbo$ is acyclic.
% the fact that all happens-before cycles in $\atrace$ contain two successive $\cfo$. Thus,  $\arbo_{1}$ is a well defined total order.
%Also, since $\arbo_{0}^+ \subset \arbo_{1}$ then $\axcoarb$ holds.
%Similar to above $\viso_{1}$ is a well defined partial order.
%Note that $\viso_{1} \subset \arbo_{1}$ as well. Also,  since $\viso_{0}^+ \subset \viso_{1}$ then $\axpoco$ holds.
$\axpc$ holds because $\arbo_{1} ; \viso_{1} = \arbo_{1};(\arbo_{0}^{+} \cup \arbo_{1};\arbo_{0}^{+})^+ = \arbo_{1};\arbo_{0}^{+} \subset \viso_{1}$.

The axiom $\axretval$ is equivalent to the acyclicity of $\viso_{1};\cfo$ when $\axpoco$ and $\axcoarb$ hold. Assume by contradiction that $\viso_1;\cfo$ is cyclic.
From the definition of $\viso_1$ and the fact that $\arbo_{1}$ is total order we obtain that either: %$\arbo_{0}^{+};\cfo$ or $\arbo_{1};\arbo_{0}^{+};\cfo$ (since ) is cyclic:
\begin{itemize}
\item $\arbo_{0}^{+};\cfo$ is cyclic, which implies that there exists a happens-before cycle that does not contain two successive $\cfo$, which contradicts the hypothesis, or
\item $\arbo_{1};\arbo_{0}^{+};\cfo$ is cyclic, which implies that there exist $\atr_{1}$, $\atr_{2}$, and $\atr_{3}$ such that $(\atr_{2}, \atr_{3}) \in \arbo_{0}^{+}$, $(\atr_{3},  \atr_{1}) \in \cfo$ and $(\atr_{1},\atr_{2}) \in \arbo_{1}$.  This contradicts the fact that $(\atr_{2}, \atr_{3}) \in \arbo_{0}^{+}$ and $(\atr_{3},  \atr_{1}) \in \cfo$ implies $(\atr_{2},\atr_{1}) \in \arbo_{1}$.
%by definition if $(\atr_{1},\atr_{2}) \not\in \arbo_{0}^{+}$, otherwise, we get $\arbo_{0}^{+};\arbo_{0}^{+};\cfo = \arbo_{0}^{+};\cfo$ is cyclic which leads to the previous case.
\end{itemize}
Therefore, $\atrace$ satisfies $\axretval$ for $\viso_1$ and $\arbo_1$, which concludes the proof.
\end{proof}

\medskip
Next, we present an important lemma that characterizes happens before cycles possible under the \pcc{} semantics.
This is a strengthening of a result in~[12] which shows that all happens before cycles under \pcc{} must have two successive dependencies in ${,}$ and at least one $$. We show that the two successive dependencies cannot be $$ followed $$, or two successive $$.

\begin{proof}[Proof of Lemma~\ref{lem:pccycles}]
It was shown in [12] that all happens-before cycles under \pcc{} must contain two successive dependencies in $\{\cfo,\sto\}$ and at least one $\cfo$.
Assume by contradiction that there exists a cycle with $\cfo$ dependency followed by $\sto$ dependency or two successive $\sto$ dependencies. This cycle must contain at least one additional dependency. Otherwise, the cycle would also have a $\sto$ dependency followed by a $\cfo$ dependency, or it would imply a cycle in $\sto$, which is not possible (since $\sto \subset \arbo$ and $\arbo$ is a total order).
%    it does this implies a cycle in $\sto \subset \arbo$ which is a contradiction.
Then, we get that the dependency just before $\cfo$ is either $\po$ or $\rfo$ (i.e., $\viso_0$) since we cannot have $\cfo$ or $\sto$ followed by $\cfo$. Also, the relation after $\sto$ is either $\po$ or $\rfo$ or $\sto$ (i.e., $\arbo_0$) since we cannot have $\sto$ followed by $\cfo$. Thus, the cycle has the following shape:

\medskip
\scalebox{0.65}
\begin{tikzpicture}
\node[shape=rectangle ,draw=none,font=\large] (A0) at (0,0)  [] {$\atr_1$ };
\node[shape=rectangle ,draw=none,font=\large] (A1) at (1.3,0)  [] {$\atr_2$};
\node[shape=rectangle ,draw=none,font=\large] (B1) at (2.6,0)  [] {$\atr_3$};
\node[shape=rectangle ,draw=none,font=\large] (B2) at (3.9,0)  [] {$\atr_4$};
\node[shape=rectangle ,draw=none,font=\large] (C0) at (4.5,0)  [] {$\cdots$ };
\node[shape=rectangle ,draw=none,font=\large] (C1) at (5.1,0)  [] {$\atr_i$};
\node[shape=rectangle ,draw=none,font=\large] (D1) at (6.4,0)  [] {$\atr_{i+1}$};
\node[shape=rectangle ,draw=none,font=\large] (D2) at (7.9,0)  [] {$\atr_{i+2}$};
\node[shape=rectangle ,draw=none,font=\large] (D0) at (9.4,0)  [] {$\atr_{i+3}$};
\node[shape=rectangle ,draw=none,font=\large] (E0) at (10.2,0)  [] {$\cdots$ };
\node[shape=rectangle ,draw=none,font=\large] (E1) at (11,0)  [] {$\atr_{n-4}$};
\node[shape=rectangle ,draw=none,font=\large] (F1) at (12.5,0)  [] {$\atr_{n-3}$};
\node[shape=rectangle ,draw=none,font=\large] (F2) at (14,0)  [] {$\atr_{n-2}$};
\node[shape=rectangle ,draw=none,font=\large] (F3) at (15.5,0)  [] {$\atr_{n-1}$};
\node[shape=rectangle ,draw=none,font=\large] (F4) at (17,0)  [] {$\atr_{n}$};

\begin{scope}[ every edge/.style={draw=black,very thick}]
\path [->] (A0) edge[] node [above,font=\small] {$\cfo$}  (A1);
\path [->] (A1) edge[] node [above,font=\small] {$\sto$}  (B1);
\path [->] (B1) edge[] node [above,font=\small] {$\arbo_0$}  (B2);

\path [->] (C1) edge[] node [above,font=\small] {$\viso_0$}  (D1);
\path [->] (D1) edge[] node [above,font=\small] {$\cfo$}  (D2);
\path [->] (D2) edge[] node [above,font=\small] {$\sto$}  (D0);

\path [->] (E1) edge[] node [above,font=\small] {$\viso_0$}  (F1);
\path [->] (F1) edge[] node [above,font=\small] {$\cfo$}  (F2);
\path [->] (F2) edge[] node [above,font=\small] {$\sto$}  (F3);
\path [->] (F3) edge[] node [above,font=\small] {$\arbo_0$} (F4);
\path [->] (F4) edge[bend left=11] node [above,font=\small] {$\viso_0$} (A0);
\end{scope}
\end{tikzpicture}}

\medskip
Since $\viso_0;\cfo\subseteq \arbo$ is a consequence of the \pcc{} axioms~[26], we get that $(\atr_{n}, \atr_2) \in \arbo$, $(\atr_{i}, \atr_{i+2}) \in \arbo$ and $(\atr_{n-4}, \atr_{n-2}) \in \arbo$, which allows to ``short-circuit'' the cycle.
Using the fact that $\sto \subset \arbo$, $\viso_0 \subset \arbo$, and $\arbo_0 \subset \arbo$, and applying the short-circuiting process multiple times, we obtain a cycle in the arbitration order $\arbo$ which contradicts the fact that $\arbo$ is a total order.
\end{proof}

\begin{proof}[Proof of Theorem~\ref{them:RobCcSi}]
For the only-if direction: assume that $\aprog$ is robust against \ccc{} relative to \sic{}. Then,
the set of traces of $\aprog$ under the two consistency models coincide.
Since the set of traces under \sic{} is subset of the one under \pcc{}, then
the set of traces under \ccc{} is subset of the one under \pcc{}.
This implies that $\aprog$ is robust against \ccc{} relative to \pcc{}. % because the set of traces under \pcc{} is a subset of the set of executions under \ccc{}.
Thus, we obtain that the set of traces of $\aprog$ under the three consistency models coincide.
Therefore, $\aprog$ is robust against \pcc{} relative to \sic{} as well.

For the if direction: assume that $\aprog$ is robust against \ccc{} relative to \pcc{} and $\aprog$ is robust against \pcc{} relative to \sic{}. Then, the set of traces of $\aprog$ under the three consistency models coincide. Thus, we obtain that $\aprog$ is robust against \ccc{} relative to \sic{}.
\end{proof}

%!TEX root = draft.tex
\section{Proofs for Section~\ref{sec:commutativitygraph}}
\label{sec:commutativitygraphProofs}

\begin{proof}[Proof of Theorem~\ref{them:MovRobCcPc}]
It is enough to show: if $\aprog$ is not robust against \ccc{} relative to \pcc{} then we have a simple cycle in the commutativity dependency graph of $\aprog_\pcinstr$ of the form above.  Assume $\aprog$ is not robust against \ccc{} relative to \pcc{}.
Then, from Theorem \ref{them:RobCcPc}, we obtain $\aprog_\pcinstr$ is not robust against \ccc{} relative to \serc{}.
Also it was shown in [10] that if a program is not robust then there must exist a robustness violation trace (\ccc{} relative to \serc{}) $\atrace_\pcinstr$ of the shape $\atrace_\pcinstr = \alpha \cdot \atr_1 \cdot \beta \cdot \atr_i \cdot  \atr_{i+1} \cdot \gamma \cdot \atr_n$ where $(\atr_1,\atr_i) \in (\po \cup \rfo)^{+}$, $(\atr_{i},\atr_{i+1}) \in (\sto \cup \cfo)$, $(\atr_{i+1},\atr_n) \in \hbo$, and  $(\atr_n,\atr_1) \in \cfo$. Note that since transactions in the trace $\atrace_\pcinstr$ can either be read-only or write-only. Then, $(\atr_{i},\atr_{i+1}) \in (\sto \cup \cfo)$ and $(\atr_{n},\atr_1) \in \cfo$ imply that $\atr_1$ and $\atr_{i+1}$ must be a write-only transactions and $\atr_{n}$ must be a read-only transaction.
Note that we may have $\beta = \gamma = \epsilon$ as the case for the trace of the $\mathsf{SB}$ program given in Figure \ref{fig:litmus1}.

%In the trace $\atrace_\pcinstr$, we let $\atr_1$ to be $\atr_1$, $\atr_i$ to be $\atr_2$, $\atr_3$ to be $\atr_{i+1}$, and $\atr_4$ to be $\atr_n$ of Theorem \ref{them:MovRobCcPc}.
We consider first the general case when $\atr_1 \not\equiv \atr_2$. The other case can be proved in the same way.

Consider the prefix $\atrace_{p}$ of $\atrace_\pcinstr$: $\atrace_{p} = \alpha \cdot \atr_1 \cdot \beta \cdot \atr_{i}$ where $(\atr_1,\atr_{i}) \in (\po \cup \rfo)^{+}$ which is a \serc{} trace of $\aprog_{\pcinstr}$.
Then, we have a sequence of transactions from $\atr_1$ to $\atr_{i}$ that are related by either $\po$ or $\rfo$.
In the case two transactions are only related by $\rfo$, then the first transaction is not a right mover because of the second transaction reads from a write in the first transaction. Thus, we can relate the two transactions using the relation $\mrfo$ in the commutativity dependency graph.

Similarly consider the following trace $\atrace_{s}$ extracted from $\atrace_\pcinstr$: $\atrace _{s} = \alpha \cdot  \atr_{i+1} \cdot \gamma \cdot \atr_n$ where $(\atr_{i+1},\atr_n) \in \hbo$ which is a \serc{} trace of $\aprog_{\pcinstr}$.
Similar to before, we have a sequence of transactions from $\atr_{i+1}$ to $\atr_n$ that are related by either $\po$, $\rfo$, $\sto$, or $\cfo$.
For any two transactions that are related only by either $\rfo$, $\sto$, or $\cfo$, this implies that the first transaction is not a right mover because of the second transaction and a write-read, write-write, or read-write dependency between the two, respectively. Thus, we can relate the two transactions using either $\mrfo$, $\msto$, or $\mcfo$, respectively.

Now consider the following trace $\atrace_{1}$ extracted from $\atrace_\pcinstr$: $\atrace_{1} = \alpha \cdot \atr_1 \cdot \beta \cdot \atr_{i} \cdot \atr_{i+1}$ where $(\atr_{i},\atr_{i+1}) \in  (\sto \cup \cfo)$  is a \serc{} trace of $\aprog_{\pcinstr}$.
Because $\atr_{i}$ and $\atr_{i+1}$ are related by either $\sto$ or $\cfo$, then $\atr_{i}$ is not a right mover because of $\atr_{i+1}$ and a write-write or read-write dependency between the two, respectively.
Thus, we can relate the two transactions using either $\msto$ or $\mcfo$, respectively.

Finally, consider the following trace $\atrace_{2}$ extracted from $\atrace_\pcinstr$: $\atrace_{2} = \alpha \cdot  \atr_{i+1} \cdot \gamma \cdot \atr_n \cdot \atr_1$  where $(\atr_n,\atr_1) \in \cfo$  is a \serc{} trace of $\aprog_{\pcinstr}$.
Because $\atr_{n}$ and $\atr_{1}$ are related by $\cfo$, then $\atr_{n}$ is not a right mover because of $\atr_{1}$ and a read-write dependency between the two. Thus, we can relate the two transactions using $\mcfo$.
\end{proof}

\begin{proof}[Proof of Theorem~\ref{them:MovRobPcSi}]
Similar to before it is enough to show: if $\aprog$ is not robust against \pcc{} relative to \sic{} then we have a simple cycle in the commutativity dependency graph of $\aprog_\pcinstr$ of the form above. Assume $\aprog$ is not robust against \pcc{} relative to \sic{}.
Then, from Theorem \ref{them:RobPcSiInstr}, we obtain that if $\sem{\aprog}$ reaches an error state under \serc{} then we will have the following trace $\atrace$ under \serc: $\atrace = \alpha \cdot \atrrd{\atr_{\instr}}  \cdot \atr_3 \cdot  \beta \cdot \atr_n \cdot \atrwr{\atr_{\instr}}$\footnote{For simplicity, we assume here that after reaching the error state we execute the writes of $\atr_{\instr}$, i.e., $\atrwr{\atr_{\instr}}$.} where $(\atrrd{\atr_{\instr}},\atr_3) \in \cfo$, $(\atr_3,\atr_n) \in \hbo$, $(\atr_n,\atrwr{\atr_{\instr}}) \in \sto$, and we don't have two successive $\cfo$ in the happens before between $\atr_3$ and $\atr_n$. In $\atrace$, $\atrwr{\atr_{\instr}}$ (resp., $\atrrd{\atr_{\instr}}$) represents $\atr_1$ (resp., $\atr_2$) in the theorem statement.
Note that we may have $\alpha = \beta = \epsilon$ as is the case of the transformed $\mathsf{LU}$ program given in Figure \ref{fig:litmus2Instr}.
The construction of the cycle in the commutativity dependency graph follows the same procedure taken in the proof of Theorem \ref{them:MovRobCcPc}. The only difference is that for every two transactions of $\atrace$ that are part of the happens before between $\atr_3$ and $\atr_n$, if the two are not connected by either $\po$, $\rfo$, $\sto$, or $\cfo$ then they must be the reads and writes of the same original transaction in $\aprog$. In this case, in the commutativity dependency graph we have the two transactions related by $\sametro$.
%Notice that we abused notation by using the two components $\atrrd{\atr 1}$ and $\atrwr{\atr_1}$ of $\atr_1$ in $\atrace$ to denote that $\atr 1$ writes were not immediately written to the shared variables.
\end{proof}

\end{document}