Мир протоколов SPIN


Миллион строк кода. Сегодня эта фраза стала эквивалентом риторического вопроса своего времени "А что вы делали до 17-го года?". Если добавить к ней еще и пароль "большой проект", можно смело утверждать, что у вас в руках пропуск в мир "больших технологий".



Миллион строк кода…

…Представляя объем валовой
чугуна и свинца, обалделой тряхнешь головой…
И. Бродский

Да простит читатель автора, но эта часть статьи будет сугубо субъективной. При желании (если, например, вы испытываете неприязнь к материалам такого рода) ее можно пропустить совершенно без ущерба. Но все же…

Как говаривал горлопан и бунтарь, "к любым чертям с матерями катись любая бумажка…". Хотя бы потому, что действительно великие программисты (имена которых даже и не хочется перечислять) "мандата миллиона строк"… не имеют. Один из перечня великих — Никлас Вирт — в свое время жестко и беспрекословно определил барьер сложности программ: 2 тыс. строк кода. За этим пределом начинается кошмар. Но оценка Вирта сугубо технологическая. Если же говорить о сложности программного проекта, учитывая трудности изучения и формализации прикладной области, то окажется, что менее ста строк генератора псевдослучайных чисел Mersenne Twister (MT) несоизмеримо сложнее 100 тыс. строк некоего клиента СУБД. Хотя бы потому, что за "программными крохами" MT скрываются десятилетия кропотливых сложнейших исследований в весьма экзотичных областях теоретической математики, а пресловутое приложение бизнес-класса проектировалось за несколько недель методом неформального анализа функционирования менеджера X компании Y на рабочем месте Z (т. е. фактически представляет собой видение этого функционирования самым активным из проектировщиков).

К чему это отступление? К сожалению, автор не относится к числу людей, "вдохновляемых" размахами. Хуже того, размер программного проекта в понимании автора является симптомом. И если он "дорастает" до сотен тысяч строк (о миллионах уже умолчим) — в этом проекте что-то не так.

Естественно, из правила есть исключения, определяемые только истинностью одного-единственного условия. Имя последнего — время. "Большой проект" воспринимается автором, только если время его активной жизни (проектирование, программирование, эксплуатация, сопровождение, модернизация) составляет десятки лет. Исключения, как правило, гениальны (если предыдущие высказывания были спорными, с этим не согласиться нельзя) — X Window (1,5—2 млн. строк кода), стандартная библиотека C, компилятор языка C (именно C, без всяких расширений), ОС Oberon (со всеми компонентами, как единое целое), ОС Plan 9, ядро ОС Unix, языки Modula-2 и Ada, компонентно-скриптовая среда Tcl/Tk.

Список можно продолжать, но в нем есть нечто общее. А именно, вопреки распространенному мнению, что большие программные проекты — скорее промышленные изделия, чем произведения искусства, автор берется утверждать прямо противоположное. Реальные большие проекты, живущие "долго и счастливо", на самом деле являются исключительными образчиками искусства проектирования и программирования. По мнению автора, этот факт очевиден…

Протоколы

Вступление закончилось, а вот отступлений от главной темы не избежать. Пусть они не будут такими пространными, как в книге, которую неизбежно придется прочитать заинтересовавшимся статьей читателям, но они необходимы. И тема первого главного отступления — протоколы.

Термин этот расхожий, что сразу вынуждает внести ясность. В дальнейшем под "протоколом" будет пониматься набор правил, форматов, процедур, совместно принятый двумя (или более) сторонами для облегчения процесса общения. Как видите, определение не менее емкое и абстрактное, чем "ключевые понятия ООП". К счастью, в действительности это не совсем так (дальше будет понятно почему), а обобщение принято автором умышленно. Дело в том, что предмет нашего обсуждения настолько универсален и всеобъемлющ, что даже к категории "швейцарских ножей" его отнести трудно. Если добавить к изложенным фактам сугубо инструментальный характер этого предмета… Короче говоря, мы сталкиваемся с очередной "маленькой бездной", требующей серьезных затрат сил на изучение, но и сулящей очень привлекательные дивиденды.

