Het artikel bespreekt programmasynthese, het proces waarbij automatisch een programma wordt geconstrueerd dat voldoet aan een specifieke logische specificatie. Omdat de zoekruimte voor programma's exponentieel groot is, richt de auteur zich op component-gebaseerde, loop-vrije programma's.
De centrale methodiek is Counterexample-Guided Iterative Synthesis (CEGIS). Dit iteratieve proces bestaat uit twee hoofdfasen:
- Eindige synthese: Het vinden van een programma dat correct is voor een kleine, specifieke set inputs.
- Verificatie: Het controleren of dit programma voor alle mogelijke inputs correct is door te zoeken naar een tegenvoorbeeld.
Indien er een tegenvoorbeeld wordt gevonden, wordt dit toegevoegd aan de inputset en herhaalt het proces zich tot er een universeel correct programma is gevonden of is bewezen dat er geen oplossing bestaat. De implementatie is geschreven in Rust en maakt gebruik van de Z3 SMT-solver. De auteur illustreert de praktische waarde aan de hand van complexe bit-manipulaties en het automatiseren van peephole optimizers voor compilers.
Programmasynthese van loop-vrije programma's met Rust en Z3
Het automatisch vinden van een programma dat voldoet aan een gegeven specificatie wordt programmasynthese genoemd. De grootste uitdaging is dat de zoekruimte enorm is: het aantal programma's van grootte $n$ groeit exponentieel. Het naïef enumereren van elk programma van grootte $n$, controleren of deze aan de specificatie voldoet en vervolgens doorgaan naar programma's van grootte $n+1$, schaalt niet. Het vakgebied is echter vooruitgegaan door slimmere zoektechnieken te gebruiken om de zoekruimte in te perken, te profiteren van prestatieverbeteringen in SMT-solvers en soms de reikwijdte van het probleem te beperken.
In dit artikel leg ik een benadering uit voor moderne programmasynthese: counterexample-guided iterative synthesis (CEGIS) van component-gebaseerde, loop-vrije programma's, zoals beschreven in Synthesis of Loop-Free Programs door Gulwani et al. We zullen precies analyseren wat elk van deze termen betekent en we lopen door een implementatie in Rust die de Z3-solver gebruikt.
Mijn doelen voor dit artikel zijn tweeledig:
- Ik hoop dat mensen die onbekend zijn met programmasynthese iets nieuws over het onderwerp leren. Ik heb geprobeerd veel voorbeelden te geven en de complexe logische formules uit het paper op te splitsen in kleinere, begrijpelijke stukken.
- Ik hoop dat mensen die al bekend zijn met dit soort synthese mij kunnen helpen bij het diagnosticeren van prestatieproblemen in de implementatie, waar ik de resultaten uit de literatuur niet heb kunnen reproduceren. Voor sommige van de moeilijkere benchmark-problemen slaagt de synthesizer er niet eens in een oplossing te vinden voordat mijn geduld op is.
Motivatie
Waarom zou je een programma schrijven dat andere programma's voor je schrijft? Naast gemak zijn er veel valide redenen waarom men programma's zou willen synthetiseren.
Sommige programma's zijn erg lastig om handmatig correct te schrijven, terwijl een programmasynthesizer kan slagen waar een mens faalt. Neem bijvoorbeeld het isoleren van het meest rechtse nul-bit in een woord met slechts drie bit-manipulatie-instructies.
Voorbeeld: Het meest rechtse nul-bit isoleren
- Input:
011010011
- Output:
000000100 (alleen dat bit is gezet)
De oplossing is als volgt:
isolate_rightmost_zero_bit(x): // x = 011010011
a ← not x // a = 100101100
b ← add 1, x // b = 011010100
c ← and a, b // c = 000000100
return c
Onze programmasynthesizer vindt een oplossing in minder dan een seconde, en de minimale oplossing in ongeveer een minuut.
Een andere reden is de noodzaak om veel meer programma's te schrijven dan handmatig haalbaar is. Denk aan de peephole optimizer van een compiler. Deze bekijkt een glijdend venster van instructiesequenties en controleert of er een equivalente, maar snellere of kleinere sequentie bestaat.
Peephole-optimizers worden meestal geconstrueerd uit pattern-matching regels:
new PeepholeOptimizer(
pattern0 → replacement0
pattern1 → replacement1
// ...
patternn → replacementn
)
Elke replacement_i is een klein, geoptimaliseerd mini-programma. In LLVM's InstCombine optimizer zijn er meer dan 1.000 van deze paren. In plaats van deze handmatig te schrijven, kunnen we elke originele sequentie als specificatie gebruiken en een synthesizer vragen de optimale sequentie te vinden. Dit idee is voorgesteld door Bansal et al. in Automatic Generation of Peephole Superoptimizers.
Een overzicht van de taak
Programmasynthese is het proces van het nemen van een specificatie en het automatisch vinden van een programma dat hieraan voldoet. Om het probleem beheersbaar te maken, beperken we de reikwijdte op twee manieren:
- Loop-vrij: We synthetiseren alleen programma's zonder lussen.
- Component-gebaseerd: We synthetiseren alleen programma's die kunnen worden uitgedrukt als de compositie van een gegeven bibliotheek van componenten.
Component-gebaseerde synthese betekent dat de synthesizer een bibliotheek van componenten krijgt en programma's synthetiseert die elk van deze componenten exact één keer gebruiken. De synthesizer herschikt de componenten en verbindt hun inputs en outputs totdat er een configuratie is gevonden die aan de specificatie voldoet.
Gegeven een bibliotheek van $N$ componenten, wordt een programma geconstrueerd in de vorm:
synthesized_program(inputs...):
temp0 ← component0(params0...)
temp1 ← component1(params1...)
// ...
tempN-1 ← componentN-1(paramsN-1...)
return tempN-1
Waarbij elke parameter in paramsi ofwel een eerder gedefinieerde tempj variabele is, of een van de oorspronkelijke inputs.
Vergelijking: Algemene vs. Component-gebaseerde Synthese
| Eigenschap | Algemene Synthese | Component-gebaseerde Synthese |
|---|
| Vorm van programma's | Elke combinatie van taalexpressies | Alleen componenten uit de bibliotheek |
| Grootte van programma's | Variabel | Exact de grootte van de bibliotheek (elk component wordt één keer gebruikt) |
In onze synthesizer zijn componenten functies over integers met een vaste bitbreedte (bitvectoren) en corresponderen ze met een enkele instructie (zoals add, and, xor).
Formalisering van het probleem
Een specificatie is een logische expressie die de gewenste output beschrijft bij gegeven inputs.
- $\vec{I}$ zijn de programmainputs.
- $O$ is de programma-output.
- $\phi_{\mathrm{spec}}(\vec{I}, O)$ is de expressie die de inputs aan de output relateert.
De bibliotheek van componenten is een multi-set van specificaties. Voor elk component $i$:
- $\vec{I}_i$ zijn de inputvariabelen van het component.
- $O_i$ is de outputvariabele.
- $\phii(\vec{I}i, O_i)$ is de logische expressie die de input aan de output relateert.
Voor het voorbeeld van het isoleren van het meest rechtse nul-bit ziet de minimale bibliotheek er als volgt uit:
| Component | Definitie | Beschrijving |
|---|
| $\phi0(I0, O_0)$ | $O0 = \texttt{bvadd}(1, I0)$ | Optellen van één op bitvectoren |
| $\phi1(I1, I2, O1)$ | $O1 = \texttt{bvand}(I1, I_2)$ | Bitwise AND operatie |
| $\phi2(I3, O_2)$ | $O0 = \texttt{bvnot}(I3)$ | Bitwise NOT operatie |
Programmasynthese kan worden uitgedrukt als een exists-forall probleem: we willen weten of er een programma $P$ bestaat dat voor alle mogelijke inputs en outputs aan de specificatie voldoet. $$\exists P: \forall \vec{I}, O: P(\vec{I}) = O \implies \phi_{\mathrm{spec}}(\vec{I}, O)$$
Een korte introductie tot SMT-solvers
SMT-solvers, zoals Z3, nemen een logische formule en geven aan of deze:
- Satisfiable (Vervulbaar): Er is een toewijzing aan de variabelen die de beweringen waar maakt (inclusief een model van deze toewijzing).
- Unsatisfiable (Niet vervulbaar): Er is geen enkele toewijzing die de beweringen waar kan maken.
SMT-solvers gebruiken een Lisp-achtige taal genaamd SMT-LIB2. Voorbeeld van een satisfiable query:
(declare-const Int x)
(assert (= 5 (+ x 2)))
(check-sat)
(get-model) ; x is 3
De meeste solvers zijn optimaal in first-order, implicitly existential queries. Gekoppelde $\exists$ en $\forall$ quantifiers maken solvers vaak traag of incompleet.
Counterexample-Guided Iterative Synthesis (CEGIS)
CEGIS stelt ons in staat om exists-forall queries op te lossen door ze op te splitsen in meerdere first-order existential queries.
Het CEGIS-algoritme
- Initialisatie: Kies een kleine, eindige set inputs $S$.
- Loop:
- Eindige synthese: Zoek een programma $P$ dat correct is voor de inputs in $S$. Als dit onmogelijk is (
unsat), is er geen oplossing.
- Verificatie: Controleer of $P$ correct is voor alle mogelijke inputs. Zoek naar een input $\vec{I}$ waarvoor $P(\vec{I}) = O \land \lnot \phi_{\mathrm{spec}}(\vec{I}, O)$.
- Resultaat:
- Als er geen tegenvoorbeeld is (
unsat), dan is $P$ de oplossing.
- Als er een tegenvoorbeeld is, voeg $\vec{I}$ toe aan $S$ en begin de loop opnieuw.
Eindige synthese vs. Verificatie
- Eindige synthese: Vindt een programma dat werkt voor een specifieke set voorbeelden. Dit is een existentiële query over $P$.
- Verificatie: Probeert te bewijzen dat het programma overal werkt door te zoeken naar één enkel tegenvoorbeeld.
CEGIS met componenten
Voor component-gebaseerde programma's gebruiken we een locatiemapping. In plaats van het programma regel voor regel te beschrijven, definiëren we voor elk component:
- Op welke regel het staat.
- Van welke bron (input of regel van een ander component) de argumenten komen.
Verificatie van een component-gebaseerd programma
Verificatie verbindt de componenten via de locatiemapping en vraagt de solver naar een tegenvoorbeeld. We definiëren:
- $\textbf{P}$: De set van alle parameters van alle componenten in de bibliotheek.
- $\textbf{R}$: De set van alle resultaten van de componenten.
- $\phi_{\mathrm{lib}}(\textbf{P}, \textbf{R})$: De combinatie van alle individuele component-specificaties.
- $\phi_{\mathrm{conn}}(\vec{I}, O, \textbf{P}, \textbf{R})$: De verbindingen tussen componenten bepaald door de locatiemapping.
De verificatie-constraint is: $$\exists \vec{I}, O, \textbf{P}, \textbf{R} : \phi{\mathrm{conn}}(\vec{I}, O, \textbf{P}, \textbf{R}) \land \phi{\mathrm{lib}}(\textbf{P}, \textbf{R}) \land \lnot \phi_{\mathrm{spec}}(\vec{I}, O)$$
Eindige synthese van een component-gebaseerd programma
Hier zoeken we naar een locatiemapping $L$ die voldoet aan de specificaties voor de set $S$. Om ongeldige programma's te voorkomen, voegen we constraints toe:
- Consistentie ($\psi_{\mathrm{cons}}$): Geen twee componenten mogen op dezelfde regel staan.
- Acycliciteit ($\psi_{\mathrm{acyc}}$): Parameters moeten gedefinieerd zijn vóór het component dat ze gebruikt (geen dataflow-cycli).
- Well-formed program ($\psi_{\mathrm{wfp}}$): De mapping moet consistent en acyclisch zijn, en alle locaties moeten binnen de grenzen vallen.
De finale query voor eindige synthese is: $$\exists L, Oi, \textbf{P}i, \textbf{R}i : \psi{\mathrm{wfp}}(L) \land \bigwedge{i=0}^{|S|-1} (\phi{\mathrm{lib}}(\textbf{P}i, \textbf{R}i) \land \psi_{\mathrm{
Programmasynthese van loop-vrije programma's met Rust en Z3
Het automatisch vinden van een programma dat voldoet aan een gegeven specificatie wordt programmasynthese genoemd. De grootste uitdaging is dat de zoekruimte enorm is: het aantal programma's van grootte $n$ groeit exponentieel. Het naïef enumereren van elk programma van grootte $n$, controleren of deze aan de specificatie voldoet en vervolgens doorgaan naar programma's van grootte $n+1$, schaalt niet. Het vakgebied is echter vooruitgegaan door slimmere zoektechnieken te gebruiken om de zoekruimte in te perken, te profiteren van prestatieverbeteringen in SMT-solvers en soms de reikwijdte van het probleem te beperken.
In dit artikel leg ik een benadering uit voor moderne programmasynthese: counterexample-guided iterative synthesis (CEGIS) van component-gebaseerde, loop-vrije programma's, zoals beschreven in Synthesis of Loop-Free Programs door Gulwani et al. We zullen precies analyseren wat elk van deze termen betekent en we lopen door een implementatie in Rust die de Z3-solver gebruikt.
Mijn doelen voor dit artikel zijn tweeledig:
- Ik hoop dat mensen die onbekend zijn met programmasynthese iets nieuws over het onderwerp leren. Ik heb geprobeerd veel voorbeelden te geven en de complexe logische formules uit het paper op te splitsen in kleinere, begrijpelijke stukken.
- Ik hoop dat mensen die al bekend zijn met dit soort synthese mij kunnen helpen bij het diagnosticeren van prestatieproblemen in de implementatie, waar ik de resultaten uit de literatuur niet heb kunnen reproduceren. Voor sommige van de moeilijkere benchmark-problemen slaagt de synthesizer er niet eens in een oplossing te vinden voordat mijn geduld op is.
Motivatie
Waarom zou je een programma schrijven dat andere programma's voor je schrijft? Naast gemak zijn er veel valide redenen waarom men programma's zou willen synthetiseren.
Sommige programma's zijn erg lastig om handmatig correct te schrijven, terwijl een programmasynthesizer kan slagen waar een mens faalt. Neem bijvoorbeeld het isoleren van het meest rechtse nul-bit in een woord met slechts drie bit-manipulatie-instructies.
Voorbeeld: Het meest rechtse nul-bit isoleren
- Input:
011010011
- Output:
000000100 (alleen dat bit is gezet)
De oplossing is als volgt:
isolate_rightmost_zero_bit(x): // x = 011010011
a ← not x // a = 100101100
b ← add 1, x // b = 011010100
c ← and a, b // c = 000000100
return c
Onze programmasynthesizer vindt een oplossing in minder dan een seconde, en de minimale oplossing in ongeveer een minuut.
Een andere reden is de noodzaak om veel meer programma's te schrijven dan handmatig haalbaar is. Denk aan de peephole optimizer van een compiler. Deze bekijkt een glijdend venster van instructiesequenties en controleert of er een equivalente, maar snellere of kleinere sequentie bestaat.
Peephole-optimizers worden meestal geconstrueerd uit pattern-matching regels:
new PeepholeOptimizer(
pattern0 → replacement0
pattern1 → replacement1
// ...
patternn → replacementn
)
Elke replacement_i is een klein, geoptimaliseerd mini-programma. In LLVM's InstCombine optimizer zijn er meer dan 1.000 van deze paren. In plaats van deze handmatig te schrijven, kunnen we elke originele sequentie als specificatie gebruiken en een synthesizer vragen de optimale sequentie te vinden. Dit idee is voorgesteld door Bansal et al. in Automatic Generation of Peephole Superoptimizers.
Een overzicht van de taak
Programmasynthese is het proces van het nemen van een specificatie en het automatisch vinden van een programma dat hieraan voldoet. Om het probleem beheersbaar te maken, beperken we de reikwijdte op twee manieren:
- Loop-vrij: We synthetiseren alleen programma's zonder lussen.
- Component-gebaseerd: We synthetiseren alleen programma's die kunnen worden uitgedrukt als de compositie van een gegeven bibliotheek van componenten.
Component-gebaseerde synthese betekent dat de synthesizer een bibliotheek van componenten krijgt en programma's synthetiseert die elk van deze componenten exact één keer gebruiken. De synthesizer herschikt de componenten en verbindt hun inputs en outputs totdat er een configuratie is gevonden die aan de specificatie voldoet.
Gegeven een bibliotheek van $N$ componenten, wordt een programma geconstrueerd in de vorm:
synthesized_program(inputs...):
temp0 ← component0(params0...)
temp1 ← component1(params1...)
// ...
tempN-1 ← componentN-1(paramsN-1...)
return tempN-1
Waarbij elke parameter in paramsi ofwel een eerder gedefinieerde tempj variabele is, of een van de oorspronkelijke inputs.
Vergelijking: Algemene vs. Component-gebaseerde Synthese
| Eigenschap | Algemene Synthese | Component-gebaseerde Synthese |
|---|
| Vorm van programma's | Elke combinatie van taalexpressies | Alleen componenten uit de bibliotheek |
| Grootte van programma's | Variabel | Exact de grootte van de bibliotheek (elk component wordt één keer gebruikt) |
In onze synthesizer zijn componenten functies over integers met een vaste bitbreedte (bitvectoren) en corresponderen ze met een enkele instructie (zoals add, and, xor).
Formalisering van het probleem
Een specificatie is een logische expressie die de gewenste output beschrijft bij gegeven inputs.
- $\vec{I}$ zijn de programmainputs.
- $O$ is de programma-output.
- $\phi_{\mathrm{spec}}(\vec{I}, O)$ is de expressie die de inputs aan de output relateert.
De bibliotheek van componenten is een multi-set van specificaties. Voor elk component $i$:
- $\vec{I}_i$ zijn de inputvariabelen van het component.
- $O_i$ is de outputvariabele.
- $\phii(\vec{I}i, O_i)$ is de logische expressie die de input aan de output relateert.
Voor het voorbeeld van het isoleren van het meest rechtse nul-bit ziet de minimale bibliotheek er als volgt uit:
| Component | Definitie | Beschrijving |
|---|
| $\phi0(I0, O_0)$ | $O0 = \texttt{bvadd}(1, I0)$ | Optellen van één op bitvectoren |
| $\phi1(I1, I2, O1)$ | $O1 = \texttt{bvand}(I1, I_2)$ | Bitwise AND operatie |
| $\phi2(I3, O_2)$ | $O0 = \texttt{bvnot}(I3)$ | Bitwise NOT operatie |
Programmasynthese kan worden uitgedrukt als een exists-forall probleem: we willen weten of er een programma $P$ bestaat dat voor alle mogelijke inputs en outputs aan de specificatie voldoet. $$\exists P: \forall \vec{I}, O: P(\vec{I}) = O \implies \phi_{\mathrm{spec}}(\vec{I}, O)$$
Een korte introductie tot SMT-solvers
SMT-solvers, zoals Z3, nemen een logische formule en geven aan of deze:
- Satisfiable (Vervulbaar): Er is een toewijzing aan de variabelen die de beweringen waar maakt (inclusief een model van deze toewijzing).
- Unsatisfiable (Niet vervulbaar): Er is geen enkele toewijzing die de beweringen waar kan maken.
SMT-solvers gebruiken een Lisp-achtige taal genaamd SMT-LIB2. Voorbeeld van een satisfiable query:
(declare-const Int x)
(assert (= 5 (+ x 2)))
(check-sat)
(get-model) ; x is 3
De meeste solvers zijn optimaal in first-order, implicitly existential queries. Gekoppelde $\exists$ en $\forall$ quantifiers maken solvers vaak traag of incompleet.
Counterexample-Guided Iterative Synthesis (CEGIS)
CEGIS stelt ons in staat om exists-forall queries op te lossen door ze op te splitsen in meerdere first-order existential queries.
Het CEGIS-algoritme
- Initialisatie: Kies een kleine, eindige set inputs $S$.
- Loop:
- Eindige synthese: Zoek een programma $P$ dat correct is voor de inputs in $S$. Als dit onmogelijk is (
unsat), is er geen oplossing.
- Verificatie: Controleer of $P$ correct is voor alle mogelijke inputs. Zoek naar een input $\vec{I}$ waarvoor $P(\vec{I}) = O \land \lnot \phi_{\mathrm{spec}}(\vec{I}, O)$.
- Resultaat:
- Als er geen tegenvoorbeeld is (
unsat), dan is $P$ de oplossing.
- Als er een tegenvoorbeeld is, voeg $\vec{I}$ toe aan $S$ en begin de loop opnieuw.
Eindige synthese vs. Verificatie
- Eindige synthese: Vindt een programma dat werkt voor een specifieke set voorbeelden. Dit is een existentiële query over $P$.
- Verificatie: Probeert te bewijzen dat het programma overal werkt door te zoeken naar één enkel tegenvoorbeeld.
CEGIS met componenten
Voor component-gebaseerde programma's gebruiken we een locatiemapping. In plaats van het programma regel voor regel te beschrijven, definiëren we voor elk component:
- Op welke regel het staat.
- Van welke bron (input of regel van een ander component) de argumenten komen.
Verificatie van een component-gebaseerd programma
Verificatie verbindt de componenten via de locatiemapping en vraagt de solver naar een tegenvoorbeeld. We definiëren:
- $\textbf{P}$: De set van alle parameters van alle componenten in de bibliotheek.
- $\textbf{R}$: De set van alle resultaten van de componenten.
- $\phi_{\mathrm{lib}}(\textbf{P}, \textbf{R})$: De combinatie van alle individuele component-specificaties.
- $\phi_{\mathrm{conn}}(\vec{I}, O, \textbf{P}, \textbf{R})$: De verbindingen tussen componenten bepaald door de locatiemapping.
De verificatie-constraint is: $$\exists \vec{I}, O, \textbf{P}, \textbf{R} : \phi{\mathrm{conn}}(\vec{I}, O, \textbf{P}, \textbf{R}) \land \phi{\mathrm{lib}}(\textbf{P}, \textbf{R}) \land \lnot \phi_{\mathrm{spec}}(\vec{I}, O)$$
Eindige synthese van een component-gebaseerd programma
Hier zoeken we naar een locatiemapping $L$ die voldoet aan de specificaties voor de set $S$. Om ongeldige programma's te voorkomen, voegen we constraints toe:
- Consistentie ($\psi_{\mathrm{cons}}$): Geen twee componenten mogen op dezelfde regel staan.
- Acycliciteit ($\psi_{\mathrm{acyc}}$): Parameters moeten gedefinieerd zijn vóór het component dat ze gebruikt (geen dataflow-cycli).
- Well-formed program ($\psi_{\mathrm{wfp}}$): De mapping moet consistent en acyclisch zijn, en alle locaties moeten binnen de grenzen vallen.
De finale query voor eindige synthese is: $$\exists L, Oi, \textbf{P}i, \textbf{R}i : \psi{\mathrm{wfp}}(L) \land \bigwedge{i=0}^{|S|-1} (\phi{\mathrm{lib}}(\textbf{P}i, \textbf{R}i) \land \psi_{\mathrm{
Groetjes,