Линеаризуемость - Linearizability

Серым цветом обозначена линейная под-история, процессы, начинающиеся в b, не имеют линеаризуемой истории, потому что b0 или b1 могут завершиться в любом порядке до того, как произойдет b2.

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

1. Расширенный список может быть повторно выражен как последовательная история ( сериализуемая ).
2. Эта последовательная история является подмножеством исходного нерасширенного списка.

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

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

История линеаризуемости

Линеаризуемость была впервые введена в качестве модели консистенции по Херлихе и крылу в 1987 году охватывает более ограничительные определения атомного, такие как «атомный операция является тот , который не может быть (или нет) прерван параллельных операций», которые, как правило расплывчатого о когда операция считается началом и завершением.

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

Определение линеаризуемости

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

История представляет собой последовательность вызовов и ответов , сделанные из объекта с помощью набора нитей или процессов. Вызов можно рассматривать как начало операции, а ответ - как сигнализируемый конец этой операции. Каждый вызов функции будет иметь последующий ответ. Это можно использовать для моделирования любого использования объекта. Предположим, например, что два потока, A и B, оба пытаются захватить блокировку, отступая, если она уже занята. Это будет смоделировано как оба потока, вызывающие операцию блокировки, затем оба потока получают ответ, один успешный, другой нет.

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

История является линеаризуемой, если существует такой линейный порядок завершенных операций, что: ${\ displaystyle \ sigma}$

1. Для каждой завершенной операции в , операция возвращает тот же результат при выполнении, что и операция, если бы каждая операция выполнялась одна за другой по порядку .${\ displaystyle \ sigma}$${\ displaystyle \ sigma}$
2. Если операция op ₁ завершается (получает ответ) до того, как op ₂ начинается (вызывает), то op ₁ предшествует op ₂ в .${\ displaystyle \ sigma}$

Другими словами:

• его вызовы и ответы могут быть переупорядочены для получения последовательной истории;
• что последовательная история верна в соответствии с последовательным определением объекта;
• если ответ предшествовал вызову в исходной истории, он все равно должен предшествовать ему при последовательном изменении порядка.

(Обратите внимание, что первые два пункта соответствуют сериализуемости : операции выполняются в определенном порядке. Это последний пункт, который уникален для линеаризуемости и, таким образом, является основным вкладом Herlihy и Wing.)

Давайте рассмотрим два способа переупорядочения приведенного выше примера блокировки.

Изменение порядка вызова B под ответом A дает последовательную историю. Об этом легко рассуждать, так как теперь все операции происходят в очевидном порядке. К сожалению, это не соответствует последовательному определению объекта (не соответствует семантике программы): A должен был успешно получить блокировку, а B должен был впоследствии прерваться.

Это еще одна правильная последовательная история. Это тоже линеаризация! Обратите внимание, что определение линеаризуемости исключает изменение порядка только ответов, предшествующих вызовам; поскольку исходная история не имела ответов перед вызовами, мы можем изменить ее порядок по своему усмотрению. Следовательно, исходная история действительно линеаризуема.

Объект (в отличие от истории) является линеаризуемым, если все действительные истории его использования могут быть линеаризованы. Обратите внимание, что это утверждение намного сложнее доказать.

Линеаризуемость против сериализуемости

Рассмотрим следующую историю двух объектов, взаимодействующих с замком:

Эта история недействительна, потому что есть точка, в которой и A, и B удерживают блокировку; более того, его нельзя переупорядочить в действительную последовательную историю без нарушения правила упорядочивания. Следовательно, его нельзя линеаризовать. Однако при сериализуемости операция разблокировки B может быть перемещена до исходной блокировки A, которая является допустимой историей (при условии, что объект начинает историю в заблокированном состоянии):

Такое переупорядочение целесообразно при условии, что нет альтернативных средств связи между A и B. Линеаризуемость лучше при рассмотрении отдельных объектов по отдельности, поскольку ограничения на переупорядочение гарантируют, что несколько линеаризуемых объектов, рассматриваемых как единое целое, по-прежнему линеаризуемы.

Точки линеаризации

Это определение линеаризуемости эквивалентно следующему:

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

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

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

Примитивные атомарные инструкции

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

• атомарное чтение-запись;
• атомарный своп (инструкция RDLK в некоторых мэйнфреймах Burroughs и инструкция XCHG x86 );
• испытание и установка ;
• выборка и добавление ;
• сравнить и поменять местами ;
• загрузка-ссылка / магазин-условный .

Большинство процессоров включают операции хранения, которые не являются атомарными по отношению к памяти. К ним относятся хранилища нескольких слов и строковые операции. Если прерывание с высоким приоритетом происходит, когда часть хранилища завершена, операция должна быть завершена, когда будет возвращен уровень прерывания. Подпрограмма, обрабатывающая прерывание, не должна изменять изменяемую память. Это важно учитывать при написании подпрограмм прерывания.

