OberonCore

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

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




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

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


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

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

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


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

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


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Пятница, 08 Декабрь, 2017 20:56 

Зарегистрирован: Понедельник, 25 Июнь, 2012 17:26
Сообщения: 473
viewtopic.php?f=152&t=6158&start=40#p102994
Дмитрий Дагаев писал(а):
Вот еще интересная цитата из AREAVE OASIS касательно Esterel и Lustre:
Цитата:
Synchronous languages like Esterel [4] or Lustre [5] relies on strong formal definitions, and allows for formal checksand validations of the modeled system. This permitted their use in critical environments and especially for aviation and transportation. Nonetheless, for the concrete implementation of a synchronous model, the usual approach is either to generate C code for a Posix compliant RT kernel (e.g.VxWorks) or generate statically scheduled sequential C code for a barebone execution (or on top of interrupt services,e.g. [ссылка 6]). The former is nearly impossible to validate with regards to the standards. The later could probably be away to generate an application in the traditional design of ISO-60880 (periodic execution of a single program divided as statically scheduled RT activities). Nonetheless, to our knowledge, no efforts were made toward such a goal. Webelieve that aiming to such a goal would be achievable but would not reduce the cost of validation, even thought the cost of programming would be roughly on par with OASIS.

Злыми конкурентами утверждается, что синхронные языки не подходят под 60880 из-за реализации. Ничего такого не сделано. При этом второй вариант, кажущийся приемлемым, на самом деле оставляет много вопросов, например в части кучи GOTO, необходимости специальных компиляторов для Lustre с измененной семантикой.

На сайте Esterel заявлена совместимость в т.ч. и с 60880 для их SCADE, но за подробностями отправляют в службу продаж:
http://www.esterel-technologies.com/ind ... tification

Однако, в целом, любопытно (и полезно) оценить возможности используемого языка, точнее понять его ограничения (на фоне мэйнстрима). Всё-таки, не только академический проект, но и широкая промышленная эксплуатация.
Ниже краткий обзор диалекта Lustre, применяемый в SCADE (причём в текстовой форме, раскрывая содержательный смысл того, чего там зарисовывают в диаграммах):
Scade 6: A Formal Language for Embedded Critical Software Development

Базовые принципы кодогенерации:
Clock-directed Modular Code Generation for Synchronous Data-flow Languages

Сам императивный язык Esterel был "закрыт" в 2008 г. на версии V7, тюненгованный для hardware-реализации, но проблематичный для эффективной software-реализации, в т.ч. была затруднительна статическая верификация (согласно док-м). "Императивщину" в Lustre добавили конструкциями "activate if ..." для блоков уравнений, "automaton", измененной поддержкой массивов.

Явные "автоматы" соответствуют понятию "высокоуровневых гиперпроцессов", плюс явная иерархическая и параллельная композиция функций-состояний:
http://forum.drakon.su/viewtopic.php?f= ... 64#p100964

На фоне ограничений даже не заметны на первый взгляд такие фишки, как примитивный полиморфизм (выше по ссылке есть примеры декларации процессов с абстрактным типом numeric и применении процессов с конкретным float).


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Пятница, 08 Декабрь, 2017 21:00 

Зарегистрирован: Понедельник, 25 Июнь, 2012 17:26
Сообщения: 473
viewtopic.php?f=86&t=6188#p103053
Comdiv писал(а):
Исходя из рекомендаций к коду для атомных станций, которые регламентируют, что цикл должен иметь константное максимальное количество итераций и того, что в общем случае проанализировать количество итераций для инструментальных средств может быть затруднительным, то, по-хорошему, язык должен предоставлять цикл подобного вида:
Код:
Loop =
  IdentOk ":=" LOOP Limit WHILE Expression DO
    Statements
  END .

Limit = ConstExpr | MIN(ExprLimit, ConstExpr) .

Или какого другого? Или не должен?

В SCADE нет явных циклов. Предоставляются средства для работы с массивами. Поначалу были "slices" (удобные для hardware-реализации), но затем их заменили "итераторами"-функциями:
http://laure.gonnord.org/pro/research/E ... arrays.pdf
https://link.springer.com/content/pdf/1 ... F59130.pdf

