OberonCore

Библиотека  Wiki  Форум  BlackBox  Компоненты  Проекты
Текущее время: Вторник, 19 Март, 2024 09:12

Часовой пояс: UTC + 3 часа




Начать новую тему Ответить на тему  [ Сообщений: 28 ]  На страницу 1, 2  След.
Автор Сообщение
 Заголовок сообщения: Про гранулярность у coroutines
СообщениеДобавлено: Четверг, 05 Октябрь, 2017 13:12 

Зарегистрирован: Пятница, 13 Март, 2009 16:36
Сообщения: 987
Откуда: Казань
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 программы могут выполняться параллельно, то есть не в рамках одного потока с разделением времени между подзадачами, а реально могут выполняться параллельно. В рамках одного потока может выполняться цикл, который принимает и посылает сообщения - этим программам.
Так вот такую схему можно рассматривать как недетерминированный цикл Дейкстры и для программиста верификация этой схемы логически будет выглядеть как рассуждение над одним потоком. В случае же других моделей параллельных программ, рассуждения о правильности сильно усложняются.
Возможно, я не до конца понял ваш подход. Но как мне показалось, в вашем подходе гранулярность выполнения - это один оператор языка программирования. Если это так, то это конечно лучше, чем гранулярность ассемблерных инструкций, но для доказательства корректности, это довольно низкий уровень. Лучше, когда гранулярность равна одной подпрограмме, тогда гораздо легче доказывать корректность получившейся параллельной программы.


Дмитрий Дагаев писал(а):
Добрый вечер, Рифат,
Давайте опубликуем все, что написали, на форуме, каждый свой монолог. Я Вам там и отвечу.


Дмитрий Дагаев писал(а):
Если в двух словах, то предмета спора нет. Вы говорите о том же. Сопрограммы обмениваются только через сообщения с семафорами, а так они изолированы. Причём последнее нужно доказывать.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Про гранулярность у coroutines
СообщениеДобавлено: Четверг, 05 Октябрь, 2017 14:50 
Аватара пользователя

Зарегистрирован: Воскресенье, 12 Апрель, 2015 18:12
Сообщения: 1134
Откуда: СССР v2.0 rc 1
Что-то Рифат сильно усложняет.

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

Верифицировать программу невозможно, если одна часть программы лезет в данные другой части программы.
Пример дурного кода:
Код:
MODULE A;
VAR
  i*: INTEGER:
..........
MODULE B;
BEGIN
F.i := Random(infinity);
END B.


Пример уже кода получше:
Код:
MODULE A;
CONST
  MAX_i = 1000;
VAR
  i-: INTEGER:
PROCEDURE Set_i(val:INTEGER);
BEGIN
  ASSERT(val<MAX_i);
  i := val;
END Set_i;
..........
MODULE B;
BEGIN
F.Set_i(Random(infinity));
END B.

Здесь контракт присвоения сделает своё чёрное дело. Память не общая + контролируемый доступ на присвоение.
Соответственно, присвоение не требует дополнительного контроля. Оберон-07 рулит.

На уровне присвоения гранулирование обеспечено.

Второй этап. Даже если значения правильные, один гринлет (* уж простите, сопоток -- может вызвать недопонимание *) может конкурировать за текущие значение с другим гринлетом за глобальный объект. Вот здесь диспетчер и нужен. Планировщик решает, что и когда будет исполняться, и диспетчер решает что исполняется. Т. е. СЕЙЧАС. И если какой-то глобальный объект нужен всем, а гринлет не успевает, диспетчер ему говорит: значит так зелёный: твой контекст сохраняю, досвидос. И когда наступает очередной квант этого гринлета -- диспетчер ему восстанавливает контекст (если он ещё актуален). Либо у гринлета есть альтернатива -- закончит работу с глобальным объектом досрочно.

Отсюда давно известное правило: глобальных объектов должно быть как можно меньше.

