У Льоні сьогодні

Ну, годі про формальну верифікацію. Я нещодавно був вражений простим, але дієвим підходом Kafka до послідовності повідомлень.

Для побудови простої в розумінні системи бажано, щоб послідовність подій на виході була така сама, як на вході. Втім, зазвичай зі збільшенням масштабу гарантія послідовності втрачається. Це відбувається тому, що повідомлення можуть бути отримані різними вузлами в кластері. А при читанні послідовність обробки вузлів також не визначена, тому може перемішатись ще й там.

Розглянемо приклад. де нам треба обробляти журнал у форматі “запит”-“відповідь”. Через втрату гарантій послідовності ми не можемо очікувати, що побачимо повідомлення “запит” раніше, ніж “відповідь”, та нам доведеться додатково продумати, що робити з відповіддю, яка прийшла раніше свого запита.

Звісно, рішення існують — наприклад, в AWS SQS є режим FIFO - хоч і суворо обмежений - 300 повідомлень в секунду проти мільйонів у Кафки.

Що робить Кафка? У Кафки одиниця масштабування — це розділ. Кожна “черга” (topic) ділиться на розділи (partition). На рівні розділу послідовність повідомлень гарантована. Кожний розділ призначений до конкретного вузла, який приймає всі записи в нього. Зі збільшенням масштабу кількість розділів та вузлів може зростати стільки, скільки треба, зі збереженням гарантій.

Ключовим є те, що виробники можуть самі вирішувати, в який розділ писати кожне повідомлення. Наприклад, якщо ми пишемо журнал подій, та їх треба групувати за субʼєктом, можна зробити ID субʼєкта ключем розподілу. А в системі “запит”-“відповідь” - просто стежити, щоб відповідь була записана в той самий розділ. (Єдине розумне обмеження — щоб розподіл був рівномірним та не створював “гарячих розділів”.)

А з боку споживача існує механізм групи споживачів. Група споживачів ділить між собою всі розділі топіка — кожний розділ дістається тільки одному клієнту з групи. Таким чином, кожний споживач отримує “скибочку” повідомлень. Послідовність в скибочці гарантована. як і відсутність конфліктів. Коли клієнти підключаються чи відключаються, призначення у групі балансуються наново.

Така от неочевидна архітектурна перевага (а я спочатку думав — навіщо ті розділи?)

Всі ці теореми та конʼюнктивні нормальні форми звучать дуже абстрактно, але що воно являє собою та як з ним працювати. Думаю, не буде новиною, якщо я скажу, що тут теж синтаксичне дерево. Ну, або ж просто дерево, бо воно не відповідає ніякому синтаксису.

В ліспах взагалі код та структура мають буквально ідентичний вигляд. Хіба що для того, щоб якось відрізняти, я використовував не списки, а масиви як вузли дерева. (Може здаватись дивно, що масиви, а не обʼєкти, але в ліспі працювати з масивами природніше.) Операції пишуться в польській нотації, тобто спочатку йде оператор, а потім операнди.

Доведення виразу буде успішнішим, якщо спростити його. Вручну зрозуміло, як це робити: якщо ми бачимо вираз X || false, то відразу можемо замінити його просто на X. Щоб досягти такого результату автоматично, я побудував рушій пошуку зразків у виразі та заміни їх. Це виявилося зручною абстракцією - залишилось тільки зібрати словник відомих алгебраїчних тотожностей. Також рушій спрощення знаходив фрагменти виразу, де всі операнди є константами, та заміняв на результат обчислення.

Що мені особливо подобалось, так це те, як зручно обробляти деревоподібні структури функціональним кодом. А також те, що в Clojure всі структури даних мають порівняння за значенням. Це корисно, наприклад, коли треба шукати піддерева, що повторюються для пошуку зразків.

Код для цієї частини

Коли в нас є теорема про вірність програми, залишається її довести. Що то взагалі значить — довести? В логіці теорема — це просто логічний вираз з невідомими. Довести — значить, показати, що для будь-якого набору значень невідомих теорема буде вірною. Як приклад: A || ~A (A або не A) буде вірним завжди, як можна побачити тривіально. На жаль, теореми про вірність виходять не такими простими. Тож як можна довести теорему — та ще й автоматичним шляхом?