Базовые итераторы -- типовые для "функциональщины": map, reduce, fill, map_reduce, forall. С возможностью оптимизаций ("склейки" операций и избегания лишних циклов и построения промежуточных структур). Прочий функционал подключается как "external".

Примечательно, что доступ к элементу массива по индексу запрещён на основе динамических выражений, т.е. допустим доступ только на основе константных выражений, определяемых ещё в compiletime. Даже нет проверок в runtime насчёт корректности диапазонов для массивов.


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Пятница, 08 Декабрь, 2017 21:32 

Зарегистрирован: Вторник, 01 Март, 2011 09:34
Сообщения: 583
Откуда: Москва
PSV100 писал(а):
На сайте Esterel заявлена совместимость в т.ч. и с 60880 для их SCADE, но за подробностями отправляют в службу продаж:
http://www.esterel-technologies.com/ind ... tification
..
В SCADE нет явных циклов.

Если Вы заметили, я упоминал средства здесь, но разумно предоставил слово разработчикам AREVA - их прямым конкурентам.

Можно внимательно ознакомиться с представленной ими Certification Kit и непосредственно сертификатом.
Представленный сертификат:
1. По стандарту 61508, т.е. может быть и 60880, и 62138 - а это уже категории B, C;
2. Сертификат выдан на кодогенератор на обычной ОС, а не на рантайм, где реальное время, циклы и все жесткие требования. Я это упоминал.

Так что, когда столь серьезная компания получит сертификаты, она их обязательно опубликует. А пока ...
Если у Вас будет информация, давайте ссылки, очень полезно!


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

Зарегистрирован: Понедельник, 25 Июнь, 2012 17:26
Сообщения: 473
Дмитрий Дагаев писал(а):
Если Вы заметили, я упоминал средства здесь, но разумно предоставил слово разработчикам AREVA - их прямым конкурентам.

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

Насколько я понял, сертифицированные тулзы должны запускаться на определенных версиях винды, т.е. есть требования к исполнительной среде для самого компилятора и остальных инструментов. А вот конкретика целевых платформ, для которых генерируется код и прочее, не раскрыта.

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

Про SCADE в целом очень мало общедоступной информации про технические детали, на любой чих отсылают в службу продажи. В своих разборках с dataflow-языками я лишь косвенно наблюдал материалы про runtime-платформы или модели исполнения. Здесь в теме были некоторые ссылки. Повторю (с дополнениями), вдруг что-то найдётся полезное. Но ничего не могу уточнить насчёт соответствия каким-то стандартам. Полагаю, при потребности возможен уже более предметный разбор полётов.

"Квази-синхронные" процессы -- совместно работающие (асинхронные) процессы, взаимодействующие через общую память по некоторым правилам (методика была первично обкатана на Airbus-ах):
https://www.lri.fr/~mandel/papiers/Halb ... D-2006.pdf
https://tel.archives-ouvertes.fr/tel-01545630/document

(по первой ссылке -- кратко, по второй -- развёрнуто, с использованием языка Zélus -- подготовка внедрения в SCADE гибридных (дискретно-непрерывная семантика) автоматов).


На глаза попадался Prelude -- язык описания архитектуры в стиле Lustre-like с realtime-ограничениями. Но это уже не Esterel и не SCADE. Краткое введение и диссертация с подробностями:
http://www.cristal.univ-lille.fr/~forge ... -SAC10.pdf
http://www.cristal.univ-lille.fr/~forge ... thesis.pdf

Вокруг него были всякие публикации насчёт платформ, к примеру -- под многоядерные (многопоточные) архитектуры:
http://www2.compute.dtu.dk/~wopu/papers/fmtv14.pdf


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

Зарегистрирован: Понедельник, 25 Июнь, 2012 17:26
Сообщения: 473
PSV100 писал(а):
В SCADE нет явных циклов. Предоставляются средства для работы с массивами. Поначалу были "slices" (удобные для hardware-реализации), но затем их заменили "итераторами"-функциями...

Да, и функционал циклов также реализуется через явные "автоматы" -- конструкция "automaton". К тому же, в целом, тамошние "node" -- сами по себе есть реагирующие автоматы с "вечным" (циклическим) исполнением.