Теперь можно уточнить наше всеобъемлющее определение протокола. Так как нас интересует строго определенная прикладная область — программы, термин "протокол" приобретает более четкие границы: он должен содержать описания соглашений об инициализации и завершении процесса "общения", о синхронизации этого процесса, обнаружении и исправлении ошибок, о форматах допустимых "сообщений". С такой точки зрения протокол фактически является формализацией языка общения, и самый близкий пример известного всем протокола — учебники родного языка обычной средней школы. Как это ни странно, но уточнение границ в очередной раз привело нас к краю очередной бездны. И все же попробуем сделать еще один шаг…

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

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

Агитпроп

Вот и настало самое подходящее время для обзорно-рекламного знакомства с предметом обсуждения. Хотя бы потому, что автор спешит избавиться от обвинений в "откапывании" чего-то никому не нужного, никчемного и заумного. И от возможных обвинений в PR-продвижении некоторого товара — к счастью, объект нашего обсуждения легально бесплатен. Как и легально бесплатна и доступна учебная литература, ему посвященная.

Итак, знакомьтесь — формальный верификатор распределенных программных систем SPIN. На деле это сравнительно небольшая программа (упаси Бог, какие миллионы строк кода?!), дистрибутив которой в исходных текстах занимает приблизительно столько же дискового пространства, сколько страшно объектно-ориентированная и "полезная" игрушка из состава KDE (графической пользовательской оболочки для Unix-систем), выводящая на экран при старте красивую приветствующую картинку. Короче говоря, загрузка файла размером 300 KB доступна даже владельцам самых допотопных модемов. Впрочем, size no matter: SPIN — кросс-платформенная разработка, прекрасно "живущая" практически на любой системе, а для самых "ходовых" доступны готовые бинарные исполняемые файлы.

С "маркетинговой" точки зрения SPIN является исключительно… популярной системой. Существует обширная мировая community пользователей SPIN, каждый год проводятся международные конференции (с 1995 г.) пользователей, программа живет и развивается. Естественно, не без участия "главного виновника" — исследовательских лабораторий Bell Labs, упоминание которых сразу наводит на мысль, что мы имеем дело с Действительно Хорошей Программой.

Технологически SPIN представляет собой специализированный язык моделирования PROMELA, очень эффективный интерпретатор этого языка и графический интерфейс, облегчающий восприятие результатов выполнения PROMELA-программ (и все это "умещается" в трехсоткилобайтовый дистрибутив…). Кроме такой короткой справки, следует все же упомянуть и то, что реализация SPIN является образцом создания действительно сложного проекта в лучших (канонических) традициях разработчиков Bell Labs. Фактически полное отделение пользовательского интерфейса от семантической части программы, максимальное использование инструментальных средств (генераторов программ синтаксического и семантического разборов), компонентная модель, поддерживаемая возможностями Tcl/Tk, — все это настоящая учебная парта для профессионального программиста.

И наконец, главное — для чего используется SPIN? Здесь, учитывая брошенный в предыдущем разделе статьи "взгляд в бездну протоколов", ответ "для всего" уже не покажется странным. И действительно, AT&T использует SPIN для формальной верификации C-программ, обеспечивающих работу телефонных и сетевых устройств, разработчики ОС Plan 9 применяли SPIN при верификации реализаций сетевых протоколов 9P и IL, многие компании, специализирующиеся на создании ПО для встраиваемых систем класса mission-critical, обязательно верифицируют с помощью SPIN все свои разработки. В перечень традиционных "корпоративных" клиентов входят и NASA, и научные центры вооруженных сил разных стран, и крупнейшие производители аэрокосмической отрасли. Список можно продолжать до бесконечности, главное — всем пользователям SPIN обеспечивает формальное построение модели программной системы и формальную же проверку правильности этой модели.

Такая бездна может уместиться в 300 KB файла с расширением tgz… На самом деле, как и для любого действительно хорошего инструментального средства, возможности SPIN в области высокоуровневого проектирования ПО почти безграничны, просто эту систему надо серьезно и основательно изучать — на каждой пользовательской конференции SPIN открываются новые перлы ее применения.

