Автомат ввода / вывода - Input/output automaton

Автоматы ввода / вывода предоставляют формальную модель , применимую для описания большинства типов асинхронных параллельных систем . Сама по себе модель автомата ввода-вывода содержит очень простую структуру, которая позволяет моделировать различные типы распределенных систем . Для описания конкретных типов асинхронных систем к этой базовой модели необходимо добавить дополнительную структуру. Модель представляет собой явный метод описания и рассуждения о компонентах системы, таких как процессы и каналы сообщений, которые взаимодействуют друг с другом, работая с произвольной относительной скоростью. Автоматы ввода-вывода были впервые представлены Нэнси А. Линч и Марком Р. Таттлом в «Иерархических доказательствах корректности для распределенных алгоритмов», 1987.

«Автомат ввода-вывода моделирует компонент распределенной системы, который может взаимодействовать с другими компонентами системы. Это простой тип конечного автомата, в котором переходы связаны с именованными действиями ». Есть три типа действий: ввод , вывод и внутренние действия. Автомат использует свои входные и выходные действия для связи со своей средой, тогда как внутренние действия видны только самому автомату. В отличие от внутренних и выходных действий, которые выбираются и выполняются автоматом, входные действия, которые просто поступают из окружающей среды, не контролируются автоматом.

Примеры

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

Автомат ввода / вывода процесса

На рисунке 1 показан пример автомата ввода-вывода для процесса в асинхронной распределенной системе с передачей сообщений. В этом случае процесс P _i взаимодействует с другими процессами с помощью системы передачи сообщений. Его выходные действия имеют форму send (m) _{i, j} , которая представляет процесс P _i, отправляющий сообщение с содержимым m процессу P _j . Действия ввода имеют форму receive (m) _{k, i} , представляющую получение сообщения с содержанием m процессом P _i от процесса P _k . (Внутренние действия P _i , которые соответствовали бы алгоритму, в котором выполняется процесс, не показаны.)

Канал сообщений FIFO

Канал сообщений также можно смоделировать с помощью автомата ввода-вывода. На рисунке 2 показан типичный автомат однонаправленного канала FIFO с именем C _{i, j} . Он имеет действия ввода формы send (m) _{i, j} и действия вывода формы receive (m) _{i, j} . Каждое сообщение m может содержать 0 или 1 (m ∈ {0,1}). Состояние автомата хранит очередь FIFO всех сообщений, которые были отправлены, но еще не получены.

В типичной распределенной системе, где существуют как технологические автоматы, так и автоматы каналов связи, они составлены таким образом, что выходные действия одного автомата сопоставляются и выполняются с идентично названными входными действиями других автоматов. Например, рассмотрим систему, состоящую из двух процессов, P _i и P _j , и канала связи C _{i, j} от процесса P _i к процессу P _j . В этой настройке процесс P _i выполняет действие вывода send (m) _{i, j} , если и только если канал C _{i, j} также выполняет свое действие ввода send (m) _{i, j} .

Атомарный регистр чтения / записи

На рисунке 3 показан атомарный автомат ввода-вывода регистров чтения / записи в системе с общей памятью с двумя процессами, P ₁ и P ₂ . Значение V, хранящееся в регистре, имеет целочисленный тип (V ∈ Z ). Состояние автомата хранит это значение. Действия ввода состоят из записи _i (V), которая представляет процесс P _i, запрашивающего запись значения V в регистр (где i ∈ {1,2} и V ∈ Z ), и чтения _i , что соответствует процессу P _i. запрашивает чтение значения, хранящегося в данный момент в регистре. Выходное действие ack _i используется для информирования процесса P _i об успешном завершении запроса на запись. Выходное действие V _i представляет значение V, возвращаемое как ответ на запрос чтения процессом P _i .

Автомат также включает внутренние действия perform_Write (V), которые записывают значение V в регистр (путем обновления состояния автомата), и perform_Read, которые используются для чтения значения V, хранящегося в состоянии. (Эти внутренние действия не показаны на рисунке 3.)

Формальная спецификация

Автомат ввода-вывода A или просто автомат состоит из пяти компонентов:

