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

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

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

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

Для обнаружения гонок данных OCaml поддерживает ThreadSanitizer (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, а также для архитектур POWER, riscv и s390x в Linux.

Для сборки 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. Согласно модели памяти (см. главу 10), a и b — «неатомарные» ячейки, и синхронизации между обращениями к ним нет. Следовательно, здесь возникают две гонки данных — по одной для каждой из ячеек памяти 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 не выдает ложноположительных результатов, то есть не создает ошибочных сообщений.

При смешивании кода OCaml и C с помощью примитивов C понятие ложноположительного результата становится менее однозначным, поскольку задействованы две модели памяти — OCaml и C11. Тем не менее TSan должен вести себя в целом ожидаемым образом: неатомарные чтения и записи в C будут конфликтовать с неатомарными чтениями и записями в OCaml, а атомарные операции в C не будут конфликтовать с атомарными операциями в OCaml. Теоретически возможен один случай ложноположительного результата: если значение value инициализируется из C без использования caml_initialize (это разрешено при условии, что сборщик мусора не запускается между выделением памяти и записью, см. главу 23), а позднее другой поток выполняет конфликтующее обращение. Это не является гонкой данных, но 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 записывает такие события, как вход в функцию и выход из нее, и используется для восстановления трассировок стека. Иногда для получения второй трассировки стека необходимо увеличить размер истории, однако это также повышает потребление памяти. Эта настройка не меняет число обращений к памяти, запоминаемых для каждой ячейки.

Еще один полезный параметр среды выполнения — exitcode=0: он по-прежнему сообщает о гонках данных, но не меняет код завершения. Это может быть полезно, если 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 будут отсутствовать соответствующие записи.

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

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

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

« Преобразование программы «Tail Modulo Constructor»Основная библиотека »
Авторское право © 2026 Institut National de Recherche en Informatique et en Automatique

© 1995-2026 INRIA.
https://ocaml.org/manual/5.5/tsan.html

Spec-Zone.ru

Настройки Оффлайн Что нового Помощь О нас
Spec-Zone .ru
спецификации, руководства, описания, API