Generalized data flow graphs : theory and applications
de Gg Gjalt Gerrit Jong · TU/e Research Portal · 1993
Het toepassingsgebied van de concepten die in dit proefschrift worden gedefinieerd, en van de theorema's en eigenschappen die worden bewezen, is het automatisch genereren van gefutegreerde schakelingen.Uitgaande van een hoog niveau beschrijving van de specificatie van de functie van een systeem, leidt hoog niveau syntbese tot een netwerk graaf, dat wil zeggen een beschrijving op structuur-, of register-transfer, niveau, en een controle-graaf, die definieert welke modulen actief zijn op welk moment.De netwerkgraaf is bet belangrijkste resultaat van de allocatie-fase, terwijl de controle-graaf bet resultaat is van de scheduling fase.De hoog niveau beschrijving is veelal een programma of een algoritme die de functie van het te ontwerpen systeem beschrijft.Het data flow graaf concept is een zeer geschikt fonnalisme voor synthese, omdat het alle noodzakelijke details bevat die nodig zijn om synthese te bedrijven, zonder rekening te hoeven houden met specifieke syntactische constructies van een taal.Het is daarom een algemeen formalisme.Een data flow graaf legt ook geen andere beperkingen op aan de uitvoering van het systeem dan die voorgeschreven zijn door de data afhankelijkheden in de hoog niveau beschrijving.In dit proefschrift is het data flow graaf concept uitgebreid met takken die meer dan een eindpunt en (meer dan een) beginpunt hebben, de zogenoemde hypertakken.Data flow grafen hebben normaal gesproken alleen maar takken met een begin-en een eindpunt.Het toestaan van takken met meerdere eindpunten leidt niet tot een grotere expressiviteit, maar van takken met meerdere beginpunten wel.Deze laatste takken leiden tot het begrip 'keuze'.Op deze manier is een netwerk X SAMENVA TilNG een speciaal geval van deze veralgemeniseerde data flow grafen, namelijk die in welke alle knopen zijn gedefinieerd als verschillende soorten hardware modulen in plaats van door een bepaald soort abstract gedrag.De takken met meerdere einden beginpunten in de data flow graaf zijn gelijk aan netten in een netwerk.Ook wordt aangetoond dat de controle-graaf ~n abstractie is van de beschouwde data flow graaf.Daarom is hoog niveau synthese een graaftransformatie op het data flow graaf niveau.Scheduling blijkt dan een partitionering van de flow graaf te zijn, welke geiinpliceerd wordt door het aanbrengen van volgorde-takken.Volgorde-takken hebben in principe dezelfde functie als de normale data-takken, namelijk zij stellen een data precedentie relatie voor.Een andere belangrijke taak van hoog niveau synthese is het minimaliseren van het aantal multiplexers en demultiplexers.De (de)multiplexers worden geihtroduceerd door de scheduling (in welke zij meestal niet eens expliciet genoemd worden), en door de controle statements in de specificatie, zoals de if en de while.Ook scheduling is een graaftransformatie waarvan bewezen kan worden dat zij gedragsbehoudend is.Met de hier gepresenteerde concepten zijn een aantal eisen geformuleerd onder welke synthese resulteert in een goed werkend en equivalent gedragend netwerk, en waarin het systeem alleen beperkt wordt in het aantal executie-volgordes.Deze eisen blijken minder restrictief te zijn dan die van bestaande synthesesystemen.Dit geeft de mogelijkheid om betere oplossingen te vinden.Gewone data flow grafen kunnen beschouwd worden als 'marked Petri nets', terwijl keuze inbegrepen is in bet hier gepresenteerde veralgemeniseerde data flow graaf concept, hetgeen tot mogelijk niet-determinisme leidt.In principe is het begrip conflict ook toegevoegd.De meeste resultaten veronderstellen een conflictvrije flow graaf, omdat conflict niet voorkomt in het toepassingsgebied van hoog niveau synthese.Conflict wordt echter wel beschouwd in een van de belangrijkste resultaten, namelijk de reductietechniek om zo weinig mogelijk van de bereikbare toestandsruimte van een data flow graaf te berekenen.Deze techniek wordt anticipatie genoemd.Het is bijvoorbeeld bewezen dat een keuze-vrije graaf deterministisch is, en dat maar een toestandsreeks van de bereikbare toestandsruimte nodig is om het gedrag van de flow graaf te bepalen.Een paar executie-volgordes zijn maar nodig, wanneer de data flow graaf niet keuze-vrij is.Omdat conflict in gewone, dat wil zeggen ongeiitterpreteerde, Petri netten en keuze in data flow grafen elkaars duale zijn, is hetzelfde resultaat geldig voor Petri netten.Verscheidene semantieken zijn gedefinieerd voor de veralgemeniseerde data flow grafen: een operationele semantiek en twee denotationele semantieken.Een denotationele semantiek modelleert alleen maar het (input-output) gedrag van een SAMENVAT!lNGXi flow graaf, terwijl de andere ook de verschillende executie-volgordes representeert, dat wil zeggen bet interne gedrag.Een andere denotationele semantiek die gepresenteerd wordt is gebaseerd op een proces algebra.Van al deze semantieken wordt bewezen dat ze equivalent aan elkaar zijn, en dat zij gelijk zijn aan de semantieken zoals die gedefinieerd zijn voor gewone, dat wil zeggen keuzevrije, data flow grafen.Met deze semantieken zijn enkele eigenschap-behoudende transformaties gedefinieerd, die hoofdzakelijk gebruikt worden in hierarchische expansie van knopen en voor abstractie.Verders zijn er enkele voorbeelden gegeven om de afwezigheid aan te tonen van enige andere beperking dan de data afhankelijkheden zelf in het data flow graaf concept.Deze voorbeelden tonen ook de kracht van de anticipatie strategie, zelfs voor Petri netten, en illustreren enkele andere theorema's.Ook is er aangetoond hoe data flow grafen gebruikt kunnen worden voor specificaties welke op het eerste gezicht botsen met het data flow principe, zoals het geval is voor bepaalde constructies die veelal voorkomen in parallelle programma's en in specificaties waarbij controle de belangrijkste rol speelt.Ook wordt een techniek beschreven die gebruikt kan worden om eisen aan welke een systeem moet voldoen, en die geen deel uitmaken van de functionele specificatie, te verifieren.Voorbeelden van zulke extra eisen zijn het niet optreden van deadlock en de afwezigheid van •verhongering' voor een verzameling van samenwerkende flow grafen.De gebruikte techniek is 'model checking' van temporele logische formules.Temporele logica staat een grote verscheidenheid van eigenschappen toe om te controleren, en is niet beperkt tot de klassieke eigenschappen van liveness en safeness in Petri netten.Een uitbreiding op deze methode van 'model checking' is gepresenteerd, waarbij beperkingen worden aangedragen waaronder het beschouwde systeem aan (de) bepaalde extra eisen zou kunnen voldoen, voorzover mogelijk.Deze suggesties zijn in de vorm van extra volgorde-takken, zodat alleen het zich correct gedragende deel van de toestandsruimte bereikbaar is.I should mention here Jos van Eijndhoven as manager of the Esprit BRA 3281 project, better known as the ASCIS project.He also was stimulating me on discovering the possibilities of data flow graphs.