Изковано и търсене, което заслужава доказателството си
Старият трик с проблема
Всяка сериозна софтуерна система има няколко парчета код, които имат значение далеч повече, отколкото размерът им подсказва. Цикъл, който се изпълнява милиони пъти. Битовa операция в пътя за компресия. Малка матрична рутина. Ядро за модулна аритметика. Нещо, което изглежда безобидно при преглед на кода и после тихо решава сметката за ток, бюджета за закъснение или броя машини, които трябва да купите. Много демократичен е софтуерът. Една мъничка функция може да съсипе срещата на всички.
Исторически тези ядра се подобряват от хора. Старши инженер си спомня трик от научна статия. Някой рови из стара публикация във форум. Написва се набор от бенчмаркове. Изпробват се няколко кандидата. Най-бързият печели, ако все още изглежда коректен. После организацията го замразява, защото пипането му отново прилича на боцкане на спящ трансформатор с вилица.
Forge е изследване на по-добра версия на този процес. Той е двигател за синтез на програми за малки, критични реализации: дайте му типизирана спецификация и свойства, оставете го да търси кандидат-програми, да измерва и сравнява компромиси, да проверява еквивалентност, после да сведе откритата реализация до целите, които имат значение. Важната дума не е търсене. Важната дума е все още. Тя все още трябва да е коректна.
Затова Forge живее в изследванията. Той не е публичен продуктов бутон, където някой пише направи по-бързо и получава чудо. Той е работна маса за синтез за партньорски експерименти, откриване на ядра и изследване докъде може да стигне автоматизираното търсене, когато е вързано за верификация, а не за бенчмарк театър.
Спецификацията е стартовата линия
Оптимизация без спецификация е просто хазарт с по-хубави имена на променливи. В момента, в който се появи умен кандидат, екипът трябва да знае какво трябва да запази. Обработва ли всеки вход или само приятелските от бенчмарка? Зачита ли поведението при препълване? Валидна ли е алгебричната идентичност при представянето, което реално се използва? Запазва ли същата семантика, когато се сведе до различен бекенд?
Forge започва от типизирани изрази и свойства, защото търсенето има нужда от граница. Границата казва какво се счита за еквивалентно. Без нея двигателят може да намери нещо удивително бързо, като изтрие половината работа. Компютрите са отлични в злонамереното съответствие, когато договорът е неясен.
Страната на търсенето е умишлено в множествено число. Изчерпателното търсене е полезно, когато пространството е достатъчно малко, за да се покрие. CEGIS е полезен, когато контрапримерите могат да насочват прецизирането. Генетичното програмиране и MCTS изследват по различен начин. Търсенето с машинно обучение може да учи ценови модели и да приоритизира обещаващи области. Нито едно от тях не е универсално най-добро. Това не е слабост. Така се държи търсенето в реалния свят. Ако един чук решаваше всяко ядро, кутиите с инструменти щяха да са много скучни, а производителите на хардуер безработни.
Изследователският въпрос е как да се комбинират тези двигатели с достатъчно доказателствен натиск, така че резултатът да не е просто умен. Синтезираното ядро трябва да оцелее и в бенчмарка по щастливия път, и във верификатора по нещастния път. Иначе подобрението не е инженерство. То е фокус с цена за поддръжка.
Верификаторът е възрастният в стаята
Forge използва стек за верификация, защото нито една проверка не е достатъчна за всяка област. Бързите примери са евтини и полезни. Тестовете със свойства откриват широки класове грешки и свеждат контрапримерите до нещо, което човек може да прочете. SMT решаватели като Z3 и CVC5 могат да докажат еквивалентност там, където кодирането е податливо. Изчерпателната проверка е практична за малки области. E-graph равенствената сатурация дава друг път към алгебрична еквивалентност.
Стекът е важен, защото ядрата се провалят по досадни начини. Кандидат може да мине през всеки обикновен бенчмарк и пак да е грешен в краен случай. Може да е коректен за беззнакови входове и грешен за знакови. Може да е коректен в математическо поле и грешен след като избраното представяне прелее. Може да е коректен преди понижаването и фино грешен след решение за селекция на инструкции. Верификаторът съществува, защото оптимизмът не е стратегия за тестване. Проверихме. Многократно. Остава вярно.
Има и практическа причина да се поддържат няколко пътя за доказателство. Формалните методи са мощни, но не са безплатни. Някои кодирания изтичат по време. Някои области са твърде големи за изчерпателна проверка. Някои свойства е по-лесно да се тестват вероятностно първо и да се докажат по-късно. Forge третира верификацията като фуния, а не като ритуал за чистота. Евтините проверки отхвърлят очевидни глупости. По-силните проверки защитават крайния кандидат.
Бързо не е едно число
Работата по производителност става нелепа, когато на един показател е позволено да доминира всеки разговор. Латенцията има значение. Броят операции има значение. Използването на памет има значение. Регистровият натиск има значение. Времето за компилация понякога има значение. Преносимостта има значение, когато едно и също ядро трябва да живее на повече от един бекенд. Кандидат, който печели латенция, като гори регистри като малък огън, може да е грешен за действителната цел. Кандидат, който е мъничък, но бавен, може да е полезен другаде. Контекстът остава непобеден.
Затова Forge рамкира оптимизацията като проблем на Парето. Двигателят може да търси по множество цели, вместо да се преструва, че има един универсален резултат, даден от много самоуверена електронна таблица. Полезният изход не винаги е единственият най-бърз кандидат. Понякога това е семейство от кандидати с видими компромиси, така че инженерът да може да избере този, който отговаря на ограничението за разгръщане.
Това е и причината да не харесвам голите твърдения за ускорение в публикации в блогове. Страницата за изследвания може да описва вътрешни очаквания и експериментални цели, но публичните твърдения се нуждаят от свежи изпълнения, текущ хардуер, текущи флагове на компилатора и точен контекст на натоварването. В противен случай числото става сувенир. Сувенирите са хубави. Те не са архитектура.
Честното твърдение е по-силно така или иначе: Forge е за това търсенето да бъде възпроизводимо, сравнимо и проверимо. Когато кандидат спечели, трябва да знаем коя цел е спечелил, кои кандидати е победил, кой верификатор го е приел и кой бекенд е насочен. Това е много по-полезно от число, което се носи из презентация и изглежда скъпо.
Понижаването е мястото, където доказателствата отиват да бъдат тествани
Едно открито изпълнение е полезно само ако оцелее пътя до реалните цели. Изследванията на Forge обхващат снижаване до бекенди като x86-64, RISC-V, WASM, Vulkan GPU пътища, C и Verilog. Този списък с цели не е декорация. Всеки бекенд има свои ограничения, форми на инструкциите, поведение на паметта и начини на отказ. Една и съща спецификация трябва да запази значението си, докато изпълнението се превръща в нещо, което целта действително може да изпълни.
Тук синтезът се свързва с останалата част от стека на Dweve. Core иска ефективни вътрешни цикли. Numerus се грижи за детерминирани числови ядра. BitWeave иска двоични векторни и матрични операции, които не губят ресурсите на процесора. Kera се грижи за снижаване на изчислителни графи до реален хардуер. Forge може да захранва тези слоеве само ако генерираното изпълнение е повече от бързо. То трябва да е еквивалентно, достатъчно преносимо за избраната цел и проверимо, когато нещо се промени.
Какво променя това за екипите
За един екип интересната промяна не е, че машина може да открие по-бързо ядро. Тя е, че работата по ядрата става по-малко зависима от фолклора. Вместо един експерт да помни правилния трик, процесът става: формулирай договора, претърси пространството, измери кандидатите, докажи еквивалентността, запиши компромиса и генерирай целеви код. Хората все още решават. Те просто спират да вършат цялото откривателство на ръка.
Това има значение за операциите, защото дългът от производителността е скъп по начин, който организациите често скриват. Бавно ядро означава повече сървъри. Повече сървъри означават повече разходи, повече енергия, повече сложност при разгръщането и повече шум в планирането. Грешна оптимизация се превръща в инциденти. Правилен, но недокументиран трик се превръща в бъдещ миграционен риск. Forge е изследване за намаляване на тази купчина от предотвратими глупости.
Има и културна промяна. Ръчната работа по производителността често възнаграждава героизма. Някой изчезва в пещерата и се връща с умен битов трик. Всички ръкопляскат, никой не го разбира напълно и компанията е придобила малък свещен предмет. Forge тласка процеса към доказателства: ето спецификацията, ето пътя на търсенето, ето отхвърлените кандидати, ето верификатора, ето избрания бекенд. По-малко митология. Повече разписки.
Къде работата все още е трудна
Нищо от това не прави синтеза лесен. Спецификациите са трудни. Ако спецификацията е грешна, двигателят може вярно да открие грешното нещо. Пространствата за търсене могат да експлодират. Решаващите програми могат да изтекат по време. Моделите на разходите могат да подведат. Бекендите могат да разкрият детайли, за които абстрактният израз не се е интересувал. Верификацията може да е силна в една област и неудобна в друга. Всеки, който продава програмния синтез като автомат за оптимален код, или пропуска трудните части, или таксува допълнително за разочарованието.
Forge е интересен точно защото се изправя директно срещу тези трудни части. Той комбинира няколко стратегии за търсене. Държи верификацията близо. Отнася се към целите като към компромиси. Насочва се към реални бекенди. Остава изследователска програма, защото все още учим къде е границата между автоматизираното откривателство, човешката преценка, ограниченията на решаващите програми и реалността на разгръщането.
Тази граница си струва да бъде изследвана. Софтуерната индустрия има твърде много малки горещи цикли, твърде много дублиран фолклор за производителността и твърде много оптимизации, които никой не иска да пипа отново. Ако Forge успее да превърне дори част от тази работа в повтаряем процес на доказателства, резултатът не е просто по-бърз код. Той е по-спокоен код. По-спокойният код е подценяван, най-вече от хора, които не са били викани по телефона в 02:17.
Какво е нужно за един добър прогон на Forge
Един сериозен експеримент с Forge започва преди да заработи двигателят. Екипът трябва да донесе истинско ядро, а не неясно оплакване от производителността. Нужни са представителни входни данни, познати гранични случаи, целеви хардуер, актуални бенчмаркове и бизнес причината, поради която това ядро има значение. В противен случай синтезният двигател може да прекара много време в решаване на проблем, който никой всъщност няма. Изследователските инструменти не са имунизирани срещу некачествени входни данни. Те просто правят некачествените данни по-скъпи за проверка.
Най-полезният вход е малък, ясен договор. Какво се очаква функцията да изчислява? Кои алгебрични закони имат значение? Кое поведение при препълване е умишлено? Кои диапазони са невъзможни по конструкция и кои просто не са се появили в последния тестов прогон? Кои резултати могат да толерират приближение и кои не могат? Екип, който не може да отговори на тези въпроси, вероятно все още няма проблем с оптимизацията. Той има проблем с изясняването на продукта, облечен в дрехите на компилатор.
Един добър прогон се нуждае също и от целева позиция. x86-64 и RISC-V не са едно и също. WASM има различни ограничения. Графичните пътища на Vulkan се интересуват от формите и движението на паметта. Verilog повдига хардуерни въпроси, които обикновените приложни екипи рядко оценяват преди кафето. Forge може да изследва целевото снижаване, но не може да решава организационните приоритети. Ако преносимостта е по-важна от скоростта на една платформа, кажете това. Ако латентността е по-важна от паметта, кажете това. Ако натискът върху регистрите е практическото ограничение, кажете и това. Двигателят е мощен, не е ясновидец.
Резултатът трябва да се третира като пакет от доказателства. Кандидат, цел, път за доказване, отхвърлени контрапримери, бекенд, контекст на бенчмарка и открити уговорки. Този пакет е това, което позволява на хората да вземат разумно решение. Понякога печелившият ход е да се приеме кандидатът. Понякога е да се запази старото ядро, защото компромисът с преносимостта не си струва. Понякога откритието е, че спецификацията е била твърде свободна. И трите резултата са полезни. Само един от тях изглежда вълнуващо на демонстрация, поради което демонстрациите са слаб заместител на инженерната работа.
Урокът
Урокът на Forge е прост: производителността не трябва да изпреварва доказателството. Търсенето е мощно, но търсачка без проверка е просто много енергичен начин да създавате грешки. Проверката е мощна, но без търсене тя чака хората да ѝ донесат кандидати. Forge събира двете заедно и пита какви ядра можем да открием, когато на машината е позволено да изследва, но не ѝ е позволено да лъже.
Това е изследването, което си струва да се прави. Типизирани спецификации, търсене на кандидати, фунии за доказване, Парето цели и снижаване към бекенд. Не магия. Не продуктова отсечка. Начин да се създава по-добър малък код с приложени доказателства.