Однако, семантика Lustre подразумевает, что "главная" node (аля "main"-функция в программе, содержащая вызовы прочих суб-node) исполняется после получения всех необходимых входных данных. Т.е. при генерации конечного исполняемого кода (или спецификации для "железа") исходный код для node заворачивается в операции ввода/вывода (и прочего необходимого) согласно требуемой платформе ("главных" node может быть множество). Семантика же императивного языка Esterel заключается в "мгновенной" реакции на возникновение сигнала: при операциях аля "emit" -- "широковещательной" эмиссии данных (сигналов) -- условно сразу же реагируют параллельные процессы (сопрограммы) на ожидающих операциях вида await.
Пример поддержки "мгновенно реагирующей" семантики в самом языке Lustre здесь уже был -- проект InteLus (вроде пока академический, но под крышей Esterel) -- расширение Lustre для дополнительной управляющей логики:
Sheep in wolf’s clothing: Implementation models for data-fl̘ow multi-threaded software

Здесь, прежде всего, многопоточное управление. Базовая модель исчисления "clock"-ов расширяется мат. моделями согласованности операций с памятью, семафорами и пр.


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

Зарегистрирован: Понедельник, 25 Июнь, 2012 17:26
Сообщения: 473
PSV100 писал(а):
Сам императивный язык Esterel был "закрыт" в 2008 г. на версии V7, тюненгованный для hardware-реализации, но проблематичный для эффективной software-реализации, в т.ч. была затруднительна статическая верификация (согласно док-м).

Есть такой язык Quartz -- императивный в стиле Esterel:
http://www.averest.org/

с некоторыми фишками "классики" data-flow (напр., поддержка default-значений для переменных -- символизируют состояние "проводов" в цифровых схемах, когда как прочие "переменные в памяти" -- аля "регистры". Вместо типовых операций вида "pre" -- сохраненные результаты вычислений на предшествующем такте -- используется оператор "next", видимо из-за используемых верификаторов семейства SMV, как NuSMV).

Однако, чтобы программы были "корректными по конструкции", вынужденны были добавить исчисление "clock"-ов, в данном случае на базе языка Signal. Ниже подробнее (где, прежде всего, раскрыта мат. семантика языка Signal в виде операционной интерпретации):
Constructive polychronous systems


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

Зарегистрирован: Понедельник, 25 Июнь, 2012 17:26
Сообщения: 473
Интересна платформа Heptagon (вроде как, здесь также видны следы Esterel по некоторым именам авторов публикаций, всё open source):
http://heptagon.gforge.inria.fr/

Ранее были уже ссылки насчёт расширенной поддержки массивов (с оптимизацией):
http://www.di.ens.fr/~guatto/papers/lctes12.pdf
и реализации асинхронных data-flow процессов:
https://www.di.ens.fr/~pouzet/bib/emsoft12.pdf

Но основное -- поддержка "discrete controller synthesis" -- синтез программ управляющей логики на основе ограничений (язык Lustre расширяется специальными контрактами). Кратко:
Contracts for modular discrete controller synthesis

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

Реализация "fault-tolerant"-техники -- отслеживание "отваливания" процессоров и переброска задач между вычислителями при проблемах:
A formal approach for the synthesis and implementation of fault-tolerant industrial embedded systems

Применение для FPGA:
Autonomic Management of Reconfigurable Embedded Systems using Discrete Control: Application to FPGA

А это пример уже за рамками embedded -- учебный примерчик Java-серверов (синтезируемый Lustre-код может быть скомпилирован в Java) как "сервис новостей" -- переключение режимов работы распределенной системы в зависимости от сетевой нагрузки, политики организации ресурсов и пр.:
Behavioural Model-based Control for Autonomic Software Components

Фреймворк по ссылке выше есть развитие "Nemo":
A Domain-Specific Language for Multi-task Systems, applying Discrete Controller Synthesis


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