Это не доказательство правильности алгоритма гринлета. Вообще, при взаимодействии с открытым миром -- могут быть какие угодно алгоритмы (например, через сериализацию/экстернализацию -- динамическая подгрузка модулей). Как их проверять? Вторая проблема уже была озвучена в соседней ветке форума: как будем доказывать правильность доказательной части алгоритма?

Поэтому, я склоняюсь к варианту, когда нет потери контроля над гринлетами, и есть элементы контрактного программирования. Тут даже динамические языки могут что-то из себя изобразить.

З.Ы. Нечаянно подумал, что сериализация -- куда менее удачный термин, чем экстернализация. В википедии "сериализация" есть, а "экстернализации" -- нет.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Про гранулярность у coroutines
СообщениеДобавлено: Четверг, 05 Октябрь, 2017 19:01 

Зарегистрирован: Вторник, 01 Март, 2011 09:34
Сообщения: 583
Откуда: Москва
Рифат писал(а):
Лучше, когда гранулярность равна одной подпрограмме, тогда гораздо легче доказывать корректность получившейся параллельной программы

Во-первых, подтверждается мой тезис, что угроз может быть больше, чем преимуществ. Представьте, что я принес Вам, как эксперту программу на сертификацию в смысле доказательства частичной корректности (Хоар, Дейкстра). И привел аргументы в части: гранулярности присваивания, защиты стека, обеспечения целостности указателей. А Вы мне говорите: А докажите еще, отсутствие
Цитата:
взаимодействия каждого оператора одной процедуры с каждым оператором другой процедуры
. Вывод - программу честно верифицировать непросто.

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


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Про гранулярность у coroutines
СообщениеДобавлено: Пятница, 06 Октябрь, 2017 10:31 

Зарегистрирован: Пятница, 13 Март, 2009 16:36
Сообщения: 987
Откуда: Казань
Дмитрий Дагаев писал(а):
Рифат писал(а):
Лучше, когда гранулярность равна одной подпрограмме, тогда гораздо легче доказывать корректность получившейся параллельной программы

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

Давайте на каком-нибудь реальном примере рассмотрим сопрограммы и угрозы, которые там могут оказаться. Можно рассмотреть пример из книги "Verification of sequential and concurrent programs", там есть такая задача. Есть какая-то целочисленная функция y = F(x), где аргумент тоже целое число. Известно, что данная функция, точно имеет хотя бы один ноль (F(x) = 0). Необходимо найти один корень данной функции, то есть найти x, при котором F(x) = 0. Данную программу можно распаллелить на две части, одна часть будет искать положительный корень, а вторая неположительный.
Напишите, пожалуйста, небольшую такую программку, используя сопрограммы.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Про гранулярность у coroutines
СообщениеДобавлено: Пятница, 06 Октябрь, 2017 11:14 
Аватара пользователя

Зарегистрирован: Воскресенье, 12 Апрель, 2015 18:12
Сообщения: 1134
Откуда: СССР v2.0 rc 1
Не из жизни.
Типичная задача асушника: быстро и много опрашивать полевой порт. Фиксировать, выбраковывать неадекватные показания. Применяя несложный фильтр -- сглаживать выводимые показания, но предупреждать, например, что аномалии -- участились в 1,76 раза по сравнению с аналогичным прошлым периодом, и прогноз на выход из строя в течение месяца -- 72%.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Про гранулярность у coroutines
СообщениеДобавлено: Пятница, 06 Октябрь, 2017 11:24 

Зарегистрирован: Вторник, 01 Март, 2011 09:34
Сообщения: 583
Откуда: Москва
Рифат,

Я все, что мог - объяснил. Верификация не сопрограмм - а уже Вашей программы. Хотите пробовать на примерах - пробуйте. Не верите - не верьте, это правильно, критический подход. Будут конкретные вопросы, куда вставить Co.Yield - помогу.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Про гранулярность у coroutines
СообщениеДобавлено: Пятница, 06 Октябрь, 2017 11:43 

