Почти эволюционным путем программисты научились в основном избегать блокировок и разделяемой изменяемой памяти. Только когда дело доходит до драки, мы тянемся к этим примитивам. К сожалению, при написании расширения POPE Tree для Postgres мне понадобились некоторые блокировки. При создании прототипа я попал в ад блокировки. К счастью для меня, у нас есть мощные инструменты, которые могут помочь в таких ситуациях — это моя история использования Infer, чтобы избежать увольнения.
Описание дерева POPE (PDF) несколько академично; вам не нужно понимать это, чтобы читать дальше. Это дерево заполняется лениво. Каждый узел дерева буферизует данные при вставке. Только запросы вызывают создание дочерних узлов и объединение элементов буфера в узлы следующего уровня. Хотите разрешить высокопроизводительные запросы с параллельным чтением? Поздравляю, чтения вызывают мутацию дерева, и мой прототип использовал блокировки… плохо.
К счастью, эта криптографическая структура была лишь половиной моей дневной работы. В другую половину мы были заняты разработкой способа сделать статический анализатор Facebook Infer более доступным. Давайте посмотрим, что такое Infer и как его применение разыгрывается.
Вывод: что это такое, а что нет
Infer — это инструмент статического анализа. Если вы дадите Infer некоторый код Java или C/C++/Objective-C, он выдаст список потенциальных ошибок.
Какая замечательная фраза. Infer находит ошибки или, может быть, ошибки. На самом деле вы не можете просто дать ему код — вы должны сказать ему, как создавать код. Это связано с тем, что Infer не является линтером, он не просто просматривает ваш код в локальном контексте, но рассматривает, как функции взаимодействуют между единицами компиляции (файлами, пакетами).
Во время анализа Infer присваивает каждой функции своего рода сигнатуру типа. Сигнатуры описывают влияние ввода/вывода, которое функция оказывает на кучу и полученные ресурсы (распределение, блокировки, записи — все похоже, если присмотреться). Если вызывающий объект не предоставляет кучу подходящей формы, которая требуется вызываемому, что ж, это ошибка.
К делу: использование Infer на игрушках
Хватит стеба, устанавливайте infer и приступайте к делам. Сначала давайте загрузим infer в док-контейнер.
docker run --rm -it tommd/infer bash
Во-вторых, давайте сделаем игрушечный C-файл и расскажем, как его собрать.
cat <<EOF >toy.c #include <stdlib.h> int main() { int *ptr = malloc(sizeof(int)); *ptr = 1; return *ptr; } EOF
Ясно правильно. Теперь позволим сделать вывод. Система сборки не требуется, просто инструкция по сборке с указанием gcc.
infer run -- gcc toy.c Capturing in make/cc mode... Found 1 source file to analyze in /infer-out
Так просто. Вы сообщаете infer команды компиляции, а infer сообщает вам об обнаруженных ошибках. Что может быть лучше? Что ж, настоящий проект для стартов. Итак, давайте сделаем это!
К делу: использование Infer на реальных вещах
Для этого следующего шага я собираюсь откопать свое старое расширение psql, исходный код которого еще не открыт. Вы можете продолжить играть дома, используя проект C или Java по вашему выбору. Подумайте о zeromq или redis, если вы рисуете пустое место.
На данный момент у меня есть довольно типичное расширение Postgres. Здесь нет ничего удивительного, некоторые файлы включены, существует make-файл, и с установленным postgresql-server-dev-9.6 я могу собрать расширение. Просто… иногда запрос вызывает взаимоблокировку. Я также могу запустить infer для кода — он еще не находит взаимоблокировки, но находит ошибки.
infer run -- make
Почему не находит взаимоблокировки? Ну, английское название функцииReleaseBuffer
не помогает Infer понять, что это блокировка или выделение. Однако мы можем научить его новым функциям — дать ему модель того, что делает функция, в терминах, которые она понимает.
Для LockBuffer(), которая является функцией, предоставляемой psql, давайте научим выводить некоторый смысл, злоупотребляя распределением:
#if __INFER__ void LockBuffer(Buffer b, int lock) { void *val = *(void**)b; switch (lock) { case BUFFER_LOCK_EXCLUSIVE: if(NULL != val) { __infer_fail("Locking a locked buffer..."); } else { *((void**)b) = malloc(1); } break; case BUFFER_LOCK_UNLOCK: if(NULL == val) { __infer_fail("Unlocking an unlocked buffer..."); } else { free(val); *(void**)b = NULL; } break; case BUFFER_LOCK_SHARE: if(NULL != val) { __infer_fail("Read Locking a locked buffer..."); } else { *((void**)b) = malloc(2); } break; default: while(1); } } #endif /* __INFER__ */
Довольно просто, как только вы преодолеете новые имена функций. Это просто моделирование блокировки буфера как выделения и разблокировки как освобождения. Я сделал, но не показал, аналогичные спецификации для psql UnlockReleaseBuffer
, ReadBuffer
и ReleaseBuffer
. Как это меняет отчеты?
make clean && infer run -- make
Золотая жила! Это может показаться не таким уж большим, но этот метабуфер закреплен и его нужно разблокировать/освободить с отсутствующим вызовом unlockReleaseBuffer
. Знание того, какой ресурс был получен, является огромным шагом к пониманию того, где его высвободить.
Заключительные мысли
Infer работает довольно быстро и дает потрясающие результаты. Настройка не требуется, но может помочь в крайнем случае, как показано. Посмотрите вокруг, что мир произвел за последние несколько лет. Такие инструменты, как полное символьное выполнение (дорогой и немасштабируемый процесс), больше не являются частью индустрии. Посмотрите на инструменты, доступные сегодня, и ваши коллеги будут вам благодарны.