Язык координации Рео

Язык ^[1]^[2] — это предметно-ориентированный язык для программирования и анализа протоколов координации, которые объединяют отдельные процессы в полные системы в широком понимании. Примеры классов систем, которые можно составить с помощью Reo, включают на основе компонентов системы , сервис-ориентированные системы, многопоточные системы, биологические системы и криптографические протоколы. Reo имеет графический синтаксис, в котором каждая программа Reo, называемая соединителем или схемой , представляет собой помеченный направленный гиперграф . Такой график представляет поток данных между процессами в системе. Reo имеет формальную семантику , которая лежит в основе различных методов формальной проверки и инструментов компиляции.

Определения

В Reo параллельная система состоит из набора компонентов, склеенных вместе схемой, обеспечивающей поток данных между компонентами. Компоненты могут выполнять операции ввода-вывода на граничных узлах схемы, к которой они подключены. Существует два типа операций ввода-вывода: запросы put отправляют элементы данных на узел, а запросы get извлекают элементы данных из узла. Все операции ввода-вывода блокируются, что означает, что компонент может продолжить работу только после успешной обработки ожидающей операции ввода-вывода.

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

Формально структура схемы определяется следующим образом:

Определение 1. Схема – это тройка $R=(N,B,C,t)$ где:

$N$ — набор узлов ;
$B\subseteq N$ – набор граничных узлов ;
$C\subseteq 2^{N}\times 2^{N}$ представляет собой набор каналов ;
$t:C\rightarrow T$ присваивает типы каждому каналу.

такой, что $|I\cup O|=2$ , для всех $(I,O)\in C$ . Если $c=(I,O)\in C$ является каналом, то $I$ называется набором входных узлов $c$ , а $O$ называется набором выходных узлов $c$ .

Динамика схемы напоминает поток сигналов через электронную схему .

Узлы имеют фиксированное поведение репликатора слияния: данные одного из входящих каналов распространяются на все исходящие каналы без сохранения или изменения данных (т. е. поведение репликатора). Если несколько входящих каналов могут предоставлять данные, узел делает недетерминированный выбор среди них (т. е. поведение слияния). Узлы, имеющие только входящие или исходящие каналы, называются узлами-приемниками или узлами-источниками соответственно; узлы, имеющие как входящие, так и исходящие каналы, называются смешанными узлами .

В отличие от узлов, каналы имеют определяемое пользователем поведение, представленное их типом. Это означает, что каналы могут хранить или изменять элементы данных, проходящие через них. Хотя каждый канал соединяет ровно два узла, эти узлы не обязательно должны быть входными и выходными. Например, вертикальный канал на рисунке в правом верхнем углу имеет два входа и не имеет выходов. Тип канала определяет поведение канала по отношению к данным. Ниже приведен список распространенных типов:

$Синхронизация$ : атомарно получает данные со своего входного узла и передает их на выходной узел.
$LossySync$ : То же, что и Sync, но может потерять данные, если его выходной узел не готов принимать данные.
$Fifo ⟨ n ⟩$ : получает данные из своего входного узла, временно сохраняет их во внутреннем буфере размера $n$ и передает их на свой выходной узел (всякий раз, когда этот выходной узел готов принять данные).
$SyncDrain$ : атомарно получает данные из обоих входных узлов и теряет их.
$Фильтр ⟨ c ⟩$ : атомарно получает данные из своего входного узла и передает их в свой выходной узел, если условие фильтра $c$ удовлетворено; в противном случае теряет данные.

Свойства программной инженерии

Экзогенность

Один из способов классифицировать координационные языки - это их локус : локус координации относится к тому, где происходит координационная деятельность, классифицируя координационные модели и языки как эндогенные или экзогенные . ^[3] Эндогенные модели и языки, такие как Linda , предоставляют примитивы, которые необходимо включить в вычисления для их координации. В приложениях, использующих такие модели, примитивы, влияющие на координацию каждого модуля, находятся внутри самого модуля. Напротив, Reo — это экзогенный язык, предоставляющий примитивы, поддерживающие координацию сущностей извне. В приложениях, использующих экзогенные модели, примитивы, влияющие на координацию каждого модуля, находятся вне самого модуля.

