💻 computer science

Separation Logic for Memory Conflict Detection in High-Level Synthesis

Dit artikel presenteert een raamwerk voor ruimtelijke verificatie op LLVM IR-niveau dat Separation Logic en SMT-solvers gebruikt om geheugenconflicten in High-Level Synthesis te detecteren en te voorkomen door niet-affine array-toegangen te modelleren als polymorfe ruimtelijke predicaten, waardoor veilige parallellisatie mogelijk wordt zonder de prestatiebeperkende overbenaderingen van conventionele polyhedrale methoden.

Oorspronkelijke auteurs: Yeonseok Lee

Gepubliceerd 2026-07-09

📖 4 min leestijd☕ Koffiepauze-leesvoer

CC BY 4.0

Oorspronkelijke auteurs: Yeonseok Lee

Oorspronkelijk artikel gelicentieerd onder CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dit is een AI-gegenereerde uitleg van het onderstaande artikel. Het is niet geschreven of goedgekeurd door de auteurs. Raadpleeg het oorspronkelijke artikel voor technische nauwkeurigheid. Lees de volledige disclaimer

Stel je voor dat je de directeur bent van een drukke fabriek (het High-Level Synthesis of HLS-proces). Je doel is om een supersnelle machine te bouwen die veel taken tegelijkertijd kan uitvoeren. Om dit te doen, vertel je je werkers dat ze moeten stoppen met dingen één voor één te doen en te beginnen met alles tegelijkertijd te doen in één enkele "klokcyclus".

Maar er is een groot probleem: De Memory Bottleneck.

Het Probleem: De magazijnpoort met één deur

In jouw fabriek moeten al je werkers onderdelen pakken uit een gigantisch magazijn (de Memory Bank). Maar dit magazijn heeft slechts één deur.

Als Werker A en Werker B allebei op exact hetzelfde moment door die enkele deur willen lopen, botsen ze tegen elkaar op. Dit is een Memory Conflict.
Om dit te voorkomen, zijn je oude veiligheidsregels (genaamd Polyhedral Frameworks) erg voorzichtig. Ze kijken naar de instructies van de werkers. Als de instructies complexe wiskunde bevatten (zoals het delen of vermenigvuldigen van getallen die tijdens het proces veranderen, ook wel niet-affiene rekenkunde genoemd), raken de oude regels in de war.
Omdat ze niet kunnen bewijzen dat de werkers niet zullen botsen, zeggen de oude regels: "Beter veilig dan laat. Laten we iedereen in de rij laten wachten." Dit verandert je supersnelle parallelle fabriek weer in een trage, een-voor-een rij, waardoor je snelheidswinst verloren gaat.

De Oplossing: De "Separation Logic" Kaart

Dit artikel introduceert een nieuwe, slimmere manier om crashes te controleren met beh concept genaamd Separation Logic. Zie dit niet als een wiskundige vergelijking, maar als een ruimtelijke kaart van de fabrieksvloer.

1. De "Getelementptr" Vertaler
Eerst vertaalt het systeem de complexe code naar eenvoudige, platte instructies (zoals een GPS die een enkel straatadres geeft in plaats van een complexe reeks aanwijzingen). Het kijkt naar de ruwe instructies die de computer begrijpt (LLVM IR) om precies te zien waar een werker naartoe probeert te gaan.

2. De "Exclusieve Eigendom" Regel
Separation Logic heeft een gouden regel: Je kunt niet twee keer eigenaar zijn van hetzelfde stuk land.

Stel je voor dat het magazijn is verdeeld in 4 kleinere kamers (Memory Banks).
Het systeem vraagt: "Is Werker A eigenaar van Kamer 1, en is Werker B eigenaar van Kamer 2?"
Als het antwoord ja is, zijn ze veilig. Ze kunnen tegelijkertijd naar binnen omdat ze in verschillende kamers zijn.
De magie gebeurt als ze beiden proberen Kamer 1 op te eisen. In deze logica creëert het proberen te zeggen "Ik ben eigenaar van Kamer 1" EN "Ik ben ook eigenaar van Kamer 1" op hetzelfde moment een logische tegenstrijdigheid (een crash in de logica zelf). Het systeem ziet dit direct als "Onmogelijk" en markeert het als een conflict.

3. De "Wiskundige Detective" (SMT Solver)
Het systeem gebruikt een krachtige wiskundige detective (een SMT Oracle) om de paden van de werkers te controleren.

Als de wiskunde eenvoudig is: Bewijst de detective snel: "Ja, Werker A gaat naar Kamer 1, Werker B gaat naar Kamer 2. Geen crash!" De fabriek draait parallel.
Als de wiskunde te vreemd is (onbeslisbaar): Soms bevat de wiskunde van de paden van de werkers zaken die zo complex zijn dat de detective ze niet op tijd kan oplossen.
- Oud Systeem: Zou gokken "Misschien botsen ze" en een rij afdwingen.
- Dit Systeem: Geeft toe: "Ik kan niet bewijzen dat het veilig is." Het activeert dan een Safe Fallback. Het zegt: "Omdat ik niet kan bewijzen dat het veilig is, laat ik ze om de beurt werken." Dit zorgt ervoor dat de machine nooit echt crasht, zelfs als hij iets langzamer is dan hij zou kunnen zijn.

