• Партиционная компиляция (ocamlc)
• Система верхнего уровня или REPL (ocaml)
• Система выполнения (ocamlrun)
• Компиляция нативный код (ocamlopt)
• Генераторы лексических и синтаксических анализаторов (ocamllex, ocamlyacc)
• Генератор зависимостей (ocamldep)
• Генератор документации (ocamldoc)
• Отладчик (ocamldebug)
• Профилирование (ocamlprof)
• Интерфейс C с OCaml
• Оптимизация с помощью Flambda
• Fuzzing с afl-fuzz
• Отслеживание выполнения с помощью событий выполнения
• Преобразование программы «Tail Modulo Constructor»
• Обнаружение гонок данных во время выполнения с помощью ThreadSanitizer

Глава 27 Обнаружение гонок данных во время выполнения с помощью ThreadSanitizer

1 Обзор и использование

OCaml с версии 5.0 поддерживает параллелизм с общей памятью, а значит, позволяет изменять данные, общие для нескольких потоков. Это создаёт возможность возникновения гонок данных, то есть не упорядоченных обращений к одному и тому же месту памяти, причём, по крайней мере, одно из них должно быть записью. В OCaml легко ввести гонки данных, и поведение программ с гонками может быть неинтуитивным — наблюдаемое поведение нельзя объяснить простым переключением операций из разных конкурирующих потоков. Более подробную информацию о гонках данных и их последствиях можно найти в разделе ‍9.4 и главе ‍10.

Для обнаружения гонок данных OCaml поддерживает ThreadSantizer (TSan) — динамический детектор гонок данных, успешно применявшийся в таких языках, как C/C++, Swift и др. Поддержка TSan для OCaml доступна начиная с OCaml 5.2.

Для использования TSan необходимо настроить компилятор с помощью --enable-tsan. Также можно установить opam с включённой функцией TSan следующим образом:

opam switch create <YOUR-SWITCH-NAME-HERE> ocaml-option-tsan

В настоящее время поддержка TSan для OCaml доступна для архитектуры x86_64 на FreeBSD, Linux и macOS, а также для архитектуры arm64 на Linux и macOS. Для компиляции OCaml с поддержкой TSan требуется GCC или Clang. Минимальные поддерживаемые версии — GCC 11 и Clang 14. Обратите внимание, что сообщения о гонках данных TSan с GCC 11 могут иметь плохую отчётность по стеку вызовов (без номеров строк), что исправлено в GCC 12.

Компилятор с поддержкой TSan отличается от обычного компилятора тем, что все программы, скомпилированные с помощью ocamlopt, снабжаются вызовами времени выполнения TSan, и TSan будет обнаруживать гонки данных, возникающие во время выполнения.

Например, рассмотрим следующую программу:

let a = ref 0 and b = ref 0

let d1 () =
  a := 1;
  !b

let d2 () =
  b := 1;
  !a

let () =
  let h = Domain.spawn d2 in
  let r1 = d1 () in
  let r2 = Domain.join h in
  assert (not (r1 = 0 && r2 = 0))

Эта программа имеет гонки данных. Места памяти a и b читаются и записываются одновременно несколькими доменами d1 и d2. a и b являются «неатомными» местами памяти в соответствии с моделью памяти (см. главу ‍10), и между доступами к ним нет синхронизации. Следовательно, здесь две гонки данных, соответствующие двум местам памяти a и b.

При компиляции и запуске этой программы с помощью ocamlopt вы можете увидеть сообщения о гонках данных в стандартном потоке ошибок, например:

==================
WARNING: ThreadSanitizer: data race (pid=3808831)
  Write of size 8 at 0x8febe0 by thread T1 (mutexes: write M90):
    #0 camlSimple_race.d2_274 simple_race.ml:8 (simple_race.exe+0x420a72)
    #1 camlDomain.body_706 stdlib/domain.ml:211 (simple_race.exe+0x440f2f)
    #2 caml_start_program <null> (simple_race.exe+0x47cf37)
    #3 caml_callback_exn runtime/callback.c:197 (simple_race.exe+0x445f7b)
    #4 domain_thread_func runtime/domain.c:1167 (simple_race.exe+0x44a113)

  Previous read of size 8 at 0x8febe0 by main thread (mutexes: write M86):
    #0 camlSimple_race.d1_271 simple_race.ml:5 (simple_race.exe+0x420a22)
    #1 camlSimple_race.entry simple_race.ml:13 (simple_race.exe+0x420d16)
    #2 caml_program <null> (simple_race.exe+0x41ffb9)
    #3 caml_start_program <null> (simple_race.exe+0x47cf37)
