Имея программу, состоящую из переменных и инструкций, которые модифицируют эти переменные, и примитива синхронизации (монитор, мьютекс, синхронизированный java или блокировка C #), можно ли доказать, что такая программа является поточно-ориентированной?
Есть ли даже формальная модель для описания таких вещей, как безопасность потоков или условия гонки?
Ответы:
Доказать, что программа является «поточно-ориентированной», сложно. Однако можно конкретно и формально определить термин «гонка данных». И можно определить, имеет ли трасса выполнения определенного запуска программы или нет гонку данных во времени, пропорциональную размеру трассы. Этот тип анализа восходит по крайней мере к 1988 году: Бартон П. Миллер, Чон-Деок Чой, «Механизм эффективной отладки параллельных программ», Conf. на прог. Lang. Dsgn. и импл. (PLDI-1988): 135-144 .
Стандарт C ++ 11 является хорошим примером. (Соответствующий раздел - 1.10 в черновиках спецификаций, которые доступны онлайн.) В C ++ 11 проводится различие между объектами синхронизации (мьютексами и переменными, объявленными с
atomic<>
типом) и всеми другими данными. Спецификация C ++ 11 говорит, что программист может рассуждать о доступе к данным на трассе многопоточной программы, как если бы она была последовательно последовательной, если доступ к данным свободен от гонки данных.Инструмент Helgrind (входит в Valgrind) выполняет такое обнаружение данных на основе данных, которое происходит раньше, как и некоторые коммерческие инструменты (например, Intel Inspector XE). Алгоритмы в современных инструментах основаны на сохранении векторных часов, связанных с каждым потоком, и синхронизации объект. Я думаю, что эта методика использования векторных часов для обнаружения гонки данных была впервые разработана Michiel Ronsse; Коэн Де Босшере: «RecPlay: полностью интегрированная практическая система записи / воспроизведения», ACM Trans. Вычи. Сист. 17 (2): 133-152, 1999 .
источник
С практической точки зрения, существует система проверки VCC, которая может быть использована для формального доказательства безопасности потоков программ на Си.
Это цитата с веб-сайта:
источник
Это очень сложная область для обеспечения корректности программы, поскольку исключаются условия гонки, своего рода «ахиллесова пята» параллельной обработки. Наилучший подход к корректности программы обычно состоит в том, чтобы избегать низкоуровневых примитивов и работать с высокоуровневыми шаблонами проектирования (например, из библиотек), которые обеспечивают синхронизацию потоков. Существует одна модель CSP, сообщающая о последовательных процессах Hoare, у которой есть некоторые доказательства правильности, учитывая, что разработчики ограничивают себя "структурой". Он имеет некоторое концептуальное сходство и хронологическое происхождение / совпадение с «трубами и фильтрами» в Unix, хотя (пока?) Не нашел прямой связи между ними.
Две другие платформы, которые пытаются улучшить правильность распараллеливания с помощью шаблонов проектирования и которые используют для этого большинство стандартных / известных алгоритмов / шаблонов проектирования:
источник