Невозможно что-либо доказать, не опираясь на гарантии, поэтому первое, что вы хотите сделать, это ознакомиться с моделью памяти вашей целевой платформы; У Java и x86 есть надежные и стандартизированные модели памяти - я не очень уверен насчет CLR, но если все остальное даст сбой, вы будете опираться на модель памяти вашей целевой архитектуры ЦП. Исключением из этого правила является то, что если вы намереваетесь использовать язык, который вообще не допускает общего изменяемого состояния - я слышал, что Эрланг такой.
Первая проблема параллелизма - это общее изменяемое состояние.
Это можно исправить с помощью:
- Создание состояния неизменным
- Нет общего состояния
- Защита общего изменяемого состояния с помощью одного и того же замка (два разных замка не могут охранять один и тот же элемент состояния, если только вы не всегда используете только эти два замка)
Вторая проблема параллелизма - безопасная публикация. Как вы делаете данные доступными для других потоков? Как вы выполняете передачу? Вы найдете решение этой проблемы в модели памяти и (надеюсь) в API. В Java, например, есть много способов публикации состояния, а пакет java.util.concurrent содержит инструменты, специально предназначенные для обработки межпотокового взаимодействия.
Третья (и более сложная) проблема параллелизма - блокировка. Неправильное упорядочение блокировок является источником тупиковых ситуаций. Опираясь на гарантии модели памяти, вы можете аналитически доказать, возможны ли мертвые блокировки в вашем коде. Однако вам необходимо спроектировать и написать свой код с учетом этого, в противном случае сложность кода может быстро сделать такой анализ невозможным для выполнения на практике.
Затем, как только вы докажете или правильно докажете правильное использование параллелизма, вам придется доказать однопотоковую корректность. Набор ошибок, которые могут возникнуть в параллельной базе кода, равен набору однопоточных программных ошибок плюс все возможные ошибки параллелизма.