Automatische generatie van verweven C code

De moderne software engineering droomt van automatisch gegenereerde implementaties. Redenen daarvoor zijn de hogere mate van betrouwbaarheid van computergegenereerde code (denk aan compilers die assembly genereren) en de mogelijkheid om allerlei slimme optimalisaties in te bouwen.

Codegeneratie mag aanlokkelijk klinken, het is ook een beetje een utopie. Ten eerste is de output alleen foutloos als de input dat is (denk aan een compiler die programmeerfouten verschuift van assembly naar een hoger niveau) en ten tweede wil je voor optimalisatie zoveel mogelijk van de input weten, terwijl je dat vanwege flexibiliteit liever juist niet wilt. Bij mijn werk aan Life cycles stel ik mij tot doel om deze problemen de baas te worden op de volgende wijze.

Het probleem van correcte invoer voor een codegenerator wil ik aanpakken door een stuk bewijsvoering te doen over een systeem van life cycles. Deze bewijsvoering kan enerzijds gebaseerd zijn op de model-inhoud (en dus door de ontwerper gespecificeerd zijn ter zelfcontrole), anderzijds zullen er eigenschappen zijn die noodzakelijk zijn om correcte codegeneratie te waarborgen. Al deze eigenschappen worden door de bewijstool nagegaan en dus weet je al voor je aan codegeneratie begint dat de uitvoer correct zal zijn.

De strijdigheid qua optimalisatie is volgens mij ook oplosbaar. Een heel practisch voorbeeld daarvan is de manier waarop de Linux kernel enerzijds heel flexibel te configureren is, maar anderzijds zo veel mogelijk verbanden hard (=efficient) codeert. Deze ogenschijnlijke tegenstelling wordt ondervangen door conditionele compilatie (#ifdefs). Op deze manier is het mogelijk om zowel een algemeen-maar-traag stuk code alsook een efficient-maar-niet-altijd bruikbaar stuk code op te nemen en daartussen te selecteren door toepassen van kennis die elders in de programmatuur is opgenomen, in dit voorbeeld ten gevolge van gemeenschappelijk bekende `kernel opties'.

Als optimalisatietechniek denk ik dat het dooreenweven van lagen code van groot belang is. In Life cycles zijn die lagen expliciet zichtbaar als refinement. Deze structuren zijn soms om te zetten in aanroepen van methodes, soms in inlined code (het dooreenvlechten of -weven).

Een casus voor een domein als dit dient vanzelfsprekend meerdere lagen van refinement te kennen, en dient de dynamische mogelijkheden van Life cycles uit te buiten. Om de efficientie voelbaar te maken is het goed wanneer het gaat om code die vaak executeert en dat dan zeer snel moet doen. Een goede casus lijkt me het genereren van C-code uit een Life cycle specificatie van paar lagen van de Blue Tooth protocollen voor draadloos netwerken. Netwerkcode wordt voor alle/veel netwerkpakketjes uitgevoerd en moet daarom snel zijn, en dat is eigenlijk alleen goed te bereiken door nauwe verweving van de lagen.

Voor deze opdracht zoeken we binnenkort mogelijk een werknemer die bereid is hier een aantal dagen per week aan te besteden, tegen de gebruikelijke vergoedingen. Deze opdracht wordt vermoedelijk gecombineerd met de implementatie van de life cycle checker. Voor informatie kun je langskomen, bellen of mailen met Rick van Rein.