> -- Rifat писал(а):
> Вчера смотрел ваше выступление. Там Вы говорили про то, что по умолчанию при параллельном программировании даже оператор присваивания не будет гранулярным, а может быть прерван где-то по середине. И как я понял, Вы вставляете специальный код, чтобы прерывания могли быть, только в этих местах, то есть между операторами, а не внутри них.Я недавно читал книги "Verification of sequential and concurrent programs" (Apt K.R., de Boer F.S., Olderog E.-R. (eds.)) там говорится о том, что если, допустим, у нас есть две процедуры, где, допустим, операторы гранулярны, то для того, чтобы верифицировать всю эту параллельную программу необходимо рассмотреть взаимодействия каждого оператора одной процедуры с каждым оператором другой процедуры. Я так думаю, что на практике это осуществить практически невозможно
Если анализировать реальный программный код на каком-то универсальном алгоязыке, то неизбежно придётся рассматривать все операторы и выявлять взаимодействие. Тяжело, но возможно, и, скорее всего, ограниченно. Пример для Java (в принципе, в публикации в целом проблематика):
http://www.math.spbu.ru/user/dkoznov/pa ... ifanov.pdf

Однако в любом случае в модели вычислений для верификации, будь она синтезирована или составлена с нуля вручную, обычно абстрагируются от прочих операций, не связанных непосредственно со взаимодействием. Т.е. пусть хоть в исходниках каждый оператор занимается соответствующим вводом/выводом, систему верификации это не должно волновать (хотя конечно, влияние масштабов имеется, но так и техники должны быть соответствующие). Или же упрощают "фоновую" работу (и соответственно её учитывают), к примеру, в TLA+ выше есть понимание "stuttering step", нечто подобное (и шире) у глушковцев в их "инсерционном программировании", в Promela (Spin, для "недетерминированных циклов") минимум вспомогательных операторов.