Зарегистрирован: Вторник, 01 Март, 2011 09:34
Сообщения: 583
Откуда: Москва
PSV100 писал(а):
Насколько я понял, сертифицированные тулзы должны запускаться на определенных версиях винды, т.е. есть требования к исполнительной среде для самого компилятора и остальных инструментов. А вот конкретика целевых платформ, для которых генерируется код и прочее, не раскрыта.

Кодогенератор SCADE настраивается на целевые платформы, организации-разработчики могут купить этот САПР, который, похоже, действительно сертифицирован по 60880 (я со SCADE не работал). А сертификация уже конкретных целевых платформ - это уже головная боль их производителей, как-то так.


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

Зарегистрирован: Понедельник, 25 Июнь, 2012 17:26
Сообщения: 473
Со стороны так ситуация и выглядит.

В статейке про язык в SCADE (ранее здесь по ссылке) отмечено про "new challenge" в вопросах сертификации -- создание полностью формально верифицированного компилятора, по типу CompCert -- использование прувера (Coq в данном случае) для доказательства соответствия (корректности) целевого генерируемого кода исходной семантике в Lustre-коде. Первый шаг в этом направлении:
A Formally Verified Compiler for Lustre

Видать, своего головняка у них там также хватает.

Тем не менее, для IT в целом платформа даёт неплохие решения. Ранее здесь был упомянут PretC -- расширение для C по мотивам Esterel:
https://hal.inria.fr/hal-00786378/document

У этих же товарищей (причём как минимум один из авторов "светится" в самой Esterel) есть и ForeC -- в аналогичном стиле, только уже под многопоточную платформу (с реальными асинхронными процессами с раздельными исполнителями).
Презентация: http://slideplayer.com/slide/6392145/
Введение: https://hal.inria.fr/hal-00842402/document

Сохраняется семантика "синхронной" модели, что определяет независимость (условно) от диспетчера (шедулинга). Там же предлагается алгоритм для "Mixed-Criticality Systems" -- смешанное управление критически важных по времени задач и не очень (как некое развитие модели Prelude, ранее были ссылки):
http://www.bromans.com/publ/yip-et-al-2 ... cality.pdf

Рекомендую взглянуть, очень таки интересные штуки, причём далеко не только для embedded. Можно наглядно сравнить и оценить (для себя) стили построения систем: императивный и на dataflow-уравнениях. К примеру, на картинке ниже --организация конвейера в ForeC (из презентации выше), ранее здесь неоднократно были ссылки на асинхронные процессы в Heptagon, есть что пощупать, так сказать.
Вложение:
pipelining.png
pipelining.png [ 57.94 КБ | Просмотров: 11360 ]


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

Зарегистрирован: Понедельник, 25 Июнь, 2012 17:26
Сообщения: 473
Вызывает интерес "предикатное" и "автоматное" программирование В.И. Шелехова:
http://forum.drakon.su/viewtopic.php?t=5915

Содержательная дискуссия (и далее по контексту):
http://forum.drakon.su/viewtopic.php?f= ... 07#p100107

Намечается подключение Дракон-а:
http://forum.drakon.su/viewtopic.php?f=143&t=6160

Остановлюсь на любопытной технике "меток" в "гиперфункциях" -- функция может возвращать несколько "меток" -- альтернативные результаты как "переходы". Подробнее:
Шелехов В.И. Язык и технология автоматного программирования
В.И. Шелехов, Э.Г. Тумуров. Технология автоматного программирования на примере программы управления лифтом

Автор (В.И. Шелехов) где-то (в какой-то статье) упоминал, что ему известна лишь единственная схожая техника, с некоторой натяжкой -- в языке Smart в этом проекте:
http://www.provenrun.com/products/proventools/

Описания языка толком нигде нет, пожалуй, единственное (и то -- "капля в море"):
ProvenCore: Towards a Verified Isolation Micro-Kernel

