Слабые модели памяти: буферизации записи на x86

    Об авторе


    Антон Подкопаев является постдоком в MPI-SWS, руководителем группы слабых моделей памяти в лаборатории языковых инструментов JetBrains Research и преподавателем Computer Science Center.

    Еще в 1979 году Лесли Лампорт в статье «How to make a multiprocessor computer that correctly executes multiprocess programs» ввел, как следует из названия, идеализированную семантику многопоточности — модель последовательной консистентности (sequential consistency, SC). Согласно данной модели, любой результат исполнения многопоточной программы может быть получен как последовательное исполнение некоторого чередования инструкций потоков этой программы. (Предполагается, что чередование сохраняет порядок между инструкциями, относящимися к одному потоку.)

    Рассмотрим следующую программу SB:



    В этой программе два потока, в каждом из которых первая инструкция — инструкция записи в разделяемую локацию (x или y), а вторая — инструкция чтения из другой разделяемой локации. Для этой программы существует шесть чередований инструкций потоков:



    В этом и последующих примерах мы предполагаем, что разделяемые локации инициализированы значением 0. Тогда, согласно модели SC, у этой программы есть только три возможных результата исполнения: [a=1, b=0], [a=0, b=1] и [a=1, b=1].

    Первый из них соответствует последовательному исполнению первого чередования инструкций, второй — второму, а третий — оставшимся четырем. Никакие другие результаты исполнения программы SB, в частности [a=0, b=0], моделью SC не допускаются.

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



    Давайте проверим, что на практике все так же. Для этого мы реализуем программу
    SB-impl на С++:

     1: #include <thread>
     2: #include <iostream>
     3: 
     4: using namespace std;
     5: 
     6: int x, y, a, b;
     7: 
     8: void thread1() {
     9:  cout.flush();
    10:  x = 1;
    11:  a = y;
    12: }
    13: 
    14: void thread2() {
    15:  y = 1;
    16:  b = x;
    17: }
    18: 
    19: int main() {
    20:  int cnt = 0;
    21:  do {
    22:    a = 0; b = 0;
    23:    x = 0; y = 0;
    24: 
    25:    thread first(thread1);
    26:    thread second(thread2);
    27: 
    28:    first.join();
    29:    second.join();
    30:    cnt++;
    31:  } while (a != 0 || b != 0);
    32:  cout << cnt << endl;
    33:  return 0;
    34: }

    Здесь аналог SB запускается в цикле (строки 21–31), пока не будет получен результат [a=0, b=0]. Если он будет получен, то на экране появится номер соответствующей итерации (строка 32). (Зачем в функции thread1 на строке 9 нужна команда cout.flush(), будет описано ниже.)

    С точки зрения модели SC, данная программа не должна завершиться, однако если скомпилировать этот код с помощью GCC и запустить на x86-машине,

    g++ -O2 -pthread sb.cpp -o sb && ./sb

    то можно увидеть на экране, например, 23022 или 56283 — такие результаты получил автор, запустив данный код на своем компьютере.

    Это пример показывает, что идеализированная модель SC не описывает реальное положение дел. Почему так? Откуда у программы SB берется результат [a=0, b=0]? На самом деле, причины две: компиляторные и процессорные оптимизации. Так, компилятор, в нашем случае — GCC, может заметить, что инструкции в левом (аналогично и в правом) потоке программы SB независимы друг от друга, и, как следствие, может их переставить:



    Для этой программы [a=0, b=0] является корректным с точки зрения модели SC. И эта перестановка действительно происходит! Для того чтобы в этом убедится, можно посмотреть на ассемблерный код, который GCC генерирует для функции thread1:

    g++ -O2 -c -S sb.cpp

    1: ...
    2: call    _ZNSo5flushEv@PLT
    3: movl    y(%rip), %eax
    4: movl    $1, x(%rip)
    5: movl    %eax, a(%rip)
    6: ...

    На строке 2 происходит чтение из переменной y и значение записывается в регистр eax, на строке 3 происходит запись в переменную x значения 1, а на строке 5 значение из регистра eax записывается в переменную a.

    Зачем нужен вызов функции cout.flush()
    Теперь пришло время объяснить, зачем нужен вызов функции cout.flush(). Как было упомянуто ранее, поскольку запись в x и чтение из y независимы, то компилятор, в нашем случае — GCC, может принять решение их переставить. Тем не менее, он не обязан этого делать: например, GCC не проводит перестановку для функции thread2. Для того чтобы сделать перестановку, компилятор должен предположить, что код после перестановки станет более эффективным. И, как показала практика, вызов функции cout.flush() заставляет GCC считать, что инструкции стоит переставить. При этом необязательно использовать именно эту функцию — достаточно функции, вызов которой GCC не уберет как бесполезный. Так, печать не пустой строки cout << " " подойдет, а вызов арифметических функций sqrt() и abs() без использования их результата не подойдет.

    Отметим, что cout.flush() не делает ничего в в программе SB-impl, хотя GCC и не может это вывести самостоятельно: cout.flush() сбрасывает буфер вывода в консоль, однако на каждом вызове cout.flush() буфер пуст, поскольку программа пишет в консоль только в конце (строка 34).

    Есть способ явно запретить компилятору переставлять инструкции чтения и записи в функциях thread1 и thread2. Для этого достаточно вставить компиляторный барьер памяти asm volatile("" ::: "memory") между инструкциями (в данном случае добавление инструкции cout.flush() не меняет ничего):

    void thread1() {
      x = 1;
      asm volatile("" ::: "memory");
      a = y;
    }
    
    void thread2() {
      y = 1;
      asm volatile("" ::: "memory");
      b = x;
    }

    Тем не менее, если запустить программу с компиляторными барьерами, то все еще можно получить результат [a=0, b=0], поскольку, как было упомянуто ранее, не только компилятор, но и процессор может быть причиной появления результатов, выходящих за пределы модели SC — результат [a=0, b=0] для программы SB не только разрешается спецификацией архитектуры x86, но и наблюдается на большинстве процессоров семейства x86.

    Для того чтобы понять, как подобный результат получается на процессоре, нужно обратиться к модели памяти архитектуры, т.е. к ее формальной семантике. Модель памяти архитектуры x86 называется TSO (total store order). TSO разрешает исполнения программ, выходящие за пределы модели SC, в частности исполнение программы SB, завершающиеся с результатом [a=0, b=0]. Такие исполнения называются слабыми, как и допускающие их модели памяти. Все основные процессорные архитектуры (x86, ARM, RISC-V, POWER, SPARC) обладают именно слабыми моделями памяти.

    Схематически модель TSO можно изобразить так:



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

    Рассмотрим исполнение программы SB в модели TSO, которое заканчивается с результатом [a=0, b=0]. В начале исполнения состояние программы и памяти выглядит следующим образом:



    P обоих потоков показывают на первые инструкции, все локации в памяти проинициализированы 0, а регистры a и b не определены. Далее левый поток выполняет инструкцию записи в локацию x, и соответствующий запрос попадает в буфер записи:



    Далее правый поток может выполнить аналогичный шаг:



    Теперь правый поток выполняет инструкцию чтения из локации x. Поскольку в его буфере нет запроса на запись в эту локацию, поток получает значение из основной памяти, присваивая соответствующее значение 0 регистру b:



    Аналогичным образом левый поток присваивает значение 0 регистру a:



    После чего запрос из буфера левого потока попадает в память:



    А за ним и запрос из буфера правого потока:



    Так, в модели TSO получается слабое исполнение для программы SB. Кстати, название программы SB является аббревиатурой от store buffering — эффекта, наблюдаемого в ее слабом исполнении.

    Тем не менее, существует способ запретить результат [a=0, b=0] для программы SB-impl, а значит и реализовать алгоритм Деккера на архитектуре x86. Для этого в программу нужно добавить процессорный барьер памяти mfence — специальную инструкцию x86 — которая, как и ранее использованный компиляторный барьер, запрещает GCC переставлять инструкции вокруг нее, но и дополнительно требует при своем исполнении уже на процессоре, чтобы буфер записи соответствующего потока был пуст:

    void thread1() {
      x = 1;
      asm volatile("mfence" ::: "memory");
      a = y;
    }
    
    void thread2() {
      y = 1;
      asm volatile("mfence" ::: "memory");
      b = x;
    }

    Так, чтение a :=[y] в левом потоке исправленной программы SB-impl может быть выполнено только после того, как запись [x] := 1 обновила основную память. Аналогичное утверждение верно для чтения b := [x] из правого потока. В итоге результат [a=0, b=0] становится невозможным.

    Заключение


    Мы рассмотрели пример многопоточной программы, которая может быть исполнена на архитектуре x86 неожиданным образом — продемонстрировать так называемое слабое исполнение, выходящее за пределы привычной модели SC. Это исполнение программы является результатом как компиляторных оптимизаций, так и оптимизаций используемых в процессоре семейства x86.

    В дальнейшем, если тема слабых исполнений и моделей памяти вызовет интерес, автор планирует написать серию постов на эту тему.

    Комментарии 21

      +6

      Отличное объяснение через буфер записи потока.

        +1

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


        Жду продолжения!

          0
          Отличное объяснение. Возник вопрос, связанный со слабым исполнением, по программе реализующей алгоритм Деккера, в том виде в котором он описывается:
          Мы отказываемся от слабого исполнения и обязываем процессор обновить глобальную память после первой инструкции (как я это понял). Как данная модификация сказывается на быстродействии?
            +1
            Скорость исполнения программы, конечно, уменьшается. Конкретные цифры для этой программы я не готов предоставить, но есть работы, которые тестировали, насколько происходит замедление для реальных программ, если форсировать отсутствие слабых исполнений. Проще всего будет сослаться на мой доклад в CSCenter (ссылка уже с нужной отметкой по времени).
            0
            Очень интересно, спасибо! Я собирался запись вашего недавнего доклада в Питере в compsciclub посмотреть, но, если вы содержание изложите в виде текста, то с гораздо большим удовольствием прочитаю текст, этот формат куда приятнее. И, если будете писать продолжение, то добавьте еще ссылок, куда дальше копать, если не трудно (особенно в связи с lock-free алгоритмами с atomic-ами).
              +1
              Спасибо! Доклад гораздо более общий. Содержание этой статьи там в первых 5 минутах. Пока доклад не планирую полностью в текст переносить.
              Про ссылки учту)
              0

              Я так понимаю здесь рассматривается именно реальное поведение на конкретном процессоре, т.к с точки зрения C++ просто нельзя писать в неатомарнвы переменные без синхронизации. Они вообще могли какую нить ерись выдать.


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

                +2

                Ну, asm volatile("mfence" ::: "memory") — это как раз своего рода синхронизация и есть. Но да, это непереносимо и работает только на одном процессоре.

                  +1
                  Я так понимаю здесь рассматривается именно реальное поведение на конкретном процессоре, т.к с точки зрения C++ просто нельзя писать в неатомарнвы переменные без синхронизации. Они вообще могли какую нить ерись выдать.

                  Вы правы, но я просто решил не упоминать atomic в первой статье. На самом деле, то же самое можно повторить, если сделать x и y atomic'ами и обращаться к ним с помощью memory_order_relaxed.
                  Модель C/C++ достоина отдельного вдумчивого поста)

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

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

                  Спасибо за очень ясную нотацию.


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

                  Через какое? И может быть, что не попадет вовсе в гипотетическом случае, когда кроме наших 2-х потоков ничего более не выполняется?

                    0
                    Это интересный вопрос) Если программа корректно работает, то архитектура гарантирует, что когда-нибудь запись попадёт в основную память. Но конкретнее в комментарии ответить не получится — это вопрос уже близок к той части формализации поведения процессоров, которая не очень хорошо изучена.
                      0

                      Вот и мне интересно. Но можно усугубить :) В смысле то же самое, но с NUMA. А так же на разных арх-рах: Intel, AMD, ARM...

                        0
                        Про ARM, надеюсь, ещё поговорим)
                      0

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


                      А вот в C++ такое может произойти запросто, потому что компилятор имеет право передвинуть присваивание куда угодно или даже вовсе удалить, если докажет что присвоенное значение нигде не используется.

                        0
                        Через какое?

                        Через минимально возможное в данной ситуации. Это не то чтобы точные данные, но просто держать в этом буфере что-то лишнее время тупо бесполезно, и процессор его выливает (в цепочку кэши — память) так быстро, как возможно без порчи остальной работы (а если в этом буфере и так места нет, то его выливу предоставляется приоритет перед другими операциями с памятью).

                        0
                        Подскажите пожалуйста, а если мы скомпилируем вариант SB без барьеров с флагом -O0 и запустим на x86, правильно ли я понимаю, что у нас все равно остается вероятность получить a=0; b=0 из-за аппаратных оптимизаций связанных с буфером записи?
                        Вам удавалось в тестах воспроизвести ситуацию нарушения SC именно из-за аппаратных оптимизаций x86?
                          0
                          Вам удавалось в тестах воспроизвести ситуацию нарушения SC именно из-за аппаратных оптимизаций x86?

                          Я воспроизвёл. i3-4170 и Ryzen 5 2400G.

                            0
                            тогда не совсем понятно, зачем автор вставляет cout.flush().
                            по-идее, даже без перестановки строк компилятором студенты могут получить нарушение SC только из-за буферов записи.
                              0
                              тогда не совсем понятно, зачем автор вставляет cout.flush().

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


                              Компилятор может переставить две строки в thread1 (в показанном варианте кода без барьеров), но не обязан. А от чего это зависит — выглядит как погода на Марсе, но является результатом взаимодействия исходника, версии компилятора, опции сборки и т.п. Вот автор и нашёл эмпирический вариант, как это сделать. Не был бы cout — нашлось бы что-то другое.

                          0

                          Тема интересная, имеет смысл именно такие крайние тонкие случаи подробно рассматривать. Замечания по сказанному:


                          ​1. Есть разные уровни "слабости" моделей памяти. X86, например, не переупорядочивает чтения одного ядра (соответственно одной нити) между собой, аналогично записи, аналогично записи с более поздними чтениями… а большинство RISC может делать хотя бы часть из этого. Особенность с буфером записи, конечно, сильно изменяет обстановку, но не фатально для обычной синхронизации. Фактически, модель X86 следовало бы назвать сильной, а не слабой (как обычно и делают) — специфика буфера записи (или строковых команд) тут влияет на очень специфические случаи. Хотя по сравнению с SystemZ она, да, слабая :)


                          Но вот классический документ "Intel64 Architecture Memory Ordering" (318147) про store buffer не говорит ни слова, зато,


                          Stores are not reordered with older loads.

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


                          ​2. Имеет смысл добавить, что использовать asm тут не нужно: в C++11 есть стандартные переносимые эквиваленты:


                          asm("":::"memory") -> std::atomic_signal_fence(std::memory_order_acq_rel);
                          asm("mfence":::"memory") -> std::atomic_thread_fence(std::memory_order_seq_cst);


                          это даже без атомарных переменных.


                          ​3. А теперь интересное: если я в каждой нити вставлю синхронизацию по следующему типу:


                          void thread2() {
                           y = 1;
                           std::atomic_thread_fence(std::memory_order_acq_rel);
                           b = x;
                          }
                          

                          то GCC (8, 9), Clang (6, 10) при -O0 сохраняют mfence, а при O уже нет! Им надо заменить acq_rel на seq_cst, чтобы сохранился mfence на всех уровнях оптимизации.


                          Я в первой версии этого комментария начал откровенно недоумевать, почему acq_rel по его мнению не должен включать все меры, чтобы выпихнуть предыдущие сбросы в память, если он знает про существование store buffer. Но, кажется, таки понятно: на обычную синхронизацию по типу мьютексов это не влияет. А вот с lock-free хитрее, за время доступного редактирования точно не успею обдумать во всех деталях. Прошу объяснений, кто может.

                            0
                            про store buffer не говорит ни слова

                            Недоредактировал. Говорит — в пункте 2.4, который надо отдельно грок.


                            PS: Понял. older loads — это которые раньше в потоке команд, а я почему-то подумал в обратную сторону. Да, порядка между более ранними записями и более поздними чтениями никто не обещал, его при необходимости надо требовать явно. Но сама необходимость такого типа как раз и выходит за рамки обычной mutex-style синхронизации.

                          Только полноправные пользователи могут оставлять комментарии. Войдите, пожалуйста.

                          Самое читаемое