Rifat писал(а):
Здравствуйте, Дмитрий Викторович!
Вчера смотрел ваше выступление. Там Вы говорили про то, что по умолчанию при параллельном программировании даже оператор присваивания не будет гранулярным, а может быть прерван где-то по середине. И как я понял, Вы вставляете специальный код, чтобы прерывания могли быть, только в этих местах, то есть между операторами, а не внутри них.
Я недавно читал книги "Verification of sequential and concurrent programs" (Apt K.R., de Boer F.S., Olderog E.-R. (eds.)) там говорится о том, что если, допустим, у нас есть две процедуры, где, допустим, операторы гранулярны, то для того, чтобы верифицировать всю эту параллельную программу необходимо рассмотреть взаимодействия каждого оператора одной процедуры с каждым оператором другой процедуры. Я так думаю, что на практике это осуществить практически невозможно. Сам же я интересовался, какой же метод параллельного программирования, можно верифицировать на практике. И нашел, что распределенные программы без общей памяти, которые могут обмениваться сообщениями можно свести к недетерминированному циклу Дейкстры, который в свою очередь можно верифицировать как обычный цикл, нужно только найти инвариант цикла. И если использовать этот метод, то можно верифицировать (и рассуждать о программе во время проектирования и разработки) как над обычной последовательной программой.
Я думаю, что будущее за тем методом параллельного программирования, который легко верифицировать. Если какую-то параллельную программу сложно верифицировать, то значит, что и практической пользы от этого метода будет не много, так как написать параллельную программу можно будет, но как убедиться, что она правильная, много и долго тестировать? (Даже для обычных программ тестирование покрывает лишь мизерную часть всех возможных ситуаций, а с параллельными программами, мне кажется, что тестирование, вообще безнадежно, так как на реальной системе скорости могут быть одни, при тестировании другие).
Единственное, что теоретически я понимаю, как можно распределенные программы свести к недетерминированному циклу Дейкстры, но как это сделать практически, то есть какие специальные команды ввести, какие очереди сообщений создать не совсем понятно. Нужно над этим подумать.
Дмитрий Дагаев писал(а):
Уважаемый Рифат!
В докладе
https://forum.oberoncore.ru/viewtopic.php?f=127&t=6091&p=101972#p101972 рассмотрены последствия проблем при добавлении сопрограмм и методы купирования, т.е. создания верифицированных сопрограмм.
Рассматриваемый Вами случай - Анонимные сопрограммы по приведенной классификации, - реализуют логический параллелизм в рамках одного потока. Я говорил, что нужно обеспечить в т.ч. "Memory Protection", имея в виду изоляцию данных одной задач от другой (стр 15 доклада). Да, защищать данные при неатомарности копирования для сопрограмм не нужно. Но сами реализации, наследуемые от сопрограмм, должны быть изолированы друг от друга. Как подпрограмма с локальными параметрами может рассматриваться автономно. Если есть взаимовлияние одного оператора на другой, то анонимные сопрограммы не автономны, и встает вопрос о верификации (может, и по упомянутой Вами книге).
Целью Дейкстры являлось построение структурной программы, а не анализ любой другой существующей на предмет верификации. Аналогично, моей целью было правильно построить взаимодействие сопрограмм, а не анализировать заведомо неправильные решения. Там же, на стр 15 я предлагаю обмениваться только через сообщения, для управления почтовыми ящиками которых в пакет Co_ введены семафоры. Это - полностью верифицируемый подход (при условии, что все остальные проблемы купированы). Причем, семафоры используются не для защиты данных при копировании, а для управления взаимодействия параллельных программ.
Rifat писал(а):
Здравствуйте, Дмитрий Викторович!
> Рассматриваемый Вами случай - Анонимные сопрограммы по приведенной классификации, - реализуют логический параллелизм в рамках одного потока.
Вы не совсем правильно меня поняли. Я говорил про то, что если придерживаться терминологии книги Apt, то есть "distributed programs consist of components with local memory that
can communicate only by sending and receiving messages.". И эти distributed программы могут выполняться параллельно, то есть не в рамках одного потока с разделением времени между подзадачами, а реально могут выполняться параллельно. В рамках одного потока может выполняться цикл, который принимает и посылает сообщения - этим программам.
Так вот такую схему можно рассматривать как недетерминированный цикл Дейкстры и для программиста верификация этой схемы логически будет выглядеть как рассуждение над одним потоком. В случае же других моделей параллельных программ, рассуждения о правильности сильно усложняются.
Возможно, я не до конца понял ваш подход. Но как мне показалось, в вашем подходе гранулярность выполнения - это один оператор языка программирования. Если это так, то это конечно лучше, чем гранулярность ассемблерных инструкций, но для доказательства корректности, это довольно низкий уровень. Лучше, когда гранулярность равна одной подпрограмме, тогда гораздо легче доказывать корректность получившейся параллельной программы.
Дмитрий Дагаев писал(а):
Добрый вечер, Рифат,
Давайте опубликуем все, что написали, на форуме, каждый свой монолог. Я Вам там и отвечу.
Дмитрий Дагаев писал(а):
Если в двух словах, то предмета спора нет. Вы говорите о том же. Сопрограммы обмениваются только через сообщения с семафорами, а так они изолированы. Причём последнее нужно доказывать.