Зарегистрирован: Пятница, 13 Март, 2009 16:36
Сообщения: 987
Откуда: Казань
Допустим есть две сопрограммы:
Код:
found := FALSE;
x := 0;
WHILE ~found DO
  x := x + 1;
  found := f(x) = 0;
END;
и
found := FALSE;
y := 1;
WHILE ~found DO
  y := y - 1;
  found := f(y) = 0
END;

Где надо поставить Co.Yield-ы?


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Про гранулярность у coroutines
СообщениеДобавлено: Пятница, 06 Октябрь, 2017 12:49 

Зарегистрирован: Вторник, 01 Март, 2011 09:34
Сообщения: 583
Откуда: Москва
Код:
PROCEDURE (c: Cor1) Do
  VAR x: INTEGER; found: BOOLEAN
BEGIN
found := FALSE;
x := 0;
WHILE ~found DO
  x := x + 1;
  found := f(x) = 0;
  Co.Yield();
END;
END Do;
и
PROCEDURE (c: Cor2) Do
  VAR x: INTEGER; found: BOOLEAN
BEGIN
found := FALSE;
y := 1;
WHILE ~found DO
  y := y - 1;
  found := f(y) = 0;
   Co.Yield();
END;
END Do;

при этом f() должна содержать только локальные переменные


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Про гранулярность у coroutines
СообщениеДобавлено: Пятница, 06 Октябрь, 2017 13:30 

Зарегистрирован: Пятница, 13 Март, 2009 16:36
Сообщения: 987
Откуда: Казань
В данном случае found должна быть общей переменной, а не локальной переменной каждой сопрограммы. Как сделать её общей?


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Про гранулярность у coroutines
СообщениеДобавлено: Пятница, 06 Октябрь, 2017 13:35 

Зарегистрирован: Вторник, 01 Март, 2011 09:34
Сообщения: 583
Откуда: Москва
Код:
c.found := found

Глобальных переменных нет.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Про гранулярность у coroutines
СообщениеДобавлено: Пятница, 06 Октябрь, 2017 13:52 

Зарегистрирован: Пятница, 13 Март, 2009 16:36
Сообщения: 987
Откуда: Казань
c.found тоже нормально.
Правильно ли я понимаю, что в данном случае, сопрограммы будут фактически выполняться по очереди, сначала будет вызвана одна подпрограмма, которая выполнит одну итерацию своего цикла до Co.Yield(), затем будет вызвана вторая подпрограмма, которая выполнит одну итерацию своего цикла до Co.Yield(), затем передаст управление первой сопрограмме, которая выполнит вторую итерацию цикла и т.д.?


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Про гранулярность у coroutines
СообщениеДобавлено: Пятница, 06 Октябрь, 2017 14:31 

Зарегистрирован: Вторник, 01 Март, 2011 09:34
Сообщения: 583
Откуда: Москва
Точно так. Только выбор, на которую будет переключение, будет осуществляться планировщиком в зависимости от его алгоритмов. При моем имеющемся планировщике за 1 цикл Services.Action, например, будет вызвано 50 циклов первой сопрограммы (сработает Co.Yield() на 50-й раз) а затем будет вызвано 60 циклов второй сопрограммы.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Про гранулярность у coroutines
СообщениеДобавлено: Пятница, 06 Октябрь, 2017 14:35 
Аватара пользователя

Зарегистрирован: Воскресенье, 12 Апрель, 2015 18:12
Сообщения: 1134
Откуда: СССР v2.0 rc 1
Теперь ты понимаешь правильно))
Фактически, диспетчер в приведённом примере -- прослойка между рулём и сиденьем.
Можно и без неё обойтись. Но если вдруг ты захочешь какому-то потоку дать больше времени чем другому -- последовательный вызов процедур без дополнительных ухищрений -- сделать это не позволит.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Про гранулярность у coroutines
СообщениеДобавлено: Пятница, 06 Октябрь, 2017 14:42 

