Как обосновать правильность состава мьютекса?

Question

Я пытаюсь реализовать семафор с мьютексом, чтобы узнать больше о параллельных примитивах и шаблонах и о том, как писать правильные параллельные программы.

Вот ресурс, который я нашел: http://webhome.csc.uvic.ca/~mcheng/460/notes/gensem.pdf

Решение № 1 помечено как «неправильное» на странице 9. Я реализовал алгоритм здесь . Запуск этой программы несколько раз может привести к зависанию потоков. Я провел некоторый анализ и понял, что может произойти следующая последовательность операций с мьютексом d:

            // d was initialized as locked
d.unlock(); // d is unlocked
d.unlock(); // d is still unlocked (unaffected)
d.lock();   // d is locked
d.lock();   // d is still locked (deadlock)

Это приведет к тупику последнего d.lock().

Решение № 2 решило эту проблему, обеспечив переход от сигнального потока к активному потоку путем повторного использования мьютекса m. Я реализовал эту версию здесь .

В этом решении после d.unlock(), m остается заблокированным, что означает последующее Операции post() будут заблокированы до разблокирования m. Тогда d.lock() вызывается после m.unlock(), убедившись, что d находится в заблокированном состоянии перед разрешить выполнение последующих post() операций.

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

Я хочу задать этот вопрос из-за следующих 2 решений из записки. Я реализовал решение # 3 и решение # 4 , но у обоих были замороженные потоки при тестировании несколько раз. Я не уверен, что это проблема моей реализации или само решение неверно.

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

Answer 1

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

Если вы работаете с C или C ++, вы можете проверить ThreadSanitizer, который доступен в GCC и Clang и поможет вам обнаружить взаимоблокировки и другие ошибки, связанные с параллелизмом, во время выполнения.

Более исчерпывающий подход - это систематическое параллельное тестирование, которое перечислит возможные чередования и выполнит их. Существуют различные методы, такие как проверка модели без сохранения состояния и состояния, которую вы должны проверить.

Spin - это инструмент проверки модели, который можно использовать для формальной проверки. Вы пишете свои модели на Promela и используете LTL для утверждений.

Наконец, вот список из Википедии для различных языков.

Answer 2

Документация по lockdep (пример: https://lwn.net/Articles/705379/) - один из многих источников, описывающих общий критерий, который вы ищете: вам нужна реализация без циклов в графе зависимостей.

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

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

А для дополнительного вопроса: существуют ли реализации, в которых порядок блокировок и выпусков не является зеркальным отображением, но где еще нет циклов?