Как я могу проверить алгоритмы без блокировок?

Question

Теоретически, должна быть возможна, по крайней мере, проверка алгоритма без блокировок методом "грубой силы" (существует не так много пересекающихся комбинаций вызовов функций).Существуют ли какие-либо инструменты или процессы формального обоснования, доступные для фактического доказательства правильности алгоритма без блокировок (в идеале он также должен иметь возможность проверять условия гонки и проблему ABA)?

Примечание:Если вы знаете способ просто доказать одну точку зрения (напримертолько докажите, что это безопасно от проблемы ABA) или проблемы, о которой я не упоминал, тогда все равно опубликуйте решение.В худшем случае каждый метод может быть применен по очереди, чтобы полностью проверить его.

Answer 1

Вам обязательно следует попробовать Проверка модели вращения.

Вы пишете программную модель на простом C-подобном языке под названием Promela, который Spin внутренне преобразует в конечный автомат.Модель может содержать несколько параллельных процессов.

То, что затем делает Spin, это проверяет всевозможное чередование инструкций из каждого процесса для какие бы условия вы ни хотели протестировать -- как правило, отсутствие условий гонки, свобода от взаимоблокировок и т.д.Большинство из этих тестов могут быть легко написаны с помощью assert() заявления.Если существует какая-либо возможная последовательность выполнения, которая нарушает утверждение, эта последовательность распечатывается, в противном случае вам выдается сообщение "все чисто".

(Ну, на самом деле для достижения этой цели используется гораздо более сложный и быстрый алгоритм, но таков эффект.По умолчанию проверяются все доступные состояния программы.)

Это является невероятно программа, она выиграла в 2001 Премия ACM за системное программное обеспечение (среди других победителей - Unix, Postscript, Apache, TeX).Я начал использовать его очень быстро, и через пару дней смог реализовать модели функций MPI MPI_Isend() и MPI_Irecv() в Промеле.Спин нашел пару хитрый условия гонки в одном сегменте параллельного кода я преобразовал в Promela для тестирования.

Answer 2

Вращение действительно отличное, но также учитывайте Детектор расы Реляций автор: Дмитрий В'Юков.Он специально создан для проверки параллельных алгоритмов, включая неблокирующие алгоритмы (без ожидания / блокировки).Это открытый исходный код и свободно лицензированный.

Relacy предоставляет примитивы синхронизации POSIX и Windows (мьютексы, переменные условия, семафоры, CriticalSections, события win32, Interlocked * и т.д.), Поэтому ваша фактическая реализация на C ++ может быть передана Relacy для проверки.Нет необходимости разрабатывать отдельную модель вашего алгоритма, как в случае с Promela и Spin.

Относительность обеспечивает C ++ 0x std::atomic (явное упорядочение памяти для победы!), так что вы можете использовать препроцессор #defines чтобы выбрать между реализацией Relacy и вашей собственной атомной реализацией, специфичной для конкретной платформы (tbb::атомный, наддув::атомный, и т.д.).

Планирование поддается контролю:доступен случайный, привязанный к контексту и полный поиск (все возможные чередования).

Вот пример программы Relacy.Несколько вещей, на которые следует обратить внимание:

• В $ это макрос Relacy, который записывает информацию о выполнении.
• rl::var<T> помечает "нормальные" (неатомные) переменные, которые также необходимо учитывать как часть проверки.

Код:

#include <relacy/relacy_std.hpp>

// template parameter '2' is number of threads
struct race_test : rl::test_suite<race_test, 2>
{
    std::atomic<int> a;
    rl::var<int> x;

    // executed in single thread before main thread function
    void before()
    {
        a($) = 0;
        x($) = 0;
    }

    // main thread function
    void thread(unsigned thread_index)
    {
        if (0 == thread_index)
        {
            x($) = 1;
            a($).store(1, rl::memory_order_relaxed);
        }
        else
        {
            if (1 == a($).load(rl::memory_order_relaxed))
                x($) = 2;
        }
    }

    // executed in single thread after main thread function
    void after()
    {
    }

