Почти эволюционным путем программисты научились в основном избегать блокировок и разделяемой изменяемой памяти. Только когда дело доходит до драки, мы тянемся к этим примитивам. К сожалению, при написании расширения 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 работает довольно быстро и дает потрясающие результаты. Настройка не требуется, но может помочь в крайнем случае, как показано. Посмотрите вокруг, что мир произвел за последние несколько лет. Такие инструменты, как полное символьное выполнение (дорогой и немасштабируемый процесс), больше не являются частью индустрии. Посмотрите на инструменты, доступные сегодня, и ваши коллеги будут вам благодарны.