Melange — DSL для сетевых протоколов

в 20:07, , рубрики: mpl, ocaml, qt, qt quick, Qt Software, spl, ненормальное программирование, сериализация, сетевые протоколы, функциональное программирование, метки: , , , , , ,

Melange — DSL для сетевых протоколовВсем программистам рано или поздно приходится передавать данные. Ни для кого не секрет, что библиотек сериализации в Java существует примерно >9000, а в C++ они вроде и есть, а вроде их и нет. К счастью для большинства, несколько лет назад появился Google Protobuf, который принёс достаточно удобный способ определять структуры данных и быстро завоевал всенародную любовь. Это была фактически первая, доступная широким массам библиотека, позволяющая гонять по сети готовые структуры данных, не связываясь при этом с чем-то вроде XML. На дворе был 2008 год.

Вернёмся немного назад. В 2006 году простой индийский программист (как бы подозрительно это ни звучало!) Анил Мадхавапедди, один из самых известных сейчас в мире OCaml-разработчиков и автор свежевышедшей книги Real World OCaml, защищал в Кембридже кандидатскую диссертацию. Именно о ней я сегодня вам и расскажу.

Анил сразу пошёл дальше, чем Google. Он сразу подумал, для чего люди обычно пересылают по сети какие-то формализованные структуры данных? Чтобы реализовать какой-то протокол. А что такое протокол? Это какой-то конечный автомат. А где мы можем взять хороший пример сложного, хорошо спроектированного и проверенного временем протокола? Да прямо в обычном сетевом стеке! Итак, были взяты набор сетевых структур данных и протоколов: Ethernet frame, IPv4, ICMP, TCP, UDP, SSH, DNS и DHCP и постановка задачи: большая часть этих протоколов (особенно SSH и DNS) реализуются, что называется «руками», а хочется, чтобы не было типичных для C переполнений буфера, все переходы совершались автоматически, это всё можно было верифицировать, и чтобы работало быстро, а не как обычно.

Поскольку никто не будет читать диссертацию, сразу скажу: это более чем удалось. По результатам работы были написаны референсные реализации DNS и SSH-сервера и произведено сравнение с BIND и OpenSSH. OCaml-реализации давали по сравнению с традиционными прирост производительности от незначительного, до почти двухкратного. Кроме того была найдена ошибка в RFC на SSH (рабочая группа была уведомлена и RFC исправлен). О том, что было сделано, и как с этим жить, читайте под катом.

MPL

Первым делом были написаны два языка описаний и их трансляторы на OCaml. Первый язык — это Meta Packet Language или MPL, описывающий структуру пакета. В общих чертах он является аналогом protobuf, но не совсем. Во-первых, MPL не добавляет никакого оверхеда к вашей структуре. Вообще. Никаких дополнительных битов, указывающих тип данных или ещё что-то. С одной стороны, это не позволяет, как в protobuf, легко расширять структуру, добавляя к ней новые поля, с другой — вы никогда не прочитаете с помощью protobuf TCP-заголовок. Во-вторых, MPL сразу реализует всю ту логику, которая бывает необходима в сетевых структурах — упаковку или выравнивания, а также такие вещи, как переменный набор полей или значения полей, зависящие от других полей структуры. Для примера посмотрите на заголовок IPv4:

packet ipv4 {
    version: bit[4] const(4);
    ihl: bit[4] min(5) value(offset(options) / 4);
    tos_precedence: bit[3] variant {
        |0 => Routine |1 -> Priority
        |2 -> Immediate |3 -> Flash
        |4 -> Flash_override |5 -> ECP
        |6 -> Internetwork_control |7 -> Network_control
    };
    tos_delay: bit[1] variant {|0 => Normal |1 -> Low};
    tos_throughput: bit[1] variant {|0 => Normal |1 -> Low};
    tos_reliability: bit[1] variant {|0 => Normal |1 -> Low};
    tos_reserved: bit[2] const(0);
    length: uint16 value(offset(data));
    id: uint16;
    reserved: bit[1] const(0);
    dont_fragment: bit[1] default(0);
    can_fragment: bit[1] default(0);
    frag_offset: bit[13] default(0);
    ttl: byte;
    protocol: byte variant {|1->ICMP |2->IGMP |6->TCP |17->UDP};
    checksum: uint16 default(0);
    src: uint32;
    dest: uint32;
    options: byte[(ihl * 4) - offset(dest)] align(32);
    header_end: label;
    data: byte[length-(ihl*4)];
}

