We define a new sound relation weak-causally-precedes (WCP), which is
weaker than causally-precedes. The definition and its soundness proof,
as claimed in [41], is challenging:
"It is worth emphasizing that multiple researchers have fruitlessly pursued
such a weakening of HB in the past. . . . (Both the definition of CP
and our proof of soundness are results of multi-year collaborative work, with
several intermediate failed attempts.)"
Even though we had the benefit of
following the work on CP, our experience concurs with the above
observation. The subtlety in these ideas is highlighted by the fact
that the soundness proof for CP, presented in [41], is incorrect;
informed readers can find an explanation of the errors in the CP
soundness proof in Appendix B. Our attempts at fixing the CP proof led
us to multiple years of fruitless labor until finally the results
presented here. Our soundness proof for WCP (which also, by
definition, applies to CP) requires significant extensions to the
proof ideas outlined in [41]