Рассуждение о переупорядочении операции IORef в параллельных программах

Ответ 1

Я не знаю Haskell concurrency, но я кое-что знаю о моделях памяти.

Процессоры могут переупорядочивать инструкции так, как им нравится: нагрузки могут идти впереди грузов, нагрузки могут идти впереди магазинов, нагрузки зависимого материала могут опережать грузы, от которых они зависят (a [i] может загрузить значение из сначала массив, затем ссылку на массив a!), магазины могут быть переупорядочены друг с другом. Вы просто не можете наложить на него пальцем и сказать: "эти две вещи определенно появляются в определенном порядке, потому что их невозможно переупорядочить". Но для того, чтобы работали параллельные алгоритмы, им необходимо наблюдать состояние других потоков. Здесь важно, чтобы состояние потока выполнялось в определенном порядке. Это достигается путем установки барьеров между инструкциями, которые гарантируют, что порядок инструкций должен выглядеть одинаково для всех процессоров.

Как правило (одна из простейших моделей), вы хотите два типа упорядоченных инструкций: упорядоченная нагрузка, которая не идет впереди других заказываемых нагрузок или магазинов, а также упорядоченное хранилище, которое не выполняет никаких инструкций вообще, и гарантия того, что все заказываемые инструкции отображаются одинаково для всех процессоров. Таким образом, вы можете рассуждать о проблеме IRIW:

Thread 1: x=1

Thread 2: y=1

Thread 3: r1=x;
          r2=y;

Thread 4: r4=y;
          r3=x;

Если все эти операции являются упорядоченными нагрузками и упорядоченными магазинами, то вы можете сделать вывод (1,0,0,1)=(r1,r2,r3,r4) невозможен. Действительно, упорядоченные магазины в потоках 1 и 2 должны появляться в некотором порядке для всех потоков, а r1 = 1, r2 = 0 является свидетельством того, что y = 1 выполняется после x = 1. В свою очередь это означает, что Thread 4 никогда не может наблюдать r4 = 1 без наблюдения r3 = 1 (который выполняется после r4 = 1) (если упорядоченные магазины выполняются таким образом, наблюдая y == 1, следует x == 1).

Кроме того, если нагрузки и магазины не были упорядочены, процессорам обычно разрешалось наблюдать, что присвоения отображались даже в разных порядках: можно было бы увидеть x = 1 перед y = 1, а другой мог бы видеть y = 1 появляются до x = 1, поэтому допускается любая комбинация значений r1, r2, r3, r4.

Это достаточно реализовано так:

упорядоченная нагрузка:

load x
load-load  -- barriers stopping other loads to go ahead of preceding loads
load-store -- no one is allowed to go ahead of ordered load

упорядоченное хранилище:

load-store
store-store -- ordered store must appear after all stores
            -- preceding it in program order - serialize all stores
            -- (flush write buffers)
store x,v
store-load -- ordered loads must not go ahead of ordered store
           -- preceding them in program order

Из этих двух я вижу, что IORef реализует упорядоченное хранилище (atomicWriteIORef), но я не вижу упорядоченную нагрузку (atomicReadIORef), без которой вы не можете рассуждать о проблеме IRI выше. Это не проблема, если ваша целевая платформа - x86, потому что все загрузки будут выполняться в порядке программы на этой платформе и никогда не будут превышать нагрузки (фактически, все нагрузки - это упорядоченные нагрузки).

Атомное обновление (atomicModifyIORef) представляется мне реализацией так называемого цикла CAS (цикл сравнения и набора, который не останавливается до тех пор, пока значение не будет атомарно установлено на b, если его значение равно а), Вы можете видеть операцию изменения атома как слияние упорядоченной нагрузки и упорядоченного хранилища со всеми этими барьерами и выполняться атомарно - никакому процессору не разрешается вставлять инструкцию модификации между загрузкой и хранением CAS.

Кроме того, writeIORef дешевле, чем atomicWriteIORef, поэтому вы хотите использовать writeIORef столько, сколько позволяет ваш протокол обмена между потоками. Принимая во внимание, что writeIORef x vx >> writeIORef y vy >> atomicWriteIORef z vz >> readIORef t не гарантирует порядок, в котором writeIORefs отображаются другим потокам относительно друг друга, есть гарантия, что они оба появятся перед atomicWriteIORef - поэтому, увидев z == vz, вы можете сделать это в этот момент x == vx и y == vy, и вы можете заключить, что IORef t был загружен после того, как магазины в x, y, z могут наблюдаться другими потоками. Эта последняя точка требует, чтобы readIORef была упорядоченной нагрузкой, которая не указана, насколько я могу судить, но она будет работать как упорядоченная нагрузка на x86.