Здесь содержимое пакета описано как массив байтов data (чтобы не описывать все остальные возможные протоколы), но на его месте вполне могла бы быть запись:

classify (protocol) { 
    |1: "ICMP"-> data: packet icmp(); 
    |2: "TCP" -> data: packet tcp(); 
    |3: "UDP" -> data: packet udp(); 
}; 

И тогда при чтении IPv4-пакета мы сразу разбирали бы и его содержимое. В результате (де)сериализация любого пакета превращается в увлекательное занятие, не требующее никаких мыслей о том, как правильно упаковать данные и что где надо выравнивать. Так, практически полная реализация популярного формата MessagePack заняла у меня примерно 40 строк.

К сожалению, и у этого языка есть свои недостатки. Я насчитал их ровно два. Первый: запрещены рекурсивные пакеты. Это как раз стало причиной невозможности полной реализации MessagePack — MPL нельзя сказать, что в списке или мапе могут лежать списки или мапы, придётся описывать их просто как пачку байтов, а потом разбирать ещё одним вызовом десериализации. Это сделано специально, чтобы каждое чтение пакета было строго конечным, но нам от этого не легче. Вторая проблема: нельзя определять свои типы данных. Анил реализовал стандартные для сети типы, такие, как байты, биты, числа, строки или даже mpint, который присутствует в SSH, но этот список фиксирован. Если вы вдруг захотите реализовать протокол ssh-agent, который использует тип mpint1, вам остаётся только описывать его как массив байтов и разбирать у себя в коде. Единственный способ расширения списка поддерживаемых типов — это написание патчей к компилятору MPL, что является не самой тривиальной задачей.

SPL

Вторым языком стал Statecall Policy Language или SPL. Это язык описания конечных автоматов, то есть, сердце нашего протокола. Строго говоря, библиотек для создания конечных автоматов под все языки существует порядочно. Отличий у SPL от них (не считая своего языка описания вместо программного задания автомата) всего несколько. Во-первых, компилятор SPL умеет сразу генерировать описание на языке PROMELA для верификатора программных моделей SPIN. Буду честен, я не смог разобраться со SPIN, поэтому в этом месте был вынужден поверить автору на слово, что это круто. Во-вторых, используя имена состояний Receive_NAME и Transmit_NAME (где NAME — это тип сообщения из MPL), можно тесно интегрировать конечный автомат со структурами данных из MPL. Об этом мы поговорим позже, а пока что посмотрим на пример описания конечного автомата для авторизации в SSH:

automaton
auth (bool success, bool failed)
{
    Receive_Transport_ServiceAccept_UserAuth;
    Transmit_Auth_Req_None;
    Receive_Auth_Failure;
    do {
        either {
            always_allow (Receive_Auth_Banner) {
                either {
                    Transmit_Auth_Req_Password_Request;
                    auth_decision (success);
                } or {
                    Transmit_Auth_Req_PublicKey_Request;
                    auth_decision (success);
                } or {
                    Transmit_Auth_Req_PublicKey_Check;
                    either {
                        Receive_Auth_PublicKeyOK;
                    } or {
                        Receive_Auth_Failure;
                    }
                }
            }
        } or {
            Notify_Auth_Permanent_Failure;
            failed = true;
        }
    } until (success || failed);
}

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

Как с этим работать?

К сожалению, проект (весь целиком он называется Melange) не слишком богат на документацию, основным её источником является сама диссертация. Поэтому я решил написать небольшой Proof of concept, демонстрирующий работу всего продукта, а заодно являющийся небольшим таким Quick Start guide. Для этого надо написать какое-нибудь небольшое сетевое приложение. Для роли простого приложения с простым и понятным протоколом я выбрал старую добрую игру — морской бой. Вот так будет выглядеть наша структура сообщения:

packet message { 
    message_type: byte; 
    message_id: uint16; 
    classify (message_type) { 
        | 0:"Shot" -> 
            row: bit[4]; 
            column: bit[4]; 
        | 1:"ShotResult" -> 
            result: byte variant { |0 -> Missed |1 -> Damaged |2 -> Killed }; 
        | 2:"Disconnect" -> (); 
    }; 
} 

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

