Technische Samenvatting: Snelle Ramsey Quantifier Eliminatie in LIRA

Probleemstelling

Programmaverificatie, met name voor oneindige toestandsystemen, vereist vaak redeneren over eigenschappen die niet uitdrukbaar zijn in standaard eerste-orde logica. Hoewel Satisfiability Modulo Theories (SMT) solvers effectief zijn in het afhandelen van veiligheidseigenschappen met behulp van eerste-orde theorieën (bijv. Lineaire Integer Arithmetica - LIA, Lineaire Reële Arithmetica - LRA), vereist het bewijzen van liveness (zoals terminatie) doorgaans redeneren over wel-gegrondheid (well-foundedness). Deze eigenschap is niet eerste-orde definieerbaar, zelfs niet met recursieve predicaten.

Recent werk heeft Ramsey-kwantoren voorgesteld als een verenigd raamwerk om dergelijke eigenschappen te behandelen. Een Ramsey-kwantor, genoteerd als $\exists^{\text{ram}} x, y: \phi(x, y, z)$, stelt de existentie van een oneindige gerichte klik aan in de graaf gedefinieerd door $\phi$. Dit is waar als er een oneindige sequentie van onderling onderscheidbare vectoren $a_1, a_2, \dots$ bestaat waarvoor $\phi(a_i, a_j, z)$ geldt voor alle $1 \le i < j$. Dit formalisme maakt het mogelijk om liveness en monadische decomponeerbaarheid te coderen.

Echter, ondanks theoretische bewijzen dat Ramsey-kwantoren in polynomiale tijd geëlimineerd kunnen worden voor de existentiële fragmenten van LIA, LRA en de gemengde casus (LIRA), heeft praktische implementatie hiervan ontbroken. Eerdere implementaties waren:

1. Prototypaal en beperkt: Bestaande tools waren primair prototypes voor LIA en LRA, zonder een volledige implementatie voor de gemengde LIRA-casus.
2. Schaalbaarheidsissues: Testen was beperkt tot kleine micro-benchmarks.
3. Gebruikersbarrières: Implementaties leunden zwaar op specifieke API's (bijv. Z3 Python), wat het voor gebruikers onmogelijk maakte om constraints in standaard SMT-LIB-formaten te specificeren of te integreren met andere solvers.

Methodologie

Het artikel presenteert REAL (Ramsey Elimination for Arithmetic Logic), een solver-agnostische tool ontworpen om Ramsey-kwantoren te elimineren uit existentiële formules in LIA, LRA en LIRA. De methodologie bestaat uit een drietraps-pipeline:

1. Input Specificatie (SMT-LIB Extensie):
   REAL breidt de SMT-LIB-standaard uit om Ramsey-kwantoren te ondersteunen. Het introduceert nieuwe syntaxisregels voor termen, waardoor gebruikers constraints kunnen specificeren met behulp van (ramsey ...) constructen. Dit stelt de tool in staat om inputs in een gestandaardiseerd formaat te accepteren in plaats van te vertrouwen op propriëtaire API-aanroepen.

2. Eliminatie Algoritme:
   Bouwend op het theoretische raamwerk gevestigd in eerder werk [5], berekent REAL een equivalente formule die alleen standaard existentiële kwantoren bevat. Het algoritme:

   • Vervangt existentieel gekwantificeerde variabelen in de oorspronkelijke formule door aanvullende Ramsey-gekwantificeerde variabelen.
   • Identificeert voldoende en noodzakelijke condities voor de existentie van een oneindige klik, en formuleert deze als existentiële LIRA-formules.
   • Bijvoorbeeld, een conditie die een oneindige sequentie $a, a+b, a+2b, \dots$ vereist, wordt vertaald naar constraints op de basisvector $a$ en de stapvector $b$.

3. Implementatie Optimalisaties (REAL vs. Prototype):
   De auteurs hebben de oorspronkelijke prototype-implementatie aanzienlijk verbeterd door middel van drie hoofdcategorieën van optimalisatie:

   • Datastructuren: Implementatie van caching en sharing voor (sub)formules, efficiëntere normalisatie van atoomvormen, en het combineren van duplicerende boom-wandelingen (tree walks) om computationele overhead te verminderen.
   • Formule Structuur: Directe afhandeling van integer gelijkheden en niet-strikte reële ongelijkheden, het delen van gemeenschappelijke subexpressies in Booleaanse abstracties, en het vervangen van onnodige theorie-variabelen door Booleaanse variabelen om compactere formules te produceren.
   • Interoperabiliteit: De tool geeft de resulterende kwantorvrije formule uit als een standaard SMT-LIB bestand, dat verwerkt kan worden door elke SMT solver die LIA, LRA of LIRA ondersteunt (bijv. Z3).