А вот в Lustre/Signal/Esterel идентичный функционал (в некоторой степени) достигается через управление сигналами и переходы в "автоматных" конструкциях. В сопоставлении с языком Signal "метки" выше являются частным случаем, когда "clock"-и выходных сигналов являются взаимоисключающими (по сравнению с Lustre язык Signal имеет расширенную семантику "clock"-исчисления, а также и более широкие средства манипулирования "тактами"). В статейке ниже -- пример реализации "автоматов" в Signal (нет явных конструкций аля "automaton" как в Lustre, автоматы задаются на уравнениях, что позволяет, к примеру, организовывать все возможные реакции на переходы (вход, выход) и пр., есть разные варианты операторов и зарисовок на диаграммах (в др. публикациях)), а также как раз на примерах показана суть теоретико-множественного подхода в понимании "clock"-ов (да, и автоматы здесь также представляются как "гиперпроцессы"):
Polychronous Automata

Однако, вызывают настороженность и недопонимание такие вещи, как "многовходовые" операторы в "автоматном программировании":
http://forum.drakon.su/viewtopic.php?f= ... 60#p100894
Цитата:
...
Циклы и условные операторы станут многовходовыми.
Например, можно будет запрыгнуть на ветку условного оператора напрямую минуя проверку условия.
Возможно, появятся несводимые циклы, т.е. циклы с несколькими точками возврата на начало тела цикла.

При наличии двух и более входов в оператор возможно следующее решение:
декомпозировать (устранить) такой оператор с помощью операторов перехода.
Тогда в дополнение к иерархической операторной структуре появляется набор кусков кода,
завершающихся переходом на другой кусок кода.

http://forum.drakon.su/viewtopic.php?f= ... 60#p100904
Цитата:
...
Реализация автомата через DSL (Domain-Specific Language) это еще одно проявление отрыжки структурного программирования.

Сложно понять, что намечается насчёт "многовходовости". А Esterel-платформа демонстрирует вполне жёсткую структурность. Прыгнуть куда-то, минуя проверку условия -- нарушить "clock"-исчисление, недопустимо.


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

Зарегистрирован: Понедельник, 25 Июнь, 2012 17:26
Сообщения: 473
Цитата:
Исходя из рекомендаций к коду для атомных станций, которые регламентируют, что цикл должен иметь константное максимальное количество итераций и того, что в общем случае проанализировать количество итераций для инструментальных средств может быть затруднительным, то, по-хорошему, язык должен предоставлять цикл подобного вида ...

Кроме итераторов и автоматов (в этой презентации: "From Lustre to Lucid Synchrone" есть акцент на конструкциях автомата, мол в текстовом языке они удобнее по сравнению с типовыми диаграммами в SCADE, Simulink/Stateflow, LabView, Modelica и пр.), организующих функционал циклов (здесь уже были соответствующие заметки), как минимум в академической версии Lustre имеются и "пользовательские" рекурсии (краткая документация по языку):
Код:
node consensus_gen<<const n: int>>(T: bool^n) returns (a: bool);
let
    a = with (n = 1)
        then T[0]
        else T[0] and consensus_gen << n-1 >> (T[1 .. n-1]);
tel;

-- примеры использования:

node consensus = consensus_gen<<8>>;

node use_recursive_nodes (T : bool^4) returns (c : bool);
let
    c = consensus_gen<<4>>(T);
tel

, где оператор with применяется к статическим параметрам.

Илья Ермаков писал(а):
Там у них, конечно, довольно ограниченный формализм описания поведения: КА + dataflow.

Фактически, по грубой оценке, условная вычислительная мощность ограничена лишь требованиями предметки -- статически выделенные объекты. Причём на борту достаточно упрощённых средств для обобщённого кода -- полиморфизм, включая параметрический, вплоть до модульности по мотивам Ada или ML, примеры:
https://github.com/jahierwan/lustre-exa ... model2.lus
https://github.com/jahierwan/lustre-exa ... _model.lus


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Пятница, 19 Январь, 2018 18:53 

Зарегистрирован: Понедельник, 25 Июнь, 2012 17:26
Сообщения: 473
В рамках исследовательской группы под крышей ANSYS/Esterel наблюдается любопытный проект: ADFG (Affine dataflow graphs) -- тулза для генерации алгоритмов планировщика задач, где модель взаимодействующих (через условные токены) процессов представляется в виде dataflow-графа (Cyclo-Static DataFlow):
ADFG: a scheduling synthesis tool for dataflow graphs in real-time systems

