Об авторе
Антон Подкопаев является постдоком в
MPI-SWS, руководителем группы слабых моделей памяти в
лаборатории языковых инструментов JetBrains Research и преподавателем Computer Science Center.
Еще в 1979 году Лесли Лампорт в статье «
How to make a multiprocessor computer that correctly executes multiprocess programs» ввел, как следует из названия, идеализированную семантику многопоточности —
модель последовательной консистентности (sequential consistency, SC). Согласно данной модели, любой результат исполнения многопоточной программы может быть получен как последовательное исполнение некоторого чередования инструкций потоков этой программы. (Предполагается, что чередование сохраняет порядок между инструкциями, относящимися к одному потоку.)
Рассмотрим следующую программу
SB:
В этой программе два потока, в каждом из которых первая инструкция — инструкция записи в разделяемую локацию (x или y), а вторая — инструкция чтения из другой разделяемой локации. Для этой программы существует шесть чередований инструкций потоков: