Kovanje in iskanje, ki si zasluži svoj dokaz
Stari trik s problemom
Vsak resen programski sistem ima nekaj delov kode, ki so veliko pomembnejši, kot bi po velikosti sodili. Zanka, ki se zažene milijonkrat. Bitna operacija v poti stiskanja. Majhna matrična rutina. Jedro modularne aritmetike. Nekaj, kar je v pregledu kode videti nenevarno, nato pa tiho odloča o računu za energijo, proračunu zakasnitve ali številu strežnikov, ki jih moraš kupiti. Programska oprema je zelo demokratična. Ena drobcena funkcija lahko pokvari sestanek za vse.
V preteklosti so ta jedra izboljševali ljudje. Starejši inženir se spomni trika iz članka. Nekdo prebrska staro objavo na forumu. Napiše se nabor meril uspešnosti. Preizkusi se nekaj kandidatov. Najhitrejši zmaga, če je še vedno videti pravilen. Nato ga organizacija zamrzne, ker se ga znova dotakniti zdi kot zbodsti speči transformator z vilicami.
Forge je raziskava boljše različice tega procesa. Je sintezni pogon za majhne, ključne implementacije: daj mu tipizirano specifikacijo in lastnosti, pusti mu iskati kandidatne programe, meri in primerjaj kompromise, preveri enakovrednost, nato pa odkrito implementacijo prenesi na cilje, ki so pomembni. Pomembna beseda ni iskanje. Pomembna beseda je še vedno. Še vedno mora biti pravilen.
Zato Forge živi v raziskavah. Ni javni gumb izdelka, kamor nekdo vpiše naredi hitreje in dobi čudež. Je sintezna delovna miza za partnerjeve poskuse, odkrivanje jeder in raziskave o tem, kako daleč lahko gre avtomatizirano iskanje, ko je povezano s preverjanjem in ne s teatrom meril uspešnosti.
Specifikacija je štartna črta
Optimizacija brez specifikacije je zgolj igra na srečo z lepšimi imeni spremenljivk. Ko se pojavi domiseln kandidat, mora ekipa vedeti, kaj naj bi ohranil. Ali obravnava vsak vnos ali le prijazne iz meril uspešnosti? Ali spoštuje obnašanje pri prelivu? Ali je algebraična identiteta veljavna pri reprezentaciji, ki se dejansko uporablja? Ali ohranja enako semantiko, ko se prenese na drug zaledni sistem?
Forge začne s tipiziranimi izrazi in lastnostmi, ker iskanje potrebuje mejo. Meja pove, kaj šteje kot enakovredno. Brez nje lahko pogon najde nekaj osupljivo hitro tako, da izbriše polovico dela. Računalniki so odlični v zlonamerni ubogljivosti, kadar je pogodba nejasna.
Iskalna stran je namenoma v množini. Naštevalno iskanje je uporabno, ko je prostor dovolj majhen, da ga pokrijemo. CEGIS je uporaben, kadar lahko protiprimeri usmerjajo izboljševanje. Genetsko programiranje in MCTS raziskujeta drugače. Iskanje z vodeno strojno učenje se lahko nauči modele stroškov in daje prednost obetavnim območjem. Nobena od teh metod ni univerzalno najboljša. To ni slabost. Tako se iskanje obnaša v resničnem svetu. Če bi eno kladivo rešilo vsako jedro, bi bile škatle z orodjem zelo dolgočasne in proizvajalci strojne opreme bi bili brezposelni.
Raziskovalno vprašanje je, kako te pogone združiti z dovolj dokaznega pritiska, da rezultat ni zgolj domiseln. Sintetizirano jedro mora preživeti tako merila uspešnosti na srečni poti kot preverjevalnik na nesrečni poti. Sicer izboljšava ni inženirstvo. Je čarovniški trik s stroški vzdrževanja.
Preverjevalnik je odrasla oseba v prostoru
Forge uporablja sklop preverjanj, ker nobeno posamezno preverjanje ni dovolj za vsa področja. Hitri primeri so poceni in uporabni. Testi lastnosti odkrijejo široke razrede napak in skrčijo protiprimere na nekaj, kar lahko človek prebere. Reševalniki SMT, kot sta Z3 in CVC5, lahko dokažejo enakovrednost tam, kjer je kodiranje obvladljivo. Izčrpno preverjanje je praktično za majhna področja. Izravnava enakovrednosti z e-grafi ponuja še eno pot skozi algebraično enakovrednost.
Sklop je pomemben, ker jedra odpovedo na siten način. Kandidat lahko prestane vse običajne primerjalne teste in je še vedno napačen pri robnem primeru. Lahko je pravilen za nepredznačene vnose in napačen za predznačene. Lahko je pravilen v matematičnem polju in napačen, ko izbrana predstavitev prekorači obseg. Lahko je pravilen pred prevajanjem in subtilno napačen po odločitvi o izbiri navodil. Preverjevalnik obstaja, ker optimizem ni strategija testiranja. Preverili smo. Večkrat. In še vedno drži.
Obstaja tudi praktičen razlog za več poti dokazovanja. Formalne metode so zmogljive, a niso brezplačne. Nekatera kodiranja presežejo časovno omejitev. Nekatera področja so prevelika za izčrpno preverjanje. Nekatere lastnosti je lažje najprej preveriti verjetnostno in dokazati pozneje. Forge obravnava preverjanje kot lijak, ne kot ritual čistosti. Poceni preverjanja zavrnejo očitne nesmisle. Močnejša preverjanja zaščitijo končnega kandidata.
Hitro ni ena sama številka
Delo s zmogljivostjo postane smešno, ko ena metrika prevlada nad vsem pogovorom. Zakasnitev je pomembna. Število operacij je pomembno. Poraba pomnilnika je pomembna. Pritisak na registre je pomemben. Čas prevajanja je včasih pomemben. Prenosljivost je pomembna, ko mora isto jedro delovati na več kot enem zaledju. Kandidat, ki zmaga pri zakasnitvi, a pri tem požiga registre kot majhen kres, je lahko napačen za dejanski cilj. Kandidat, ki je majhen, a počasen, je lahko uporaben drugje. Kontekst ostaja neporažen.
Forge zato optimizacijo oblikuje kot problem Pareto. Pogon lahko išče po ciljih, namesto da se pretvarja, da obstaja en univerzalen rezultat, ki ga je izdala zelo samozavestna preglednica. Uporaben rezultat ni vedno edini najhitrejši kandidat. Včasih je to družina kandidatov z vidnimi kompromisi, da lahko inženir izbere tistega, ki ustreza omejitvam uvajanja.
To je tudi razlog, zakaj v objavah na spletnem dnevniku ne maram golih trditev o pospešitvi. Raziskovalna stran lahko opisuje notranja pričakovanja in eksperimentalne cilje, javne trditve pa potrebujejo sveže izvedbe, trenutno strojno opremo, trenutne zastavice prevajalnika in natančen kontekst delovne obremenitve. Sicer številka postane spominek. Spominki so lepi. Niso arhitektura.
Poštena trditev je tako ali tako močnejša: Forge je o tem, da iskanje postane ponovljivo, primerljivo in preverljivo. Ko kandidat zmaga, moramo vedeti, kateri cilj je dosegel, katere kandidate je premagal, kateri preverjevalnik ga je sprejel in katero zaledje je njegov cilj. To je veliko bolj uporabno kot številka, ki plava skozi predstavitev in izgleda draga.
Prevajanje je kraj, kjer se dokazi preizkusijo
Odkrita implementacija je uporabna le, če preživi pot do dejanskih ciljev. Raziskave Forge zajemajo prevajanje na zaledja, kot so x86-64, RISC-V, WASM, grafične poti Vulkan, C in Verilog. Ta seznam ciljev ni okras. Vsako zaledje ima svoje omejitve, oblike ukazov, pomnilniško vedenje in načine odpovedi. Ista specifikacija mora ohraniti svoj pomen, medtem ko implementacija postane nekaj, kar cilj dejansko lahko izvaja.
Tu se sinteza poveže s preostalim delom sklada Dweve. Core želi učinkovite notranje zanke. Numerus skrbi za deterministična numerična jedra. BitWeave želi binarne vektorske in matrične operacije, ki ne zapravljajo procesorja. Kera skrbi za prevajanje računskih grafov na dejansko strojno opremo. Forge lahko napaja te plasti le, če je ustvarjena implementacija več kot le hitra. Biti mora enakovredna, dovolj prenosljiva za izbrani cilj in pregledna, ko se kaj spremeni.
Kaj to pomeni za ekipe
Za ekipo zanimiv premik ni v tem, da bi stroj morda odkril hitrejše jedro. Gre za to, da delo z jedri postane manj odvisno od ljudskega izročila. Namesto da se en strokovnjak spomni pravega trika, postane postopek naslednji: določi pogodbo, preišči prostor, izmeri kandidate, dokaži enakovrednost, zabeleži kompromis in ustvari ciljno kodo. Ljudje še vedno odločajo. Le ne opravljajo več vsega odkrivanja ročno.
To je pomembno za operacije, ker je dolg zaradi zmogljivosti drag na način, ki ga organizacije pogosto skrivajo. Počasno jedro pomeni več strežnikov. Več strežnikov pomeni več stroškov, več energije, več zapletenosti pri uvajanju in več šuma pri načrtovanju. Napačna optimizacija postane incident. Pravilen, a nedokumentiran trik postane prihodnje tveganje pri selitvi. Forge je raziskava za zmanjšanje tega kopičenja izogibnih neumnosti.
Sprememba je tudi kulturna. Ročno delo z zmogljivostjo pogosto nagrajuje junaštvo. Nekdo izgine v votlino in se vrne s pametnim trikom. Vsi ploskajo, nihče ga povsem ne razume, podjetje pa je pridobilo majhen sveti predmet. Forge usmerja proces k dokazom: tukaj je specifikacija, tukaj je pot iskanja, tukaj so zavrnjeni kandidati, tukaj je preverjevalnik, tukaj je izbrano zaledje. Manj mitologije. Več dokazil.
Kje je delo še vedno težko
Nič od tega ne naredi sinteze lahke. Specifikacije so težke. Če je specifikacija napačna, lahko pogon zvesto odkrije napačno stvar. Prostori iskanja lahko eksplodirajo. Reševalniki lahko presežejo časovno omejitev. Modeli stroškov lahko zavedejo. Zaledja lahko razkrijejo podrobnosti, ki jih abstraktni izraz ni upošteval. Preverjanje je lahko močno na enem področju in nerodno na drugem. Vsakdo, ki prodaja sintezo programov kot avtomat za optimalno kodo, bodisi preskoči težke dele bodisi zaračuna dodatno za razočaranje.
Forge je zanimiv prav zato, ker se s temi težkimi deli sooča neposredno. Združuje več strategij iskanja. Preverjanje ohranja blizu. Na cilje gleda kot na kompromise. Cilja na resnična zaledja. Ostaja raziskovalni program, ker se še vedno učimo, kje je meja med avtomatiziranim odkrivanjem, človeško presojo, omejitvami reševalnikov in realnostjo uvajanja.
To mejo je vredno raziskovati. Programska industrija ima preveč majhnih vročih zank, preveč podvojenega izročila o zmogljivosti in preveč optimizacij, ki se jih nihče ne želi več dotakniti. Če lahko Forge tudi le del tega dela spremeni v ponovljiv proces z dokazi, rezultat ni le hitrejša koda. Je mirnejša koda. Mirnejša koda je podcenjena, večinoma pri ljudeh, ki jih ob 02:17 niso klicali na intervencijo.
Kaj dobra izvedba Forge potrebuje
Resen Forge poskus se začne, preden se pogon zažene. Ekipa mora prinesti pravo jedro, ne nejasne pritožbe o zmogljivosti. Potrebuje reprezentativne vhode, znane robne primere, ciljno strojno opremo, trenutne primerjalne teste in poslovni razlog, zakaj je to jedro pomembno. V nasprotnem primeru lahko sintezni pogon porabi veliko časa za reševanje problema, ki ga nihče dejansko nima. Raziskovalna orodja niso imuna na smetanske vhode. Le poskrbijo, da je smetano dražje pregledati.
Najbolj uporaben vhod je majhna, ostra pogodba. Kaj naj funkcija izračuna? Kateri algebraični zakoni so pomembni? Katero vedenje pri prelivu je namerno? Kateri obsegi so po konstrukciji nemogoči in kateri se preprosto niso zgodili v zadnjem testnem zagonu? Kateri izhodi lahko prenesejo približek in kateri ne? Ekipa, ki ne more odgovoriti na ta vprašanja, verjetno še nima problema z optimizacijo. Ima problem z razjasnitvijo izdelka, oblečen v prevleko prevajalnika.
Dober zagon potrebuje tudi ciljno držo. x86-64 in RISC-V nista enaka. WASM ima drugačne omejitve. Vulkan GPU poti so odvisne od oblik in premikanja pomnilnika. Verilog odpira strojna vprašanja, ki jih običajne aplikacijske ekipe redko uživajo pred kavo. Forge lahko raziskuje ciljno nižanje, vendar ne more odločati o organizacijskih prioritetah. Če je prenosljivost pomembnejša od hitrosti na enem cilju, to povejte. Če zakasnitev pretehta pomnilnik, to povejte. Če je pritisk na registre praktična meja, povejte tudi to. Pogon je zmogljiv, ne jasnoviden.
Izhod je treba obravnavati kot paket dokazov. Kandidat, cilj, pot dokaza, zavrnjeni protiprimeri, zaledje, kontekst primerjalnega testa in odprte omejitve. Ta paket je tisto, kar ljudem omogoča sprejeti razumno odločitev. Včasih je zmagovalna poteza sprejeti kandidata. Včasih je obdržati staro jedro, ker kompromis pri prenosljivosti ni vreden tega. Včasih je odkritje, da je bila specifikacija preohlapna. Vsi trije izidi so uporabni. Le eden od njih je videti razburljiv v predstavitvi, zato so predstavitve slab nadomestek za inženirstvo.
Nauk
Nauk Forge je preprost: zmogljivost ne sme prehiteti dokaza. Iskanje je močno, vendar je iskalnik brez preverjanja le zelo energičen način za ustvarjanje hroščev. Preverjanje je močno, vendar brez iskanja čaka, da mu ljudje prinesejo kandidate. Forge združi oboje in se vpraša, kakšna jedra lahko odkrijemo, ko stroju dovolimo raziskovati, vendar mu ne dovolimo lagati.
To je raziskava, ki se jo splača opraviti. Tipizirane specifikacije, iskanje kandidatov, lijaki dokazov, Pareto cilji in nižanje zaledja. Ne čarovnija. Ne bližnjica do izdelka. Način za ustvarjanje boljše majhne kode z dokazi.