> -- Rifat писал(а):
> Опасности начинаются, если есть какие-то общие поля...
Вот пример PRET-C -- расширение С для реализации (в т.ч. и в "железе") конкурентных процессов в стиле Esterel (упрощённо) целенаправленно (и контролируемо) над разделяемыми данными (с картинками для лучшего понимания):
https://hal.inria.fr/hal-00786378/document
> -- Rifat писал(а):
> Я думаю, что будущее за тем методом параллельного программирования, который легко верифицировать.
Методы параллельности зависят от задачи. Те же аля "акторы без общей памяти" нужны к месту. Вот тут их критика вполне заслужена (в смысле не модели взаимодействия, а методики использования):
http://rsdn.org/forum/philosophy/6156290.flat#6156290

Или вот "научное исследование":
https://www.ideals.illinois.edu/bitstre ... ission.pdf

Аналогично и верификация необходима для разных задач. Для базовых свойств безопасности и "живости" для тех же конкурентных процессов можно взглянуть, к примеру, на TLA+ (там даже взаимодействие моделируется именно через изменение переменных, а не в стиле операций для сообщений вида send/recv):
https://en.wikipedia.org/wiki/TLA%2B

А если взглянуть на материалы проекта F-Star (диалект ML под крышей Microsoft), то даже возникает откровенное удивление, какие свойства безопасности можно контролировать на "зависимых типах":
https://www.fstar-lang.org/

И необходимо решать совсем другие задачи для правильной расстановки yield (в PRET-C -- EOT) с учётом времени, чтоб, к примеру, за оборудованием поспевать, или не допустить того, что "было на Марсе":
http://www.cs.cmu.edu/afs/cs/user/raj/www/mars.html