Зарегистрирован: Вторник, 01 Март, 2011 09:34
Сообщения: 583
Откуда: Москва
Да, можно ставить приоритеты задачам


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Про гранулярность у coroutines
СообщениеДобавлено: Пятница, 06 Октябрь, 2017 15:01 

Зарегистрирован: Пятница, 13 Март, 2009 16:36
Сообщения: 987
Откуда: Казань
Теперь лучше понимаю вашу библиотеку. В принципе, если использовать только локальные переменные, то вообще ничего опасного нет. Опасности начинаются, если есть какие-то общие поля, например:
Код:
PROCEDURE (c: Cor1) Do
  VAR x: INTEGER;
BEGIN
c.found := FALSE;
x := 0;
WHILE ~c.found DO
  x := x + 1;
  c.found := f(x) = 0;
  Co.Yield();
END;
END Do;
и
PROCEDURE (c: Cor2) Do
  VAR x: INTEGER;
BEGIN
c.found := FALSE;
y := 1;
WHILE ~c.found DO
  y := y - 1;
  c.found := f(y) = 0;
   Co.Yield();
END;
END Do;


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Про гранулярность у coroutines
СообщениеДобавлено: Пятница, 06 Октябрь, 2017 18:01 

Зарегистрирован: Понедельник, 25 Июнь, 2012 17:26
Сообщения: 473
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


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Про гранулярность у coroutines
СообщениеДобавлено: Пятница, 06 Октябрь, 2017 18:07 

Зарегистрирован: Понедельник, 25 Июнь, 2012 17:26
Сообщения: 473
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, для "недетерминированных циклов") минимум вспомогательных операторов.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Про гранулярность у coroutines
СообщениеДобавлено: Пятница, 06 Октябрь, 2017 21:00 
Аватара пользователя

Зарегистрирован: Воскресенье, 12 Апрель, 2015 18:12
Сообщения: 1134
Откуда: СССР v2.0 rc 1
И всё-таки верификация не решает проблем системы и сети. Это ооочень накладно. Где-то видел шуточный селфтест: он проверял правильность того, что процедура принимала два числа и всегда возвращала ноль. Исполнение -- идеальное. Смысл? Верификация верифицировала процедуру на то, что та работает верно, результат смысла не имеет.
Опять же, как верифицировать результат при квантовых вычислениях? Это точно возможно?
Считаю подход Вирта -- строить программы в оборонительном стиле -- достаточным вместе с контрактным программированием.
Многопоточность и многопроцессность -- особенно последнее -- требует усилий. Что-то, конечно можно сделать. Даже наверное нужно (раз Дмитрий сделал).
Но важно вовремя остановиться. Чем изощрённей методика -- тем больше вероятность ошибки. А нет ничего дороже на этом свете чем глупость.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Про гранулярность у coroutines
СообщениеДобавлено: Понедельник, 09 Октябрь, 2017 10:09 

Зарегистрирован: Пятница, 13 Март, 2009 16:36
Сообщения: 987
Откуда: Казань
Как мне кажется, сопрограммы так же опасны, как и goto. Почему я так считаю?
Для однопоточной программы:
Код:
PROCEDURE (VAR c: SomeRecord);
  VAR x: INTEGER;
BEGIN
c.found := FALSE;
x := 0;
WHILE ~c.found DO
  x := x + 1;
  c.found := f(x) = 0;
END;
END Do;

Данный код корректен.
Но, если мы используем сопрограммы, то следующий код становится уже некорректным:
Цитата:
PROCEDURE (c: Cor1) Do
VAR x: INTEGER;
BEGIN
c.found := FALSE;
x := 0;
WHILE ~c.found DO
x := x + 1;
c.found := f(x) = 0;
Co.Yield();
END;
END Do;
и
PROCEDURE (c: Cor2) Do
VAR x: INTEGER;
BEGIN
c.found := FALSE;
y := 1;
WHILE ~c.found DO
y := y - 1;
c.found := f(y) = 0;
Co.Yield();
END;
END Do;

