Как проверить, что возможное исполнение является ООТА? ⇐ C++

[Anonymous]

Рассмотрим этот пример:

Код: Выделить всё

#include 
#include 
int main(){
std::atomic x = 0, y = 0;
auto t1 = std::thread([&](){
if(x.load(std::memory_order::relaxed)==42){ // #1
y.store(42,std::memory_order::relaxed); // #2
}
});
auto t2 = std::thread([&](){
while(y.load(std::memory_order::relaxed)==0); // #3
x.store(42,std::memory_order::relaxed);  // #4
});
t1.join();
t2.join();
}

Это типичный случай OOTA, который является вариантом примера в [atomics.order] p9. Потому что вычисление #1 циклически зависит от самого себя.

Реализации должны гарантировать, что не вычисляются никакие «из воздуха» значения, которые циклически зависят от их собственных вычислений.

Однако, если изменить t1 на следующее:

Код: Выделить всё

  auto t1 = std::thread([&](){
if(x.load(std::memory_order::relaxed)==42){ // #1
y.store(42,std::memory_order::relaxed); // #2
}else{
y.store(42,std::memory_order::relaxed);
}
});

Или функционально эквивалентная форма, описанная выше.

Код: Выделить всё

  auto t1 = std::thread([&](){
x.load(std::memory_order::relaxed) // #1
y.store(42,std::memory_order::relaxed); // #2
});

Является ли измененный пример OOTA? Интуитивно я думаю, что последующие измененные примеры не являются ООТА; однако я не могу объяснить почему. Несмотря на то, что формального определения того, что такое OOTA, не существует, существует ли неформальный способ объяснить их разницу и почему первый из них является OOTA, а другой нет?
Я думаю, что мы не можем различить/объяснить их с точки зрения потока управления. #2 зависит от того, возвращается ли поток управления из #1 во всех трех случаях. Другими словами, #2 недоступен, если выполнение #1 не завершено (с точки зрения абстрактного машинного смысла); Например, #2 не был бы выполнен, если бы #1 мог вызвать исключение.
Итак, как их объяснить?

Подробнее здесь: https://stackoverflow.com/questions/798 ... on-is-oota