Диссертация (1149932), страница 12
Текст из файла (страница 12)
приобретающее чтение может быть частью синхронизации, следовательно в результате перестановки может быть изменено отношение62“предшествует” hb. Поэтому промышленные компиляторы, такие как GCC [102]и Clang [103], эту оптимизацию не реализуют. В то же время все корректные схемы компиляции инструкций приобретающего чтения для основных процессорных архитектур (x86, Power, ARM) также гарантируют, что сценарий поведения,который разрешается в C/C++11 MM, но запрещён в OpC11 MM, не наблюдаетсяна этих архитектурах.В нашей модели не позволяется выполнять не по порядку инструкции, относящиеся к одной локации. Как следствие, наша модель не разрешает слабый сценарий поведение теста ARM-weak (см.
приложение А.10), в результате которогоa = 1. При этом такой результат возможен в С/C++11 MM. Подробное описаниеданного теста приведено в главе 3.Кроме того, наша модель не совпадает с C/C++11 MM на примерах со “значениями из воздуха” (OOTA-lb, OOTA-if ), что является преимуществом.2.3.2Проверка модели на примере RCU-структурыКроме “лакмусовых” тестов OpC11 MM была также проверена в контексте тестирования и отладки многопоточной структуры данных RCU (read-copyupdate) [104, 105]. RCU-структура является одной из стандартных стратегий реализации неблокирующего доступа к связной структуре данных, такой как списокили дерево, для одного писателя и множества читателей. Автор диссертационного исследования реализовал RCU-структуру для односвязного списка на основе освобождения памяти в момент затишья (quiescent state-based reclamation,QSBR) [106].
Центральной идеей RCU-структуры является то, каким образом писатель обновляет её узлы. Если писатель собирается изменить некоторый узел всписке, то вместо того, чтобы изменить его непосредственно, он создаёт копиюстарого узла, обновляет её, а потом изменяет ссылки в структуре таким образом,чтобы они указывали на новый узел вместо старого. Далее писатель ждёт, пока всечитатели не перестанут использовать старый узел, после чего память, отведеннаяпод узел, может быть переиспользована или освобождена.
Для корректности алгоритма необходима правильная синхронизация между писателем и читателями:писатель обновляет ссылки на узлы с помощью высвобождающей записи, тогдакак читатели обходят список с помощью приобретающих чтений. Это гарантирует, что читатели не увидят частичные изменения в структуре данных.63Название тестаVF WF SCF NAF PO ARR CRSB-rel-acq3SB-sc33SB-sc-rel33SB-sc-acq33LB-rlx33LB-rel-rlx33LB-acq-rlx33LB-rel-acq-rlx333LB-rlx-use33LB-rlx-let33LB-rlx-join33LB-rel-rlx-join33LB-acq-rlx-join33MP-rlx-na33MP-rel-rlx-na33MP-rlx-acq-na33MP-rel-acq-na333MP-rel-acq-na-rlx(_2)3 333MP-con-na(_2)333MP-cas-rel-acq-na333MP-cas-rel-rlx-na33CoRR-rlx3CoRR-rel-acq3IRIW-rlx3IRIW-rel-acq3IRIW-sc33WRC-rlx3WRC-rel-acq3WRC-cas-rel33WRC-cas-rlx3OOTA-lb33OOTA-if33WR-rlx33WR-rlx-rel333WR-rel333SE-simple33SE-prop33SE-nested33ARM-weak33Блокировка Деккера33Блокировка Коэна [66] 33JN C1133333373333 33 3373333333333333333377333333733Табл.
1. Результаты запуска интерпретатора OpC11 MM на “лакмусовых” тестах64Программа:[cw] :=na 0; [cr1] :=na 0; [cr2] :=na 0; [lhead] :=na null;[a] :=rlx (1, null);[ltail] :=na a;[lhead] :=rel a;append(b, 10, ltail);append(c, 100, ltail);updateSecondNode(d, 1000)Функции:append(loc, value, ltail) ≜[loc] :=rlx (value, null);rt :=na [ltail];rtc :=rlx [rt];[rt] :=rel (fst rtc, loc);[ltail] :=na locupdateSecondNode(loc, value) ≜r1 :=rlx [lhead];r1c :=rlx [r1];r2 := snd r1c;r2c :=rlx [r2];r3 := snd r2c;[loc] :=rel (value, r3);[r1] :=rel (fst r1c, loc);sync(cw, cr1, cr2);delete r2sync(cw, cr1, cr2) ≜rcw :=rlx [cw];rcwn := rcw + 2;[cw] :=rel rcwn;syncWithReader(rcwn, cr1);[sum11] :=na 0;rcuOnline(cw, cr1);traverse(lhead, cur1, sum11);rcuOffline(cw, cr1);[sum21] :=na 0;rcuOnline(cw, cr2);traverse(lhead, cur2, sum21);rcuOffline(cw, cr2);[sum12] :=na 0;rcuOnline(cw, cr1);traverse(lhead, cur1, sum12);rcuOffline(cw, cr1);[sum22] :=na 0;rcuOnline(cw, cr2);traverse(lhead, cur2, sum22);rcuOffline(cw, cr2);r11 :=na [sum11];r12 :=na [sum12]r21 :=na [sum21];r22 :=na [sum22]traverse(lhead, curN odeLoc, resLoc) ≜rh :=acq [lhead];[curN odeLoc] :=na rh;repeatrCurN ode :=na [curN odeLoc];if rCurN ode ̸= nullthen rN ode :=acq [rCurN ode];rRes :=na [resLoc];rV al := fst rN ode;[resLoc] :=na rV al + rRes;[curN odeLoc] :=na snd rN ode;0else 1fiendsyncWithReader(rcwn, cr) ≜repeat r0 :=acq [cr]; r0 >= rcwn endrcuOnline(cw, cr) ≜r0 :=acq [cw];[cr] :=rlx r0 + 1rcuOffline(cw, cr) ≜r0 :=rlx [cw];[cr] :=rel r0syncWithReader(rcwn, cr2)Рис.
19. Реализация алгоритма QSBR RCU65QSBR-реализация RCU-списка и использующая его клиентская программаприведена на рис. 19. В первой строке происходит инициализация счётчиков потоков: cw – счётчик (первого) потока-писателя, cr1 и cr2 – счётчики второго итретьего потоков программы, которые являются читателями структуры. В той жестроке происходит инициализация указателя lhead на начало списка. Далее происходит запуск трёх потоков.Поток-писатель добавляет в список три значения: 1, 10 и 100. Заметим, чтопоскольку в нашей модели не описывается выделение памяти, то для записи значений используются константные локации a, b и c.
После того, как поток записывает три значения, он заменяет второй элемент списка, в котором хранится значение 10, на новый узел d, в который записывается значение 1000. При обновлениисписка с помощью функции updateSecondNode поток-читатель вызывает функцию синхронизации sync, внутри которой происходит обновление счётчика cw, иожидает обновления других потоков (вызовы функции syncWithReader).Рассмотрим подробнее функцию append, которая используется для добавления второго и третьего значений в список.
В этой функции сначала создаётся новый узел ([loc] :=rlx (value, null)), далее указатель на последний элемент списка записывается в переменную rt (rt :=na [ltail]), происходит разыменованиеуказателя (rtc :=rlx [rt]), после чего по указателю rt записывается старое значение последнего элемента списка (fst rtc) и указатель на новый узел (loc). В концеобновляется указатель на последний элемент списка ([ltail] :=na loc). Отметим,что в функции append все обращения к памяти, кроме [rt] :=rel (fst rtc, loc), являются неатомарными или расслабленными.
Это связано с тем, что локация ltailи переменные rt и rtc локальны для первого потока. При этом высвобождающаязапись [rt] :=rel (fst rtc, loc) делает так, что потоки-читатели, обходящиесписок с помощью приобретающих чтений в функции traverse, становятся осведомлёнными о записи в новый узел ([loc] :=rlx (value, null)) в тот момент,когда получают указатель на ячейку loc.Потоки-читатели по два раза обходят список, создаваемый писателем, и вычисляют сумму его элементов (переменные r11, r12, r21 и r22).
Перед началомобхода списка они вызывают функцию rcuOnline, которая выполняет две задачи.Во-первых, эта функция выполняет приобретающее чтение из cw, которое синхронизирует поток с некоторой версией списка. Во-вторых, с помощью увеличения счётчика cr поток сигнализирует писателю о том, что он начал обход списка.66Симметрично, читатель обновляет свой счётчик и уведомляет поток-писатель после обхода списка с помощью функции rcuOffline.Дополнительная инфраструктура для тестирования RCUструктурыС помощью запускаемой операционной семантики можно провести динамический анализ приведённой выше программы, а именно, построить пространство состояний исполнения программы в OpC11 MM и проверить его свойства,такие как отсутствие гонок по данным. Тем не менее, такой подход не являетсяреалистичным, поскольку пространство состояний для этой программы очень велико.
Это связано с тем, что модель имеет три аспекта недетерминированности:– планирование потоков;– отложенные операции;– недетерминированное чтение даже из фиксированной локации.Все эти аспекты приводят к комбинаторному взрыву пространства состояний.Для того, чтобы сделать динамический анализ возможным на практике (хотя бы в ограниченном варианте), диссертантом была реализована версия модели,которая строит некоторый случайный путь в пространстве состояний исполненияпрограммы. На первом шаге к текущему состоянию машины недетерминированно применяются все возможные правила.
Далее проверяется, есть ли в получившемся множестве stuck-состояние, которое сигнализирует о том, что программа имеет неопределённое поведение. Если такого состояние нет, то из множестваслучайным образом выбирается новое состояние, и процедура повторяется. Имеятакое представление модели, мы можем проводить свойство-ориентированное тестирование программы [107].Дополнительно, в язык задания модели был добавлен оператор delete, который “удаляет” переданную ему локацию. Данный оператор может быть использован для проверки того, что некоторая локация, начиная с некоторого моментаисполнения программы, больше не используется, что является одним из свойствRCU-структуры.
Для задания семантики этому оператору в состояние машиныOpC11 был добавлен дополнительный список “удалённых” локаций. Обращениек локации из этого списка приводит к stuck-состоянию.67# r111234567891011121314151617181920000000010010110000111r12r21r22stuckвремя (сек.)111101101110111011101110111010110111100011101110111111101100001111111100110001011011101011001101011011101111010111110101101010325.221.412.925.416.317.522.116.519.226.423.820.521.521.522.116.018.122.226.020.1333Табл. 2. Результаты тестирования модифицированной программы с RCUТестирование и отладка RCU-структурыС помощью рандомизированной модели автор диссертационного исследования протестировал приведенную RCU-структуру.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
