lin-check

Page tree

Versions Compared

Key

  • This line was added.
  • This line was removed.
  • Formatting was changed.
Table of Content Zone

Table of Contents

Introduction

Существующие техники можно разбить на 3 категории гарантий покрытия:

...

Грубо говоря, все техники применяют отношение частичного порядка. То есть, в каждом алгоритме есть последовательность операций, которая должна произойти раньше другой. При этом, в разные потоки не имеют между собой никаких связей. Во всех случаях мы ищем паттерны вида "чтение и запись в одну переменную" в разных потоках и моделируем расписание таким образом, чтобы эти паттерны были в разных порядках. Если ничего плохого не произошло, то значит всё нормально.
Притом, 1 категория просто получает данные и алгоритм, который нужно к ним применить, находит баг - всё плохо, не находит, то считаем программу корректной. Очевидно, что данный подход не дает гарантии, что на других данных всё не сломается (вдруг есть к примеру, какой-либо if, который всё разрушит).
Методы 2 категории, же действуют иным образом. Они ищут все паттерны. И генерируют множество перестановок. Очевидно, что на каких-то данных расписание будет отличаться от запланированного, тогда даем этому расписанию другие данные чтобы всё было хорошо. При таком подходе, нужно учитывать, что при новых входных данных, нужно задать новое множество линеаризуемых результатов (например, так работает CHESS).

Представители 1 категории.

F. Chen, T. Serbanuta, and G. Roşu. JPredictor: A Predictive Runtime Analysis Tool for Java. In ICSE, pages 221–230,2008.

http://fsl.cs.illinois.edu/index.php/JPredictor


Выделяют 2 вида зависимостей

...

Атомарность проверяются попарно, сопоставляя с 11 паттернами.

 

 

A. Farzan, P. Madhusudan, N. Razavi, and F. Sorrentino. Predicting Null-Pointer Dereferences in Concurrent Programs. In FSE, pages 47:1–47:11, 2012.

На вход получает программу и входной вектор. Запускает и ищет пары событий (w,r) - null WR пара:

...

Запускаем найденное решение.

 

 

PENELOPE: Weaving Threads to Expose Atomicity Violations

Считаем, что нам известны результаты последовательного выполнения. На вход получаем какой-то алгоритм и входные данные. Начинаем работу. Работа разбита на 3 этапа:

  1. Мониторинг. Выполняем программу на входных данных, наблюдаем за ходом выполнения. Записываем операции чтения/записи в (потенциально) общие переменные, получение/снятие блокировок, создание потоков и барьеры.
  2. Предсказание. Конструируем иные запуски, чтобы они содержали как минимум один из подозрительных шаблонов. Подозрительными считаем такие шаблоны:
    1. RWR
    2. WRW
    3. RWW
    4. WWR
    5. WWW
  3. Изменение расписания. ВЫполняем программу на 1 процессоре, путем переплетения потоков на 1 процессоре. Если успешно выполняется - всё ок, если нет - рапортуем о баге. Если не можем составить расписание для запуска, то просто отбрасываем его.

 

Представители 2 категории.

Status
titleTBD