С ю з е в
МАТЕМАТИЧЕСКАЯ МОДЕЛЬ
МНОГОПОТОЧНОЙ ПРОГРАММЫ И ПРАВИЛА
БЕЗОПАСНОГО МНОГОПОТОЧНОГО
ПРОГРАММИРОВАНИЯ
Одной из основных проблем разработки многопоточного программного обеспечения являются взаимные блокировки потоков. <...> Взаимные блокировки потоков чрезвычайно трудно выявить, поскольку их
возникновение напрямую связано с относительной динамикой выполнения потоков в программном обеспечении, которая зависит от
множества трудно учитываемых факторов. <...> Представлена система правил разработки многопоточной структуры программного
обеспечения, направленная на уменьшение числа вносимых на этапе
разработки ситуаций взаимной блокировки. <...> Преимущество данной
системы перед эмпирически выведенными аналогами заключается
в том, что она выведена в процессе разработки математической
модели взаимных блокировок. <...> Одна из основных проблем разработки многопоточного программного обеспечения (ПО) — это обеспечение доступа различных потоков
к разделяемым ресурсам. <...> Для решения данной проблемы современные системы и средства программирования предоставляют средства
синхронизации, которые позволяют решать проблему доступа потоков к разделяемым ресурсам за счет временного перевода некоторых
потоков, обращающихся к ресурсам в состояние ожидания. <...> Однако
использование средств синхронизации привело к проблеме возникновения взаимных блокировок — ситуаций, когда потоки, переведенные
в состояние ожидания, ожидали события, которое никогда не произойдет. <...> Ошибки, связанные с взаимной блокировкой потоков, чрезвычайно трудно выявить, поскольку возникновение взаимных блокировок
напрямую связано с относительной динамикой выполнения потоков
в ПО, которая зависит от множества трудно учитываемых факторов,
часть которых может проявиться только в будущем, например: при переходе на новую платформу или добавлении новой подсистемы. <...> Верификация моделей по методу Model Checking основана на построении формальной <...>