Как я могу эффективно представлять или моделировать последовательность блокировки?

Question

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

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

I.e. Я хотел бы объяснить проблему и решение, которое я кодирую с помощью какой-либо диаграммы, которая позволяет мне отображать последовательность блокировки, последствия параллелизма (например, если мы выпустим эту блокировку до этого, у нас будет эта проблема и т. Д.) И другие подобные Полезная информация.

Что было бы хорошим способом представить модели блокировки?

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

Есть ли другие визуальные инструменты, которые позволили бы мне представить эту проблему?

Как инженеры решают эту проблему для действительно сложных проблем, таких как распределенные системы и т. Д.?

Есть ли какая-нибудь диаграмма для этого или это больше похоже на набор диаграмм, которые используются для описания этого?

Answer 1

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

E.g. пожалуйста, взгляните на Spin, который предназначен для проверки каждой комбинации одновременно выполняемых потоков. Одним из примеров такой модели для спина является следующее:

// a small example spin model 
// Peterson's solution to the mutual exclusion problem (1981) 

bool turn, flag[2];  // the shared variables, booleans 
byte ncrit;    // nr of procs in critical section 

active [2] proctype user() // two processes 
{ 
    assert(_pid == 0 || _pid == 1); 
again: 
    flag[_pid] = 1; 
    turn = _pid; 
    (flag[1 - _pid] == 0 || turn == 1 - _pid); 

    ncrit++; 
    assert(ncrit == 1); // critical section 
    ncrit--; 

    flag[_pid] = 0; 
    goto again 
} 
// analysis: 
// $ spin -a peterson.pml 
// $ cc -o pan pan.c 
// $ ./pan 

Здесь описывают способ, как потоки связи и определить условия ожидаемого состояния программы. Если какая-либо из возможных комбинаций выполнения приводит к ошибке утверждения, она будет сообщаться вместе с управляющим потоком, который ведет к нему.

Answer 2

Я должен был начать с нескольких диаграмм последовательности UML (по одному для каждого случая конфликта) с умным использованием маркеров (цвет, аннотация, фрагмент, OCL).

Системы реального времени, которые были разработаны с большим количеством временных диаграмм. Но я не привык.

В большинстве случаев у меня есть хорошая карта ума моего кода, и я спрашиваю себя о каждой инструкции, что произойдет, если в это время работает какой-либо поток, что такое запрещенные состояния. Это очень похоже на Design by contract (контракты, которые могут быть показаны на диаграмме последовательности через «маркеры».

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

Answer 3

Описание этой запирающей микроархитектуры может потребовать два или три вида на механизм. Может быть, диаграмма состояний (Вот пример, изящно иллюстрирующий состояния и жизненный цикл Java 6) Thread States.

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

Наконец, диаграмма Swimlane в UML может хорошо отображать параллельные действия различных агентов - запросы на чтение и запись, монитор и т. Д.

Одна из лучших книг, которые я нашел на архитектуре программного обеспечения, - "Documenting Software Architectures, Views and Beyond". Вы найдете, что это стоит вашего времени (ИМХО).

Приветствия! Замечательная проблема!

Answer 4

Petri nets Исторически используются для моделирования параллелизма (и параллельных распределенных систем). Будучи формальной математической концепцией, они позволяют вам рассуждать о последовательностях операций, достижимости состояния (может быть удобно, например, для доказательства неприемлемой конфигурации блокировок и/или состояний ресурсов никогда не возникает), живучести, ограниченности, взаимоблокировки и другой такой полезной информации. Кроме того, они имеют приятное и чистое визуальное представление. Но, используя сети Петри, нужно работать с понятиями низкого уровня, такими как места и переходы, и нет никаких средств для абстрактного моделирования. Вследствие этого их визуальное изображение обычно становится огромным даже для проблем среднего размера. Цветные, приоритетные, приуроченные и другие дополненные сети Петри иногда приходят на помощь, но для более сложных абстрактных систем UML statecharts подходят лучше.

Вот некоторые иллюстрации, касающиеся анализ последовательности блокировки с использованием сетей Петри (см публикации для более подробной информации):

1. Петри моделирование двухфазной стратегии запирающей от "Petri net Based Model for Concurrent Control of Database System" by HOD Jie, LI Fengying and WANG Huijiao
2. сети Петри модели для разделяя стратегию для образца пластины из потока "Scheduling Single-Armed Cluster Tools With Reentrant Wafer Flows" by Hwan-Yong Lee and Tae-Eog Lee (этот анализ содержит более детальное взаимоблокировки)