Как правило, вы не используете конкретные значения x, y, z при рассуждении об алгоритме. Вместо этого некоторые зависящие от алгоритма инварианты относительно назначенных значений должны выполняться и могут быть доказаны - например, как в случае с IRIW, вы можете гарантировать, что Thread 4 никогда не увидит (0,1)=(r3,r4), если Thread 3 видит (1,0)=(r1,r2), а Thread 3 может воспользоваться этим: это означает, что что-то взаимно исключается, не приобретая никаких мьютексов или блокировок.

Пример (не в Haskell), который не будет работать, если нагрузки не упорядочены, или упорядоченные хранилища не очищают буферы записи (требование сделать заметные записи заметными до того, как выполняется упорядоченная загрузка).

Предположим, что z покажет либо x до вычисления y, либо y, если x также был вычислен. Не спрашивайте, почему, не так просто видеть вне контекста - это своего рода очередь - просто наслаждайтесь, какие рассуждения возможны.

Thread 1: x=1;
          if (z==0) compareAndSet(z, 0, y == 0? x: y);

Thread 2: y=2;
          if (x != 0) while ((tmp=z) != y && !compareAndSet(z, tmp, y));

Итак, два потока задают x и y, затем устанавливают z в x или y, в зависимости от того, были ли вычислены y или x. Предполагая, что изначально все равны 0. Переходя в нагрузки и магазины:

Thread 1: store x,1
          load z
          if ==0 then
            load y
            if == 0 then load x -- if loaded y is still 0, load x into tmp
            else load y -- otherwise, load y into tmp
            CAS z, 0, tmp -- CAS whatever was loaded in the previous if-statement
                          -- the CAS may fail, but see explanation

Thread 2: store y,2
          load x
          if !=0 then
          loop: load z -- into tmp
                load y
                if !=tmp then -- compare loaded y to tmp
                  CAS z, tmp, y  -- attempt to CAS z: if it is still tmp, set to y
                  if ! then goto loop -- if CAS did not succeed, go to loop

Если Thread 1 load z не является упорядоченной нагрузкой, тогда будет разрешено идти впереди упорядоченного хранилища (store x). Это означает, где z загружается (регистр, строка кэша, стек,...), значение такое, которое существовало до того, как значение x может быть видимым. Глядя на это значение бесполезно - вы не можете судить о том, к чему относится Thread 2. По той же причине у вас должна быть гарантия того, что буферы записи были сброшены до выполнения load z - в противном случае она по-прежнему будет отображаться как загрузка значения, существовавшего до того, как Thread 2 мог увидеть значение x. Это важно, как будет показано ниже.

Если Thread 2 load x или load z не являются упорядоченными нагрузками, они могут идти впереди store y и будут наблюдать значения, которые были записаны до того, как y будет видимым для других потоков.

Однако посмотрите, что если заказы и магазины упорядочены, то потоки могут согласовать, кто должен установить значение z без конкурирующего z. Например, если Thread 2 соблюдает x == 0, существует гарантия, что Thread 1 определенно выполнит x = 1 позже и увидит z == 0 после этого, так что Thread 2 может выйти, не пытаясь установить z.

Если Thread 1 наблюдает z == 0, то он должен попытаться установить z на x или y. Итак, сначала проверьте, установлен ли y. Если он не был установлен, он будет установлен в будущем, поэтому попробуйте установить x - CAS может выйти из строя, но только если Thread 2 одновременно установил z на y, так что не нужно повторять попытку. Аналогично, нет необходимости повторять попытку, если был задан параметр 1, отмеченный y: если CAS терпит неудачу, то он задается потоком 2 на y. Таким образом, мы можем видеть, что Thread 1 устанавливает z в x или y в соответствии с требованием и не слишком сильно противоречит z.

С другой стороны, Thread 2 может проверить, был ли x уже вычислен. Если нет, то задание на тему 1 задает z. Если Thread 1 вычислил x, тогда нужно установить z в y. Здесь нам нужен цикл CAS, потому что один CAS может выйти из строя, если Thread 1 пытается установить z на x или y одновременно.

Важным выводом здесь является то, что если "несвязанные" нагрузки и хранилища не сериализуются (включая сброс буферов записи), такое рассуждение невозможно. Однако, как только нагрузки и магазины упорядочены, оба потока могут определить путь каждый из них _will_take_in_the_future, и таким образом устранить конфликт в половине случаев. Большую часть времени x и y будут вычисляться в значительно разные времена, поэтому, если y вычисляется до x, вероятно, что Thread 2 не коснется z вообще. (Как правило, "касание z" также может означать "пробудить поток, ожидающий на cond_var z", поэтому это не только вопрос загрузки чего-либо из памяти)