Het Resultaat: Een Veiligere, Snellere Fabriek

Door deze "Ruimtelijke Kaart"-aanpak te gebruiken, beweert het artikel dat het:

Niet meer gokt: Het neemt niet zomaar aan dat alles gevaarlijk is omdat de wiskunde moeilijk is. Het probeert precies te bewijzen welke kamers samen veilig gebruikt kunnen worden.
Onzichtbare crashes vangt: Het vangt conflicten op die de oude "rij-vormende" regels over het hoofd hadden gezien, waardoor meer werkers parallel kunnen draaien.
Veiligheid Garandeert: Als de wiskunde te moeilijk is om op te lossen, schakelt het systeem terug naar een veilige, langzame modus. Het belooft dat de uiteindelijke machine (de hardware) nooit twee werkers zal hebben die tegelijkertijd door dezelfde deur proberen te lopen.

Kortom: Dit artikel vervangt een voorzichtige, "ga uit van het slechtste" veiligheidsregel door een slim, op kaarten gebaseerd systeem dat probeert te bewijzen dat werkers veilig samen kunnen werken. Als het dat niet kan bewijzen, dwingt het hen te wachten, wat garandeert dat de uiteindelijke hardware volledig botsingsvrij is.

Technische Samenvatting: Separation Logic voor Detectie van Geheugenconflicten in High-Level Synthesis

Probleemstelling

High-Level Synthesis (HLS) versnelt de hardwareontwikkeling door C/C++ code te vertalen naar Register Transfer Level (RTL) ontwerpen, waarbij gebruik wordt gemaakt van loop unrolling en array partitioning om parallellisme te maximaliseren. Echter, een kritieke bottleneck ontstaat bij het plannen van gelijktijdige geheugentoegang waarbij niet-affine aritmetiek (bijv. symbolische vermenigvuldiging, deling of modulo-operaties) betrokken is.

Traditionele HLS-frameworks vertrouwen op het polyedrische model voor afhankelijkheidsanalyse. Deze geometrische aanpak vereist dat loop bounds en array access functies affien zijn (lineaire combinaties van loop variabelen). Wanneer geconfronteerd met niet-affine indices, overschatten polyhedrische solvers afhankelijkheden systematisch om veiligheid te garanderen. Dit dwingt een conservatieve fallback af: het aannemen dat alle geheugenstatements van elkaar afhankelijk zijn, wat resulteert in een monolithische heap-allocatie en de serialisatie van operaties die anders parallel zouden kunnen draaien. Deze kunstmatige serialisatie degradeert de hardware-throughput en efficiëntie. Bovendien vereisen bestaande dynamische technieken vaak runtime-checks of gespecialiseerde controllers, wat overhead toevoegt.

Methodologie

Het paper stelt een ruimtelijk verificatieframework voor dat direct opereert op de LLVM Intermediate Representation (IR) om geheugenconflicten te detecteren zonder afhankelijk te zijn van affine geometrische restricties. De kernmethodologie integreert Separation Logic (SL) met Satisfiability Modulo Theories (SMT) solving.

1. Ruimtelijke Modellering op LLVM IR-niveau

In tegenstelling tot eerdere benaderingen die C/C++ Abstract Syntax Trees (ASTs) analyseren, opereert dit framework op LLVM IR. Het maakt gebruik van de getelementptr (GEP) instructie, die de compiler gebruikt om meerdimensionale array-indices mechanisch te platten naar 1D-aritmetische expressies.

Dual-State Architectuur: Het framework modelleert de systeemtoestand met behulp van twee onderscheidende componenten:
- Monotonic Store ( $s$ ): Mapt onveranderlijke Static Single Assignment (SSA) virtuele registers naar waarden. Vanwege SSA worden registers nooit overschreven, wat staatrekking vereenvoudigt.
- Spatial Heap ( $h$ ): Mapt fysieke geheugenadressen (subset van waarden) naar data, wat on-chip SRAM banks representeert.
Polymorfe Bank Predicaten: Het framework definieert ruimtelijke predicaten bank(k, A, N) die het exclusieve eigendom claimen van de $k$ -de geheugenbank voor array $A$ die is gepartitioneerd in $N$ banks. Deze predicaten passen zich dynamisch aan op basis van de partitioning strategie (Cyclic, Block, of Complete) die uit LLVM-metadata wordt geëxtraheerd.

2. De Conflict-Free Unrolling (CFU) Conditie

Om te verifiëren dat $U$ unrolled loop iteraties gelijktijdig kunnen worden uitgevoerd zonder structurele hazards, formuleert het framework de Conflict-Free Unrolling (CFU) conditie.

