Eugene Kirpichov ([info]antilamer) wrote,
@ 2009-05-27 13:31:00
Previous Entry  Add to memories!  Tell a Friend  Next Entry
Презентация про многопоточное программирование и Java
Большая (135 слайдов) презентация про многопоточное программирование вообще и Java в частности, рассказанная мною давеча коллегам.
Отличается широтой, но не глубиной изложения - всего понемножку: немного про LTL и тулы для верификации, немного про векторные алгоритмы, немного про ОО-паттерны, способствующие хорошим многопоточным программам, и т.п. Цель - заинтересовать читателя соответствующими концепциями, дабы он сам продолжил их изучение по приведенным ссылкам.

Вот и она, а вот и TeX-сорцы.

(18 comments) - (Post a new comment)


[info]from_somewhere
2009-05-27 08:10 pm UTC (link)
А ты где-нибудь вне работы будешь эту презентацию рассказывать?

(Reply to this) (Thread)

[info]antilamer
2009-05-28 06:56 am UTC (link)
Принимаю предложения :)

(Reply to this) (Parent)

[info]smalgin
2009-05-27 08:27 pm UTC (link)
Литературу про структуры Крипке и LTL посоветуете?

(Reply to this) (Thread)

[info]smalgin
2009-05-27 08:31 pm UTC (link)
А, беру вопрос назад - вы ссылки в подпараграфах даете, а я сразу в конец полез... :)

(Reply to this) (Parent)

[info]raindog_2
2009-05-27 10:11 pm UTC (link)
У меня несколько вопросов о "корректности программ", которые всегда интересовали, но никак не мог собраться об этом почитать. Может быть, вы подскажете:

1) Что понимается под "корректной" программой?

2) Если под этим понимается соответствие некоторой спецификации, то для любого реального приложения (и правильно выбранного высокоуровневого языка) спецификация, во-первых, будет по объему стремиться к объему программы. Во-вторых, спецификация будет так же подвержена багам, как и сама программа. Нет ли тут проблемы?

3) Как насчет performance и scalability? Входит ли это в сферу доказательств корректности?

(Reply to this) (Thread)

[info]nivanych
2009-05-28 06:23 am UTC (link)
> будет по объему стремиться к объему программы.

Что-то "промышленное" я на "таких" языках не программировал,
но есть основания предполагать, что объём спецификации будет
заметно меньше, чем объём программы, по крайней мере,
для таких языков, как Agda/Coq.

> Во-вторых, спецификация будет так же подвержена багам, как и сама программа.

Можно делать спецификации на спецификации ;-)

> 3) Как насчет performance и scalability?
> Входит ли это в сферу доказательств корректности?

Да, этого тоже можно проверять.
Но для начала бы разобраться
с более общими свойствами :-)

(Reply to this) (Parent)

[info]antilamer
2009-05-28 07:07 am UTC (link)
По объему вряд ли будет стремиться. Даже десяток тысяч LTL-формул (по слухам, более чем реалистичная цифра для промышленных масштабов верификации) это не так уж много кода.

Багам - конечно, будет подвержена; заодно можно будет, наблюдая за автоматически найденными трассами, нарушающими заявленные требования, уточнять спецификацию. Но по-моему баг в спецификации, во всяком случае заданной в виде LTL, сделать труднее - формулы все-таки очень маленькие и модульные, независимые.

Кстати, помимо LTL есть еще CTL и CTL*. Правда, у CTL* гораздо менее эффективные алгоритмы верификации, но по крайней мере чисто для задания требований она гораздо более выразительна.

P.S. Вообще-то я сам с верификацией знаком лишь по универскому курсу, но курс был очень хорошим, так что я счел необходимым поделиться знанием с общественностью в надежде, что в общественности найдутся гуру, которые просветят и меня заодно :)

(Reply to this) (Parent)(Thread)

[info]raindog_2
2009-05-29 02:57 am UTC (link)
Но все-таки, чтобы определиться с базовыми понятиями, что значит "корректная" программа?

...Я попытался описать, что меня смущает в этом понятии и ушел в сторону.
Это, в-общем, почти не связано с темой вашего постинга, потэтому я перенес к себе в журнал: http://raindog-2.livejournal.com/3953.html
Спасибо за интересную темы и пищу к размвшлениям.

(Reply to this) (Parent)

[info]_gi
2009-05-29 08:31 am UTC (link)
в МГУ читается теоретический (и лишь отчасти практический) курс по верификации программ на моделях. Скачать его можно отсюда:
http://savenkov.lvk.cs.msu.su/mc.html

теормин и всякие определения, набранные студентами при подготовке к экзмену, доступны здесь:
http://esyr.org/wiki/ВПнМ/Теормин

возможно, что-то из этого будет Вам интересно

(Reply to this) (Parent)(Thread)

[info]antilamer
2009-05-29 09:24 am UTC (link)
Ух ты ё-мое, спасибо большое! Наш препод свой курс зачем-то убрал из инета; а этот курс, похоже, покруче будет.

(Reply to this) (Parent)

[info]raindog_2
2009-05-30 12:06 am UTC (link)
Спасибо!

(Reply to this) (Parent)

[info]blackyblack
2009-05-28 11:28 am UTC (link)
Erlang то будет?

(Reply to this) (Thread)

[info]antilamer
2009-05-28 11:32 am UTC (link)
Где?

(Reply to this) (Parent)(Thread)

[info]blackyblack
2009-05-28 12:05 pm UTC (link)
В лекции. Это же очевидный вопрос. Все эти темы уже поднимались авторами Эрланга. Поэтому я лично ожидал сравнения Явы и Эрланга.

(Reply to this) (Parent)(Thread)

[info]antilamer
2009-05-28 12:24 pm UTC (link)
Да, про стиль программирования с message passing concurrency я не успел ничего написать. Я вообще еле успел эту презентацию доделать; закончил за час до доклада :) Если буду еще где-нибудь рассказывать, то надо будет добавить про message passing побольше.

(Reply to this) (Parent)(Thread)

[info]netch
2009-06-08 08:49 am UTC (link)
В общем-то можно добавить один (или два?) важный пункт(а) в слайд про Message-passing concurrency: даже если дедлоки не деваются, то значительно проще делаются такие вещи, как

- ограниченное во времени ожидание результата (конечно, учитывая, что операция может и состояться)
- возможность спросить специальными вызовами подробности состояния актора или сдвинуть его с мёртвой точки

и особенно второе крайне помогает в отладке.

Ещё там в районе 44-го слайда 5 одинаковых слайдов.

(Reply to this) (Parent)(Thread)

[info]antilamer
2009-06-08 04:54 pm UTC (link)
Ага, чистая правда.

5 одинаковых слайдов - там типа разные вещи подсвечены.

(Reply to this) (Parent)

[info]localstorm
2009-06-12 02:29 pm UTC (link)
http://localstorm.livejournal.com/147471.html

Не могли бы Вы прокомментировать? Заранее спасибо.

(Reply to this)

(18 comments) - (Post a new comment)

Create an Account
Forgot your login or password?
Login w/ OpenID
English • Español • Deutsch • Русский…