Якщо невідомих небагато, можна довести повним перебором — тобто обчислити значення теореми для кожної комбінації та перевірити, що воно завжди буде істиною. Складність доведення росте експоненційно; для десяти невідомих це тривіально, для пʼятдесяти — нереально. (Кожний логічний вираз в програмі — рівність чи нерівність — стає невідомою в теоремі, та ще й деколи в різних варіаціях.) Я використовував такий метод до 20 невідомих.

А для складніших теорем я використовував метод резолюцій. Це підхід до доведення від оберненого: щоб довести нашу теорему, ми знаходимо підтвердження тому, що обернена теорема хибна. Для цього в оберненій теоремі треба знайти суперечність.

Пошук суперечностей відбувається за ітеративним алгоритмом. Спочатку теорему перетворюємо на конʼюнктивну нормальну форму — отримуємо, просто кажучи, ззовні AND, а всередині OR -дизʼюнкти. Достатньо знайти пару дизʼюнктів, які є протилежностями, щоб їхній AND ніколи не був істиною. Якщо з першої спроби не виходить - “схрещуємо” наявні дизʼюнкти, поки не знайдемо протилежні.

Буває й таке, що суперечність знайти неможливо — тоді теорема не буде доведеною, відповідно, вірність програми неможливо встановити. На жаль, остаточну відповідь “ні” ми не отримуємо — тільки відсутність успіху.

Код до цієї частини

Після того, як отримали синтаксичне дерево програми, починається його обробка, а саме, як я писав на початку, створення теореми про вірність. Для цього використовується така модель як семантики перетворення предикатів.

Починаємо з післяумови, яка вже повинна бути задана. (До речі, я про це не згадав, але одна додаткова синтаксична функція моєї граматики — оголошення перед- та післяумов у коментарях.) Далі беремо останню команду та перетворюємо післяумову на найслабкішу передумову, яка гарантує справдження післяумови після цієї команди.

Розглянемо найпростіший приклад. Якщо команда — це присвоєння x = y+1, то всі згадки про x у післяумові треба замінити на y+1. Якщо післяумова була x > 0, то найслабкіша передумова - y+1 > 0.

Так рухаємось від останньої команди до першої, та послідовно перетворюємо умову. Перетворення для умовного оператора if лише трохи складніше та являє собою поєднання двох гілок. Перетворення для циклу суттєво складніше та потребує від нас оголошення інваріанта та обмеженої змінної. Інваріант — це умова, яка справджується після кожної ітерації циклу. Обмежена змінна — зобовʼязана зменшуватись з кожною ітерацією, але бути додатною. Ці анотації допомагають довести, що цикл закінчиться.

Нарешті, отримуємо найслабкішу передумову для всієї програми. Залишається тільки поєднати її з оголошеною передумовою знаком “випливає” (⇒) та теорема про вірність готова!

Мабуть, потрібно подумати про те, що така теорема стверджує. Вона обмежена тим змістом, який вклав програміст; без хорошої перед- та післяумови доведення не буде корисним — або навпаки, не буде можливим. У цьому формальна верифікація схожа на юніт-тести - “правильність” програми все одно залежить від людського розуміння. Різниця в тому, що юніт-тести перевіряють обмежений набір випадків, а формальна верифікація — буквально всі.

Код для цієї частини

Будь-яка обробка коду, будь то компіляція, перевірка на вірність, форматування, або формальна верифікація, зазвичай починається з розбору на синтаксичне дерево. Так і тут. Для цього проєкту я обрав генератор парсерів ANTLR. Він видатний зокрема тим, що підтримує декілька мов — проміж них Java та C#. Для реалізації на Clojure я згенерував класи Java, а коли переписував на F# - то підійшла та сама граматика. Також ANTLR офіційно підтримує Golang та TypeScript. Одним словом, рекомендую мати у своєму арсеналі.

Граматику я писав з нуля. Спочатку намагався знайти готову, але це виявилося складно — бо те, що є, не підходило під мою семантичну модель. (Тут допомогла б стандартна модель esast, з системи Unified, але її ще не існувало.) На мою думку, для простих випадків граматику краще писати наново.

