Стендап Сьогодні

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

05.08.2023

CouchDB - база даних з крутою реплікацією

Є така база даних - CouchDB - про яку майже ніхто не знає. Вона була помірно популярна десь біля 2010-го, але й досі отримує регулярні оновлення, причому досить вагомі. Я використовував її в маленькому сайд-проєкті, де робив з нею багато, проте у світ проєкт не вийшов, тож як воно в справжньому продакшні, сказати не можу.

З першого погляду, CouchDB - документна СУБД з максимально простою структурою, яка, до речі, схожа з OpenSearch. Документи складаються в бази даних, бази даних живуть на серверах. Цікавий момент — баз даних може бути скільки завгодно, наприклад, по базі на користувача.

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

Що робити з конфліктами? Власне, вирішати нам — в CloudFlare потужний механізм розвʼязання конфліктів. Можна робити це автоматично, за правилами переваги, а можна й написати код зі специфічною логікою.

А ще, реплікувати можна не всю базу, а частину документів за правилом. Наприклад, може ми хочемо завантажувати на сервер тільки опубліковані документи. А ще можна обмежити реплікацію тільки одним з напрямків. А ще реплікувати багато баз в одну або навпаки — одну в декілька…

Окрім самої CouchDB, є ще повноцінна реалізація на JavaScript - PouchDB. Її можна запускати в браузері або в React Native, та синхронізувати з сервером CouchDB.

04.08.2023

Бітові поля в базах даних та чому це погана ідея

Розкажу про одну зі своїх поганих ідей. Треба було зберігати в базі для кожного рядка набір булевих відміток. А потім — шукати за комбінацією цих відміток. Все це являло собою такий собі скінченний автомат.

Мені здалося дуже розумно не робити по стовпчику на кожну відмітку, а зробити бітове поле. Тоді можна додавати біти операцією OR, а шукати на кшталт bits AND 0b101 != 0. Бітові поля — крута технологія, та дозволяє розвʼязувати задачі, які здаються неможливими. Тільки історія не про це, а про те, як любов до крутої технології мене підвела.

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

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

А в OpenSearch - базі, що побудована навколо ефективного пошуку — взагалі немає можливості шукати за бітовими операціями. Щоб не кортіло.

У цьому стародавньому треді знайшов гарну альтернативу — зробити замість бітового поля масив цілих чисел — множину. Та побудувати для нього індекс GIN.

03.08.2023

Міграції в OpenSearch

Хоч в OpenSearch й немає жорстко заданої структури даних, потреба в однорідності даних залишається. Ну, може, не у всіх застосунках, може десь є проєкт, який просто індексує аби який JSON - але зазвичай все ж таки ми очікуємо бачити в документах певні атрибути.

Та, як всі знають, сьогодні атрибути одні — завтра можуть бути інші. Що робити з тими документами, які вже існують? На відміну від бази SQL, де можна легко додати новий стовпчик зі значенням за замовчуванням, в OpenSearch готового рішення немає.

Найпростіший технічно варіант — це нічого не робити, а при читанні чи пошуку враховувати, що поле може бути порожнім (тобто null). Не знаю, як ви, а я дуже не люблю перевірки на null “про всяк випадок”. Особливо коли воно скероване не бізнес-логікою, а невпевненістю бази даних.

Можна ввести версії схеми документів. Тобто в кожному документі є атрибут версії. При читанні документа робиться міграція до поточної версії (та, можливо, запис її в базу.) Так я робив, тільки не в OpenSearch, а в CouchDB - моделі документів в них дуже схожі. Впровадження явної версії спрощує обробку порожніх полів. Вона нагадує міграції бази, як в Rails, тільки на рівні кожного документа. (Особливо цікаво воно в розподіленій базі CouchDB, бо старі документи можуть бути приховані на вузлі, який давно не синхронізувався.)

Нарешті, є механізм Update by query, який, здається, і призначений робити міграції даних. Тут можна запустити масову операцію оновлення — хоч для всіх документів. Є тільки одна проблема — на відміну від SQL бази, ця операція не є атомарною або транзакційною. Вона обробляє документи поступово, та ті документи, що встигли помінятись іншим шляхом, не будуть оброблені взагалі.

02.08.2023

Як Kafka гарантує послідовність повідомлень

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

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

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

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

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

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

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

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

01.08.2023

Формальна верифікація: перетворення виразів

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

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

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

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

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

31.07.2023

Формальна верифікація: доведення теореми

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

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

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

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

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

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

30.07.2023

Формальна верифікація: найслабкіша передумова

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

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

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

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

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

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

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

29.07.2023

Формальна верифікація: обробка коду та граматики

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

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

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

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

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

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

28.07.2023

Вступ до формальної верифікації програм

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

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

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

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

27.07.2023

Terraform, його шари та редагування стану

Давно вже хочу написати про це статтю; кожного разу, як доводиться хірургічно виправляти стан. От сьогодні я створив неправильний 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 застосовується водночас з рештою конфігурації, що розвʼязує руки для рефакторингу в будь-який зручний момент.

Раніше

Пізніше