Consider this example:

#include 
#include 

int main(){
  std::atomic val = 0;
  std::atomic flag = false;
  std::jthread t1([&](){
     if(val.load(std::memory_order::relaxed) == 1){ // #1
       flag.store(true, std::memory_order::release); // #2
     }
  });
  std::jthread t2([&](){
    while(!flag.load(std::memory_order::acquire)); // #3
    val.store(1,std::memory_order::relaxed); // #4
  });
}

The way I try to prove the behavior of the program is in this way; First, assuming the loop at #3 exit. So, the first logic statement based on this assumed premise is:

1. The loop at #3 exit ⟾ #3 reads from #2

[stmt.while] p1: In the while statement, the substatement is executed repeatedly until the value of the condition ([stmt.pre]) becomes false.

2. #3 reads from #2 ⟾ #2 is executed somewhere in the whole lifetime of the program

[intro.races] p10: The value of an atomic object M, as determined by evaluation B, is the value stored by some unspecified side effect A that modifies M, where B does not happen before A.

3. #2 is executed somewhere in the whole lifetime of the program ⟾ the condition of the if at #1 is true

[stmt.if] p1: If the condition ([stmt.pre]) yields true, the first substatement is executed. If the else part of the selection statement is present and the condition yields false, the second substatement is executed.

4. The condition of the if at #1 is true ⟾ #1 reads from #4

Applying the hypothetical syllogism, we can get the conclusion that:

5. The loop at #3 exit ⟾ #1 reads from #4

In addition, #3 reads from #2 means #2 happens-before #3, which means #1 happens-before #4,which in turn means that #1 doesn't read from #4. So, we can infer that

6. #3 reads from #2 ⟾ ¬(#1 reads from #4)

Again, applying hypothetical syllogism to the first and the sixth inference, which result in that

7. The loop at #3 exit ⟾ ¬(#1 reads from #4)

Associating the 5 and 7 inference, we get a contradiction that

The loop at #3 exit ⟾ ¬(#1 reads from #4) ∧ (#1 reads from #4)

That is

The loop at #3 exit ⟾ False

NOTE: the symbol ⟾ means logical implication

So, the contradiction means the assumed premise is false. The loop at #3 cannot exit in this program.

Is this a correct way to do the formal proof?