[...]

WARNING: ThreadSanitizer: data race (pid=3808831)
  Read of size 8 at 0x8febf0 by thread T1 (mutexes: write M90):
    #0 camlSimple_race.d2_274 simple_race.ml:9 (simple_race.exe+0x420a92)
    #1 camlDomain.body_706 stdlib/domain.ml:211 (simple_race.exe+0x440f2f)
    #2 caml_start_program <null> (simple_race.exe+0x47cf37)
    #3 caml_callback_exn runtime/callback.c:197 (simple_race.exe+0x445f7b)
    #4 domain_thread_func runtime/domain.c:1167 (simple_race.exe+0x44a113)

  Previous write of size 8 at 0x8febf0 by main thread (mutexes: write M86):
    #0 camlSimple_race.d1_271 simple_race.ml:4 (simple_race.exe+0x420a01)
    #1 camlSimple_race.entry simple_race.ml:13 (simple_race.exe+0x420d16)
    #2 caml_program <null> (simple_race.exe+0x41ffb9)
    #3 caml_start_program <null> (simple_race.exe+0x47cf37)
[...]

==================
ThreadSanitizer: reported 2 warnings

Для каждой обнаруженной гонки данных TSan указывает местоположение конфликтующих обращений, их тип (чтение, запись, атомное чтение и т. д.) и соответствующий стек вызовов.

Если вы запустите вышеприведённую программу несколько раз, вывод может отличаться: иногда TSan сообщит о двух гонках данных, иногда об одной, а иногда ни о одной. Это связано с сочетанием двух факторов:

• Во-первых, TSan сообщает только о гонках данных, возникших во время выполнения, то есть о конфликтующих, неупорядоченных обращениях к памяти, которые фактически выполняются.
• Кроме того, в этой программе в зависимости от выполнения таких обращений к памяти может не быть: если d1 возвращается до того, как d2 закончит создание, то все обращения к памяти, исходящие от d1, могут произойти перед теми, которые исходят от d2, так как создание домена подразумевает межпоточную синхронизацию. В этом случае обращения считаются упорядоченными, и о гонках данных не сообщается.

Этот пример демонстрирует тот факт, что гонки данных иногда могут скрываться от не связанных с ними синхронизирующих операций.

2 Последствия для производительности

Инструментарий TSan накладывает не незначительные затраты во время выполнения. Эмпирически было замечено, что эти затраты приводят к замедлению, которое может варьироваться от 2 до 7 раз. Одним из основных факторов высоких замедлений является частый доступ к изменяемым данным. В отличие от этого, начальные записи в неизменяемые места памяти и чтения из них не обрабатываются. TSan также выделяет очень большие объёмы виртуальной памяти, хотя использует только часть из неё. Потребление памяти увеличивается в 4-7 раз.

3 Ложные отрицательные и ложные положительные результаты

Как показано на предыдущем примере, TSan будет сообщать только о гонках данных, обнаруженных во время выполнения. Ещё один важный момент заключается в том, что TSan запоминает только конечное число обращений к памяти на каждый элемент памяти. На момент написания это число равно 4. Гонки данных, связанные с забытым доступом, не будут обнаружены. Наконец, в документации TSan указано, что существует небольшая вероятность пропустить гонку, если два потока обращаются к одному и тому же месту одновременно. TSan может пропустить гонки данных только в этих трёх особых случаях.

Для гонок данных между двумя обращениями к памяти, выполненными из кода OCaml, TSan не генерирует ложных положительных результатов; то есть TSan не будет выдавать ложных сообщений.