Крылом волны касаясь…

К сожалению, никакой возможности серьезно углубиться в теоретические основы SPIN нет. Да и попытка трактовки на нескольких страницах семантики "страшных слов" (линейная темпоральная логика, структуры Крайпки, автоматы Бьючи) заведомо обречена на провал. Поэтому вся "теневая" часть SPIN оставляется заинтересованному читателю для самостоятельных битв за знания. Мы же просто попытаемся кратко взглянуть на сугубо технологические особенности реализации SPIN как программного продукта.

К чести разработчиков системы, они не стали "выдумывать" нечто невообразимо сложное, несмотря на сложность и "свежесть" используемых теоретических построений. Последний момент очень важен — SPIN фактически базируется на совсем современной (по научным меркам) теории, основополагающие теоремы которой были доказаны в начале 80-х годов, практически одновременно с началом самого проекта SPIN. Несмотря на то что эти исторические справки интересны сами по себе, несомненно, более интересной является здравая консервативность, присущая как самому проекту, так и его программному воплощению. Язык моделирования PROMELA обладает очень близким к наиболее распространенному языку программирования (естественно, C) синтаксисом, а описание его семантики сделано с исключительным мастерством и фактически не требует специальных математических знаний. Все это, мягко говоря, необычно для современного мира, где сверхзапутанные спецификации толкуются с помощью заумных слов. Впрочем, с другой стороны, и легко объяснимо — SPIN абсолютно конкретен и потому не требует ни слишком умных индульгенций, дающих право на существование, ни слишком активных рекламных кампаний, ни вульгарных эпитетов типа "серебряной пули". Это просто хороший инструмент, используя который, можно добиться хороших результатов.

Ну что же, все почти готово к первому "касанию крылом…". Здесь автор вынужден прибегнуть к "стилю Тарантино" с постоянными забеганиями вперед и откатами назад для того, чтобы "утрамбовать" в сжатый объем статьи максимум информации, позволяющей хотя бы получить первое представление о SPIN. Итак, взглянем на простейшую программу на PROMELA, дающую возможность чуть-чуть почувствовать "вкус" этого языка. Пока пугаться не стоит, ничего особенно необычного она из себя не представляет, по крайней мере, синтаксически:

byte target = 5 ;
proctype One()
itc_drupal_ (target == 1) -> target = 6
proctype Two()
itc_drupal_ target = target -- 1
init itc_drupal_ run One() ; run Two()

Попробуем проанализировать эту примитивную PROMELA-программу построчно, по ходу знакомясь с базовыми понятиями языка. В первой строке, что достаточно очевидно для хотя бы в общих чертах знакомого с языком C человека, объявляется переменная с именем target. Тип этой переменной — byte — является зарезервированным (ключевым) словом PROMELA и, по традиции, описывает объект размером 8 бит. Всего же PROMELA поддерживает пять базовых типов данных — bit и bool (объекты размером 1 бит), уже упомянутый byte, short (объект размером 16 бит) и int (32-битовый объект). Семантика понятия "переменная" в PROMELA не сильно отличается от аналога из мира программирования — в переменных хранятся информация о системе в целом или локальная информация, "скрытая" в одном из процессов, составляющих систему. В нашем случае переменная target объявлена вне прочих описаний, поэтому она моделирует свойство системы в целом и называется глобальной. Пока все было очень похоже на обычные языки программирования, и вот настало время рассмотреть первое существенное отличие. В первой же строке PROMELA-программы проявляется одно из главных семантических свойств этого языка — выражение присваивания, записанное в ней, обладает признаком "вычислимости всегда". Это означает, что для его вычисления не требуется выполнение дополнительных условий. Пока этого достаточно для первой строки, и продвинемся по тексту дальше. Три предложения PROMELA, начинающиеся с ключевого слова proctype и init, описывают три различных типа процессов, которые будут существовать в нашей системе.

