Я видел инструмент, который может сообщить вам, если у вас есть проблемы с дизайном в вашем проекте, и мне интересно, есть ли инструмент, который может динамически сообщить вам, если есть какие-то проблемы с параллелизмом в вашем проекте.
Шахматы от MS Research отличные (http://research.microsoft.com/en-us/projects/chess/) Он обнаруживает ошибки параллелизма с помощью юнит-тестов и важно: они воспроизводимы шахматами.
Я думаю, вы обнаружите, что обнаружение такого типа вещей с помощью статического анализа кода в основном является скрытой проблемой остановки и, следовательно, неразрешимо в общем случае. Такой инструмент почти наверняка не существует.
Самым близким к существующему инструменту проверки является моделирование вычислений как 'Передача последовательных процессов', , которое может быть подвергнуто формальным математическим рассуждениям. Тем не менее, это не позволяет вам создать инструмент, который может взять произвольную программу на произвольном языке и вычислить для нее доказательство.