Эндогенные модели иногда более естественны для конкретного приложения. Однако они обычно приводят к смешиванию примитивов координации с вычислительным кодом, что запутывает семантику вычислений с протоколами координации. Такое смешивание имеет тенденцию разбрасывать примитивы связи/координации по всему исходному коду, делая модель сотрудничества и протокол координации приложения туманными и неявными: как правило, нет фрагмента исходного кода, который можно было бы идентифицировать как модель сотрудничества или протокол координации приложения. , которые можно проектировать, разрабатывать, отлаживать, поддерживать и повторно использовать отдельно от остального кода приложения. С другой стороны, экзогенные модели стимулируют разработку координационных модулей отдельно и независимо от вычислительных модулей, которые они должны координировать. Следовательно, результат значительных усилий, вложенных в проектирование и разработку компонента координации приложения, может проявиться в виде осязаемых «чистых модулей координации», которые легче понять и которые также можно повторно использовать в других приложениях.

Композиционность/многоразовость

Схемы Рео являются композиционными. Это означает, что можно создавать сложные схемы, повторно используя более простые схемы. Чтобы быть более явным, две цепи можно склеить в своих граничных узлах, чтобы сформировать новую объединенную цепь. В отличие от многих других моделей параллелизма (например, пи-исчисления ), синхронность сохраняется при композиции. Это означает, что если мы составим контур с синхронным потоком между узлами A и B с другим контуром с синхронным потоком между узлами B и C, то в объединенном контуре будет синхронный поток между узлами A и C. Другими словами, композиция двух синхронных цепей дает синхронную схему.

Семантика

Семантика схемы Рео — это формальное описание ее поведения. Существуют различные семантики Рео. ^[4]

Исторически первая семантика Рео была основана на коалгебраическом понятии потоков (т.е. бесконечных последовательностей). ^[5] Эта семантика основана на концепции синхронизированного потока данных , который представляет собой пару, состоящую из потока элементов данных и потока монотонно возрастающих меток времени (действительных чисел). Связав каждый узел с таким синхронизированным потоком данных, поведение канала можно смоделировать как отношение к потокам на подключенных узлах.

Позже была разработана автоматная семантика, получившая название автоматов с ограничениями . ^[6] Автомат ограничений — это помеченная система переходов, в которой метки перехода состоят из ограничения синхронизации и ограничения данных . Ограничение синхронизации определяет, какие узлы синхронизируются на этапе выполнения, моделируемом переходом, а ограничение данных указывает, какие элементы данных передаются по этим узлам.

Одним из ограничений автоматов с ограничениями (и синхронизированных потоков данных) является то, что они не могут напрямую моделировать контекстно-зависимое поведение, когда поведение канала зависит от (не)доступности ожидающей операции ввода-вывода. Например, используя автоматы с ограничениями, невозможно напрямую смоделировать поведение LossySync, который должен терять данные только в том случае, если его выходной узел не имеет ожидающего запроса на получение. Для решения этой проблемы была разработана еще одна семантика Reo, называемая раскраской коннектора . ^[7]

Другая семантика Reo позволяет моделировать синхронизированные ^[8] или вероятностный ^[9] поведение.

Реализации

Расширяемые инструменты координации (ECT) — это набор плагинов для Eclipse , которые составляют интегрированную среду разработки (IDE) для Reo. ECT состоит из графического редактора для рисования схем и механизма анимации для анимации потока данных через схемы. Для генерации кода ECT содержит компилятор Reo-to-Java, который генерирует код для схем на основе семантики их автоматов ограничений. В частности, на входе схемы Reo он создает класс Java, который имитирует автомат с ограничениями, моделирующий схему. Для проверки ECT содержит инструмент, который преобразует схемы Reo в определения процессов в mCRL2 . Пользователи впоследствии могут использовать mCRL2 для проверки модели на соответствие спецификациям свойств мю-исчисления . (В качестве альтернативы средство проверки моделей Vereofy также поддерживает проверку схем Reo.)

Другая реализация Reo разработана на языке программирования Scala и выполняет схемы распределенным образом. ^[10]

Ссылки

