viewtopic.php?f=31&t=6128#p102165prospero78 писал(а):
И всё-таки верификация не решает проблем системы и сети. Это ооочень накладно. Где-то видел шуточный селфтест: он проверял правильность того, что процедура принимала два числа и всегда возвращала ноль. Исполнение -- идеальное. Смысл? Верификация верифицировала процедуру на то, что та работает верно, результат смысла не имеет.
Опять же, как верифицировать результат при квантовых вычислениях? Это точно возможно?
Считаю подход Вирта -- строить программы в оборонительном стиле -- достаточным вместе с контрактным программированием.
Многопоточность и многопроцессность -- особенно последнее -- требует усилий. Что-то, конечно можно сделать. Даже наверное нужно (раз Дмитрий сделал).
Но важно вовремя остановиться. Чем изощрённей методика -- тем больше вероятность ошибки. А нет ничего дороже на этом свете чем глупость.
Так ведь верификация и есть "контракты" для "оборонительного стиля". Фактически, единственное существенное отличие от традиционных "assert"-ов в runtime (во время интерпретации модели) -- попытка анализа в compiletime или на этапе построения модели.
Если написали "контракт" в виде требования возвращать ноль при любом входе -- значит, такова цель, и осмысленность возникает соответствующая такой цели. А формально выделяют задачи верификации (лат. verus -- верный) -- соответствие установленным требованиям, и валидации (validus -- здравый) -- соответствие самих требований целям системы.
Если единый "assert" покрывает всю систему -- повезло. Но обычно картина локальная -- здесь конкретная цитата по поводу:
viewtopic.php?f=152&t=6126#p102121И, как правило, "assert" зависит от конкретики алгоритма, и на конкретику влияет "репертуар" исполнителя -- его используемые команды, свойства и т.п. -- в этом лишь разница в понимании того, кто там пашет в реалиях -- человек, биомолекула или квантовый исполнитель.
Детальнее о проблемах сети (и в целом о проверках). Пусть у нас возникает потребность реализации процессов в виде какой-то транзакции (пусть даже финансовой) аля "A(K) -> Б(C) -> В(K) -> Г(C) ...", т.е. последовательность (грубо) процессов "A, Б ...", каждый из которых исполняется либо на "сервере" (С) или на "клиенте" (K). В общем, распределённые процессы (в целом на множестве сторон взаимодействия) осуществляют виртуальные транзакции, определяемые протоколом, условно постоянно появляющиеся в системе. В любой программе, каким-то способом реализующей процесс транзакции, как правило, можем выделить подсистему ввода/вывода -- условно доставку данных, и прикладную предметную реализацию транзакции Эти две подсистемы имеют точки соприкосновения.
Полагаю, не ошибусь, если предположу следующий типовой сценарий, характерный в большинстве случаев. Обычно в сетевом вводе/выводе задействованы таймауты, при истечении которых незавершенные операции считаются неудачными -- предполагается ненадёжная среда доставки, и выполняется повторное выполнение (с возможным частичным восстановлением каких-то данных) транзакции по потребности, или же прочие необходимые реакции. Однако в каких-то случаях сигналы (данные) могут отсутствовать при причине deadlock-ов и/или livelock-ов (кто-то где-то заблокирован в ожидании результатов друг друга, прямо или косвенно, или же кто-то условно "зациклился", или же технически заблокирован тред ОС, назначенный для исполнения некоторых процессов, и т.п.). В каких-то системах подобные ситуации допускаются априори (ибо заранее невозможно установить правильную модель вычислений -- нет протокола, как такового), или же "глюки" возникают из-за неправильной логики протоколов взаимодействия. В последних случаях глюки могут быть разрулены также, как и глюки среды доставки данных (таймауты), но не всегда -- в тех случаях, когда глюки протоколов возникают относительно редко, при повторном исполнении транзакций возникает иная предыстория вычислений, и в итоге всё "ок". В иных случаях проблема со временем может оказаться локализованной -- "ой, извиняемся, быстро исправляем ...". А где-то обстоятельства нагибают более ответственно. К тому же в общем случае возможно хоть и распределенное взаимодействие, но в рамках условно надёжной шины обмена данными.
В статейке ниже наглядный пример выявления глюков в протоколах взаимодействия, в данном случае -- академическая работа над контрактами каналов в Singularity ОС -- был когда-то эксперимент от MS в ответ на возникшую тогда моду на "акторы":
Вложение:
Причём проблемки выявлены после заявлений разработчиков, мол всё норм (хотя эксплуатации ОС не было, как таковой). И масштабы взаимодействующих автоматов (контрактов) малые -- вполне обозримы графы переходов, но визуально глюки незаметны (ну или необходимо сильно напрягаться для мысленной интерпретации исполнения).
Это пример "неглупости" проверок. В данном случае используется иной инструмент, не "Net-платформа" и "C#" -- нет возможности написать какие-то "runtime assert"-ы в таком языке как C# в подобных случаях (конкретнее -- проверка через Spin (инструмент) с генерацией моделей для Promela (язык "программирования"), а исходные контракты в Singularity определяются на своём DSL).
Здесь первый подход -- проверка формальных моделей взаимодействия. Методики и инструменты разные, но общий принцип -- найти пример (или контрпример) нарушения требований. Более широко -- проверить достижимость (отсутствие deadlock-ов), "справедливость" (отсутствие livelock-ов), безопасность -- конкретные предметные "assert"-ы. Для упрощения можем обобщить как задачи принципиальной достижимости и безопасности. И очень грубо говоря, делается попытка представить взаимодействие процессов в виде последовательного протокола по мотивам выше, с учётом зависимости по данным, параллельной (со своим исполнителем) работы, с учётом возникающих в итоге возможных вариантов "совместности". О последнем явлении здесь на форуме была когда-то ссылка на статейку Эдвард А. Ли, где представлена простейшая матем. интерпретация:
https://habrahabr.ru/company/nordavind/blog/195262/Но ключевое в подходе выше -- проверяется модель вычислений или протокола, а сама реализация конкретных процессов -- отдельная песня, соответствие реализации исходной формальной модели -- отдельные задачи.
В платформах вокруг Esterel такие языки как Lustre/Signal/Lucid Synchrone -- пример языка моделирования и реализации в "одном флаконе". Любая программка (каждая функция, или "node/task") по конструкции имеет гарантию принципиальной достижимости. Здесь компилятор анализирует возможность возникновения/отсутствия данных (сигналы), выявляет зависимости по данным и возможность взаимозависимости (deadlock-и, а также по возможности и livelock-и), проверяет правильность веток "if" -- все ли указаны варианты, нет ли "if" без "else" или определена ли реакция на отсутствие вычисления (данных), и т.д. и т.п. Высказывание упрощённое, поскольку расширенно в потоковых моделях вместо (или в дополнение) "if" имеются специализированные операторы "фильтра" данных (или undersampling, а также oversampling), алгебраические типы и пр. Т.е. имеется базовый анализ семантики языка, ну и далее по потребности и возможности -- вплоть до дедуктивных систем проверок ("зависимых типов", и основополагающие понятия "сигналов" -- всё через типы). Есть спец-библиотеки для построения и систем эмуляции с недетерминированным выбором данных/вычислений -- для тестирования, грубых прикидок и т.д. Причём принцип реализации -- поближе к "Бёма — Якопини" (базовые структуры процессов) да предметные уточняющие "assert"-ы для "безопасности", а необходимые "теоремы" да "леммы" -- автоматом за кадром. И, конечно же, "hard-математика" на борту для случаев необходимости.
Ограничения платформы позволяют относительно эффективно использовать инструменты. В случае динамики изменения структуры процесса/процессов -- возникают сложности, теоретически покоряемые, но гораздо труднее (в целом, для любой возможной платформы):
viewtopic.php?f=152&t=6126#p102120Итак, реализовали программку -- получили проверенную "синхронную" модель протокола работы процессов. Теперь есть возможность контролируемо сгенерить локальную или любую распределенную реализацию процессов.
Насчёт локальной модели реализации. Потоковая модель предполагает ярусно-параллельную форму асинхронности, или расширенно как на рис.:
Вложение:
async_dataflow.png [ 19.5 КБ | Просмотров: 11992 ]
Пример техники построения -- ниже (здесь уже была ссылка), причём форма консервативна в том смысле, что при отсутствии реальных альтернативных исполнителей модель остаётся синхронной -- т.е. первично можно моделировать процессы синхронно, затем по необходимости развивать "ускорение":
Programming Parallelism with Futures in LustreМожно обратить внимание на применение "буферов" или "задержек" -- приятнее, когда их правильность контролирует компилятор. Как и прочие атрибуты (напр., приоритеты процессов), или "перегрузку/недогрузку" и достижимость в этом контексте:
Transaction Parameterized Dataflow: A Model for Context-Dependent Streaming ApplicationsНасчёт распределенности. Зная модель вычислений (исходный протокол взаимодействия) и принципы конкретной подсистемы ввода/вывода или среды доставки данных -- очевидно, возможен требуемый синтез системы. В общем случае под средой доставки можно понимать всё, что угодно. К примеру, наличие подсистемы publish-subscribe (процессы могут работать в разном временном разрезе), использование GUI-интерфейса и взаимодействие с пользователем, и т.п.
На форуме Дракон-а когда-то была ссылка на проект Termite -- "интеллектуальный" синтез программ реализации драйверов:
http://ssrg.nicta.com.au/projects/TS/drivers/synthesis/, где автоматический синтез на базе теории игр как поиск оптимальной траектории системы (т.е. синтезируется даже исходный протокол по предопределенным правилам "игры"). Любопытный обзор инструментов для этого:
https://arxiv.org/abs/1506.08726Проект выше демонстрирует важную особенность -- в общем случае возникает необходимость частичного, постепенного, инкрементального построения конечной системы, в том числе и вручную. Для этого неизбежно необходимо понимать "протоколы". Здесь уточнения:
viewtopic.php?f=152&t=6126#p102121, где акцентируется на "разрыве" протокола или его интерпретацию в рамках типов -- "сессионные типы", "состояние типов", "протоколы ресурсов". Там же есть пример (по ссылке в сообщении) реализации вэб-сервера -- демонстрации "разрыва" предметного протокола, ну и сетевого взаимодействия. В целом, очевидно, что в системе возникает множество "протоколов" -- свои для реализации "прикладных транзакций" и сопутствующие "технологические" -- другие подсистемы доставки данных или какие-то смежные (все подсистемы проверяются по своим протоколам, в т.ч. возможен протокол их состыковки).
Ключевое, если возникает потребность контролирования реализации со стороны компилятора, и как бы не взаимодействовали подсистемы -- неизбежно на практике требуется "разрывать" тип или "assert". По ссылке выше был пример, он, конечно же, так себе... Для раскрытия темы -- необходима детальная содержательная постановка (вне рамках данного сообщения форума).
Итого, если в базовом языке или платформе на борту будут необходимые инструменты -- "верификацией" придётся заниматься, может быть, даже незаметно (отчасти).