• сиг (А)
• состояния (A)
• начать)
• транс (А)
• задачи (A)

Эти пять компонентов описаны ниже.

Подпись

Первым шагом в формализации автомата ввода-вывода A является определение его сигнатуры sig (A). Сигнатура S описывает действия автомата ввода-вывода с помощью трех непересекающихся наборов действий:

1. in (S): входные действия,
2. out (S): выходные действия, и
3. int (S): внутренние действия.

На основе описанной выше формализации ввода, вывода и внутренних действий можно определить следующие объекты.

• ext (S): внешние воздействия , определенные как в (S) ∪ out (S)
• local (S): локально управляемые действия , определяемые как out (S) ∪ int (S)
• extsig (S): внешняя подпись , определяемая как (in (S), out (S), ø)
• Act (S) определяется как множество всех действий сигнатуры S.

состояния

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

Отношение перехода

Отношение перехода между состояниями автомата A обозначается trans (A) ⊆ состояния (A) × действия (sig (A)) × состояния (A). Он удовлетворяет тому свойству, что «для каждого состояния s и каждого входного действия π существует переход (s, π, s ') ∈ trans (A)».

Переход, также известный как шаг автомата ввода-вывода A, определяется как элемент (s, π, s ') trans (A). Входной переход относится к переходу (с, п, с «) , когда π является входным действием, выход перехода указывает на переход (с, п, с») , когда π является выходным действие и так далее. Для любого состояния s и действия π, если автомат ввода-вывода A имеет некоторый переход вида (s, π, s '), то говорят, что π разрешен в s. Автоматы ввода- вывода описываются как доступные для ввода, поскольку все действия ввода должны быть разрешены в каждом состоянии. Состояние покоя s определяется как состояние, в котором разрешены только действия ввода.

Задания

Пятый компонент автомата ввода-вывода A, задачи (A), является разделом задач, определенным как отношение эквивалентности для локально управляемых действий A, которое имеет не более чем счетное количество классов эквивалентности . Неформально, раздел задач (A) представляет собой абстрактное описание «задач» или «потоков управления» внутри A.

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

Пример: формальное определение автомата ввода / вывода канала

Как описано выше, C _{i, j} является примером автомата ввода-вывода, который представляет однонаправленный канал FIFO от процесса P _i к процессу P _j . Пусть m - двоичное сообщение: m ∈ {0,1}. Автомат C _{i, j} формально можно определить следующим образом.

Подпись:

sig (C _{i, j} ) указывает, что автомат имеет два типа действий:

• Входное действие (C _{i, j} ) имеет вид send (m) _{i, j} , где m ∈ {0,1}.
• Выходное действие (C _{i, j} ) имеет вид receive (m) _{i, j} , где m ∈ {0,1}.

Интуитивно понятно, что действие send (m) _{i, j} указывает, что сообщение m вошло в канал, когда оно отправлено процессом P _i, а действие receive (m) _{i, j} указывает, что сообщение m покинуло канал, когда оно отправлено. доставлено в процесс P _j .

Состояния:

состояния (C _{i, j} ) - это множество всех конечных последовательностей элементов m ∈ {0,1}. Интуитивно состояние представляет собой последовательность сообщений, находящихся в настоящее время на пути от отправителя, процесса P _i , к получателю, процессу P _j , в порядке их отправки.

start (C _{i, j} ), представляющий начальные состояния очереди , содержит только пустую последовательность.

Переходы

Отношение перехода можно смоделировать в стиле предварительного условия-эффекта , где все переходы, включающие каждый конкретный тип действия, сгруппированы в один фрагмент кода. В этом коде условия, которые должны быть выполнены, прежде чем разрешить выполнение действия, формализованы как предикат для предварительного состояния s, которое является состоянием до того, как действие произойдет. Последующие изменения состояния, возникающие в результате выполнения действия, кодируются в виде простой программы. Эта программа выполняется неделимо, как единый переход. Если эта программа применяется к состоянию s, получается новое состояние s '.

Переходы C _{i, j} описываются как:

для send (m) _{i, j} :

• Предварительное условие: Нет
• Эффект: m добавляется в конец последовательности, хранящейся в состоянии (где m ∈ {1,0})

для получения (m) _{i, j} :

• Предварительное условие: m - это первый элемент в последовательности, хранящейся в состоянии (где m ∈ {1,0})
• Эффект: удалить первый элемент последовательности, хранящейся в состоянии

Интуитивно понятно, что действие отправки может быть выполнено в любое время; это вызывает добавление сообщения m в конец очереди сообщений в канале che. Действие приема удаляет и возвращает первый элемент очереди.

Задания

tasks (C _{i, j} ) представляет собой раздел задач, который объединяет все действия формы получения в одну задачу. Интуитивно понятно, что передача сообщений процессу P _j рассматривается как отдельная задача.

{receive(m)i,j : m ∈ {0,1}}.

Исполнение и отслеживание

Исполнение

При запуске автомата генерируется строка , описывающая поведение компонента, моделируемого автоматом. "Фрагмент выполнения автомата ввода-вывода A либо

• конечная последовательность, s ₀ , π ₁ , s ₁ , π ₂ , ..., π _r , s _r , или
• бесконечная последовательность, s ₀ , π ₁ , s ₁ , π ₂ , ..., π _r , s _r , ...,

чередующихся состояний и действий A такие, что (s _k , π _{k + 1} , s _{k + 1} ) является переходом A для любого k ≥ 0. "

Конечная последовательность должна заканчиваться состоянием. Исполнение определяются как фрагмент исполнения , который начинается с начальным состоянием. Набор исполнений A представлен execs (A) . Достижимо состояние , в I / O автомат А конечное состояние конечного исполнения А.

Предположим, что α - конечный фрагмент выполнения A, заканчивающийся состоянием s _f . Далее предположим, что α '- это любой фрагмент выполнения A, который начинается с s _f , последнего состояния α. В этом случае последовательность, полученная путем объединения α и α 'и исключения дублирования s _f , последнего состояния α, представлена ​​как α.α'. Эта последовательность также является исполняемым фрагментом автомата ввода-вывода A.

След

След автомата ввода-вывода A - это последовательность внешних действий, которая происходит при некотором выполнении α автомата A. Множество всех следов A представляется как следы (A) .

Пример: три казни

Выполнения a, b и c - это три выполнения автомата C _{i, j,} описанного в Формальном определении автомата ввода-вывода канала (где сообщение m ∈ {0, 1}). В этом примере состояния указаны путем помещения в скобки последовательности сообщений в очереди; пустая последовательность представлена ​​λ.

(a) [λ], отправить (1) _{i, j} , [1], получить (1) _{i, j} , [λ], отправить (0) _{i, j} , [0], получить (0) _{i, j} , [λ]

(b) [λ], отправить (1) _{i, j} , [1], получить (1) _{i, j} , [λ], отправить (0) _{i, j} , [0]

(c) [λ], отправить (1) _{i, j} , [1], отправить (1) _{i, j} , [11], отправить (0) _{i, j} , [110] ....

Операции над автоматами

Составная операция

Можно составить несколько автоматов, каждый из которых описывает отдельные компоненты системы, чтобы получить автомат, который представляет более крупную и более сложную систему. В этом случае действия, имеющие одно и то же имя в каждом из составляющих автоматов, идентифицируются вместе. Следовательно, когда компонентный автомат делает шаг, который включает действие π, все остальные компонентные автоматы с π в своих сигнатурах также выполняют это действие. Ниже изложены условия, при которых композиция автоматов A и A 'разрешена:

1. Внутренние действия A не должны пересекаться с действиями A '. Это предотвращает выполнение шага в A ', когда выполняются внутренние действия A - с тем же именем, что и действия A'.
2. Выходные действия A и A 'не должны пересекаться. Это условие гарантирует, что только один составляющий автомат контролирует выполнение выходного действия.

Если композиция построена из счетно бесконечного набора автоматов, то существует дополнительное ограничение: каждое действие должно быть действием только конечного числа составляющих автоматов. Бесконечная композиция автоматов позволяет моделировать логические системы, которые могут быть построены из многих логических компонентов. Логическая система часто реализуется на физической системе , которая содержит меньшее количество компонентов.

Пример: композиция

На рисунке 4 изображена композиция из двух процессов P _i и P _j и канала сообщений FIFO C _{i, j} , соответствующих выходным действиям одного автомата с идентично названными входными действиями других автоматов. Таким образом, вывод send (m) _{i, j,} выполняемый процессом P _i , сопоставляется и выполняется с вводом send (m) _{i, j,} выполняемым каналом C _{i, j} .

Процесс P _i отправляет сообщение m, где m ∈ {1,0}, через канал C _{i, j} процессу P _j . Процесс P _j меняет бит в полученном сообщении m от P _i, используя свое внутреннее действие в обратном направлении - не показано на рисунке - и пересылает сообщение в другие части системы.

Скрытие операции

Можно скрыть выходные действия автомата ввода-вывода посредством «переклассификации их как внутренних действий». Это исключает их связь с другими частями системы. Формально операция сокрытия подписей описывается следующим образом:

Пусть S - подпись и Φ ⊆ out (S). hide _Φ (S) - новая сигнатура S ', где

• in (S ') = in (S)
• out (S ') = out (S) - Φ
• int (S ') = int (S) ∪ Φ

Следовательно, «Если A - автомат и Φ ⊆ out (A), то hide _Φ (A) - автомат A ', полученный из A заменой sig (A) на sig (A') = hide _Φ (sig (A) ). "

Справедливость

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

В автомате ввода-вывода A пусть C представляет класс задач (A). Формально фрагмент выполнения α для A считается справедливым, если для каждого класса C выполняются следующие критерии:

1. «Если α конечно, то C не задействован в конечном состоянии α».
2. «Если α бесконечно, то α содержит либо бесконечно много событий из C, либо бесконечно много вхождений состояний, в которых C не задействован».

Событие определяется как «возникновения какого - либо действия в последовательности, например, выполнение или след.» Основываясь на определении справедливости, «бесконечно часто» каждая задача (или класс эквивалентности C) получает шанс выполнить действие. Когда задача (или класс эквивалентности) C действительно получает возможность выполнить действие, возможны два случая: действие в C включено в текущем состоянии и может быть выполнено, или ни одно из действий в C не разрешено в текущем состоянии и, следовательно, не может быть выполнено. Таким образом, конечное честное выполнение с конечным состоянием S _f может быть определено как выполнение, при котором автомат непрерывно отдает очереди всем задачам циклическим образом, но никакие действия не выполняются, поскольку ни одно из них не разрешено в S _f .

Множество честных выполнений автомата ввода-вывода A представлено fairexecs (A) . Пусть β - это след корректного выполнения A. Тогда β - правильный след A. Набор корректных следов A представлен справедливыми следами (A) .

В примере выполнения выполнение (a) является справедливым, поскольку в его конечном состоянии действие приема не разрешено. Выполнение (b) является конечным, но действие приема разрешено в его конечном состоянии. Следовательно, исполнение (b) несправедливо. Выполнение (c) бесконечно, не содержит событий приема, и во всех точках после первого шага действия приема разрешены. Следовательно, это несправедливое исполнение. Определение справедливости имеет важное свойство: «справедливое исполнение композиции - это композиция справедливого исполнения компонентов», то есть Удовлетворительное (Π _i A _i ) = Π _i Удовлетворительное (A _i ).

Свойства и методы доказательства

Автоматы ввода-вывода обеспечивают точное описание асинхронных систем. Они также используются для формализации и подтверждения «точных утверждений» о том, «что системы могут делать». В этом разделе описывается ряд важных типов свойств. Эти, а также другие свойства и методы доказательства описаны в разделе «Распределенные алгоритмы» .

Свойства разрешения ввода

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

1. Поскольку модель предназначена для работы с произвольными входными данными, основной источник системных ошибок из-за сбоя в обработке неожиданных входных данных устраняется.
2. Свойство разрешения ввода использует «простые представления о внешнем поведении автомата, основанные на последовательностях внешних действий». Доказательства некоторых теорем модели могут быть ошибочными без предположения об этом свойстве.

Свойства трассировки

Поскольку внутренние действия автомата ввода-вывода невидимы для пользователя; автомат ввода-вывода кажется черным ящиком, и пользователь просто видит «следы выполнения автоматом (или честного выполнения)». Некоторые свойства автоматов ввода-вывода и их доказательства обычно формализуются как «свойства их следов или точных следов».

Пусть P - свойство следа; P имеет следующие компоненты:

• sig (P), который представляет собой подпись без внутренних действий
• traces (P), что соответствует набору «последовательностей действий в действиях (sig (P))». Этот набор может быть бесконечным.

Свойство трассировки описывает внешнюю подпись, а также набор (или свойство) последовательностей, просматриваемых в этом интерфейсе. Иногда act (sig (P)) обозначается сокращенной записью act (P). Когда упоминается, что автомат ввода-вывода A удовлетворяет свойству трассировки P, можно иметь в виду (по крайней мере) два разных значения:

1. "extsig (A) = sig (P) and traces (A) ⊆ traces (P)"
2. "extsig (A) = sig (P) and fairtraces (A) ⊆ traces (P)"

Интуитивно это означает, что когда A генерирует внешнее поведение, это разрешено свойством P. Однако для A не требуется фактически представлять каждую трассировку P. Поскольку A поддерживает ввод, то для каждой возможной последовательности действий ввода , fairtraces (A) (и, следовательно, traces (A)) включает в себя ответ A. Если fairtraces (A) ⊆ traces (P) выполняется, то свойство P должно содержать все сгенерированные последовательности.

Свойства безопасности

Интуитивно свойство безопасности означает, что ничего «плохого» не происходит. Более формально, пусть P - свойство трассировки . P является свойством безопасности трассировки или свойством безопасности , если для трасс выполняются следующие критерии (P).

• traces (P) не пуст : что-то плохое не может случиться до наступления каких-либо событий; поэтому наличие непустоты является разумным условием для следов (P).
• traces (P) "префиксно-замкнутый" : пусть β ∈ traces (P) и β 'представляет собой конечный префикс β. В этом случае β' ∈ traces (P). Чтобы уточнить, предположим, что есть след, в котором ничего плохого не происходит. Следовательно, ни в одном префиксе этой трассы ничего плохого не происходит. Таким образом, наличие префикса-замыкания является разумным условием для трассировок (P).
• следы (Р) "предел-закрыто" : Пусть & beta ; ₁ , β ₂ ,. . . представляют собой бесконечную последовательность конечных последовательностей в следах (P). Также предположим, что для каждого i, β _i является префиксом β _{i + 1} . В этом случае уникальная последовательность β, то есть «предел β _i при последовательном порядке расширения», также существует в следах (P). Следовательно, если в трассировке произойдет что-то плохое, то это будет результатом определенного конкретного события в трассировке. Таким образом, наличие предельного замыкания в этом случае является разумным условием для трасс (P).

Свойства живучести

Неформально свойство живости можно интерпретировать как что-то «хорошее» в конечном итоге . Следовательно, независимо от того, что произошло в определенный момент времени, что-то хорошее может случиться когда-нибудь в будущем. Более формально, пусть P будет свойством трассировки . P является свойством живучести следов, или свойством живучести , «если каждая конечная последовательность над актами (P) имеет некоторое расширение в следах (P)».

дальнейшее чтение

• Автомат ввода-вывода по времени : Мерритт, Майкл; Модуньо, Фрэнсесмари; Таттл, Марк Р. (август 1991 г.). «Автоматы с ограничениями по времени (Расширенная аннотация)» . Труды 2-й Международной конференции по теории параллелизма . КОНКУР 91 года. 527 . С. 408–423.
• Вероятностный автомат ввода-вывода : Ву, Сью-Хвей; Смолка, Скотт А .; Старк, Юджин В. (апрель 1997 г.). «Состав и поведение вероятностных автоматов ввода-вывода» (PDF) . Теоретическая информатика . 176 (1–2): 1–38. DOI : 10.1016 / s0304-3975 (97) 00056-X .

Смотрите также

• Связь последовательных процессов
• Актерская модель

использованная литература