Многопоточные алгоритмы особенно сложно спроектировать/отладить/доказать. Алгоритм Деккера является ярким примером того, насколько сложно разработать корректный синхронизированный алгоритм. Tanenbaum Современные операционные системы заполнены примерами в разделе IPC. Кто-нибудь имеет хорошую ссылку (книги, статьи) для этого? Спасибо!
Доказательство корректности многопоточных алгоритмов
Ответ 1
Невозможно ничего доказать, не опираясь на гарантов, поэтому первое, что вы хотите сделать, это познакомиться с моделью памяти вашей целевой платформы; Java и x86 имеют солидные и стандартизованные модели памяти. Я не уверен в CLR, но если все остальное не удается, вы будете основываться на модели памяти вашей целевой архитектуры процессора. Исключение из этого правила - если вы намереваетесь использовать язык, который вообще не разрешает какое-либо общее изменяемое состояние, - я слышал, что Erlang такой.
Первая проблема concurrency является общим изменчивым состоянием.
Это можно исправить следующим образом:
- Сделать состояние неизменным
- Не делить состояние
- Защита общего измененного состояния одной и той же блокировкой (две разные блокировки не могут защитить одно и то же состояние, если только вы не используете именно эти два замка)
Вторая проблема concurrency - безопасная публикация. Как вы делаете данные доступными для других потоков? Как вы выполняете передачу? Вы будете решать эту проблему в модели памяти и (надеюсь) в API. Например, у Java есть много способов опубликовать состояние, а пакет java.util.concurrent содержит инструменты, специально предназначенные для обработки межпоточных связей.
Третья (и более сложная) проблема concurrency - это блокировка. Ошибочное блокирование-блокировка является источником блокировок. Вы можете аналитически доказать, основываясь на принципах памяти модели, независимо от того, возможны ли блокировки в вашем коде. Однако вам нужно разработать и написать свой код с учетом этого, иначе сложность кода может быстро сделать такой анализ невозможным на практике.
Затем, как только вы это сделаете, или до того, как вы это сделаете, докажите правильное использование concurrency, вам нужно будет доказать однопоточную правильность. Набор ошибок, которые могут возникать в базе кодового кода, равен набору однопоточных ошибок программы, плюс все возможные ошибки concurrency.
Ответ 2
Pi-Calculus, Теория мобильных процессов - это хорошее место для начала.
Ответ 3
"Принципы параллельного и распределенного программирования", М. Бен-Ари
ISBN-13: 978-0-321-31283-9
У них есть в сафари книгах онлайн для чтения:
http://my.safaribooksonline.com/9780321312839
Ответ 4
Короткий ответ: трудно.
В конце 1980-х годов в DEC SRC Modula-3 и лиственнице была действительно хорошая работа.
например.
-
Синхронизация потоков: формальная спецификация (1991) A D Birrell, J V Guttag, J J Horning, R Levin Системное программирование с Modula-3, глава 5
-
Расширенная статическая проверка (1998) Дэвид Л. Детлефс, Дэвид Л. Детлефс, К. Рустан, К. Рустан, М. Лейно, М. Лейно, Грег Нельсон, Грег Нельсон, Джеймс Б. Сакс, Джеймс Б. Сакс
Некоторые из хороших идей Modula-3 превращают его в мир Java, например. JML, хотя "JML в настоящее время ограничен последовательной спецификацией", говорится в intro.
Ответ 5
У меня нет конкретных ссылок, но вы можете захотеть взглянуть на теорию Овицки-Гриса (если вам нравится доказательство теоремы) или теория процессов/алгебра (для которых имеются также различные инструменты проверки модели).
Ответ 6
@Просто в случае: я есть. Но из того, что я узнал, сделать это для нетривиального алгоритма является серьезной болью. Я оставляю такую вещь для более умных людей. Я узнал, что я знаю из Parallel Program Design: The Foundation (1988) by K M Chandy, J Misra