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

Перевод статьи Лесли Лэмпорта (Leslie Lamport. How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Program)


 

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

Индекс терминов. Дизайн компьютера, параллельное вычисление, аппаратная корректность, многопоточность (multiprocessing), параллельная обработка.

Высокоскоростной процессор может выполнять операции в порядке, отличном от того, как они были описаны в самой программе. Корректность выполнения гарантируется если процессор удовлетворяет следующему условию: результат выполнения такой же как если бы операции были выполнены в порядке заданном в программе. Процессор удовлетворяемый этому условию будем называть последовательным. Предположим компьютер состоит из нескольких подобных процессоров, которые используют общую память. Привычный подход для проектирования и доказательства корректности многопоточных алгоритмов [1]-[3] для такого компьютера предполагает, что следующее условие будет удовлетворено: результат любого выполнения будет таким же, как если бы операции для всех процессоров были выполнены в определенно последовательном порядке, и операции для каждого процессора соответствовали последовательности заданной в программе. Многопроцессорная система удовлетворяющая данному условию будет называтся последовательно согласованной (sequentially consistent). Последовательность для каждого процессора не гарантирует что многопроцессорный компьютер будет последовательно согласованным. В данной статье мы описывем метод взаимодействия последовательных процессоров с модулями памяти которые гарантируют последовательную согласованность для системы которая будет получена в результате.

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

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

Поток 1
	A:=1
	IF B = 0 THEN Critical section;
			A:=0
		ELSE … FI
Поток 2
	B:=1
	IF A = 0 THEN Critical section;
			B:=0
		ELSE … FI

 

Оператор ELSE содержит некоторый механизм для того, что бы гарантировать возможный доступ к критической секции, но это выходит за рамки нашей дискусии. Легко осуществить доказательство, что протокол гарантирует взаимноисключающий доступ к критической секции ( Для работы над подтверждением можно воспользоваться техникой построенной на утверждениях (assertional techniques) [2], [3], здесь ее реализация опущена). Следовательно когда эта программа, содержащая два потока, выполняется на последовательно согласованном многопроцессорном компьютере, два процессора не могут выполнять свои критические секции в одно и тоже время.

Сперва мы наблюдаем, что последовательный процесор может выполнить «B:=1» и операцию «извлечения B» потоком 1 в любом порядке. (Когда программа потока 1 выполняется сама по себе, неважно, в каком порядке эти операции будут выполнены). Однако, легко заметить, что выполнение операции «извлечения B» первой может привести к ошибкам в обоих потоках и может позволить выполнение критических секций в одновременно. Это незамедлительно приводит нас к первому требованию для многопроцессорного компьютера.

Требование R1: Каждый процессор генерирует запросы к памяти в порядке заданном в программе.

Удовлетворить требование R1 сложно из-за того, что сохранение значения возможно только после, того как это значение было вычисленно. Процессор часто будет готов отправить запрос на извлечение требуемого значения до того, как получит сведения о значении сохраненном предыдущим запросом на сохранение. Что бы минимизировать время ожидания, процессор может послать запрос на сохранение модулю памяти без указания самого значения, которое будет сохранено. Разумеется, запрос на сохранение не может быть реально выполнен модулем памяти пока не будет получено соответствующее значение.

Требование R1 не является достаточным условием для того, что бы гарантировать корректное выполнение. Что бы увидеть это, предположим что каждый модуль памяти имеет несколько портов, и каждый порт обслуживает один процессор (или канал ввода-вывода). Пусть значения «a» и «b» будут сохранены в отдельных модулях памяти и рассмотрим следующую последовательность событий.

1. 
   
   Процессор 1 отсылает запрос «A:=1» на свой порт модуля памяти. Модуль в данный момент занят выполнением операции другого процессора (или порта ввода-вывода).
   
2. 
   
   Процессор 1 отсылает запрос на «извлечение B» на свой порт в модуле памяти. Модуль свободен и поэтому выполнение начинается незамедлительно.
   
3. 
   
   Процессор 2 отсылает свой запрос «B:=1» в модуль памяти 2. Этот запрос будет выполнен после того, как будет завершено выполнение запроса «извлечения B» от первого процессора.
   
4. 
   
   Процессор 2 отсылает запрос «извлечения A» на свой порт в модуле памяти 1. Модуль все еще занят.
   

 

Таким образом две операции ожидают своего выполнения в модуле памяти 1. Если операция «извлечения A» процессора 2 выполнится первой, то тогда оба процесса могут войти каждый в свою критическую секцию в одно и то же время и протокол безопасности потерпит неудачу. Это может случится если модуль памяти использует дисциплину кругового планирования (round robin scheduling discipline) выполнения запросов поступающих на его порты.

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

Требование R2. Запросы от процессоров отсылаются на один модуль памяти и обрабатываются одной FIFO (First Input - First Output) очередью. Отсылка запроса памяти представляет собой помещение данного запроса в эту очередь.

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

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

Требования R1 и R2 гарантируют что отдельные процессоры последовательны, а многопроцессорный компьютер – последовательно согласован. Для демонстрации данного факта, сперва введем отношение -> для запросов памяти. Определим A->B если и только если 1) A и B отсылаются одним процессором и A отсылается раньше B, или 2) A и B отсылаются в один модуль памяти и A помещается в очередь раньше B (и соответственно выполняется раньше B). Легко заметить что R1 и R2 предполагает что -> это частичное упорядочивание множества запросов к памяти. Используя последовательность каждого процессора, можно подтвердить следующий результат: каждая операция извлечения и сохранения извлекает или сохраняет то же значение как если бы все операции были выполнены последовательно в любом порядке и что A->B предполагает, что A выполняется раньше B. Этот порядок выполнения доказывает последовательную согласованность для многопроцессорного компьютера.

Требование R2 констатирует, что очередь запросов к модулю памяти должна обслуживаться в FIFO последовательности. Это предполагает, что модуль памяти должен бездействовать если запрос в начале очереди – это запрос на сохранение, для которого еще не получено сохраняемое значение. Условие R2 может быть ослаблено для того что бы позволить модулю памяти обслуживать другие запросы в данной ситуации. Нам необходимо только требование, согласно которому все запросы к одной ячейке памяти должны выполнятся в в той последовательности, в которой они добавлялись в очередь.Запросы к другим ячейкам памяти могут обслуживаться в другом порядке. Последовательная устойчивость сохраняется поскольку подобная политика обслуживания логически эквивалентна рассмотрению каждой ячейки памяти как отдельного модуля памяти со своей собственной очередью запросов. (В данном случае, эти модули могут влиять на скорость обслуживания запросов и возможности этих очередей, но нету никакого влияния на логические особенности последовательной согласованности).

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

Литература

[1] E. W. Dijkstra, "Hierarchical ordering of sequential processes," Acta Informatica, vol. 1, pp. 115-138, 1971.

[2] L. Lamport, "Proving the correctness of multiprocess programs," IEEE Trans.Software Eng., vol. SE-3, pp. 125-143, Mar. 1977.

[3] S. Owicki and D. Gries, 'Verifying properties of parallel programs: an axiomatic approach," Commun. Assoc. Comput. Mach., vol. 19, pp. 279-285, May 1976.