Kovanie a vyhľadávanie, ktoré si zaslúži dôkaz
Problém starého triku
Každý vážny softvérový systém má niekoľko častí kódu, ktoré sú dôležitejšie, než by naznačovala ich veľkosť. Slučka, ktorá sa spustí miliónkrát. Bitová operácia v kompresnej ceste. Malá maticová rutina. Jadro modulárnej aritmetiky. Niečo, čo v code review vyzerá neškodne a potom potichu rozhoduje o účte za energiu, rozpočte na latenciu alebo počte strojov, ktoré si musíte kúpiť. Softvér je veľmi demokratický. Jedna maličká funkcia dokáže pokaziť stretnutie všetkým.
Historicky tieto jadrá vylepšujú ľudia. Skúsený inžinier si spomenie na trik z článku. Niekto sa prehrabáva starým fórom. Napíše sa sada benchmarkov. Vyskúša sa niekoľko kandidátov. Najrýchlejší vyhrá, ak stále vyzerá správne. Potom ho organizácia zamrazí, pretože sa ho znova dotknúť je ako pichať vidličkou do spiaceho transformátora.
Forge je výskum lepšej verzie tohto procesu. Je to engine na syntézu programov pre malé, kritické implementácie: dajte mu typovanú špecifikáciu a vlastnosti, nechajte ho hľadať kandidátske programy, merať a porovnávať kompromisy, overiť ekvivalenciu a potom znížiť objavenú implementáciu na ciele, ktoré záležia. Dôležité slovo nie je hľadanie. Dôležité slovo je stále. Stále musí byť správny.
Preto Forge žije vo výskume. Nie je to verejné tlačidlo produktu, kde niekto napíše urob rýchlejšie a dostane zázrak. Je to pracovný stôl na syntézu pre partnerské experimenty, objavovanie jadier a výskum toho, ako ďaleko môže automatizované hľadanie zájsť, keď je viazané na verifikáciu namiesto divadla okolo benchmarkov.
Špecifikácia je štartovacia čiara
Optimalizácia bez špecifikácie je len hazard s krajšími názvami premenných. Len čo sa objaví šikovný kandidát, tím potrebuje vedieť, čo má zachovať. Spracuje každý vstup alebo len tie priateľské z benchmarku? Rešpektuje správanie pri pretečení? Platí algebraická identita pri reprezentácii, ktorá sa skutočne používa? Zachováva rovnakú sémantiku pri znížení na iný backend?
Forge začína z typovaných výrazov a vlastností, pretože hľadanie potrebuje hranicu. Hranica hovorí, čo sa považuje za ekvivalentné. Bez nej môže engine nájsť niečo ohromujúco rýchle tým, že vymaže polovicu práce. Počítače sú vynikajúce v zlomyseľnej poslušnosti, keď je zmluva vágna.
Strana hľadania je zámerne v množnom čísle. Enumeratívne hľadanie je užitočné, keď je priestor dosť malý na pokrytie. CEGIS je užitočný, keď protipríklady môžu viesť spresňovanie. Genetické programovanie a MCTS skúmajú inak. Hľadanie riadené ML sa môže naučiť nákladové modely a uprednostniť sľubné oblasti. Žiadne z nich nie je univerzálne najlepšie. To nie je slabosť. Tak sa hľadanie správa v reálnom svete. Ak by jedno kladivo vyriešilo každé jadro, sady nástrojov by boli veľmi nudné a predajcovia hardvéru by boli nezamestnaní.
Výskumná otázka je, ako skombinovať tieto enginy s dostatočným dôkazovým tlakom, aby výsledok nebol len šikovný. Syntetizované jadro musí prežiť benchmark na šťastnej ceste aj verifikátor na nešťastnej ceste. Inak to zlepšenie nie je inžinierstvo. Je to kúzelnický trik s nákladmi na údržbu.
Verifikátor je dospelý v miestnosti
Forge používa overovací zásobník, pretože žiadna jediná kontrola nestačí pre každú oblasť. Rýchle príklady sú lacné a užitočné. Testovanie vlastností odhaľuje široké triedy chýb a zmenšuje protipríklady na niečo, čo človek dokáže prečítať. Riešiče SMT, ako sú Z3 a CVC5, dokážu dokázať ekvivalenciu tam, kde je kódovanie zvládnuteľné. Vyčerpávajúca kontrola je praktická pre malé oblasti. Saturácia ekvivalencie cez e-grafy poskytuje ďalšiu cestu k algebraickej ekvivalencii.
Zásobník je dôležitý, pretože jadrá zlyhávajú nepríjemnými spôsobmi. Kandidát môže prejsť každým bežným benchmarkom a napriek tomu byť nesprávny v okrajovom prípade. Môže byť správny pre neznamienkové vstupy a nesprávny pre znamienkové. Môže byť správny v matematickom poli a nesprávny po pretečení zvolenej reprezentácie. Môže byť správny pred znížením úrovne a nenápadne nesprávny po rozhodnutí o výbere inštrukcií. Overovač existuje, pretože optimizmus nie je testovacia stratégia. Overovali sme. Opakovane. Stále to platí.
Existuje aj praktický dôvod mať viacero ciest dokazovania. Formálne metódy sú silné, ale nie sú zadarmo. Niektoré kódovania vypršia. Niektoré oblasti sú príliš veľké na vyčerpávajúcu kontrolu. Niektoré vlastnosti sa ľahšie testujú najprv pravdepodobnostne a dokazujú neskôr. Forge pristupuje k overovaniu ako k lieviku, nie ako k rituálu čistoty. Lacné kontroly odmietajú zjavné nezmysly. Silnejšie kontroly chránia finálneho kandidáta.
Rýchlosť nie je jedno číslo
Práca na výkone sa stáva smiešnou, keď jedna metrika môže dominovať každej konverzácii. Latencia záleží. Počet operácií záleží. Využitie pamäte záleží. Tlak na registre záleží. Čas kompilácie niekedy záleží. Prenositeľnosť záleží, keď rovnaké jadro musí žiť na viac ako jednom backende. Kandidát, ktorý vyhráva na latencii tým, že spaľuje registre ako malý táborák, môže byť nesprávny pre skutočný cieľ. Kandidát, ktorý je malý, ale pomalý, môže byť užitočný inde. Kontext zostáva neporazený.
Forge preto rámcuje optimalizáciu ako problém Pareto. Engine môže hľadať naprieč cieľmi namiesto predstierania, že existuje jedno univerzálne skóre odovzdané veľmi sebavedomou tabuľkou. Užitočný výstup nie je vždy jediný najrýchlejší kandidát. Niekedy je to rodina kandidátov s viditeľnými kompromismi, aby si inžinier mohol vybrať toho, ktorý vyhovuje obmedzeniam nasadenia.
To je tiež dôvod, prečo nemám rád holé tvrdenia o zrýchlení v blogových príspevkoch. Výskumná stránka môže opísať interné očakávania a experimentálne ciele, ale verejné tvrdenia potrebujú čerstvé behy, aktuálny hardvér, aktuálne príznaky kompilátora a presný kontext pracovnej záťaže. Inak sa číslo stane suvenírom. Suveníry sú pekné. Nie sú architektúra.
Čestné tvrdenie je napokon silnejšie: Forge je o tom, aby bolo vyhľadávanie reprodukovateľné, porovnateľné a kontrolovateľné. Keď kandidát vyhrá, mali by sme vedieť, ktorý cieľ vyhral, ktorých kandidátov porazil, ktorý overovač ho prijal a ktorý backend je jeho cieľom. To je oveľa užitočnejšie ako číslo plávajúce cez prezentačné snímky a vyzerajúce draho.
Zníženie úrovne je miesto, kde sa dôkazy testujú
Objavená implementácia je užitočná len vtedy, ak prežije cestu k reálnym cieľom. Výskum Forge pokrýva zostup na backends ako x86-64, RISC-V, WASM, Vulkan GPU cesty, C a Verilog. Tento zoznam cieľov nie je dekorácia. Každý backend má svoje vlastné obmedzenia, tvary inštrukcií, správanie pamäte a režimy zlyhania. Rovnaká špecifikácia musí zachovať svoj význam, zatiaľ čo sa implementácia stane niečím, čo cieľ dokáže skutočne spustiť.
Tu sa syntéza spája so zvyškom stacku Dweve. Core chce efektívne vnútorné slučky. Numerus sa stará o deterministické numerické jadrá. BitWeave chce binárne vektorové a maticové operácie, ktoré neplytvajú CPU. Kera sa stará o zostup výpočtových grafov na reálny hardvér. Forge môže tieto vrstvy napájať len vtedy, ak je vygenerovaná implementácia viac než len rýchla. Musí byť ekvivalentná, dostatočne prenosná pre zvolený cieľ a kontrolovateľná, keď sa niečo zmení.
Čo to znamená pre tímy
Pre tím nie je zaujímavý posun v tom, že stroj môže objaviť rýchlejšie jadro. Je v tom, že práca na jadrách sa stáva menej závislou od folklóru. Namiesto toho, aby si jeden expert pamätal správny trik, proces sa stáva: zadajte kontrakt, preskúmajte priestor, zmerajte kandidátov, dokážte ekvivalenciu, zaznamenajte kompromis a vygenerujte cieľový kód. Ľudia stále rozhodujú. Len prestanú robiť všetok objav ručne.
To je dôležité pre prevádzku, pretože výkonnostný dlh je drahý spôsobom, ktorý organizácie často skrývajú. Pomalé jadro znamená viac serverov. Viac serverov znamená viac nákladov, viac energie, väčšiu zložitosť nasadenia a viac šumu v plánovaní. Nesprávna optimalizácia znamená incidenty. Správny, ale nedokumentovaný trik znamená budúce migračné riziko. Forge je výskum zameraný na zníženie tejto hromady zbytočných nezmyslov.
Prichádza aj kultúrna zmena. Manuálna výkonnostná práca často odmeňuje hrdinstvo. Niekto zmizne v jaskyni a vráti sa s dômyselným bitovým hackom. Všetci tlieskajú, nikto tomu úplne nerozumie a spoločnosť získala malý posvätný predmet. Forge tlačí proces smerom k dôkazom: tu je špecifikácia, tu je cesta vyhľadávania, tu sú zamietnutí kandidáti, tu je verifikátor, tu je vybraný backend. Menej mytológie. Viac účteniek.
Kde je práca stále náročná
Nič z toho nerobí syntézu ľahkou. Špecifikácie sú náročné. Ak je špecifikácia nesprávna, engine môže verne objaviť nesprávnu vec. Vyhľadávacie priestory môžu explodovať. Riešiče môžu vypršať. Nákladové modely môžu zavádzať. Backends môžu odhaliť detaily, ktoré abstraktný výraz ignoroval. Verifikácia môže byť silná v jednej doméne a nemotorná v inej. Každý, kto predáva syntézu programov ako predajný automat na optimálny kód, buď preskakuje ťažké časti, alebo si účtuje extra za sklamanie.
Forge je zaujímavý práve preto, že čelí týmto ťažkým častiam priamo. Kombinuje niekoľko stratégií vyhľadávania. Drží verifikáciu blízko. Zaobchádza s cieľmi ako s kompromismi. Zameriava sa na reálne backends. Zostáva výskumným programom, pretože stále sa učíme, kde leží hranica medzi automatizovaným objavom, ľudským úsudkom, limitmi riešičov a realitou nasadenia.
Táto hranica stojí za preskúmanie. Softvérový priemysel má príliš veľa malých horúcich slučiek, príliš veľa duplikovaného výkonnostného folklóru a príliš veľa optimalizácií, ktorých sa nikto nechce znova dotknúť. Ak Forge dokáže premeniť čo i len časť tejto práce na opakovateľný proces založený na dôkazoch, výsledkom nie je len rýchlejší kód. Je to pokojnejší kód. Pokojnejší kód je nedocenený, väčšinou ľuďmi, ktorých nezobudili o 02:17.
Čo potrebuje dobrý beh Forge
Poriadny experiment s Forge sa začína ešte pred spustením enginu. Tím musí priniesť skutočné jadro, nie vágne sťažnosti na výkon. Potrebuje reprezentatívne vstupy, známe okrajové prípady, cieľový hardvér, aktuálne benchmarky a obchodný dôvod, prečo je toto jadro dôležité. Inak môže syntetický engine stráviť veľa času riešením problému, ktorý nikto nemá. Výskumné nástroje nie sú imúnne voči zlým vstupom. Len robia tie zlé vstupy drahšími na preskúmanie.
Najlepší vstup je malá, ostrá špecifikácia. Čo má funkcia počítať? Ktoré algebraické zákony sú dôležité? Ktoré správanie pri pretečení je zámerné? Ktoré rozsahy sú nemožné konštrukciou a ktoré sa len nevyskytli v poslednom testovacom behu? Ktoré výstupy znesú aproximáciu a ktoré nie? Tím, ktorý nevie odpovedať na tieto otázky, pravdepodobne ešte nemá problém s optimalizáciou. Má problém s vyjasnením produktu, ktorý nosí klobúk kompilátora.
Dobrý beh tiež potrebuje cieľovú pozíciu. x86-64 a RISC-V nie sú to isté. WASM má iné obmedzenia. Vulkan GPU cesty sa zaujímajú o tvary a pohyb pamäte. Verilog prináša hardvérové otázky, ktoré bežné aplikačné tímy nemajú radi pred kávou. Forge môže preskúmať zníženie cieľa, ale nemôže rozhodnúť o organizačných prioritách. Ak je prenosnosť dôležitejšia ako rýchlosť na jednom cieli, povedzte to. Ak latencia prebíja pamäť, povedzte to. Ak je tlak na registre praktický limit, povedzte aj to. Engine je výkonný, nie vševidiaci.
Výstup by sa mal brať ako balík dôkazov. Kandidát, cieľ, cesta dôkazu, zamietnuté protipríklady, backend, kontext benchmarku a otvorené výhrady. Tento balík umožňuje ľuďom urobiť rozumné rozhodnutie. Niekedy je víťazný ťah prijať kandidáta. Niekedy je ponechať staré jadro, pretože kompromis s prenosnosťou za to nestojí. Niekedy je zistenie, že špecifikácia bola príliš voľná. Všetky tri výsledky sú užitočné. Len jeden z nich vyzerá vzrušujúco na demu, preto sú demá zlým náhradníkom za inžinierstvo.
Ponaučenie
Ponaučenie z Forge je jednoduché: výkon by nemal predbiehať dôkaz. Vyhľadávanie je silné, ale vyhľadávací engine bez overenia je len veľmi energický spôsob, ako vytvárať chyby. Overenie je silné, ale bez vyhľadávania čaká, kým mu ľudia prinesú kandidátov. Forge spája oboje a pýta sa, aké jadrá môžeme objaviť, keď stroj môže skúmať, ale nesmie klamať.
To je výskum, ktorý sa oplatí robiť. Typované špecifikácie, vyhľadávanie kandidátov, lieviky dôkazov, Pareto ciele a zníženie backendu. Nie mágia. Nie skratka k produktu. Spôsob, ako vytvoriť lepší malý kód s priloženými dôkazmi.