Так как может быть ситуация, что сколько-то итераций работала первая сопрограмма и только она нашла корень функции и устанавливает c.found в TRUE:
Цитата:
c.found := f(x) = 0;
Co.Yield();
,
как она прерывается и запускается вторая сопрограмма, которая сбрасывает c.found в FALSE, и если у функции больше нет корней, то программа никогда не завершится.

Для того, чтобы программа с сопрограммами стала корректной необходимо исправить несколько недочетов в программе:
1) не сбрасывать c.found := FALSE; внутри сопрограммы;
2) не использовать c.found := f(x) = 0; так как после установки c.found в TRUE и запуска другой сопрограммы, c.found снова может сбросится в FALSE. Необходимо использовать:
Цитата:
IF f(x) = 0 THEN
c.found := TRUE
END


Основной вывод: нельзя взять обычную однопоточную программу, добавить туда Co.Yield(); и ожидать, что программа останется корректной.

Для верификации данных сопрограмм, с одним Co.Yield() необходимо рассмотреть по три ситуации для каждой сопрограммы: сопрограмма может быть еще не запущена или остановлена в точке Co.Yield() или уже завершилась. Таким образом, получается 9 вариантов, которые нужно рассмотреть, чтобы проверить правильная ли программа.

В случае увеличения, количества Co.Yield() и количества сопрограмм, количество вариантов, которое нужно будет рассмотреть будет равно (Number_of_yields + 2) в степени Number_of_coprograms.


Вложения:
znak_radiaciya[1].png
znak_radiaciya[1].png [ 157.87 КБ | Просмотров: 20675 ]
Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Про гранулярность у coroutines
СообщениеДобавлено: Понедельник, 09 Октябрь, 2017 10:18 
Модератор
Аватара пользователя

Зарегистрирован: Понедельник, 14 Ноябрь, 2005 18:39
Сообщения: 9459
Откуда: Россия, Орёл
Один из ключевых принципов Дейкстры - верификация по построению (а не по факту).

Соответственно, не надо "просто добавлять Yeld в существующую программу".

Если Вы возьмёте существующую структурную программу и добавите в неё goto, то тоже что-нибудь может поломаться ))

Параллельно работающие обработчики (те же Action) есть и без сопрограмм. Если Вы начнёте в них не следить за зависимостями по общим данным - то получите те же самые проблемы.
Конечные автоматы, работающие асинхронно (а они - единственная "более консервативная" замена сопрограммам в серверных задачах) - это тот ещё GOTO, вот где GOTO.

Речь-то о том, что из всех видов параллелизма сопрограммы позволяют контролировать ситуацию лучше всего (требуя совсем немного доп. анализа от программиста по сравнению с последовательным программированием).


Вернуться к началу
 Профиль  
 
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ Сообщений: 28 ]  На страницу 1, 2  След.

Часовой пояс: UTC + 3 часа


Кто сейчас на конференции

Сейчас этот форум просматривают: нет зарегистрированных пользователей и гости: 1


Вы не можете начинать темы
Вы не можете отвечать на сообщения
Вы не можете редактировать свои сообщения
Вы не можете удалять свои сообщения
Вы не можете добавлять вложения

Найти:
Вся информация, размещаемая участниками на конференции (тексты сообщений, вложения и пр.) © 2005-2024, участники конференции «OberonCore», если специально не оговорено иное.
Администрация не несет ответственности за мнения, стиль и достоверность высказываний участников, равно как и за безопасность материалов, предоставляемых участниками во вложениях.
Без разрешения участников и ссылки на конференцию «OberonCore» любое воспроизведение и/или копирование высказываний полностью и/или по частям запрещено.
Powered by phpBB® Forum Software © phpBB Group
Русская поддержка phpBB