Понимание At-Most-Once-Property в параллельной программе

Question

Я пытаюсь понять свойство по крайней мере один раз, которое гласит:

Атрибут оператора присваивания x = e, в котором либо (1) x не читается другим процессом, а e содержит в большая часть одной ссылки на переменную, измененную другим процессом, или (2) x не записана другим процессом и e не содержит ссылок на переменные, измененные другими процессами.

int x = 0, y = 0;
co x = x+1; // y= y=1; oc; 

удовлетворяет свойству, поскольку x не является прочитанный вторым процессом и не имеющий критической секции

int x = 1, y = 1;
co <x = x + y;> 
// y = 0;
// x = x - y;
oc

Я не понимаю, как эта программа удовлетворяет этому свойству. Первое утверждение является оператором atomi c, поэтому оно в любом случае недопустимо, но y = 0 повлияет на результат третьего утверждения x, поэтому я не понимаю, как это удовлетворяет свойству?

Answer 1

Мне было интересно, что это могло бы означать ... и это был особенно влажный полдень, я пошел и посмотрел, и обнаружил:

Свойство At-Most-Once

Эндрюс определили условие, называемое не более одного раза , при котором оценки и присваивания выражений будут выглядеть как атомы c.

Критическая ссылка в выражении - это ссылка на переменную, которая изменяется другим потоком.

1. Оператор присваивания x = e удовлетворяет самое большее один раз свойство, если либо:

   1.1: e содержит не более одной критической ссылки, а x не читается и не записывается другим потоком, или

   1.2: e не содержит критических ссылок , в этом случае x может быть прочитано или записано другими потоками.

2. Выражение, которое отсутствует в присваивании, удовлетворяет свойству не более одного раза, если оно содержит не более одного критическая ссылка.

Это условие вызывается не более одного раза, потому что может быть не более одной общей переменной, а на общую переменную можно ссылаться не более одного раза. ...

Я думаю, что ключом к вашей загадке является следующее предложение:

... Операторы присваивания, которые удовлетворяют свойству по крайней мере один раз, кажутся выполненными атомарно даже хотя они не атомы c.

и

... То есть мы получили бы те же результаты от выполнения этих операторов присваивания, даже если бы мы каким-то образом предотвратили чередование их машинных инструкций так, что операторы присваивания были вынуждены выполнять атомарно.

Предполагая, что я правильно понял:

• <x = x + y;> это атоми c чтение-изменение -записывать. Так что это уже атомы c - ему не нужно «казаться, что он выполняется атомарно».

• y = 0 равно самое большее один раз таким образом, удовлетворяет (1.2) выше и будет «казаться выполненным атомарно». И потому что это ...

• ... это означает, что x = x - y также не более одного раза

... я думаю. (Пожалуйста, дайте нам знать, когда найдете точный ответ.)

Мне интересно, для чего это нужно!