Процессы — одни из ключевых элементов SPIN, с помощью которых моделируется наиболее существенное в реальных (разрабатываемых) системах. Зарезервированное слово init означает главный процесс, основная задача которого, в полном соответствии с синтаксисом записи, — создание и инициализация остальных процессов. Естественно, что init обладает и одним отличительным свойством — с него начинается исполнение PROMELA-модели. Ключевое слово run, дважды использованное в последней строке, образует с именем процесса выражение, результатом исполнения которого является "овеществление" процесса — превращение его из описания в исполняющуюся сущность, иначе говоря — запуск процесса. Выражение run возвращает ненулевое положительное значение в том случае, если процесс удачно запущен (так как PROMELA-программы выполняются на реальных вычислительных машинах, всегда существует верхний предел количества моделируемых процессов). Кроме того, это значение является уникальным идентификатором процесса — так называемым pid.

Использованные в нашей первой PROMELA-модели символы ";" и "->" — синонимы, но эта кажущаяся синтаксическая избыточность на деле призвана подчеркнуть их семантику. В отличие от языков программирования, в которых обычно символ ";" служит признаком окончания описания выражения, в PROMELA его роль — разделение последовательных процессов. Вспоминая, что первая строка обладает признаком "вычислимости всегда", символ ";" в ней просто информирует читателя программы о том, что в месте программы, где встречается символ ";", выражение выполнено и пора перейти к следующему. Но когда вычислимость выражения можно определить только в ходе выполнения программы, для обозначения последовательности выражений (или процессов) применяется синоним "->", подчеркивающий, что исполнение последующего выражения наступит только после достижения состояния выполнимости и, естественно, после исполнения предыдущего.

Давайте теперь вернемся к упомянутому свойству вычислимости — одному из фундаментальных понятий SPIN. В языке PROMELA нет различия между операторами, имеющими "вычислительный" и "проверочный" характер, а условием исполнения оператора является его вычислимость — готовность всех операндов к выполнению операции. Пояснить это можно на простом примере, заимствованном из второй строки "кода" нашей PROMELA-модели. На человеческом языке выражение itc_drupal_target == 1 читается так: "Процесс One ожидает состояния, при котором значение глобальной переменной target будет равно 1". В терминах SPIN то же самое звучит так: "Процесс One заблокирован до достижения синхронизации значения переменной target со значением константы 1".

Смысл нашей примитивной программы стал понятнее — мы, оказывается, построили модель системы с двумя процессами, обменивающимися данными через глобальную переменную и использующими значение этой переменной для синхронизации исполнения. Естественно, для моделирования реальных систем таких ограниченных возможностей категорически недостаточно. Поэтому в PROMELA поддерживается встроенная модель самого распространенного и наиболее общего архитектурного решения, применяемого для взаимодействия процессов, а именно, именованных каналов передачи сообщений (message channels, в дальнейшем — просто каналы). По сути, каналы PROMELA являются дополнительным базовым типом этого языка и описывают в общей форме записи "chan имя = [количество] of [тип]" канал связи с именем "имя", способный содержать "количество" элементов типа "тип". Соответственно, PROMELA не был бы языком сверхвысокого уровня, если бы в нем не были предусмотрены операции для работы с каналами. Так, операция вида "имя_канала!выражение" посылает результат выполнения выражения в канал, трактуя канал как очередь сообщений (добавляя результат в конец очереди). Операция "имя_канала?имя_переменной" соответственно выполняет обратную операцию — сообщение из канала записывается в переменную с именем "имя_переменной" (канал — очередь, в переменную записывается первое значение из очереди).

Вспомнив, что каналы являются типом, соответственно объекты этого типа можно тоже передавать… через каналы. Такой подход позволяет моделировать практически все, что может быть создано известными программными способами в рамках существующих (и даже несуществующих) операционных сред. Так, например, весьма специфическое, на первый взгляд, описание возможного канала chan Rend = [0] of [byte] на деле моделирует так называемый порт рандеву, позволяющий без буферирования (размер очереди равен нулю) передавать один-единственный оповещающий (или синхронизирующий) байт из процесса в процесс.

