Просмотр исходного текста страницы ADD 2010: Отчет Алексеева Алексея/Евгений Кирпичев. Многопоточное программирование

;[[Многопоточное программирование (Евгений Кирпичёв на ADD-2010)]]

Был интересный доклад в формате лекции, что мне сильно понравилось.
# Гораздо лучше меня рассказал про '''структуру Крипке''', '''темпоральные логики'''. Рассказал про '''LTL'''-логику и пример нескольких утверждений. К сожалению, дал неправильные данные, о сложности верификации '''LTL'''-логики, мне даже пришлось поправить:). К сожалению, на определениях все и закончилось. Рассказал про '''Spin''' и '''Java PathFinder'''. Последняя утилита вроде находит по '''java'''-программе все '''dead-lock'''-и.
# Далее рассказывал, как небольшими изменениями в дизайне можно снизить сложность многопоточного ПО. Я и так, практически, всех шаблонов придерживался интуитивно. <br/> Что запомнилось:
#* Если надо организовать отправку писем — сделайте абстрактную многопоточную очередь, и используйте ее. Ровно так месяца три назад я и сделал.
#* Можно использовать догоняющую стратегию, сделав инфраструктуру для исполнения догоняющих заданий. Это наши Job-ы.
#* Были антипатерны, такие, что в жизни я их не встречал. Вообще, я согласен, что большая часть сложности многопоточных программ очень сильно снижается правильной организацией системы.
# Было что-то про векторизацию. Интересный факт — набор ассоциативных операций можно векторизовать, точнее не сам набор операций (с этим все понятно), а последовательный возрастающий фрагменты вычислений (лениво расписывать). Так самая быстрая сортировки — векторный radix-sort. Было очень интересно, но докладчик не стал углубляться, и опять остановился на уровне определений. Еще код в '''Хаскеле''' тоже местами векторизуется.
# Что-то про функциональное программирование. Там с параллелизмом все круто — ну мы и не сомневались особо. Рассказывал про '''STM''' (''Software transaction memory''). Это дается бесплатно в ФП, но в обычных языках практически невозможно.

Мне понравилось, что доклад был в стиле лекции. Но не хватало полноценных разборов алгоритмов, оценок, доказательств, ну хоть на пальцах.