OberonCore

Библиотека  Wiki  Форум  BlackBox  Компоненты  Проекты
Текущее время: Пятница, 20 Октябрь, 2017 19:11

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




Начать новую тему Ответить на тему  [ Сообщений: 25 ]  На страницу Пред.  1, 2
Автор Сообщение
СообщениеДобавлено: Пятница, 07 Июль, 2017 21:05 

Зарегистрирован: Понедельник, 25 Июнь, 2012 17:26
Сообщения: 171
В принципе, и вокруг мейнстрима были и есть здравые идеи. Напр., во времена моды "аспектно-ориентированности" была такая академическая задумка:
http://ptolemy.cs.iastate.edu/papers/ECOOP.08.paper.pdf

где видна попытка уменьшить "callback hell" в типовой объектной модели. Также там неплохо обобщены основные проблемы "аспектности".
Это всё к той же отмеченной ранее проблеме координации "верхнего уровня".

Для языка аля Lucid Synchrone достаточно паттерна "декоратор", т.е. переопределения функции. К примеру, для какого-то scope можно ввести модуль с альтернативной реализацией:
Код:
fn my_func(s: string) => print s;
...
// переопределяем ф-цию
impl fn my_func(s: string) =>
{
  inherit(s);  // вызов исходной ф-ции
  print 'ok';
}


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

Зарегистрирован: Понедельник, 25 Июнь, 2012 17:26
Сообщения: 171
viewtopic.php?f=31&t=6128#p102165
prospero78 писал(а):
И всё-таки верификация не решает проблем системы и сети. Это ооочень накладно. Где-то видел шуточный селфтест: он проверял правильность того, что процедура принимала два числа и всегда возвращала ноль. Исполнение -- идеальное. Смысл? Верификация верифицировала процедуру на то, что та работает верно, результат смысла не имеет.
Опять же, как верифицировать результат при квантовых вычислениях? Это точно возможно?
Считаю подход Вирта -- строить программы в оборонительном стиле -- достаточным вместе с контрактным программированием.
Многопоточность и многопроцессность -- особенно последнее -- требует усилий. Что-то, конечно можно сделать. Даже наверное нужно (раз Дмитрий сделал).
Но важно вовремя остановиться. Чем изощрённей методика -- тем больше вероятность ошибки. А нет ничего дороже на этом свете чем глупость.

Так ведь верификация и есть "контракты" для "оборонительного стиля". Фактически, единственное существенное отличие от традиционных "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 в ответ на возникшую тогда моду на "акторы":
Вложение:
Analyzing Singularity Channel Contracts.pdf [235.81 КБ]
Скачиваний: 3


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

Это пример "неглупости" проверок. В данном случае используется иной инструмент, не "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
async_dataflow.png [ 19.5 КБ | Просмотров: 95 ]

Пример техники построения -- ниже (здесь уже была ссылка), причём форма консервативна в том смысле, что при отсутствии реальных альтернативных исполнителей модель остаётся синхронной -- т.е. первично можно моделировать процессы синхронно, затем по необходимости развивать "ускорение":
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". По ссылке выше был пример, он, конечно же, так себе... Для раскрытия темы -- необходима детальная содержательная постановка (вне рамках данного сообщения форума).

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


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

Зарегистрирован: Понедельник, 25 Июнь, 2012 17:26
Сообщения: 171
Насчёт протоколов сетевого взаимодействия. В статейке ниже полезная академическая разработка, но принципы применимы широко:
A Prescription for Safely Relaxing Synchrony

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

В целом, конечно, протоколы зависят от специфики задач. К примеру, в проекте Bloom:
http://bloom-lang.net/index.html

анализируется "монотонность" вычислений -- взаимодействующие процессы понимаются как виртуальные (или реальные) БД, и осуществляется контроль недопустимости операций, нарушающий контекст предыстории вычислений в заданных аспектах (кроме "попсового" Ruby-like имеется и диалект Datalog-а (или Prolog-а) для разработки и верификации -- там это "низкий" уровень).


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Вторник, 10 Октябрь, 2017 11:58 
Аватара пользователя

Зарегистрирован: Воскресенье, 12 Апрель, 2015 18:12
Сообщения: 1043
Откуда: СССР v2.0 rc 1
Не сомневаюсь, что на уровне протокола можно защитить данные от принципиально потенциально кривого канала связи.
Если бы это было не так, речь была бы невозможно. Верификация тут не нужна, валидация осуществляется формально. И если с последней особо вопросов нет, то верификация поверх даже статических систем возможна лишь частично. Есть достаточное число алгоритмов, которое и статически верифицировать не возможно. А ведь есть ещё динамика...
Собственно, не так интересно внутреннее состояние системы, как всё те же пришлые варяги во время работы. В каком-то смысле вирусы -- незаконно верифицированные программные модули. И ровно половина из них убивается на корню просто запретом использования адресной арифметики, как источником сбоя стека.
Это просто ограничения языка, которые, по хорошему -- следовало бы вынести на уровень железа. Но это так, цветочки. Сколько ещё можно упростить неликвидного поведения программной системы рамками языка?
И кстати, на много упрощается валидация (в идеале, её даже можно исключить в силу "бесплатной" валидации исходного текста). И также существенно упрощается верификация. Как побочный эффект. Это будет даже не 80, а под 95% искомого эффекта без дополнительных усилий. Оставшиеся 5%, имхо, на текущем уровне (массовом) развития ИТ -- пока будут неэффективными тратами ресурсов. Тут хотя бы эти 95% реализовать ,а там, глядишь, и новые методы замаячат. Более простые и не менее эффективные. (* Прям по Гегелю получается ))) *)


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Вторник, 10 Октябрь, 2017 19:16 

Зарегистрирован: Понедельник, 25 Июнь, 2012 17:26
Сообщения: 171
prospero78 писал(а):
Сколько ещё можно упростить неликвидного поведения программной системы рамками языка?
И кстати, на много упрощается валидация (в идеале, её даже можно исключить в силу "бесплатной" валидации исходного текста). И также существенно упрощается верификация. Как побочный эффект.

Кстати, термины валидация и верификация, всё-таки, резиновые. Иногда подразумевают контекст "жизненного цикла": верификация -- подготовка для "сдачи в эксплуатацию" (со всеми проверками), валидация -- "приёмка заказчиком", мол опять проверки, насколько система отвечает "ожиданиям".
В программной интерпретации, видимо, следует понимать так. Воспользуюсь неоднократно упомянутым проектом F-star (как один из самых продвинутых инструментов дедуктивной верификации, под крышей MS), конкретнее -- пример просто для наглядности:
Probabilistic Relational Verification for Cryptographic Implementations

и на основе спецоператоров (согласно статейке выше) L() и R() -- "левый" и "правый" вызов функции -- для указания отношений между смежными тактами автомата -- выразим условие монотонности для функционального типа:
x: int -> y: int {L(x) <= R(x) ==> L(y) <= R(y)}

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

Ограничения типов, кстати, можно прикрутить не только к верификации, но и для задач документации, тестирования (генерация тестов), синтез реализаций и т.п.

В том же проекте F-Star, к слову, есть интересные (это мягко сказать) техники верификации, в том числе для выявления "незаконно верифицированных" -- для задач крипто-безопасности, к примеру (здесь опять же построение принципиального устройства протокола, технология отлична от того же упомянутого SPIN и ему подобных):
Wys*: A Verified Language Extension for Secure Multi-party Computations


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

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


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

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


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

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