Конспект: взаимное исключение и модели памяти

Понятия

Чередование - общий порядок операций всех потоков, где операции каждого идут в порядке его программы; у двух потоков по a и b операций их C(a + b, a). Гонка - результат зависит от чередования.

Критическая секция - код, где одновременно не больше одного потока. Требования к замку: взаимоисключение (безопасность), отсутствие взаимоблокировки и отсутствие голодания (живость).

Состояние протокола в SC - строки всех потоков плюс общая память; в TSO добавляются буферы записи. Полный перебор конечной модели доказывает проверяемое свойство в этой модели. У пекарни с неограниченными талонами состояний бесконечно много.

Последовательная согласованность - исполнение равно какому-то чередованию. TSO (x86) - записи идут через буфер ядра, чтение может обогнать свою запись в другую ячейку. Барьер - ждать, пока буфер не опустеет.

Что унести

c = c + 1 - ТРИ ОПЕРАЦИИ
1 инкремент на поток: 20 чередований, правильный итог - в 2
2 инкремента: 924 чередования, итоги 2, 3, 4; четвёрка - в 6
итог опускается до 2 при любом числе инкрементов
редкие переключения: тест иногда зелёный, иногда -117 из 400

ЗАМКИ НА ДВА ПОТОКА              состояний  итог
наивный: проверил, поднял флаг   16         двое в секции
LockOne: поднял флаг, ждёт       12         оба ждут вечно
LockTwo: только жертва           -          один ждёт вечно
Петерсон:                        26         всё соблюдено
  f[i] = 1; v = i
  ждать, пока f[j] == 1 и v == i
  секция; f[i] = 0
переставить первые две строки - двое в секции за 6 шагов

ЗАМКИ НА n ПОТОКОВ
фильтр: n − 1 уровней; level[i] = L, потом victim[L] = i,
        ждать, пока кто-то на уровне >= L и жертва - я
        уровень L проходят не больше n − L; 3 потока - 894 сост.
пекарня (Лэмпорт, 1974): флаг; талон = max + 1;
        ждать всех с флагом и меньшей парой (талон, номер)
        «кто первый пришёл»: не больше n − 1 обгонов
        талоны растут без предела, ничьи бывают
нижняя граница (Бёрнс, Линч): на чтениях и записях - n ячеек

МОДЕЛИ ПАМЯТИ
тест: x = 1; r0 = y  ||  y = 1; r1 = x
согласованная: [0,1] [1,0] [1,1]     TSO: ещё и [0,0]
TSO + барьер после записи: снова без [0,0]
Петерсон: согласованная - 26 состояний, чисто
          TSO - 400, двое в секции; барьер после v = i - 134, чисто
ARM, POWER: переставляют и записи между собой
язык: нет гонок данных → последовательная согласованность
      (Java, C++, Go); atomic по умолчанию - seq_cst

ПОИСК СЦЕНАРИЯ ПОЛОМКИ
в ширину (очередь): первое плохое состояние - ближайшее
в глубину (стек): те же состояния, путь произвольный

Ловушки джокера

«У меня работает». Гонку не ловят тестами: плохие чередования редки, на машине разработчика их почти нет.

«Если не занято - займи». Проверка и запись с зазором между ними пропускают двоих.

Порядок двух строк. Уступка раньше флага ломает Петерсона, жертва раньше уровня ломает фильтр.

Ничья талонов. Без сравнения номеров потоков двое с одинаковым талоном входят вместе.

Переполнение талона. Обнулившийся талон обгоняет всю очередь.

Перебор не в той модели. Протокол, чистый на согласованной памяти, на x86 ломается без барьера.

Барьер не там. Нужен между последней записью протокола и первым чтением чужих данных, а не после каждой строки.

• Монитор: общее состояние и замок; Condition.wait атомарно отпускает замок и перед возвратом захватывает его. Предикат проверяется в while. Notify не копит разрешения, семафор копит.

• RW-lock: читатели совместимы, писатель исключителен. Предпочтение читателей может голодать запись, предпочтение писателей - чтение. FIFO объединяет соседние чтения, но требует корректной отмены билетов.