# FAoC Response

We thank the reviewers for their careful comments. We have addressed all of these as detailed below.

Both reviewers have asked for the Isabelle/HOL formalisation. We had submitted the Isabelle/HOL as supplementary material to our submission, but this may not have been made available to the reviewers - apologies for this. We have now uploaded the Isabelle/HOL code to Figshare (https://doi.org/10.6084/m9.figshare.21507636), see also the new reference [31] of the paper.

## Reviewer: 1
> I think the examples need (much) more explanation.
>
We have added explanations covering the RNG example and the other figures highlighted by the reviewer (details below).

Detailed comments:

Page 2:

> - so the relaxed outcome r1 = r2 = 1 is forbidden. : I fail to see how this outcome would be possible under any circumstance.
>
The issue is that the C++ specification is incorrect. Indeed the outcome is not possible in any architecture, but is allowed by the C++ specification. We have added some additional discussion at lines 68-69.

> - hence may appear take effect -> hence may appear to take effect
>
Fixed

Page 3:

> - However, such models are difficult to mechanise since certain relations, e.g., the “happens-before” relation must be calculated as a transitive reflexive closure of the union of two other relations: that sounds like it can be mechanised perfectly well. Why is this difficult?
>
We have clarified that the mechanisation is not difficult, but reasoning over these is difficult (line 109).

> - within an event structures -> within an event structure
>
Fixed

> - to encode verify -> to encode and verify
>
Fixed

> - Var -> Val
>
Fixed

Page 4:

> SC accesses: please add what SC stands for here
>
Added

> - a subset of the program order of F: what is F?
>
Fixed

Page 9:

> - where and f[k := v] to denote -> where f[k := v] is used to denote
>
Fixed

> - The executes: there is a word missing here (program?)
>
Fixed. We should have said the transition executes

Page 10:

>- corresponding action, a and new thread -> corresponding action a and new thread
>
Fixed

Page 13:

> - Our state ...: this is not a sentence.
>
Fixed (line 594).

Page 16:

> - is an tagged -> is a tagged

Fixed

> - is mapping -> is a mapping

Fixed

> - the formalisation of a state in prior work is a time-stamp based semantics -> the formalisation of a state in prior work is done using a time-stamp based semantics

Fixed

Page 18:

> - so omit -> so we omit

Fixed

> - represents assertion -> represents the assertion

Fixed

> - in Thread 1 and non-trivial dependencies in thread 2: be consistent; either use “Thread” or “thread”

Consistently using Thread throughout.

> - the dependencies are condition -> “the dependencies are a condition”, or “the dependencies depend on”. It is not clear to me which one it should be

Fixed

> - If r1 = r2 = 1, then we have: first, I expect line 8 should be line 5, but second, I fail to see why these pairs of lines are dependent, but not, for instance, lines 3 and 6. Doesn’t the guard after line 4 establish that?
> - If r1 = 1 and r2 = 0: why not 4 and 8? Because you are not dependent on reading y into r2? But if you read y into r2, and after that, r2 no longer has the value 0, does that not make line 8 dependent on line 4 after all?
> - If r1 = 0 and r2 = 1: the same comment, now for lines 3 and 7

Fixed, we have reworded the explanation of this example. We now discuss how an optimised program produced by a compiler could, in this case, have semantic dependencies which differ to the syntactically available ones in its input program.

> - Random number generator: please explain this case in more detail. For instance, I fail to see how any semantics can lead to executing line 6. Please also discuss Figure 13.
>
Fixed, we have added additional comments in lines 875-881 as well as 925-971. The dependencies are easiest to explain using the event structure, and hence our focus has been to use the event structure as a basis for the discussion. Note the the event structure in our submission was an abridged version of the full event structure, which is now presented in Fig 13.

Page 19:

> - and between lines 5 and 7: there is no line 7

Fixed

Page 20:

> - LB+data-add+ctrl: please discuss Figure 16 as well. If there is nothing to discuss compared to Figure 14, then why include this example?

Additional text included 1012-1015.

Page 22:

> - one would need to calculate future sets manually: “would need” or “need”? The former suggests that this manual work would be neede at first glance, but actually, you have automated this (?), while the latter gives as fact that this manual work is needed. If that is the case, btw, why can it not be automated?

Fixed. The point is that future sets need to provided as an input to the verifier (i.e., Isabelle/HOL)

Page 24:

> - as far a possible -> as much as possible

Fixed

## Reviewer: 2

Recommendation: Minor Revision

Comments:
> In Fig. 2, a more "classical" thin-air-read example would have used "r2:=[y]" in line 3. Please double check.
>
Fixed