Я понимаю, что метод Linearizable, если он имеет точку, где он, кажется, "вступает в силу" мгновенно с точки зрения других потоков. Это имеет смысл, но также сказано, что Линеаризуемость на самом деле является свойством истории исполнения. Что значит, чтобы история выполнения была линеаризуемой, почему меня это волнует, и как она относится к методу или объекту Linearizable?
Ответ 3
Ну, я думаю, что я могу ответить на этот вопрос кратко.
Когда мы собираемся определить правильность параллельного объекта, мы всегда пытаемся найти способ расширения частичного порядка до полного порядка.
мы можем узнать, является ли последовательный объект более правильным.
Во-первых, Давайте отложим параллельный объект. Мы обсудим это позже. Теперь рассмотрим последовательную историю H_S, последовательная история - это последовательность событий (то есть Invokes и Responses), из которых каждый Invoke следует мгновенно своим соответствующим ответом. (Хорошо, "мгновенно" можно было смутить, рассмотрим выполнение однопоточной программы, конечно, там интервал между каждым вызовом и его ответом, но методы выполняются один за другим. Таким образом, "мгновенно" означает, что никакой другой Invoke/Respone не может вставить пару Invoke_i ~ Response_i)
H_S может выглядеть так:
H_S : I1 R1 I2 R2 I3 R3 ... In Rn
(Ii means the i-th Invoke, and Ri means the i-th Response)
Будет очень легко рассуждать о правильности истории H_S, потому что не существует concurrency, нам нужно проверить, работает ли выполнение, а также то, что мы ожидаем (отвечаем условиям из последовательной спецификации). Другими словами, это legel последовательная история.
Хорошо, реальность заключается в том, что мы работаем с параллельной программой. Например, мы запускаем два потока A и B в нашей программе. Каждый раз, когда мы запускаем программу, мы получаем историю H_C (History_Concurrent) извещения. Нам нужно рассмотреть вызов метода как Ii ~ Ri, как указано выше в H_S. Конечно, должно быть много совпадений между вызовами метода, вызываемыми потоком A и потоком B. Но каждое событие (например, вызовы и ответы) имеет его порядок в реальном времени. Таким образом, вызовы и ответы всех методов, называемых A и B, могут быть отображены в последовательный порядок, порядок может выглядеть так:
H_C : IA1 IB1 RA1 RB1 IB2 IA2 RB2 RA2
Порядок, кажется, запутан, это просто вид событий каждого метода вызывает:
thread A: IA1----------RA1 IA2-----------RA2
thread B: | IB1---|---RB1 IB2----|----RB2 |
| | | | | | | |
| | | | | | | |
real-time order: IA1 IB1 RA1 RB1 IB2 IA2 RB2 RA2
------------------------------------------------------>time
И мы получили H_C.
Итак, как мы можем проверить правильность выполнения H_C? Мы можем изменить порядок H_C на H_RO по правилу:
ПРАВИЛО: Если один вызов метода m1 предшествует другому м2, то m1 должен предшествовать m2 в переупорядоченной последовательности. (Это означает, что если Ri находится перед Ij в H_C, вы должны гарантировать, что Ri все еще находится перед Ij в упорядоченной последовательности, я и j не имеют своих порядков, мы также можем использовать a, b, c...) Мы говорим, что H_C эквивалентно для H_RO (history_reorder) при таком правиле.
H_RO будет иметь 2 свойства:
- Он соблюдает порядок программы.
- Сохраняет поведение в режиме реального времени.
Измените порядок H_C без нарушения вышеприведенного правила, мы можем получить некоторые последовательные истории (которые эквивалентны H_C), например:
H_S1: IA1 RA1 IB1 RB1 IB2 RB2 IA2 RA2
H_S2: IB1 RB1 IA1 RA1 IB2 RB2 IA2 RA2
H_S3: IB1 RB1 IA1 RA1 IA2 RA2 IB2 RB2
H_S4: IA1 RA1 IB1 RB1 IA2 RA2 IB2 RB2
Однако мы не можем получить H_S5:
H_S5: IA1 RA1 IA2 RA2 IB1 RB1 IB2 RB2
потому что IB1 ~ RB1 полностью предшествует IA2 ~ RA2 в H_C, его нельзя переупорядочить.
Теперь, с этими последовательными историями, как мы можем подтвердить, правильное ли наше выполнение история H_C? (я выделяю историю H_C, это означает, что мы просто заботимся о правильности истории H_C, а скорее чем правильность параллельной программы)
Ответ прост, если хотя бы одна из последовательных историй правильная (юридическая последовательная история соответствует условиям последовательной спецификации), тогда история H_C линеаризуемая, мы называем юридическую H_S линеаризация H_C. И H_C - правильное выполнение. Другими словами, это юридическое исполнение, которого мы ожидали. Если у вас есть опыт параллельного программирования, вы должны написать такую программу, которая иногда выглядит
довольно хорошо, но иногда совершенно неправильно.
Теперь мы знаем, что такое линеаризуемая история выполнения параллельной программы. Итак, как насчет самой параллельной программы?
Основная идея линеаризуемости состоит в том, что каждая параллельная история эквивалентна в следующем смысле некоторой последовательной истории. [Искусство многопроцессорного программирования 3.6.1: Линеаризуемость] ( "следующий смысл" ) это правило переупорядочения, о котором я говорил выше)
Хорошо, ссылка может немного запутаться. Это означает, что если каждая параллельная история имеет линеаризацию (эквивалентная ей эквивалентная юридическая история), параллельная программа удовлетворяет условиям линеаризуемости.
Теперь мы поняли, что такое Линеаризуемость, Если мы говорим, что наша параллельная программа линеаризуема, другими словами, она обладает свойством линеаризуемости. Это означает, что каждый раз, когда мы запускаем его, история линеаризуема (история - это то, что мы ожидаем).
Таким образом, очевидно, что линеаризуемость - это свойство безопасности (правильности).
Однако метод переупорядочения всех параллельных историй для последовательной истории, чтобы судить о том, является ли программа линеаризуемой, возможен только в принципе. На практике мы сталкиваемся с вызовами вызовов методов, вызванных двузначными потоками. Мы не можем переупорядочить все истории из них. Мы даже не можем перечислить все совпадающие истории trival-программы.
Обычный способ показать, что реализация параллельного объекта линеаризуемым является определение для каждого метода точки линеаризации где метод taks действует. [Искусство многопроцессорного программирования 3.5.1: точки линеаризации]
Мы обсудим вопрос в условиях "параллельного объекта". Он по существу такой же, как и выше. Реализация параллельного объекта имеет некоторые методы доступа к данным параллельного объекта. И многопотоки будут совместно использовать параллельный объект. Поэтому, когда они обращаются к объекту одновременно, вызывая методы объекта, разработчик параллельного объекта должен гарантировать правильность вызовов сопутствующих методов.
Он будет идентифицировать для каждого метода точку линеаризации. Самое главное - понять смысл точки линеаризации. Утверждение о том, "где метод вступает в силу", действительно трудно понять. У меня есть несколько примеров:
Сначала рассмотрим неправильный случай:
//int i = 0; i is a global shared variable.
int inc_counter() {
int j = i++;
return j;
}
Очень легко найти ошибку. Мы можем перевести я ++ в:
#Pseudo-asm-code
Load register, address of i
Add register, 1
Store register, address of i
Таким образом, два потока могут выполнять один "i ++"; одновременно, и результат i, по-видимому, увеличивается только один раз.
Мы могли бы получить такой H_C:
thread A: IA1----------RA1(1) IA2------------RA2(3)
thread B: | IB1---|------RB1(1) IB2----|----RB2(2) |
| | | | | | | |
| | | | | | | |
real-time order: IA1 IB1 RA1(1) RB1(1) IB2 IA2 RB2(2) RA2(3)
---------------------------------------------------------->time
Независимо от того, что вы пытаетесь изменить порядок в реальном времени, вы не можете найти последовательную историю legel, эквивалентную H_C.
Мы должны переписать программу:
//int i = 0; i is a global shared variable.
int inc_counter(){
//do some unrelated work, for example, play a popular song.
lock(&lock);
i++;
int j = i;
unlock(&lock);
//do some unrelated work, for example, fetch a web page and print it to the screen.
return j;
}
ОК, какова точка линеаризации inc_counter()? Ответ - это весь критический раздел. Потому что, когда много потоков многократно называет inc_counter(), критический раздел будет выполняться атомарно. И это может гарантировать правильность метода. Ответ метода - это увеличенное значение глобального i. Рассмотрим H_C как:
thread A: IA1----------RA1(2) IA2-----------RA2(4)
thread B: | IB1---|-------RB1(1) IB2--|----RB2(3) |
| | | | | | | |
| | | | | | | |
real-time order: IA1 IB1 RA1(2) RB1(1) IB2 IA2 RB2(3) RA2(4)
Очевидно, что эквивалентная последовательная история является законной:
IB1 RB1(1) IA1 RA1(2) IB2 RB2(3) IA2 RA2(4) //a legal sequential history
Мы переупорядочиваем IB1 ~ RB1 и IA1 ~ RA1, потому что они перекрываются в реальном времени, их можно переопределить неоднозначно. В случае H_C мы можем предположить, что критический раздел IB1 ~ RB1 введен первым.
Пример слишком прост. Рассмотрим еще один:
//top is the tio
void push(T val) {
while (1) {
Node * new_element = allocte(val);
Node * next = top->next;
new_element->next = next;
if ( CAS(&top->next, next, new_element)) { //Linearization point1
//CAS success!
//ok, we can do some other work, such as go shopping.
return;
}
//CAS fail! retry!
}
}
T pop() {
while (1) {
Node * next = top->next;
Node * nextnext = next->next;
if ( CAS(&top->next, next, nextnext)) { //Linearization point2
//CAS succeed!
//ok, let me take a rest.
return next->value;
}
//CAS fail! retry!
}
}
Это алгоритм стека блокировки с ошибками!, но не заботитесь о деталях. Я просто хочу показать точку линеаризации push() и pop(). Я показал их в комментариях. Подумайте, что многие потоки многократно вызывают push() и pop(), они будут упорядочены на этапе CAS. И другие шаги кажутся не важными, потому что независимо от того, что они выполняли одновременно, окончательный эффект, который они берут на стек (точно верхняя переменная), обусловлен порядком шага CAS (точка линеаризации). Если мы можем убедиться, что точка линеаризации действительно работает, то параллельный стек является правильным. Изображение H_C слишком длинное, но мы можем подтвердить, что должен быть законный последовательный эквивалент H_C.
Итак, если вы реализуете параллельный объект, как сказать правильность вашей программы? Вы должны идентифицировать каждый метод точки линеаризации и тщательно мыслить (или даже доказывать), что они всегда будут содержать инварианты параллельного объекта. Тогда частичный порядок всех вызовов метода может быть расширен до, по меньшей мере, одного юридического полного порядка (последовательная история событий), которые соответствуют последовательной спецификации параллельного объекта.
Затем вы можете сказать, что ваш параллельный объект правильный.