Граматика складається з правил для лексера та парсера. Лексер — розділяє текст на токени, тобто мінімальні значущі фрагменти. Правила лексера схожі на регулярні вирази. Токеном може бути ідентифікатор, число, дужка… Окремо визначаємося, що буде пробілами та незначущими символами. Це не тривіальне запитання — в одних мовах новий рядок розділяє команди, в інших — не має ніякого значення. В третіх мовах відступи мають значення. І так далі.

Правила парсера описують власне синтаксичне дерево. А саме, можливі варіанти того, як токени складаються у вузли дерева. Ну, наприклад: операція присвоєння: <ідентифікатор> <=> <вираз>. Найвищий вузол - програма: <команда>+, тобто програми складається з команд, а команди своєю чергою з виразів, а вирази з ідентифікаторів. Задача парсера — побудувати дерево, що відповідає тексту.

Коли синтаксичне дерево готове, можна перейти до побудови теореми про вірність.

Код для цієї частини

Сьогодні піде мова про мою бакалаврську роботу — яка ставила собою засіб формальної верифікації програм на псевдо-JavaScript. Кінцевий результат реально працює, хоч і для академічно простих прикладів. Робота була написана на Clojure - бо я тоді від неї був в захваті — та стала цікавим досвідом функціонального програмування. Настільки цікавим, що пізніше я переписав її на F#, щоб випробувати й цю мову — до речі, мабуть, перше, що я робив з VSCode.

Що взагалі таке формальна верифікація? Просто кажучи, це як юніт-тести, але без виконання коду — тільки за статичним аналізом. Визначаєш початкові та кінцеві умови, а перевірка встановлює, що код при заданих початкових умовах в будь-якому разі прийде до кінцевих. От простий приклад.

Як можна досягнути такого результату? Насправді концептуально все просто. Раз — побудувати теорему про вірність — тобто, формальний вислів, який гарантує справдження післяумов. Два — довести теорему. Проблема в тому, що теорему довести складно навіть вручну, а автоматично — ще складніше. Детальніше — в наступні дні.

Чи має це все практичний сенс? Та взагалі має. Формальна верифікація остаточно доводить те, що програма працює правильно. Є мова SPARK - вона використовується для систем з високим ризиком — наприклад, авіоніки. Або середовище Coq. На жаль, через складність доведення теорем ваш додаток React навряд чи колись стане формально верифікованим.

Давно вже хочу написати про це статтю; кожного разу, як доводиться хірургічно виправляти стан. От сьогодні я створив неправильний aws_ecs_task_definition, а потім затупив та видалив його вручну, після чого Terraform навідсіч відмовився працювати. Коли багато працюєш з Terraform, варто мати таку ментальну модель того, як код декларацій Terraform перетворюється на зміни в реальному оточенні.

В центрі цього процесу знаходиться стан Terraform. Стан — це каталог всіх ресурсів, про які Terraform вже знає. З боку коду, ресурсом є кожна декларація resource, а з боку реального світу, до нього привʼязана та сутність, якою Terraform керує. Обовʼязково у кожній сутності є ідентифікатор, який зазвичай зазначається в кінці документації про ресурс. Це важливо тому, що сама сутність нічого про Terraform не знає — саме тому Terraform можна застосувати до будь-якої предметної галузі.

Але також саме тому важливо не створювати та не видаляти ресурси з Terraform власноруч. Взагалі, краще не міняти, але зі змінами Terraform впорається, а от коли розходяться уявлення про існування ресурсів — ручних виправлень не уникнути. Для того є команди state rm та import. Причому імпортувати можна будь-що, тільки треба буде вручну визначити ідентифікатор. Але на хмарному сервісі з імпортуванням складно, бо треба оголосити локально всі наявні змінні, що дратує. Є третя команда - taint - яка просить Terraform видалити ресурс та створити наново. Це інколи єдиний спосіб виправити помилки. (Але в моєму випадку за сьогодні допомогло видалення зі стану командою state rm.)

А поки набір реальних сутностей в стані не змінюється, все інше поміняти набагато легше. Вся структура коду служить тому, щоб побудувати список ресурсів — тому створення нових локальних змінних для рефакторингу взагалі ніяк не вплине на стан. Якщо ж ресурси перейменувати або перемістити в модуль, однак залишити за ними привʼязку до світу, то з сучасним Terraform це робиться на рівні конфігурації — блоком moved. Раніше треба було вживати команду state mv, що робило перейменування окремою процедурою. Блок moved застосовується водночас з рештою конфігурації, що розвʼязує руки для рефакторингу в будь-який зручний момент.