Попробуем вернуться к нашей прежней модели и немного ее трансформировать. Например, так:

byte target = 1 ;
proctype One() itc_drupal_ (target == 1) ->
target = target + 1
proctype Two() itc_drupal_ (target == 1) ->
target = target -- 1
init itc_drupal_ run One() ; run Two()

В этой PROMELA-программе что-то не то. А именно, если один из двух процессов One или Two завершится раньше, чем другой, то оставшийся будет вечно ожидать синхронизации. Возможна и еще одна ситуация, при которой оба процесса завершатся одновременно, но и в этом случае "что-то не то" сохраняется — значение переменной target не будет определено — с равной вероятностью из диапазона 0…2. Для решения подобной проблемы в PROMELA предусмотрено ключевое слово atomic, указывающее, что выражение (или группа выражений) должно быть выполнено без учета взаимодействия с другими процессами. Если в объявленных atomic-выражениях исполнение процесса блокируется, это считается ошибкой, и весь процесс, содержащий atomic-выражение, прекращает выполнение, сообщая об ошибке.

Пользуясь заявленным "стилем Тарантино", опять "откатимся" к началу ознакомления со SPIN, к первому примеру. Без дополнительных обсуждений сейчас понятно, что поток вычислений в PROMELA-программах строится на основе следующих моделей: условно-последовательное выполнение операций внутри процесса, безусловно-последовательное выполнение atomic-операций и, наконец, параллельное выполнение процессов. Для моделирования реальных программных систем этого набора недостаточно, и в PROMELA существуют конструкции, описывающие условный выбор потока исполнения (case-конструкция), повторение потока исполнения (аналог циклов) и безусловный переход (да-да, пресловутый goto). Здесь также наблюдаются все признаки языка сверхвысокого уровня, например конструкция условного выбора потока исполнения радикально отличается от принятых в языках программирования операторов case:

if
:: выражение_1 ->
поток_выполнения_1
...
:: выражение_N ->
поток_выполнения_N
fi

Принцип работы такого селектора прост: из N потоков выполнения может быть выбран только один по критерию вычислимости выражения_i. Если сразу несколько выражений вычислимы одновременно, поток выполнения выбирается случайным образом.

Последнее замечание касается не столько языка PROMELA, сколько самой реализации SPIN как программного продукта. Упомянув единожды, что SPIN обладает "очень эффективным интерпретатором PROMELA", было бы непростительно не уточнить это понятие. Интерпретатор PROMELA действительно крайне эффективен, ведь на самом деле он реализован в виде транслятора в язык C, а сама система SPIN полностью "прячет" все процессы генерации исполняемой программы из промежуточного представления. Отдельного замечания заслуживает и вычислительная эффективность генерируемых программ — на сегодняшнем ПК среднего класса (процессор с тактовой частотой 1 GHz, 256 MB ОЗУ) SPIN легко справляется с верификацией PROMELA-моделей систем, характеризующихся несколькими миллионами возможных состояний.

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

Что же дает SPIN?

Неважно, что я напишу для Вас трактат об искусстве рассуждения, важно, чтобы Вы рассуждали.
Э.Кондильяк

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

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

Что особенно интересно, SPIN допускает так называемое "рекурсивное применение". Например, при проектировании по методике "сверху вниз" строятся и проверяются PROMELA-модели для каждого уровня детализации, вплоть до уровня нетривиальных алгоритмов (в руках профессионала SPIN прекрасно с этим справляется).

Ресурсы

SPIN доступен с сайта netlib.bell-labs.com/netlib/spin/whatispin.html, здесь же располагается и более чем исчерпывающая документация, по адресу cm.bell-labs.com/cm/cs/what/spin/Doc/Book91.html можно совершенно "за бесплатно" обзавестись персональной копией изданной в 1990 г. в Prentice Hall книги, посвященной SPIN. Остается совсем немного — интересно и хорошо поработать, благо, учебники по SPIN и PROMELA изобилуют примерами, а реальная жизнь требует хороших, изящных и правильных программ.