Ну, я думаю, что могу ответить на этот вопрос кратко.
Когда мы собираемся сказать, является ли параллельный объект корректным, мы всегда пытаемся найти способ расширить частичный порядок до общего порядка.
мы можем распознать, является ли последовательный объект более корректным.
Во-первых, давайте отложим параллельный объект в сторону.Мы обсудим это позже.Теперь давайте рассмотрим последовательную историю H_S, последовательная история - это последовательность событий (т. Е. Вызовов и ответов), за которой за каждым вызовом мгновенно следует соответствующий ответ. (Хорошо, «мгновенно» можно спутать,Рассмотрим выполнение однопоточной программы, конечно, есть интервал между каждым Invoke и его Response, но методы выполняются один за другим. Таким образом, «мгновенно» означает, что никакой другой 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, потому что нет никакого параллелизма, что нам нужноdo проверяет, работает ли выполнение так же, как мы ожидаем (соответствуют условиям последовательной спецификации).Другими словами, это 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 предшествует другому m2, то m1 должен предшествовать m2в переупорядоченной последовательности. (Это означает, что если Ri находится перед Ij в H_C, вы должны гарантировать, что Ri все еще перед Ij в переупорядоченной последовательности, i и 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: линеаризуемость] («следующий смысл» - это правило переупорядочения, о котором я говорил выше)
Хорошо, ссылка может быть немного запутанной,Это означает, что если каждая параллельная история имеет линеаризацию (эквивалентную ей легальную последовательную историю), параллельная программа удовлетворяет условиям линеаризации.
Теперь мы поняли, что такое Линеаризуемость .Если мы говорим, что наша параллельная программа линеаризуема, другими словами, она обладает свойством линеаризуемости.Это означает, что каждый раз, когда мы запускаем его, история линеаризуется (история - это то, что мы ожидаем).
Таким образом, очевидно, что линеаризуемость - это безопасность (правильность) property.
Однако метод переупорядочения всех параллельных историй в последовательную историю, чтобы определить, является ли программа линеаризуемой, возможен только в prinple.На практике мы сталкиваемся с множеством вызовов методов, вызываемых двузначными потоками.Мы не можем переупорядочить все их истории.Мы даже не можем перечислить все параллельные истории тривиальной программы.
Обычный способ показать, что реализация параллельного объекта является линеаризуемой, состоит в том, чтобы идентифицировать для каждого метода точку линеаризациигде метод получает эффект. [Искусство многопроцессорного программирования 3.5.1: точки линеаризации]
Мы обсудим этот вопрос в условиях «параллельного объекта».Это практически так же, как указано выше.Реализация параллельного объекта имеет несколько методов для доступа к данным одновременного объекта.И многопоточность будет совместно использовать параллельный объект.Поэтому, когда они обращаются к объекту одновременно, вызывая методы объекта, разработчик параллельного объекта должен обеспечить правильность одновременных вызовов метода.
Он идентифицирует для каждого метода точку линеаризации ,Самое главное, чтобы понять смысл точки линеаризации.Утверждение «где метод вступает в силу» действительно трудно понять.У меня есть несколько примеров:
Во-первых, давайте рассмотрим неправильный случай:
//int i = 0; i is a global shared variable.
int inc_counter() {
int j = i++;
return j;
}
Довольно легко найти ошибку.Мы можем перевести i ++ в:
#Pseudo-asm-code
Load register, address of i
Add register, 1
Store register, address of 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.
Итак, если вы реализуете параллельный объект, как определить правильность вашей программы? Вы должны идентифицировать каждый метод точек линеаризации и тщательно продумать (или даже доказать), что они всегда будут содержать инварианты параллельного объекта. Затем частичный порядок всех вызовов методов может быть расширен как минимум до одного допустимого общего порядка (последовательной истории событий), который соответствует последовательной спецификации параллельного объекта.
Тогда вы можете сказать, что ваш параллельный объект правильный.