В том числе подразумевается и поддержка SCJ -- Safety-Critical Java, в старых публикациях подробнее:
Design of Safety-Critical Java Level 1 Applications Using Affine Abstract Clocks
Презентация: Design of Safety-Critical Java Applications Using Affine Abstract Clocks

Собственно, в данном посте основное внимание обращаю на Safety-Critical Java -- интересный профиль:
https://jcp.org/en/jsr/detail?id=302

, возникший в рамках проекта CJ4ES -- The Certifiable Java for Embedded Systems, как некая попытка слепить стандарт в помощь для прохождения сертификации (с учётом опыта прочих профилей аля MISRA C, Ravenscar для Ada и др.). Краткое введение:
Certifiable Java for Embedded Systems

Профиль Safety-Critical Java частично основан на профиле RTSJ (Real-time Specification for Java). В публикации ниже представлена реализация SCJ поверх JOP -- Java Optimized Processor на FPGA, где как раз сжато раскрыты все основные аспекты, решаемые проблемы:
Safety-Critical Java for Embedded Systems

Стандарт SCJ не завершён, и пока непонятно его будущее. Но, как минимум, он повлиял на новые готовящиеся спецификации RTSJ версии 2:
https://www.aicas.com/cms/sites/default/files/rtsj_63.pdf
Презентация: https://www.aicas.com/cms/sites/default/files/rtsj-and-iot.pdf

Очень поверхностно об архитектуре профиля SCJ. Исполняемые задачи оформляются в виде специальных классов с необходимыми обработчиками событий ("акторы" в модели ADFG выше). Классы объединяются в кооперацию -- "миссию", которая ими управляет. Для миссии выделяются три фазы: инициализации, активного исполнения (где, как правило, действуют временные ограничения) и завершения, после чего миссия может запустить иную миссию. Вводятся три уровня в профиле (с увеличением уровня сложности и проблемности верификации/сертификации): 0 -- где предусматривается только циклическое исполнение обработчиков событий (периодические события), 1 -- подразумеваются периодические и апериодические события, но обработчики не могут себя прерывать/возобновлять (т.е. самостоятельно блокировать/управлять потоками), 2 -- дополнительно возможны и самостоятельные потоки, вложенные миссии и др.
Кратко о понятии уровней и о нечёткости декларации, что именно есть 2-й уровень:
Safety-Critical Java Level 2: Motivations, Example Applications and Issues

Ключевой и один из самых проблемных аспектов -- управление памятью. В отличие от RTSJ в SCJ не предусматривается использование сборщика мусора -- пока нет единой технологии, пригодной универсально для стандарта. Декларируется организация памяти на основе иерархических регионов (по мотивам RTSJ (этот профиль имеет и регионы, и GC), но с изменениями, с детерминизмом операций с памятью по времени, размеру, с предотвращением фрагментации). В публикации выше с примером SCJ на JOP приведена основная проблематика и принципы использования памяти, плюс:
Memory Safety for Safety Critical Java

В результате, как минимум, стандартные контейнеры данных должны предусматривать максимальную ёмкость.
Кстати, циклы в языке должны задаваться с учётом максимального количества итераций, аля:
Код:
// вместо:
for(Entry e = tab[i]; e != null; e = e.next)

// оформлять так:
Entry e = tab[i];
for (int j = 0; j < entries.length; j++) {
    if (e == null) break;
    ...
    e = e.next;
}

В презентации ниже -- некая критика стандарта (на момент 2011 г.), в т.ч. "памяти" также "досталось" -- очень муторно применять:
Harmonizing Alternative Approaches to Safety-Critical Development with Java

А в последней редакции стандарта SCJ (за 2017 г.) убрали аннотации для указания регионов (реализацию "удобств" поверх базового API возлагают на вендоров). Однако, к примеру, вот такие академические попытки на основе спецтипизации -- тоже "на любителя":
Ownership Types for Safe Region-Based Memory Management in Real-Time Java

А вот такие техники, скорее всего, будут основами коммерческих решений:
Cooperative Memory Management in Safety-Critical Embedded Systems

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

