Привет! В команде ВКонтакте мы переписываем рантайм движков баз данных — они становятся быстрее, надёжнее, а ещё с новым рантаймом проще писать код. Однако есть нюанс: в новом рантайме много конкурентных структур данных, в том числе нужных для работы с корутинами из С++20. Появляется интересная задача — проверять корректность этих конкурентных структур данных до выхода кода в продакшен.
Для решения этой задачи команда ВКонтакте вместе со студентами из университетов ИТМО и СПбГУ работала над научно-исследовательским проектом — верификацией конкурентных структур данных на языке C++. В этой статье подробно расскажем, как мы в рамках проекта проверяли корректность наших конкурентных структур данных и заодно исправили найденную в нашем новом рантайме ошибку.
![](https://habrastorage.org/getpro/habr/upload_files/820/98d/c68/82098dc68f8bc0b561560ebf4048f2c2.jpg)
Зачем нужны корутины в C++
Дать всеобъемлющее и понятное объяснение корутины сложно. Можно рассматривать её как легковесную (занимающую гораздо меньше памяти, чем тред ОС) прерываемую задачу. Если корутина захочет сделать действие, требующее ожидания, — например, подождать, пока в сокет придёт сообщение, и прочитать его, — то текущую корутину можно прервать и заставить тред ОС исполнять какую-то другую корутину. К исходной корутине можно будет вернуться, как только в сокете будут готовы данные. Прерывать корутину тоже проще, чем прерывать тред ОС. Для этого не нужны аппаратные прерывания и переключение из контекста пользователя (user space) в контекст ядра (kernel space) и обратно, а только сохранение пачки регистров и longjump. Это один из примеров реализации, а их существует достаточно много — описание одного из простых способов приведено тут.
Корутины существуют давно, со времён Scheme как минимум, но для широкой аудитории их продвинул Golang. Проблема в том, что корутины Golang нас разбаловали: в них есть почти всё, что нужно для счастья, — не блокирующая треды ОС работа с сетью, не блокирующие треды ОС примитивы синхронизации, work-stealing планировщик корутин и т. д.
Основным примитивом синхронизации корутин выступает канал. Канал — это очередь ограниченного размера, хранящая не более N элементов. При этом, если корутина хочет прочитать из канала, а в нём нет элементов, она будет ждать, пока там не появится хотя бы один элемент, который вставит другая корутина. Только после этого корутина вернёт этот элемент. Причём она будет ждать, не блокируя тред ОС, — он начнёт исполнять другую корутину, пока в канале не появятся данные, и тогда можно будет вернуться к исполнению текущей корутины.
Если корутина хочет в канал что-то положить, а в нём нет места (то есть в канале уже N элементов), она будет ждать, пока место освободится. То есть пока какая-то другая корутина не заберёт хотя бы один элемент. Только потом корутина вставит свой элемент, причём опять же будет ждать, не блокируя тред ОС, — он начнёт исполнять другую корутину, пока в канале не появится место, и тогда можно будет вернуться к исполнению текущей корутины.
Структуры данных, которые умеют приостанавливать исполнение корутин до наступления некоторого условия и только потом возвращать им управление, называются дуальными. Их сложно писать, а у нас в библиотеке их много.
А ещё рантайм Golang предоставляет нам планировщик корутин — это компонент, запускающий несколько тредов ОС и решающий для каждого момента времени, какую корутину будет исполнять каждый из доступных ему тредов ОС. Так как корутина — прерываемая задача, тред ОС исполняет назначенную ему корутину до ближайшей точки прерывания, а затем начинает исполнять другую доступную для исполнения корутину. Он откладывает исполнение текущей корутины до наступления некоторого условия — например, до появления данных в сокете или элемента в канале. После наступления этого условия корутина «разблокируется» и может снова быть исполнена одним из тредов ОС.
А что в «плюсах»? Там корутины появились в C++20, но только как языковой механизм — прерываемая функция, которую можно продолжить исполнять с того места, на котором прервались. Больше ничего нет — ни неблокирующей работы с сетью, ни примитивов синхронизации для корутин (например, каналов), ни даже планировщика корутин.
Если чего-то нет, значит, надо это написать. Вот мы и написали библиотеку, содержащую:
примитивы синхронизации для корутин;
обычные lock-free структуры данных вроде FAA-очереди;
корутинный сетевой движок;
планировщик корутин;
другие необходимые для работы наших баз данных компоненты.
Раз код есть, значит, надо его тестировать. Проблема в том, что код наш многопоточный, то есть запускаемый на множестве тредов ОС. Значит, корректность его работы зависит от того, как именно эти треды будут исполнены операционной системой.
Есть простой пример. Пусть у нас будет код, увеличивающий значение переменной Variable на единицу.
![](https://habrastorage.org/getpro/habr/upload_files/b4e/01b/91f/b4e01b91fb29836172cec91f583cd291.png)
Ещё есть два треда, увеличивающие одну и ту же переменную, изначально равную 0. В примере ниже исполнение будет корректным: два инкремента произошло, значение переменной увеличилось с 0 до 2.
![](https://habrastorage.org/getpro/habr/upload_files/8bf/fc6/d7f/8bffc6d7ff887e650c0673b94224eee4.png)
При этом исполнение на примере ниже будет некорректным: два инкремента произошли, а значение переменной увеличилось с 0 до 1, то есть один из инкрементов мы «потеряли».
![](https://habrastorage.org/getpro/habr/upload_files/2fe/735/34f/2fe73534f2ff288f4b10fea23a96cccb.png)
Мы провели один запуск теста — он показал, что проблемы нет. Можем ли мы быть уверены, что проверено в том числе проблемное второе исполнение, а не только корректное первое? На проде проблема может всплыть под нагрузкой, когда планировщик тредов ОС будет активнее переключать треды. Но в тесте под малой нагрузкой, когда планировщик тредов ОС активно треды не переключает, она может не проявиться. Из этого следует важный вывод: нужно уметь гарантировать, что мы перебрали вообще все возможные варианты исполнения.
Существует и другая возможная проблема. Допустим, мы провели тест и нашли баг (второе исполнение), а потом он перестал воспроизводиться — в последующих запусках теста операционная система не переключает треды ОС так, чтобы получилось второе исполнение. Пофиксить баг, не умея воспроизводить его, сложно. Из этого следует вывод: нужно управлять исполнением самим, не позволяя недетерминированному планировщику тредов ОС мешать нам. Таким образом, необходимо разработать способ тестирования, который, с одной стороны, будет проверять все интересующие нас варианты исполнения, а с другой — детерминировано воспроизводить найденные баги.
Была вероятность, что найти такой способ вообще не получится. Но мы рискнули и решили инвестировать вдолгую: не просто запустить процесс верификации собственного кода, а привлечь к нему студентов инженерных направлений. У них появилась бы площадка для получения опыта, а у нас — возможность исследования конкретной прикладной задачи.
Как мы организовали проект команды инфраструктуры ВКонтакте
При поддержке VK Education мы запустили научно-исследовательскую лабораторию для студентов, как делали годом ранее вместе с университетом ИТМО. В рамках такого проекта студенты пишут дипломную работу, одновременно решая задачи компании. В прошлом году они доказывали корректность распределённых систем. В этом году задача чуть изменилась — мы поручили участникам лаборатории верификацию конкурентных структур данных на языке C++.
В «прошлом сезоне» мы сотрудничали с руководителем научно-исследовательской лаборатории ИТМО Виталием Аксеновым. К нему же обратились для запуска новой лаборатории. По опыту работы с ним были уверены, что проект будет вестись грамотно и с чётким результатом. В этот раз мы расширили сотрудничество с университетами. Кроме ИТМО, с которым мы давно работаем, нашим партнёром стал СПбГУ. Там преподаёт старший разработчик баз данных ВКонтакте Илья Кокорин, который пригласил поучаствовать своих студентов и стал куратором лаборатории.
В работе лаборатории приняли участие пять бакалавров и магистров ИТМО и СПбГУ, которые прошли предварительное тестирование и собеседование. На проекте двое студентов работали с верификацией конкурентных структур данных, а остальных заинтересовали другие направления — оптимизация объектного кеша, оптимизация десериализатора языка межсервисного взаимодействия RPC/TL и разработка прототипа гибридного транзакционно-аналитического движка баз данных. Желающих попасть в лабораторию было больше. Для студентов это возможность поработать над востребованным проектом: многие пишут свои конкурентные структуры данных, но немногие умеют их проверять. А мы анонсировали, что будем работать над способом выполнять такие проверки.
Вторую лабораторию мы запустили в октябре 2023-го. Для начала провели несколько установочных встреч с участниками, где рассказали, какие компоненты есть в новом рантайме наших баз данных и почему нам важно доказательство корректности. Верификацию можно поручить человеку не из компании — это не user-facing элемент, если будет допущена ошибка, то весь продакшен не рухнет. Мы можем дать код студенту и попросить выполнить проверку — нам остаётся лишь наблюдать за процессом.
Еженедельно участники лаборатории созванивались с Ильёй Кокориным и Виталием Аксеновым, ежемесячно проходили сборы команды — каждый показывал презентацию с примерами кода и делился результатами исследования. По итогам работы лаборатории каждый студент получил R&D-проект в портфолио — причём трудился он над ним не в абстрактной ситуации, а с опытной командой работающего бизнеса. Выпускная работа может в перспективе перерасти в серьёзную научную статью, которая будет опубликована в ведущих журналах мира. К тому же ВКонтакте не забирает разработку себе — в будущем студент может свободно использовать решение в других своих проектах.
Самые талантливые из участников лаборатории могут получить офер в компанию. По итогам прошлого года мы трудоустроили двух из трёх выпускников, причём один из них сейчас занимается той же темой, с которой работал на проекте, — адаптирует модель для большего числа случаев и тестов.
Описание разработанного алгоритма проверки
Архитектура решения будет следующей: мы заведём несколько виртуальных потоков, выполняющих операции над тестируемой структурой данных. Каждый виртуальный поток — это последовательность ассемблерных инструкций, это не физический тред ОС. Будем исполнять их на одном физическом треде ОС, чередуя и переключая виртуальные потоки. К примеру, исполнить пять ассемблерных инструкций из первого виртуального потока, потом две ассемблерные инструкции из второго виртуального потока, одну ассемблерную инструкцию из третьего виртуального потока, снова переключимся на первый и так далее — такой способ чередования операций повсеместно используется при анализе конкурентных и распределённых алгоритмов.
Предположим, есть два виртуальных потока. Первый будет исполнять следующие инструкции:
![](https://habrastorage.org/getpro/habr/upload_files/ef9/aba/29c/ef9aba29c23d87c673cea629867bb6ad.png)
А второй — вот такие:
![](https://habrastorage.org/getpro/habr/upload_files/0b9/182/9d5/0b91829d5af8c6fea275b514a9f5e40f.png)
Тогда следующее исполнение будет одним из примеров допустимого чередования инструкций этих двух потоков, но не единственным:
![](https://habrastorage.org/getpro/habr/upload_files/094/4c2/7f0/0944c27f04b083364d32283f056818dc.png)
Исполнение ниже — тоже пример допустимого чередования:
![](https://habrastorage.org/getpro/habr/upload_files/4ee/9b8/93f/4ee9b893fbd49f62db6b65f39e07f66a.png)
Плюс последовательного исполнения операций в одном треде ОС в том, что оно строго детерминировано. Если однажды запуск пяти инструкций из второго виртуального потока и четырёх инструкций из первого привели к ошибке, то они будут приводить к той же самой ошибке и при дальнейших запусках (вынесем за скобки вопрос недетерминизма в коде тестируемой структуры).
Проблема в том, что язык C++ не предоставляет возможности исполнить несколько (одну, две, три) ассемблерных инструкций — он может исполнить только целую функцию. Значит, необходимо разработать такой механизм. Базово он будет работать следующим образом: тестируемая функция превращается в корутину — ведь корутины могут прерывать своё исполнение, а потом продолжать его с того же места, на котором прервались. Затем мы после каждой интересующей нас ассемблерной инструкции вставляем оператор прерывания корутины co_yield
. Этот оператор прерывает исполнение тестируемой функции, возвращая управление вызывающему коду таким образом, что потом можно продолжить исполнение с инструкции, следующей за co_yield
.
Теперь покажем, что будет с кодом ниже после этой операции:
![](https://habrastorage.org/getpro/habr/upload_files/b7e/3bc/39e/b7e3bc39e285a22af78af4142fe0ae28.png)
Он превратится в следующий код:
![](https://habrastorage.org/getpro/habr/upload_files/ede/f5c/8dc/edef5c8dcb4dbf2722388476ca012386.png)
Это позволит нам исполнять столько ассемблерных инструкций, сколько мы захотим. Например, исполнить только x := ATOMIC_READ(Variable)
, не исполняя ATOMIC_WRITE(Variable, y)
, и исполнить код другого виртуального потока между операциями чтения и записи — как на примере ниже.
![](https://habrastorage.org/getpro/habr/upload_files/b3e/659/125/b3e65912511028168143312dcdfbc9be.png)
Код нашей тестирующей системы будет всё это вызывать. Он будет работать следующим образом:
Придумываем несколько функций с аргументами:
Push(3)
,Pop()
,Pop()
,Push(5)
, и так далее, виртуальными потоками будут ассемблерные инструкции кода этих функций.Нужно выбрать один виртуальный поток и исполнить его либо до следующего
co_yield
, либо до завершения (кончились инструкции, исполнение функции завершено).Если произошёл
co_yield
, просто выберем другой (или тот же самый) виртуальный поток и продолжим его исполнение.Если функция завершилась, дадим этому виртуальному потоку исполнять другую функцию (придумаем функцию и аргументы для неё).
Когда надоест, перестаём давать виртуальным потокам новые функции и дожидаемся их завершения.
После завершения этой процедуры нам известна последовательность, в которой каждый поток вызывал функции тестируемой структуры данных, аргументы этих функций, а также их возвращаемые значения. Такая последовательность может быть проверена на корректность в конкурентной среде: мы проверяем истории обычных структур данных на линеаризуемость, а дуальных структур данных — на дуальную линеаризуемость.
Важно отметить, что код тестирующей системы должен быть особым образом адаптирован для тестирования дуальных структур данных. Например, у нас есть изначально пустой канал ch
и два виртуальных потока, первый из которых выполняет операцию взятия элемента из канала x := ch.Take()
, а второй — операцию добавления элемента в канал ch.Put(42)
. Пусть первой начинает исполняться операция взятия элемента из канала x := ch.Take()
. В ходе исполнения этой операции первый виртуальный поток понимает, что в канале нет элементов, и возвращает управление коду тестирующей системы. Теперь тестирующая система не должна передавать управление коду первого виртуального потока до тех пор, пока в канал не будет вставлен элемент 42, так как операция x := ch.Take()
блокирует исполняющую её корутину до появления в канале хотя бы одного элемента. Передача управления коду первого виртуального потока до появления в канале хотя бы одного элемента может нарушить инварианты реализации функции Take. Представить подробное описание алгоритма запуска и проверки мы планируем в отдельной статье.
Заметим, что теперь мы можем перебрать вообще все варианты чередования виртуальных потоков. Для двух инструкций из двух потоков это варианты:
![](https://habrastorage.org/getpro/habr/upload_files/022/14f/ac1/02214fac113bb5af8df1058521091f19.png)
Благодаря этому мы можем гарантировать, что никакое исполнение не будет некорректным. Чтобы ограничить пространство перебора, мы можем ограничить суммарное число исполняемых системой функций: например, запустим три виртуальных потока, каждый из которых исполнит по десять функций. Похожий алгоритм реализует TLA+. Такая методология проверки всех возможных исполнений в заданных ограничениях называется Bounded Model Checking.
К сожалению, наша верификация всё равно не может гарантировать отсутствие бага. Может быть, баг проявится на пяти виртуальных потоках, каждый из которых исполнит по сто операций. Но, будучи исполненной в разумных ограничениях (для достаточно большого числа виртуальных потоков и операций), верификация значительно повышает нашу уверенность в собственном коде. Мы круглосуточно перебираем исполнения в поисках ранее не обнаруженных проблем, резко уменьшая возможность выхода багов в прод.
На практике мы работаем не медленнее Lincheck — практической state-of-the-art системы верификации для конкурентных структур данных на языке Java. Мы выложим решение в open source, когда окончательно доведём его до ума.
Результаты и практическое применение
Мы подвели итоги проекта в конце июня, и от него уже есть практическая польза: мы верифицировали некоторые структуры из нашей библиотеки и в большинстве проверенных структур ошибок не нашли. Значит, скорее всего, их там нет. В одной из проверенных структур — очереди, относящейся к планировщику корутин, — нашли баг и исправили его. Баг в конкурентных структурах данных исправлять не так сложно, когда он стабильно воспроизводится нашим верификатором, а не выступает гейзенбагом, который воспроизвёлся однократно, а потом перестал. Теперь мы сильно повысили свою уверенность, что при выкладке кода сбоя не будет. Другие решения лаборатории ещё проходят апробацию. Пока планируем публикацию материалов в научных сборниках и участие в конференциях.
24 июня мы организовали выпускной для участников второй лаборатории, который прошёл в офисе ВКонтакте у Красного моста. Студенты делились техническими деталями своих проектов, а разработчики ВКонтакте задавали им уточняющие вопросы. Некоторые из выпускников станут нашими коллегами — один уже получил офер.
А мы обдумываем планы на продолжение исследований:
ускорять верификацию с помощью параллелизации проверки исполнения на линеаризуемость;
научиться работать со слабыми моделями памяти;
искать баги в open-source библиотеках с примитивами конкурентного программирования на C++;
минимизировать проблемное исполнение, например, как в github.com/flyingmutant/rapid;
научиться тестировать более сложные алгоритмы, управляющие жизненным циклом собственных корутин — например, RPC-сервер, запускающий собственные корутины для работы с каждым из клиентских сокетов.
Комментарии (11)
myxo
31.07.2024 12:08Базово он будет работать следующим образом: тестируемая функция превращается в корутину
Я правильно понял, что будет взят ассемблер и автоматически переписан так, чтобы получилась корутина? А что с вызовами функций?
ilyambda Автор
31.07.2024 12:08+3Я правильно понял, что будет взят ассемблер и автоматически переписан так, чтобы получилась корутина?
Работать с ассемблером сложно, поэтому мы работали с LLVM intermediate representation (для работы с ним существует удобное API, называемое LLVM passes).
А что с вызовами функций?
У нас есть два варианта работы с вызовами функций. В первом с каждой вызываемой функцией мы поступаем так же, как с исходной функцией: ставим оператор прерывания корутины
co_yield
после каждой интересующей нас инструкции. Например, кодfun g() { y := READ_ATOMIC(V2) WRITE_ATOMIC(V2, y - 1) } fun f() { x := READ_ATOMIC(V1) g() WRITE_ATOMIC(V1, x + 1) }
превратится в
fun g() { y := READ_ATOMIC(V2) co_yield WRITE_ATOMIC(V2, y - 1) } fun f() { x := READ_ATOMIC(V1) co_yield g() co_yield WRITE_ATOMIC(V1, x + 1) }
Таким образом, функция
f()
, будучи вызванной, четыре раза вернёт упаравление вызывающему коду:После инструкции
x := READ_ATOMIC(V1)
После инструкции
y := READ_ATOMIC(V2)
После инструкции
WRITE_ATOMIC(V2, y - 1)
, то есть после выхода из функцииg()
После инструкции
WRITE_ATOMIC(V1, x + 1)
, когда исполнение функцииf()
будет завершено
Второй вариант работы с вызовами функций состоит в том, что вызываемые функции мы считаем атомарными и не добавляем в их код операторы прерывания. Таким образом, код
fun g() { y := READ_ATOMIC(V2) WRITE_ATOMIC(V2, y - 1) } fun f() { x := READ_ATOMIC(V1) g() WRITE_ATOMIC(V1, x + 1) }
превращается в
fun g() { y := READ_ATOMIC(V2) WRITE_ATOMIC(V2, y - 1) } fun f() { x := READ_ATOMIC(V1) co_yield g() co_yield WRITE_ATOMIC(V1, x + 1) }
Таким образом, функция
f()
, будучи вызванной, три раза вернёт упаравление вызывающему коду:После инструкции
x := READ_ATOMIC(V1)
После инструкции
WRITE_ATOMIC(V2, y - 1)
, то есть после выхода из функцииg()
После инструкции
WRITE_ATOMIC(V1, x + 1)
, когда исполнение функцииf()
будет завершено
Функция
g()
же будет считаться атомарной, в ней исполнение прерываться не будет.
9241304
31.07.2024 12:08+3Проблема в том, что корутины Golang нас разбаловали
Фигасе проблемы у людей...
9241304
31.07.2024 12:08Если чего-то нет, значит, надо это написать. Вот мы и написали библиотеку, содержащую:
примитивы синхронизации для корутин;
обычные lock-free структуры данных вроде FAA-очереди;
корутинный сетевой движок;
планировщик корутин;
другие необходимые для работы наших баз данных компоненты.
Никогда не видел, чтобы такой самопал нормально работал и нормально поддерживался.
ilyambda Автор
31.07.2024 12:08+8Наша инфраструктурная команда поддерживает:
Самописные хранилища данных
Самописный консенсусный репликатор
Самописный распределённый компилятор C++ (видео, статья, код)
Самописную систему мониторинга больших распределённых систем (видео, код)
И ещё много всяких интересных и крутых штук. Думаю, что и с библиотекой конкурентных примитивов тоже справимся.
qq_svs
31.07.2024 12:08А возможные точки передачи управления устанавливаются вручную и представляют собой потенциальный источник ошибок? Или используете для этого статический анализ ГЗД, и, соответственно, автоматическое нахождение всех потенциально возможных конфликтных мест для установки точек переключения?
ilyambda Автор
31.07.2024 12:08Точки переключения мы выставляем автоматически, на этапе преобразования исходного кода при помощи написанного нами LLVM pass. Никакого сложного анализа мы не делали, а использовали набор достаточно простых эвристик: ставили точку переключения после каждого обращения к разделяемой переменной, то есть к переменной-члену тестируемой структуры или к глобальной переменной. После обращения к локальным переменным точки переключения мы не ставили, поскольку такие обращения никак не меняют разделяемое состояние (так как локальные переменные одного потока недоступны другим потокам). Таким образом, код
struct counter { int value; void inrement(int delta) { while (true) { const int cur_value = ATOMIC_READ(&this->value); // acess to shared variable const int new_value = cur_value + delta; // access to local variable if (COMPARE_AND_SWAP(&this->value, cur_value, new_value)) { // acess to shared variable return; } } } }
превратится в
struct counter { int value; void inrement(int delta) { while (true) { const int cur_value = ATOMIC_READ(&this->value); co_yield; const int new_value = cur_value + delta; // no co_yield here, because no shared state has been modified since the last co_yield const bool cas_res = COMPARE_AND_SWAP(&this->value, cur_value, new_value); co_yield; if (cas_res) { return; } } } }
Miceh
31.07.2024 12:08+1Интересная статья. Пара вопросов:
1) С++ компилятор переставляет statements без зависимости по данным? Если да, то как изложенный подход справится с этим?
2) конвертор в модельный Си язык для истинного параллелизма (например Promela в SPIN model checker) не проще было бы (не связываясь с "ассемблером")?
ilyambda Автор
31.07.2024 12:08+2С++ компилятор переставляет statements без зависимости по данным? Если да, то как изложенный подход справится с этим?
В этом смысле особенных проблем не будет. Ну вот пусть есть у нас код
func f() { x := ATOMIC_READ(&V1) ATOMIC_WRITE(&V1, x + 1) y := ATOMIC_READ(&V2) ATOMIC_WRITE(&V2, y - 1) }
При некоторых условиях компилятор волен будет переставить местами инструкции, получив, например
func f() { x := ATOMIC_READ(&V1) y := ATOMIC_READ(&V2) ATOMIC_WRITE(&V1, x + 1) ATOMIC_WRITE(&V2, y - 1) }
Для этого кода мы вызовем наш LLVM pass, получив в итоге корутину вида
func f() { x := ATOMIC_READ(&V1) co_yield y := ATOMIC_READ(&V2) co_yield ATOMIC_WRITE(&V1, x + 1) co_yield ATOMIC_WRITE(&V2, y - 1) }
То есть тестировать с помощью эмуляции переключения потоков мы в итоге будем непосредственно тот код, который нам сгенерировал компилятор.
Проблема, с которой мы пока справляемся плохо, заключена в другом: пусть у нас есть код вида
struct two_numbers_t { int* x = new int(0); int* y = new int(0); void thread_1_body() { *x = 1; *y = 1; } void thread_2_body() { const int local_x_value = *x; const int local_y_value = *y; assert(!(local_x_value == 0 && local_y_value == 1) && "This must not happen!"); } }
Из-за того, как работает реальное железо (в частности, кеши CPU) мы можем получить исполнение, при котором второй поток увидит
x
равным0
(то естьx
ещё не был инициализирован), аy
равным1
(то естьy
уже был инициализирован), хотя в первом потоке инициализацияx
происходит перед инициализациейy
.В нашем же тестовом фреймворке мы не сможем воспроизвести такую ситуацию, потому что всё чтения и записи происходят в пределах одного треда ОС, что убирает влияние кешей CPU на порядок видимости записей. В дальнейшем мы планируем научиться ловить и такие проблемы, есть уже пара идей, как такое можно делать.
конвертор в модельный Си язык для истинного параллелизма (например Promela в SPIN model checker) не проще было бы (не связываясь с "ассемблером")?
В нашем случае нам показалось, что расставить прерывания в коде было проще, чем учиться превращать наш код C++ в код на Promela. Что интересно, в проекте по верификации распределённых алгоритмов мы пользовались специальными языками, предназначенными для верификации, только это была не связка Promela/SPIN, а связка TLA+/TLC. С помощью TLC мы генерировали все возможные исполнения нашей системы, а потом превращали их в набор тестовых сценариев на Golang и проверяли, что код нашей системы при всех исполнениях ведёт себя так же, как TLA+-модель. Вот тут можно узнать подробнее, как это работает, если интересно.
Про саму связку Promela/SPIN мы в курсе, некоторые связанные с ней проекты (например, вот и вот) кажутся нам интересными, идеи из них мы планируем использовать и развивать в дальнейшей работе.
iushakov
А другие библиотеки, например, https://www.1024cores.net/home/relacy-race-detector смотрели?
ilyambda Автор
Это race detector, он не умеет проверять на линеаризуемость, да и на другие критерии корректности тоже: последовательную согласованность (sequential consistency), согласованность при покое (quiescent consistency), etc.