Коментар до вчорашнього посту нагадав мені про мою профдеформацію — а саме, останні роки я працюю в оточенні, де AWS є даним. Тому коли я порівнював Lambda, то в першу чергу порівнював з ECS.

Проте якщо починати з вільного вибору, то брати AWS для розгортування вебдодатка це безглуздя. Заощадження у коштах вийдуть неадекватними витратами часу та зусиль. Навіть якщо мати досвід AWS - все одно має сенс зупинитись на простішому хостингу - Fly.io, Heroku і так далі. “Сантехнікою” варто займатись, тільки коли є потреба.

На жаль, я не знаю середньої альтернативи між контейнеризованим хостингом та повним хмарним. Допомагає принаймні вести облік в Terraform та за можливістю рефакторити. Насправді є багато різних модулів для Terraform - для створення того ж сервісу ECS, наприклад. Але за моїм досвідом між сервісами залишається достатньо різниці, щоб такий підхід був непрактичним — абстракція “тече” (як сантехніка). Можливо, також Kubernetes в чомусь допомагає, але мені він не зайшов через власну складність.

До речі, ми як раз шукаємо DevOps інженера — чесно, не планував рекламувати вакансію, але був би дуже радий мати поруч досвідченого спеціаліста.

Коли я порівнював запуск Rails на AWS Lambda та AWS ECS, я нічого не сказав про складність розгортування. Хоча, було бажання написати, що ECS це просто, а Lambda потребує більше налаштувань. Проте от в чому справа — мені здавалося, що різниця обʼєктивна, а субʼєктивна, бо з ECS в мене набагато більше досвіду.

Сьогодні довелося створювати новий сервіс на ECS, та ця підозра підтвердилась. Так, сам сервіс являє собою скупчення контейнерів Docker, це ніби зрозуміло, та нагадує Heroku або мій улюблений Fly.io. Але скільки всього потрібно створити навколо сервісу, щоб він запрацював! Роль IAM - зрозуміло. Група безпеки — для цього сервісу та ще не забути оновити всі його залежності. Балансувальник навантаження — без нього сервіси ECS не працюють. Ресурси журналу (та дозволи на них.) А далі, ще налаштувати CodeDeploy. Підготувати параметри Parameter Store. І далі, і далі.

Та, якщо в чомусь припустити помилку, то, найчастіше, не отримаєш навіть базового повідомлення. Типова ситуація — коли просто “не працює”. Може, в групі безпеки бракує потрібних дозволів. Може, сервіс в підмережі, де немає зовнішнього підключення. З досвідом стає простіше написати правильно з першого разу та знати, куди дивитися, якщо не працює.

Але природа задачі залишається такою самою. Та понад усе вона мені нагадує роботу з сантехнікою. Купа складних частин, жодна з яких сама по собі нічого не робить. Кожна погано влазить та стикується. Та як остаточний результат, отримуємо не якийсь шедевр мистецтва, а просто дещо, що робить свою роботу.

Дізнався про екосистему обробки синтаксичних дерев, від якої я абсолютно в захваті. Це екосистема Unified для TypeScript (та JavaScript.) Я натрапив на неї при пошуку бібліотеки для розбору Markdown - та виявив, що бібліотека Remark побудована саме на основі Unified.

З чого взагалі складається Unified? В першу чергу, це стандартна обʼєктна модель синтаксичного дерева (ну, може, не стільки обʼєктна, стільки структурна — бо не використовує класів.) Навколо цієї моделі побудоване скупчення функцій, що її обробляють. Як базовий приклад — пакет unist-util-visit. Цією функцією можна знайти в дереві потрібні вузли — наприклад, задачі в документі Markdown.

На такій базовій системі побудовані інструменти для різних мов та задач. Кожна мова має свою специфікацію дерева — наприклад, mdast для Markdown. Але, як я був здивований дізнатись, Prettier теж використовує Unified - для форматування JavaScript!

Втім, мені нічого, окрім Markdown, не потрібно. Навіть в такому випадку наявність стандартизованого дерева спрощує створення доповнень, яких для Remark є чимало.