При смешении кода OCaml и C с помощью C-примитивов понятие ложного положительного результата становится менее ясным, так как оно включает две модели памяти — OCaml и C11. Однако TSan должен вести себя в основном так, как ожидается: неатомные чтения и записи в C будут конкурировать с неатомными чтениями и записями в OCaml, а атомные операции C не будут конкурировать с атомными операциями OCaml. Существует одна теоретическая возможность ложного положительного результата: если значение инициализируется из C без использования caml_initialize (что разрешено при условии, что сборщик мусора не запускается между выделением и записью, см. главу ‍22), и в дальнейшем другой поток выполняет конфликтующий доступ. Это не является гонкой данных, но TSan может сообщить об этом как о таковой.

4 Параметры времени выполнения

TSan поддерживает ряд параметров конфигурации во время выполнения с помощью переменной среды TSAN_OPTIONS. TSAN_OPTIONS должна содержать один или несколько параметров, разделённых пробелами. Для получения дополнительной информации см. документацию по параметрам TSan и документацию по параметрам, общим для всех инструментов проверки. Заметим, что TSAN_OPTIONS позволяет подавить некоторые сообщения о гонках данных от TSan. Подавление сообщений о гонках данных полезно для намеренных гонок или библиотек, которые нельзя исправить.

Например, чтобы подавить сообщения, исходящие от функций в модуле OCaml My_module, можно запустить

TSAN_OPTIONS="suppressions=suppr.txt" ./my_instrumented_program

где suppr.txt — файл, содержащий:

race_top:^camlMy_module

(Обратите внимание, что это зависит от формата символов OCaml в исполняемом файле. Некоторые сборщики, такие как Dune, могут давать различные форматы. Вы должны адаптировать этот пример к фактически присутствующим в ваших стеках вызовов символам.)

Переменная TSAN_OPTIONS также позволяет увеличивать размер «истории», например:

TSAN_OPTIONS="history_size=7" ./my_instrumented_program

История TSan записывает такие события, как вход и выход из функции, и используется для восстановления стеков вызовов. Иногда для получения второго стека вызовов может потребоваться увеличить размер истории, но это также увеличивает потребление памяти. Эта настройка не изменяет число обращений к памяти, запоминаемых на каждый элемент памяти.

5 Руководство по линковке

Как общее правило, программы OCaml, оснащённые TSan, должны быть связаны только с объектами OCaml или C, также оснащёнными TSan. В противном случае может произойти сбой. Единственное исключение составляют библиотеки C, которые никоим образом не обращаются к системе выполнения OCaml, то есть не выделяют память, не генерируют исключения, не обращаются обратно к коду OCaml и т. д. К таким библиотекам относятся, например, libc или системные библиотеки. Гонки данных в неинструментированных библиотеках не будут отслеживаться.

Код C, взаимодействующий с OCaml, всегда должен быть построен с помощью команды ocamlopt, которая передаст необходимые флаги инструментации компилятору C. Квалификатор CAMLno_tsan может использоваться для предотвращения инструментации функций:

CAMLno_tsan void f(int arg)
{
  /* This function will not be instrumented. */
  ...
}

Гонки из неинструментированных функций не будут отслеживаться. CAMLno_tsan следует использовать только специалистам. Он может использоваться для снижения накладных расходов на производительность в определённых особых случаях или для подавления некоторых известных сигналов тревоги. В последнем случае предпочтительнее использовать файл подавления с TSAN_OPTIONS, так как это позволяет более тонко управлять, и квалификация функции f с помощью CAMLno_tsan приводит к пропуску записей в стеках вызовов TSan при возникновении гонки данных в транзитивном вызывающем объекте f.

Отключить инструментацию в коде OCaml нельзя.

6 Изменения в доставке сигналов

TSan перехватывает все сигналы и передает их инструментированной программе. Это наложение от TSan не всегда прозрачно для программы. Синхронные сигналы, такие как SIGSEV, SIGILL, SIGBUS и т. д., будут переданы немедленно, тогда как асинхронные сигналы, такие как SIGINT, будут задерживаться до следующего вызова среды выполнения TSan (например, до следующего доступа к изменяемым данным). Это ограничение TSan может иметь неожиданные последствия: например, чистые рекурсивные функции, которые не выделяют память, не могут быть прерваны до завершения.