^ Фархад Арбаб: Reo: модель координации на основе каналов для композиции компонентов . Математические структуры в информатике 14(3):329–366, 2004.
^ Фархад Арбаб: Слойка, Магический протокол . В Гуль Аге, Оливье Данви, Хосе Месегере, редакторах, Talcott Festschrift, том 7000 LNCS, страницы 169–206. Спрингер, 2011.
^ Фархад Арбаб: Состав взаимодействующих вычислений . Дина Голдин, Скотт Смолка и Питер Вегнер, редакторы журнала Interactive Computation, страницы 277–321. Спрингер, 2006.
^ Сунг-Шик Джонгманс и Фархад Арбаб: Обзор тридцати семантических формализмов для Рео . Научные анналы информатики 22(1):201-251, 2012.
^ Фархад Арбаб и Ян Руттен: Коиндуктивный расчет соединителей компонентов . Мартин Вирсинг, Дирк Паттинсон и Рольф Хенникер, редакторы, Proceedings of WADT 2002, том 2755 LNCS, страницы 34–55. Спрингер, 2003.
^ Кристель Байер , Марджан Сирджани, Фархад Арбаб и Ян Руттен: Моделирование соединителей компонентов в Reo с помощью автоматов ограничений . Наука компьютерного программирования 61(2):75-113, 2006.
^ Дэйв Кларк, Дэвид Коста и Фархад Арбаб: Раскраска соединителя I: Синхронизация и зависимость от контекста . Наука компьютерного программирования 66(3):205-225, 2007.
^ Фархад Арбаб, Кристель Байер , Франк де Бур и Ян Руттен: Модели и временные логические спецификации для соединителей компонентов с синхронизацией . Программное обеспечение и моделирование систем 6(1):59-82, 2007.
^ Кристель Байер : Вероятностные модели для цепей соединителей Reo . Журнал универсальной информатики 11 (10): 1718–1748, 2005.
^ Хосе Проэнса: Синхронная координация распределенных компонентов . Кандидатская диссертация, Лейденский университет, 2011 г.

Внешние ссылки

Сайт Рео

[1] Фархад Арбаб: Reo: модель координации на основе каналов для композиции компонентов . Математические структуры в информатике 14(3):329–366, 2004.

[2] Фархад Арбаб: Слойка, Магический протокол . В Гуль Аге, Оливье Данви, Хосе Месегере, редакторах, Talcott Festschrift, том 7000 LNCS, страницы 169–206. Спрингер, 2011.

[3] Фархад Арбаб: Состав взаимодействующих вычислений . Дина Голдин, Скотт Смолка и Питер Вегнер, редакторы журнала Interactive Computation, страницы 277–321. Спрингер, 2006.

[4] Сунг-Шик Джонгманс и Фархад Арбаб: Обзор тридцати семантических формализмов для Рео . Научные анналы информатики 22(1):201-251, 2012.

[5] Фархад Арбаб и Ян Руттен: Коиндуктивный расчет соединителей компонентов . Мартин Вирсинг, Дирк Паттинсон и Рольф Хенникер, редакторы, Proceedings of WADT 2002, том 2755 LNCS, страницы 34–55. Спрингер, 2003.

[6] Кристель Байер , Марджан Сирджани, Фархад Арбаб и Ян Руттен: Моделирование соединителей компонентов в Reo с помощью автоматов ограничений . Наука компьютерного программирования 61(2):75-113, 2006.

[7] Дэйв Кларк, Дэвид Коста и Фархад Арбаб: Раскраска соединителя I: Синхронизация и зависимость от контекста . Наука компьютерного программирования 66(3):205-225, 2007.

[8] Фархад Арбаб, Кристель Байер , Франк де Бур и Ян Руттен: Модели и временные логические спецификации для соединителей компонентов с синхронизацией . Программное обеспечение и моделирование систем 6(1):59-82, 2007.

[9] Кристель Байер : Вероятностные модели для цепей соединителей Reo . Журнал универсальной информатики 11 (10): 1718–1748, 2005.

[10] Хосе Проэнса: Синхронная координация распределенных компонентов . Кандидатская диссертация, Лейденский университет, 2011 г.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]