4. Applicatie Pipeline (Alchemist):
   Om het nut bij liveness-checking aan te tonen, hebben de auteurs Alchemist ontwikkeld, een transpiler die bereikbaarheidsrelaties gegenereerd door FAST(er) (een tool voor het verifiëren van bereikbaarheid in integer counter systemen met de Armoise taal) omzet naar het SMT-LIB formaat dat vereist is door REAL. Dit creëert een volledige toolchain: Armoise $\to$ FAST(er) $\to$ Alchemist $\to$ REAL $\to$ SMT Solver.

Belangrijkste Bijdragen

• De Tool REAL: Een solver-agnostische eliminatieprocedure voor Ramsey-kwantoren die LIA, LRA en LIRA ondersteunt.
• Gestandaardiseerde Input/Output: De eerste implementatie waarbij constraints gespecificeerd kunnen worden via een uitgebreid SMT-LIB formaat, wat de strikte afhankelijkheid van specifieke solver API's wegneemt.
• Prestatieverbeteringen: Een substantiële versnelling ten opzichte van de oorspronkelijke prototype door geoptimaliseerde datastructuren en formule-generatietechnieken.
• Liveness Verificatie Raamwerk: Een gedemonstreerde pipeline (Fig. 1) die bereikbaarheidsrelaties van integer counter systemen vertaalt naar Ramsey-kwantor formules, wat automatische liveness verificatie voor geparametriseerde gedistribueerde protocollen mogelijk maakt.

Experimentele Resultaten

Experimenten werden uitgevoerd op een Arch Linux machine met gebruik van Z3 v4.15.1 voor satisfiability checking.

• Casestudies: De tool verifieerde succesvol de liveness voor verschillende benchmarks, waaronder de McCarthy 91 functie, het Sliding Window Protocol, Lamports Bakery Algorithm, en diverse Cache Coherence protocollen (Berkeley, Dragon, MOESI, SYNAPSE, futurbus).
  • Voor de McCarthy 91 functie verifieerde REAL succesvol de afwezigheid van oneindige kliks, waarmee terminatie werd bewezen.
  • Voor het Lamport Bakery algoritme identificeerde de tool correct dat het verifiëren van de afwezigheid van een oneindige klik die één proces uithongert (starvation), faalt zonder fairness-aannames.
• Prestatie Metrieken:
  • Schaalbaarheid: De eliminatietijd schaalt bijna lineair met de probleemdimensie over diverse benchmark-families (Sorted Chain, Average, Cyclic Dependency, Bounding Box). Formulen met duizenden atomen en variabelen werden verwerkt in sub-seconde tot lage seconden bereiken.
  • Vergelijking met Prototype: REAL presteert vele malen sneller dan het originele prototype in zowel eliminatie- als oplostijden (Fig. 5). In sommige integer gevallen is de gegenereerde output zo eenvoudig dat de tijd van de solver de eliminatietijd overstijgt.
  • Formule Grootte: REAL produceert aanzienlijk compactere formules vergeleken met het prototype, wat het aantal boomknopen in de output SMT-formules vermindert (Fig. 3).

Betekenis en Claims

Het artikel claimt dat REAL een modulaire en efficiënte verificatie-pipeline biedt voor oneindige toestandsystemen. Door de kloof tussen theoretische eliminatie-algoritmen en praktische SMT-gebaseerde verificatie te overbruggen, maakt het de automatische controle van liveness-eigenschappen mogelijk die voorheen moeilijk uit te drukken of op te lossen waren.

De auteurs merken op dat hoewel de aanpak effectief is, de gemengde lineaire integer reële arithmetica (LIRA) casus nog steeds aanzienlijke overhead met zich meebrengt vergeleken met pure LIA of LRA vanwege de huidige scheiding van integer en reële variabelen. Zij suggereren dat toekomstig werk het vervangen van FASTer door tools die direct op bereikbaarheidsrelaties targeten, of het stroomlijnen van de pipeline om SMT-encoding redundantie te verminderen, zou kunnen omvatten. Het artikel concludeert dat de huidige implementatie erin slaagt de mogelijkheden van bestaande tools zoals FASTer uit te breiden om liveness-checking voor geparametriseerde gedistribueerde protocollen te faciliteren.