Когда есть несколько инструкций, которые должны быть выполнены без прерывания, используется инструкция ЦП, которая временно запрещает прерывания. Это должно быть ограничено только несколькими инструкциями, а прерывания должны быть повторно разрешены, чтобы избежать неприемлемого времени реакции на прерывания или даже потери прерываний. Этого механизма недостаточно в многопроцессорной среде, поскольку каждый ЦП может вмешиваться в процесс независимо от того, происходят прерывания или нет. Кроме того, при наличии конвейера команд бесперебойные операции представляют угрозу безопасности, поскольку они потенциально могут быть связаны в бесконечный цикл, чтобы создать атаку отказа в обслуживании , как в случае с ошибкой Cyrix coma .

Стандарт C и SUSv3 обеспечивают sig_atomic_tпростые атомарные чтения и записи; не гарантируется, что увеличение или уменьшение будет атомарным. Более сложные атомарные операции доступны в C11 , который предоставляет stdatomic.h. Компиляторы используют аппаратные функции или более сложные методы для реализации операций; пример - libatomic GCC.

Набор команд ARM обеспечивает LDREXи STREXинструкцию , которые могут быть использованы для реализации атомного доступа к памяти, используя эксклюзивные мониторы , реализованные в процессоре , чтобы отслеживать доступ к памяти для конкретного адреса. Однако, если между вызовами и происходит переключение контекста , в документации отмечается ошибка, указывающая, что операцию следует повторить. LDREXSTREXSTREX

Атомарные операции высокого уровня

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

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

Перспективным гибридом этих двух является предоставление абстракции транзакционной памяти . Как и в случае с критическими секциями, пользователь отмечает последовательный код, который должен выполняться изолированно от других потоков. Затем реализация гарантирует, что код выполняется атомарно. Этот стиль абстракции распространен при взаимодействии с базами данных; например, при использовании Spring Framework аннотирование метода с помощью @Transactional гарантирует, что все вложенные взаимодействия с базой данных происходят в одной транзакции с базой данных . Транзакционная память идет еще дальше, гарантируя, что все взаимодействия с памятью происходят атомарно. Как и в случае транзакций с базой данных, возникают проблемы, связанные с составом транзакций, особенно транзакций с базой данных и в памяти.

Распространенной темой при разработке линеаризуемых объектов является предоставление интерфейса по принципу «все или ничего»: либо операция завершается полностью, либо не выполняется и ничего не делает. (В базах данных ACID этот принцип называется атомарностью .) Если операция завершается неудачно (обычно из-за одновременных операций), пользователь должен повторить попытку, обычно выполняя другую операцию. Например:

• Compare-and-swap записывает новое значение в местоположение, только если его содержимое совпадает с предоставленным старым значением. Это обычно используется в последовательности чтение-изменение-CAS: пользователь считывает местоположение, вычисляет новое значение для записи и записывает его с помощью CAS (сравнение и замена); если значение изменяется одновременно, CAS откажет, и пользователь попытается снова.
• Load-link / store-conditional кодирует этот шаблон более прямо: пользователь считывает местоположение с помощью load-link, вычисляет новое значение для записи и записывает его с помощью store-conditional; если значение изменилось одновременно, SC (условное хранилище) завершится ошибкой, и пользователь попытается снова.
• В транзакции базы данных , если транзакция не может быть завершена из-за одновременной операции (например, в тупике ), транзакция будет прервана, и пользователь должен будет повторить попытку.

Примеры линеаризуемости

Счетчики

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

Мы хотели бы реализовать объект счетчика, к которому могут обращаться несколько процессов. Во многих распространенных системах используются счетчики, чтобы отслеживать, сколько раз произошло событие.

К объекту счетчика могут обращаться несколько процессов, и у него есть две доступные операции.

1. Приращение - добавляет 1 к значению, хранящемуся в счетчике, возвращает подтверждение
2. Чтение - возвращает текущее значение, хранящееся в счетчике, не изменяя его.

Мы попытаемся реализовать этот объект счетчика, используя общие регистры.

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

Неатомный

Наивная, неатомарная реализация:

Приращение:

1. Прочтите значение в регистре R
2. Добавьте единицу к значению
3. Записывает новое значение обратно в регистр R

Читать:

Чтение регистра R

Эта простая реализация не поддается линеаризации, как показано в следующем примере.

Представьте, что два процесса работают, обращаясь к единственному объекту счетчика, инициализированному со значением 0:

1. Первый процесс считывает значение в регистре как 0.
2. Первый процесс добавляет единицу к значению, значение счетчика должно быть 1, но до того, как он закончит запись нового значения обратно в регистр, он может быть приостановлен, в то время как второй процесс выполняется:
3. Второй процесс считывает значение в регистре, которое все еще равно 0;
4. Второй процесс добавляет единицу к значению;
5. второй процесс записывает новое значение в регистр, теперь регистр имеет значение 1.