automaton seawar () { 
    Initialize; 
    during { 
        multiple(1..) { 
            Ready; 
            either { 
                Transmit_Message_Shot; 
                Receive_Message_ShotResult; 
            } or { 
                Receive_Message_Shot; 
                Transmit_Message_ShotResult; 
            } 
        } 
    } handle { 
        either { 
            Transmit_Message_Disconnect; 
            exit; 
        } or { 
            Receive_Message_Disconnect; 
            exit; 
        } 
    } 
}

Начинаем мы с инициализации (начальное состояние нашего автомата), а затем на каждом шаге либо мы стреляем, либо в нас. Всё просто. При этом если по какой-то причине возникает сообщение вида Disconnect, то это означает, что игра окончена и автомат надо остановить.

Теперь посмотрим, как это используется из кода. Для чтения сообщений мы будем использовать специальный буфер MPL, который будет заполняться данными — в нашем случае мы их забираем из сети.

val mutable env_ = Mpl_stdlib.new_env (String.make 4 '00'); 
val mutable tick_ = Protocol.init (); 
method tick state = tick_ <- Protocol.tick tick_ state; 
method send_message msg = ( 
    Mpl_stdlib.reset env_; 
    self#tick (msg#xmit_statecall :> Protocol.s); 
    if not (Thread.wait_timed_write sock_ 10.) then self#disconnect ~exc_text:"Timeout"; 
    Mpl_stdlib.flush env_ sock_ 
); 
method receive_message = (  
    Mpl_stdlib.reset env_; 
    if not (Thread.wait_timed_read sock_ 300.) then self#disconnect ~exc_text:"Timeout"; 
    Mpl_stdlib.fill env_ sock_; 
    let msg = Message.unmarshal env_ in 
 
    let state = Message.recv_statecall msg in 
    self#tick state; 
    msg 
); 

Обратите внимание, что каждое сообщение, как посылаемое, так и принимаемое, в обязательном порядке вызывает переход конечного автомата в новое состояние. За это отвечают вызовы msg#xmit_statecall и Message.recv_statecall msg, которые на основании сообщений (типа ShotResult) создают имена соответствующих состояний (Transmit_Message_ShotResult и Receive_Message_ShotResult). Благодаря этому, большая часть потенциальных ошибок программы будет выявляться именно здесь, когда неправильный переход автомата будет вызывать исключение Bad_statecall. Например, если в случае AI всё просто — он работает в один поток, совершенно синхронно и никаких проблем в такой простой задаче там никогда быть не может, то в графическом интерфейсе всё может быть сложнее.

Melange — DSL для сетевых протоколов
Например, простой пример, как всё легко может «взорваться». Для графического интерфейса я взял свежевышедший фреймворк Qt 5.2, для которого наш соотечественник Дмитрий Косарев написал биндинги к OCaml (достаточно интересные, если будут желающие, расскажу отдельным постом). При клике по клетке вражеского поля в отдельном треде может быть выполнен следующий код:

let send_shot col row = 
  ignore(game#send_message (Message.Shot.t ~row:row ~column:col)); 
  let result, state = game#receive_message in 
  (match result with 
      | `ShotResult x -> Board.mark opp_board row col x#result; 
              next_turn state x#result 
      | `Disconnect x -> game#disconnect ~send:false 
      | _ -> game#disconnect ~exc_text:"Unexpected_Message_Type" ~raise_exc:true ~send:true)

Если не предотвратить двойной выстрел, то этот метод будет вызван два раза — в этом случае могут быть отправлены либо два сообщения с выстрелом подряд, либо второе сообщение может быть отправлено после получения сообщения о промахе.

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

Заключение

Что дальше-то, спросит меня читатель. Ну, какой-то маргинальный, уже 4 года не обновлявшийся инструмент, работающий на непонятном языке. Зачем мне всё это, если у меня есть Node.js, MongoDB и клубничный смузи?

Читатель прав. Инструмент устарел, у него есть несколько существенных недостатков, которые я упоминал. Но при этом он показывает, в каком направлении надо развиваться. Так, весь код приложения, включая все декларативные описания, графический интерфейс и не самый тупой AI, составляет 850 строк. Это конечно не «30 строк на javascript»™, но тоже не слишком много.

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

Автор: torkve

Источник


* - обязательные к заполнению поля


https://ajax.googleapis.com/ajax/libs/jquery/3.4.1/jquery.min.js