Ответ 2

• в потоке AtomModifyIORef "никогда не наблюдается перед любыми более ранними операциями IORef или после любого последующего IORef операций", то есть мы получаем частичное упорядочение: вещи над атомным mod → atomic mod → после. Хотя формулировка "никогда наблюдаемый" здесь свидетельствует о призрачном поведении, что я не ожидается.

"никогда не наблюдается" является стандартным языком при обсуждении проблем переупорядочения памяти. Например, ЦП может выдавать спекулятивное считывание местоположения памяти раньше, чем необходимо, до тех пор, пока значение не изменяется между тем, когда выполняется чтение (раньше), и когда чтение должно быть выполнено (в порядке выполнения программы). Это полностью зависит от процессора и кэша, хотя он никогда не подвергался программисту (поэтому язык вроде "никогда не наблюдается" ).

• ReadIORef x может быть перемещен перед writeIORef y, по крайней мере, когда не зависят от данных.

True

• Логически я не вижу, как что-то вроде readIORef x → = writeIORef y может быть переупорядочено

Правильно, так как эта последовательность имеет зависимость от данных. Значение, которое нужно записать, зависит от значения, полученного от первого чтения.

По другим вопросам: newIORef False >>= \v-> writeIORef v True >> readIORef v всегда будет возвращать True (нет возможности для доступа других потоков к ссылке здесь).

В примере myprint вы можете сделать это очень мало, чтобы обеспечить надежную работу перед новыми оптимизациями, добавленными в будущие GHC и различные архитектуры процессоров. Если вы пишете:

writeIORef myRef True
x <- readIORef myRef
yourVal <- x `seq` readIORef yourRef

Несмотря на то, что GHC 7.6.3 создает правильный cmm (и, предположительно, asm, хотя я и не проверял), нет ничего, чтобы остановить CPU с непринужденной моделью памяти от перемещения readIORef yourRef до всех myref/seq вещи. Единственный 100% надежный способ предотвратить его - это ограждение памяти, которое GHC не предоставляет. (В блоге Edward есть некоторые другие вещи, которые вы можете сделать сейчас, а также почему вы не можете полагаться на них).

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

Изменить: на уровне cmm фрагмент кода выше выглядит так (упрощенный, псевдокод):

[StackPtr+offset] := True
x := [StackPtr+offset]
if (notEvaluated x) (evaluate x)
yourVal := [StackPtr+offset2]

Итак, есть пара вещей, которые могут случиться. GHC, как он в настоящее время стоит, вряд ли переместит последнюю строку раньше, но я думаю, что это могло бы сделать, если бы это показалось более оптимальным. Меня больше беспокоит, что, если вы скомпилируете LLVM, оптимизатор LLVM может заменить вторую строку на только что написанное значение, а затем третья строка может быть сведена из постоянной последовательности, что сделало бы ее более вероятной чтение может быть перемещено ранее. И независимо от того, что делает GHC, большинство моделей памяти CPU позволяют самому процессору перемещать прочитанное ранее, не имеющее барьера памяти.

Ответ 3

http://en.wikipedia.org/wiki/Memory_ordering для неатомных параллельных чтений и записей. (в основном, когда вы не используете атоматику, просто посмотрите на модель упорядочения памяти для вашего целевого процессора)

В настоящее время ghc можно рассматривать как не переупорядочивание ваших чтений и записей для неатомных (и императивных) нагрузок и хранилищ. Однако GHC Haskell в настоящее время не указывает какую-либо модель параллельной памяти, поэтому эти неатомные операции будут иметь семантику упорядочения базовой модели ЦП, как я ссылаюсь на выше.

Другими словами, в настоящее время GHC не имеет формальной модели памяти concurrency, и потому, что любые алгоритмы оптимизации, как правило, относятся к некоторой модели эквивалентности, в настоящее время нет переупорядочения.

то есть: единственная семантическая модель, которую вы можете иметь прямо сейчас, - "способ ее реализации"

стреляйте в меня по электронной почте! Я работаю над некоторыми исправлениями атоматики для 7.10, давайте попробуем приготовить семантику!

Изменить: некоторые люди, которые понимают эту проблему лучше, чем я, нажимают на поток ghc-users здесь http://www.haskell.org/pipermail/glasgow-haskell-users/2013-December/024473.html. Предположим, что я ошибаюсь как в этом комментарии, так и во всем, что я сказал в потоке ghc-users:)