А, в целом, представленные материалы -- не только для сферы embedded -- для всех интересующихся эффективной архитектурой ПО.
По ходу дела вспомнилась ссылка на reddit, где-то на форуме указывали:
https://www.reddit.com/r/programming/comments/698yyc/memory_leaks_on_missiles_dont_matter_so_long_as/dh4v8hj/
Цитата:
Here is something that was described to me as a real production configuration that was done to solve memory leaking everywhere.

It was a Java service taking fairly high amount of traffic. In order to get consistent response times they setup this configuration in each machine:

1) Each machine runs 4 JVMs. 2) 1 JVM that is starting up 3) 1 JVM that is shutting down 4) 2 JVMs that are serving traffic. 5) Every 2 minutes a JVM starts/stops. 6) No JVM lives for more than 8 minutes.

I found that to be both horrifying and a rather clever way to work around the problem.

Некоторые рецепты решения подобных проблем есть в материалах выше.
Кстати, для оракловской JVM также встречаются предложения по улучшению сборки мусора, например -- расширение стандартного мусорщика "регионами" -- динамическими "поколениями":
NG2C: Pretenuring Garbage Collection with Dynamic Generations for HotSpot Big Data Applications
Презентация: http://www.gsd.inesc-id.pt/~rbruno/publications/rbruno-ismm17-slides.pdf

Или для Substrate VM:
Safe and Efficient Hybrid Memory Management for Java
Презентация: http://www.oracle.com/technetwork/java/jvmls2015-wimmer-2637907.pdf


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Пятница, 19 Январь, 2018 19:31 
Аватара пользователя

Зарегистрирован: Воскресенье, 12 Апрель, 2015 18:12
Сообщения: 1134
Откуда: СССР v2.0 rc 1
Я правильно понимаю: взяли инструмент с исходно кривыми ручками, неудобными рабочими частями, и теперь страдая и потея пытаются исправить инструмент под давно назревшие задачи?))


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Пятница, 19 Январь, 2018 19:38 

Зарегистрирован: Вторник, 01 Март, 2011 09:34
Сообщения: 583
Откуда: Москва
Во-первых, ой, как интересно!
Во-вторых, бросилось в глаза из https://jcp.org/en/jsr/detail?id=302 требование:
Цитата:
2.5 What need of the Java community will be addressed by the proposed specification?
Safety critical systems need a certifiable (e.g., DO-178B) Java environment. Certifiability implies hard real-time resource management and generally very small implementations with low complexity.

2.6 Why isn't this need met by existing specifications?
The existing J2ME and RTSJ (JSR-1) specifications contain too many functions, and many of their functions are much more complex than can be made certifiable. For example, J2ME and the RTSJ assume the presence of a garbage collector; the proposed specification will not assume the presence of a garbage collector.

Я разбираюсь в атомных стандартах, не в авиационных стандартах, но заявляется "всего лишь" DO-178B. А наиболее жесткие требования в 60880, а потом и DO-178A. А DO-178B уже попроще, или я неправ?


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Понедельник, 22 Январь, 2018 19:21 

Зарегистрирован: Понедельник, 25 Июнь, 2012 17:26
Сообщения: 473
Дмитрий Дагаев писал(а):
Я разбираюсь в атомных стандартах, не в авиационных стандартах, но заявляется "всего лишь" DO-178B. А наиболее жесткие требования в 60880, а потом и DO-178A. А DO-178B уже попроще, или я неправ?

Увы, я не спец в сертификации и не смогу стандарты квалифицировано охарактеризовать. В отношение профиля SCJ -- на сегодня не наблюдаются явные декларации, однозначно определяющие стандарты, мол использование такого-то API при таких-то правилах соответствует такому-то стандарту (м.б. таковы инструкции где-то имеются, но пока мною не замечены). Приведены лишь общие слова, мол есть потребность в "certifiability", например под такой-то стандарт, и тут же: "as well as other safety-critical standards" (во всяком случае, как минимум, так указано в оф. редакции профиля). А тема авионики заметна в тех краях, к примеру, и в постановках задач для тестирования (бенчмарки). Видимо, сказывается факт того, кто там является основным проталкивателем (представители всяких Boeing-ов есть и в комитете).


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

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


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

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


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

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