Второй процесс завершает работу, а первый продолжает работу с того места, где он остановился:

1. Первый процесс записывает 1 в регистр, не зная, что другой процесс уже обновил значение в регистре до 1.

В приведенном выше примере два процесса вызвали команду увеличения, однако значение объекта увеличилось только с 0 до 1 вместо 2, как должно было быть. Одна из операций приращения была потеряна из-за невозможности линеаризации системы.

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

Атомный

Чтобы реализовать объект линеаризуемого или атомарного счетчика, мы изменим нашу предыдущую реализацию, чтобы каждый процесс P i использовал свой собственный регистр R i.

Каждый процесс увеличивается и считывается в соответствии со следующим алгоритмом:

Приращение:

1. Считать значение в регистре R i .
2. Добавьте единицу к значению.
3. Запишите новое значение обратно в R i

Читать:

1. Чтение регистров R 1, R 2, ... R n .
2. Вернуть сумму всех регистров.

Эта реализация решает проблему с нашей исходной реализацией. В этой системе операции приращения линеаризуются на этапе записи. Точка линеаризации операции приращения - это когда эта операция записывает новое значение в свой регистр R i. Операции чтения линеаризуются до точки в системе, когда значение, возвращаемое считыванием, равно сумме всех значений, хранящихся в каждом регистре R i.

Это банальный пример. В реальной системе операции могут быть более сложными, а ошибки вносятся чрезвычайно незаметными. Например, чтение 64-битного значения из памяти может быть реализовано как два последовательных чтения двух 32-битных ячеек памяти. Если процесс прочитал только первые 32 бита, и до того, как он прочитает вторые 32 бита, значение в памяти изменится, у него не будет ни исходного значения, ни нового значения, а будет смешанное значение.

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

Сравнить и обменять

Большинство систем предоставляют атомарную инструкцию сравнения и замены, которая читает из области памяти, сравнивает значение с «ожидаемым» значением, предоставленным пользователем, и записывает «новое» значение, если они совпадают, возвращая, было ли обновление успешным. . Мы можем использовать это, чтобы исправить алгоритм неатомарного счетчика следующим образом:

1. Прочтите значение в ячейке памяти;
2. прибавьте единицу к значению;
3. используйте функцию сравнения и замены, чтобы записать увеличенное значение обратно;
4. повторите попытку, если значение, считанное при сравнении и замене, не соответствует значению, которое мы изначально считали.

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

Получение и приращение

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

1. Используйте выборку и инкремент, чтобы прочитать старое значение и записать увеличенное значение обратно.

Использование выборки и приращения всегда лучше (требует меньшего количества обращений к памяти) для некоторых алгоритмов, таких как показанный здесь, чем сравнение и замена, хотя ранее Херлихи доказал, что сравнение и замена лучше для некоторых других алгоритмов, которые вообще не может быть реализовано с использованием только выборки и инкремента. Таким образом, конструкции ЦП с выборкой и инкрементом и сравнением и заменой (или эквивалентными инструкциями) могут быть лучшим выбором, чем конструкции с одним или другим.

Блокировка

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

1. Получите блокировку, исключающую одновременное выполнение критического раздела другими потоками (шаги 2–4);
2. прочитать значение в ячейке памяти;
3. прибавьте единицу к значению;
4. записать увеличенное значение обратно в ячейку памяти;
5. отпустить замок.

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

Смотрите также

• Атомарная транзакция
• Модель согласованности
• КИСЛОТА
• Чтение-копирование-обновление (RCU)
• Чтение-изменение-запись
• Время проверки до времени использования

Рекомендации

дальнейшее чтение

• Херлихи, Морис П .; Крыло, Жаннетт М. (1987). Аксиомы для параллельных объектов . Материалы 14-го симпозиума ACM SIGACT-SIGPLAN по принципам языков программирования, POPL '87 . п. 13. DOI : 10,1145 / 41625,41627 . ISBN 978-0-89791-215-0. S2CID  16017451 .
• Херлихи, Морис П. (1990). Методология реализации высокопараллельных структур данных . Уведомления ACM SIGPLAN . 25 . С. 197–206. CiteSeerX  10.1.1.186.6400 . DOI : 10.1145 / 99164.99185 . ISBN 978-0-89791-350-8.
• Херлихи, Морис П .; Крыло, Жаннетт М. (1990). «Линеаризуемость: условие корректности для параллельных объектов». Транзакции ACM по языкам и системам программирования . 12 (3): 463–492. CiteSeerX  10.1.1.142.5315 . DOI : 10.1145 / 78969.78972 . S2CID  228785 .
• Афир. «Модели сильной согласованности» . aphyr.com . Афир . Проверено 13 апреля 2018 года .