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

Введение

Свойство некоторых операций в параллельном программировании

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

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

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

Линеаризуемость была впервые представлена как модель согласованности Херлихи и Вингом в 1987 году. Она включала в себя более строгие определения атомарности, такие как "атомарная операция — это операция, которая не может быть (или не прерывается) другими выполняющимися одновременно операциями", которые обычно расплывчаты в отношении того, когда операция считается начатой и завершенной. Атомарный объект можно понять немедленно и полностью, исходя из его последовательного определения, как набор операций, выполняемых параллельно, которые всегда кажутся происходящими последовательно друг за другом; никаких противоречий возникнуть не должно. В частности, линеаризуемость гарантирует, что инварианты системы наблюдаются и поддерживаются всеми операциями: если каждая операция по отдельности сохраняет инвариант, то и система в целом будет его сохранять.

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

Самый простой способ добиться линеаризуемости — выполнять группы примитивных операций в критической секции. Строго говоря, независимые операции затем могут аккуратно перекрывать свои критические секции, при условии, что это не нарушает линеаризуемость. Такой подход должен балансировать между стоимостью большого количества блокировок и преимуществами повышенного параллелизма. Другой подход, предпочитаемый исследователями (но пока не получивший широкого распространения в индустрии программного обеспечения), заключается в разработке линеаризуемого объекта с использованием встроенных атомарных примитивов, предоставляемых аппаратным обеспечением. Это может максимизировать доступный параллелизм и минимизировать затраты на синхронизацию, но требует математических доказательств, подтверждающих корректность поведения объектов. Многообещающим гибридом этих двух подходов является предоставление абстракции транзакционной памяти. Как и в случае с критическими секциями, пользователь помечает последовательный код, который должен выполняться изолированно от других потоков. Реализация затем обеспечивает атомарное выполнение этого кода. Такой стиль абстракции часто используется при взаимодействии с базами данных; например, при использовании Spring Framework аннотация метода с помощью @Transactional гарантирует, что все операции с базой данных, заключенные в этот метод, будут выполнены в рамках единой транзакции базы данных. Транзакционная память идет еще дальше, обеспечивая атомарность всех операций с памятью. Как и в случае с транзакциями базы данных, возникают вопросы, касающиеся композиции транзакций, особенно транзакций базы данных и операций в памяти. Общей чертой при проектировании линеаризуемых объектов является предоставление интерфейса типа «все или ничего»: либо операция выполняется полностью успешно, либо она завершается неудачей и не оказывает никакого эффекта. (В базах данных ACID этот принцип называется атомарностью). Если операция не удается (обычно из-за конкурентных операций), пользователь должен повторить попытку, как правило, выполнив другую операцию. Например:
Compare and swap записывает новое значение в ячейку памяти только в том случае, если ее текущее содержимое соответствует предоставленному старому значению. Это часто используется в последовательности «чтение-модификация-CAS»: пользователь читает ячейку памяти, вычисляет новое значение для записи и записывает его с помощью CAS (compare and swap); если значение изменяется одновременно, CAS завершится неудачей, и пользователь попытается снова. Load link/store conditional кодирует эту схему более прямолинейно: пользователь читает ячейку памяти с помощью load link, вычисляет новое значение для записи и записывает его с помощью store conditional; если значение изменилось одновременно, SC (store conditional) завершится неудачей, и пользователь попытается снова. В транзакции базы данных, если транзакцию невозможно завершить из-за конкурентной операции (например, из-за взаимоблокировки), транзакция будет прервана, и пользователь должен повторить попытку.

The easiest way to achieve linearizability is running groups of primitive operations in a critical section. Strictly, independent operations can then be carefully permitted to overlap their critical sections, provided this does not violate linearizability. Such an approach must balance the cost of large numbers of locks against the benefits of increased parallelism. Another approach, favoured by researchers (but not yet widely used in the software industry), is to design a linearizable object using the native atomic primitives provided by the hardware. This has the potential to maximise available parallelism and minimise synchronisation costs, but requires mathematical proofs which show that the objects behave correctly. A promising hybrid of these two is to provide a transactional memory abstraction. As with critical sections, the user marks sequential code that must be run in isolation from other threads. The implementation then ensures the code executes atomically. This style of abstraction is common when interacting with databases; for instance, when using the Spring Framework, annotating a method with @Transactional will ensure all enclosed database interactions occur in a single database transaction. Transactional memory goes a step further, ensuring that all memory interactions occur atomically. As with database transactions, issues arise regarding composition of transactions, especially database and in memory transactions. A common theme when designing linearizable objects is to provide an all or nothing interface: either an operation succeeds completely, or it fails and does nothing. (ACID databases refer to this principle as atomicity.) If the operation fails (usually due to concurrent operations), the user must retry, usually performing a different operation. For example:
Compare and swap writes a new value into a location only if the latter's contents matches a supplied old value. This is commonly used in a read modify CAS sequence: the user reads the location, computes a new value to write, and writes it with a CAS (compare and swap); if the value changes concurrently, the CAS will fail and the user tries again. Load link/store conditional encodes this pattern more directly: the user reads the location with load link, computes a new value to write, and writes it with store conditional; if the value has changed concurrently, the SC (store conditional) will fail and the user tries again. In a database transaction, if the transaction cannot be completed due to a concurrent operation (e. g. in a deadlock), the transaction will be aborted and the user must try again.