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