Многопотоковые алгоритмы особенно сложно спроектировать/отладить/доказать. Алгоритм Деккера является ярким примером того, насколько сложно разработать правильный синхронизированный алгоритм. Современные операционные системы Tanenbaum заполнены примерами в разделе IPC. Кто-нибудь имеет хорошую ссылку (книги, статьи) для этого? Благодаря!Доказательство корректности многопоточных алгоритмов
@ Просто в случае: я есть. Но из того, что я узнал, сделать это для нетривиального алгоритма является серьезной болью. Я оставляю такую вещь для более умных людей. Я узнал, что знаю из Parallel Program Design: A Foundation (1988) by KM Chandy, J Misra
Невозможно ничего доказать, не строя на гарантов, поэтому первое, что вы хотите сделать, это познакомиться с модель памяти вашей целевой платформы; Java и x86 имеют солидные и стандартизованные модели памяти. Я не уверен в CLR, но если все остальное не удается, вы будете основываться на модели памяти вашей целевой архитектуры процессора. Исключение из этого правила - если вы намереваетесь использовать язык, который вообще не разрешает какое-либо общее изменяемое состояние, - я слышал, что Erlang подобен этому.
Первой проблемой параллелизма является общее изменяемое состояние.
Это может быть исправлено:
Вторая проблема лемму параллелизма - безопасная публикация. Как вы делаете данные доступными для других потоков? Как вы выполняете передачу? Вы будете решать эту проблему в модели памяти и (надеюсь) в API. Например, у Java есть много способов опубликовать состояние, а пакет java.util.concurrent содержит инструменты, специально предназначенные для обработки межпоточных связей.
Третья (и более сложная) проблема параллелизма - это блокировка. Ошибочное блокирование-блокировка является источником блокировок. Вы можете аналитически доказать, основываясь на принципах памяти модели, независимо от того, возможны ли блокировки в вашем коде. Однако вам нужно разработать и написать свой код с учетом этого, иначе сложность кода может быстро сделать такой анализ невозможным на практике.
Затем, если у вас есть или до того, как вы это сделаете, докажите правильное использование параллелизма, вам нужно будет доказать однопоточную правильность. Набор ошибок, которые могут возникать в базе параллельного кода, равен набору однопоточных ошибок программы, а также все возможные ошибки параллелизма.
Короткий ответ: это сложно.
В конце 1980-х годов в модуле DEC SRC Modula-3 и лиственница была действительно хорошая работа.
например.
Thread synchronization: A formal specification (1991) А.Д. Birrell, СП Гуттаг, JJ Хорнинг, R Левин системного программирования с Modula-3, глава 5
Extended static checking (1998) Дэвид Л. Detlefs, Дэвид Л. Detlefs, К. Rustan, К. Rustan, М. Лейно, М. Лейно, Грег Нельсон, Грег Нельсон, Джеймс Б. Сакс, Джеймс Б. Сакс
Некоторые из хороших идей Modula - 3 превращают его в мир Java, например. JML, хотя «JML в настоящее время ограничен последовательной спецификацией», говорит intro.
Ссылка gatekeeper.dec.com не работает, но отчет DEC SRC по расширенной статической проверке доступен по адресу http://research.microsoft.com/en-us/um/people/leino/papers/src-159.pdf , Я согласен, что ESC была действительно хорошей работой. – 2012-05-26 18:21:01
У меня нет каких-либо конкретных ссылок, но вы можете захотеть взглянуть на теорию Овицки-Гриса (если вам нравится доказательство теоремы) или теория процессов/алгебра (для которых имеются также различные инструменты проверки модели) ,
The Pi-Calculus, A Theory of Mobile Processes - хорошее место для начала.
"Принципы Параллельное и распределенное программирование", М. Бен-Ари
ISBN-13: 978-0-321-31283-9
Они в на сафари книг в Интернете для чтения:
http://my.safaribooksonline.com/9780321312839
Это было в значительной степени именно то, что я искал. Благодаря! – Leandro 2008-09-20 19:23:26
Попробуйте разработать. – GEOCHET 2008-09-16 16:45:35