We thank the reviewers for their detailed and insightful reviews. We first answer the individual questions of the reviewers, and then propose a changelist based on their suggestions. Response Reviewer A Sources for incompleteness The reviewer is correct in that $\phi_{src}$ and $\phi_{dst}$ would flag certain programs as non-robust even though they may actually be robust, since they do not consider the scenario where a non-maximal write $\mu_w$ may be in the $rf$ relation to a CAS event, and hence cannot cause a robustness violation if the next event (say $\mu$) to be added is a write event to the same location as $\mu_w$, and the maximal write is in $hb_{SC}$ order to the session containing $\mu$. Below, we have shown a simple litmus test to realize this behavior. For every other scenario, $\phi_{src}$ and $\phi_{dst}$ models the absence of a non-robustness witness faithfully. These conditions would be violated if the maximal write to a location is in non-$hb$ $hb_{SC}$ order to a session just before another access to the same location. In every other scenario except the one described above, if $\phi_{src}$ and $\phi_{dst}$ is violated, it would imply the presence of a non-robustness witness. We have observed that in library implementations, either all writes to a location happen through CAS operations, or none do (i.e. it doesn't happen that there is both a CAS and a normal write operation to the same location). Notice that a CAS access to a location is required to manifest the above scenario. If all accesses to a location are through CASes, we use the CAS constraints as explained in Sec. 7 (L:983) to encode additional properties, which helps us avoid any false positives arising out of the imprecision of $\phi_{src}$ and $\phi_{dst}$.

We thank the reviewers for their detailed and thoughtful comments. Overview Our response primarily focuses on (i) the technical questions posed by Reviewer-A; (ii) the relationship of our work with DRF-SC proofs as questioned by Reviewer-B; and (iii) Reviewer-C's questions on how our technique compares to model-checking approaches for weak memory. Proposed Changes In addition to addressing all the technical clarifications and minor typos raised in the reviews, our revision will provide a more detailed in-depth comparison with both DRF-based verification techniques as well as model-checking approaches developed for weak memory systems. We will also move salient material from the appendix to the main body of the paper as suggested by Reviewer-A. Response Review-A