Separating Conjunction ( $\ast$ ): De kern van de verificatie is de geïteerdeerde scheidende conjunctie:
$cfu(E, A, N) \triangleq \ast_{i=1}^{U} bank(B(expr_i, N), A, N)$
Dit stelt dat de $U$ gelijktijdige geheugentoegangens eigenaar moeten zijn van $U$ strikt disjuncte fysieke geheugenregio's.
Spatial Collapse: Een fundamenteel axioma van Separation Logic is dat een resource niet disjunct eigendom kan zijn van zichzelf ( $P \ast P \implies \bot$ ). Als twee gelijktijdige iteraties dezelfde fysieke bank $k$ targeten, probeert de ruimtelijke formule $bank(k) \ast bank(k)$ te evalueren, wat logisch instort tot een tegenspraak ( $\bot$ ). Deze instorting dient als de wiskundige detectie van een geheugenconflict.

3. Translatie naar SMT en Fallback

Om de ruimtelijke logica berekenbaar te maken, gebruikt het framework een translatiefunctie $T$ die de ruimtelijke disjunctheidseis reduceert tot een matrix van pairwise ongelijkheden over SSA-variabelen.

Verification Condition (VC): De ruimtelijke eis wordt vertaald naar een eerste-orde logica formule:
$\pi \implies \bigwedge_{1 \le i < j \le U} (k_i \neq k_j)$
waarbij $\pi$ de padconditie is en $k_i$ de symbolische bank-indices zijn.
SMT Oracle: Een SMT-solver (bijv. Z3) probeert de VC te bewijzen.
- Sat (Satisfiable): De indices zijn bewezen verschillend; parallelle synthese kan voortgaan.
- Unsat/Unknown/Timeout: Als de solver de disjunctheid niet kan bewijzen (door onbeslisbare niet-lineaire aritmetiek), triggert het framework een deterministische sequentiële fallback. Het neemt aan dat er een hazard bestaat, waardoor de operaties geserialiseerd worden via multiplexer-gestuurde stall-logica om fysieke veiligheid te garanderen.

Belangrijkste Bijdragen

Formeel Hardware Geheugenmodel: Het paper stelt een statisch geheugenframework op over LLVM IR, waarbij meerdimensionale array-indices worden geabstraheerd via GEP-instructies en worden gekoppeld aan polymorfe ruimtelijke predicaten die cyclic, block en complete partitioning afhandelen.
Conflict-Free Unrolling (CFU) Conditie: Een definitieve ruimtelijke executie-eis wordt geformuleerd met behulp van geïteerde scheidende conjunctie. Het detecteert fysieke bank-hazards door automatische ruimtelijke logische instorting ( $cfu \implies \bot$ ) in plaats van geometrische overschatting.
Geautomatiseerde SMT Translatie en Fallback: Een wiskundig solide translatiefunctie reduceert ruimtelijke proposities tot pairwise ongelijkheden over onveranderlijke SSA-registers. Cruciaal is dat het een conservatief sequentieel fallback-model bevat om absolute veiligheid te garanderen wanneer niet-lineaire integer aritmetiek onbeslisbaar is.
Theorem of Soundness: Het paper bewijst dat indien de algebraïsche Verification Condition gevalideerd wordt door de SMT-solver, de resulterende gesynthetiseerde RTL structureel immuun is voor geheugenbank-botsingen.

Resultaten en Betekenis

Het paper beweert de kloof te overbruggen tussen formele separation logic theorie en praktische hardware synthese. Door de verificatiebelasting te verschuiven van geometrische polyhedrische modellen naar algebraïsche SMT-solving over LLVM IR, bereikt het framework het volgende:

Minimaliseert Conservatieve Serialisatie: Het vermijdt de "safe but slow" fallback van traditionele tools wanneer zij geconfronteerd worden met niet-affine indices, mits de SMT-solver de algebraïsche constraints kan oplossen.
Garandeert Structurele Veiligheid: Door het "Spatial Collapse" mechanisme en de conservatieve fallback, garandeert het framework dat geen enkele gesynthetiseerde hardware lijdt onder structurele geheugenbotsingen, zelfs in de aanwezigheid van onbeslisbare aritmetiek.
Omzeilt Affine Beperkingen: Het lost complexe bank mapping afhankelijkheden op zonder lineaire geometrische bounds te vereisen of extra runtime state-machine overhead te genereren.

De betekenis ligt in het bieden van een rigoureus, algebraïsch alternatief voor het polyhedrische model voor HLS-scheduling, wat een hogere parallellisme mogelijk maakt in ontwerpen met niet-affine geheugentoegang, terwijl de absolute veiligheidsgaranties die vereist zijn voor hardwaregeneratie behouden blijven. De auteurs merken op dat toekomstig werk zal bestaan uit de implementatie hiervan als een custom LLVM pass en het verkennen van fractional permissions om read-only gelijktijdige toegang te optimaliseren.