    // executed in single thread after every 'visible' action in main threads
    // disallowed to modify any state
    void invariant()
    {
    }
};

int main()
{
    rl::simulate<race_test>();
}

Скомпилируйте с помощью вашего обычного компилятора (связь доступна только для заголовка) и запустите исполняемый файл:

struct race_test
DATA RACE
iteration: 8

execution history:
[0] 0:  atomic store, value=0, (prev value=0), order=seq_cst, in race_test::before, test.cpp(14)
[1] 0:  store, value=0, in race_test::before, test.cpp(15)
[2] 0:  store, value=1, in race_test::thread, test.cpp(23)
[3] 0:  atomic store, value=1, (prev value=0), order=relaxed, in race_test::thread, test.cpp(24)
[4] 1:  atomic load, value=1, order=relaxed, in race_test::thread, test.cpp(28)
[5] 1:  store, value=0, in race_test::thread, test.cpp(29)
[6] 1: data race detected, in race_test::thread, test.cpp(29)

thread 0:
[0] 0:  atomic store, value=0, (prev value=0), order=seq_cst, in race_test::before, test.cpp(14)
[1] 0:  store, value=0, in race_test::before, test.cpp(15)
[2] 0:  store, value=1, in race_test::thread, test.cpp(23)
[3] 0:  atomic store, value=1, (prev value=0), order=relaxed, in race_test::thread, test.cpp(24)

thread 1:
[4] 1:  atomic load, value=1, order=relaxed, in race_test::thread, test.cpp(28)
[5] 1:  store, value=0, in race_test::thread, test.cpp(29)
[6] 1: data race detected, in race_test::thread, test.cpp(29)

Последние версии Relacy также предоставляют модели памяти Java и CLI, если вы увлекаетесь подобными вещами.

Answer 3

Обнаружение гонки данных - NP сложная задача [Netzer& Miller 1990]

Я слышал об инструментах Lockset и DJit + (они научите этому в курсе CDP).Попробуйте прочитать слайды и погуглить, на что они ссылаются.В нем содержится некоторая интересная информация.

Answer 4

Я не знаю, какую платформу или язык вы используете, но на платформе .Net есть исследовательский проект Microsoft под названием Шахматы что выглядит очень многообещающе, помогая тем из нас, кто создает многопоточные компоненты, в том числе без блокировки.

Имейте в виду, я не использовал его в большом количестве.

Это работает (грубое объяснение), явно чередуя потоки максимально сжатыми способами, чтобы фактически выпустить ваши ошибки на волю.Он также анализирует код, чтобы найти распространенные ошибки и некорректные шаблоны - аналогично анализу кода.

В прошлом я также создавал специальные версии рассматриваемого кода (через блоки #if и т.д.), Которые добавляют дополнительную информацию для отслеживания состояния;подсчеты, версии и т.д., с которыми я затем могу ознакомиться в рамках модульного теста.

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

Answer 5

Если вы хотите действительно проверить код без блокировки (в отличие от исчерпывающего тестирования небольшого экземпляра), вы можете использовать VCC (http://vcc.codeplex.com), дедуктивный верификатор для параллельного кода C, который использовался для проверки некоторых интересных алгоритмов без блокировок (напримерсписки без блокировки и изменяемые по размеру хэш-таблицы с использованием указателей опасности, оптимистичная многоверсионная обработка транзакций, виртуализация MMU, различные примитивы синхронизации и т.д.).Он выполняет модульную проверку и использовался для проверки нетривиальных фрагментов промышленного кода (примерно до 20 KLOC).

Однако обратите внимание, что VCC - это верификатор, а не инструмент поиска ошибок;вам придется сделать существенные примечания к своему коду, чтобы заставить его верифицироваться, и кривая обучения может быть немного крутой.Обратите также внимание, что он предполагает последовательную согласованность (как и большинство инструментов).

Кстати, экспертная оценка не является хорошим способом проверки параллельного алгоритма (или даже последовательного).Существует долгая история известных людей, публикующих параллельные алгоритмы в важных журналах, только для того, чтобы спустя годы обнаруживались ошибки.