ROUGH DRAFT authorea.com/80928
Main Data History
Export
Show Index Toggle 4 comments
  •  Quick Edit
  • Tézisfüzet

    Bevezetés

    A magas szintű nyelvek megjelenésével egyidőben jelen meg az igény arra, hogy a fordítóprogramok képesek legyenek fordítási időben bizonyos programtulajdonságokat elemezni. Ennek eleinte két fontos praktikus oka volt. Az egyik, hogy így írt programok futási ideje felvegye a versenyt az assembly nyelven írt programokkal, ami különösen fontos volt az akkori szűkös hardvereken. Másrész, akkoriban egy lyukkártyán leadott program esetében a fordítási hibát csak napokkal később kapta kézhez a programozó, célszerű volt tehát olyan fordítót írni, ami a lehető legtöbb hibáról és hibalehetőségről visszajelzést ad a fejlesztőnek, illetve a lehető legtöbb esetben megpróbálja kitalálni a programozó szándékát.

    A helyzet mára teljesen megváltozott, a szoftverfejlesztő a fordítás kimenetéről általában perceken belül visszajelzést kap, az assembly nyelv pedig csak néhány speciális területen maradt használatban. Érdekes módon azonban a programok fordítási idejű elemzésének igénye egyáltalán nem csökkent. Ellenkezőleg, a mai szoftverek olyan méretűre nőttek, hogy azokat egy ember már képtelen átlátni, ennek következtében egyre nagyobb szerepe van a fordítónak abban, hogy az esetleges programhibákat már fordítási időben kiszűrje.

    Másrészt az utóbbi években egyre több mindent szoftver vezérel (gondoljunk a mostanában terjedő Internet of Thingsre), és ezek egy része az emberi élet szempontjából is kritikus lehet. Egy ilyen példa a repülőgépek fly-by-wire rendszere, amelyek vezérlésének válaszidejére komoly garanciákat kell a gyártónak adnia. Ezeket rendkívül bonyolult szoftverekkel lehet csak validálni, az emberi munkával történő bizonyítás az időszüksége miatt komoly versenyhátrányt jelentene a tervezőknek.

    Egy másik példa a mai beágyazott rendszerek. Egy mai készülék komoly hardver és szoftver együttese, ha valahogy meg tudjuk határozni a beágyazott rendszeren futó szoftver hardverigényét, azzal a gyártó a gyártási költségeit tudja optimalizálni, ami egy nagy példányszámban eladott termék esetén komoly megtakarítás lehet. A legtöbb ilyen termékben a gyártók a mai napig C nyelvet használnak, mert a programozóknak ezen a nyelven van a legnagyobb kontrollja a memóriahasználat felett. Sajnos egy modernebb nyelv hardverigénye és válaszideje (pl. szemétgyűjtés miatt) jóval kiszámíthatatlanabb, ezért ezekbe a szegmensekbe a modern nyelvek nem tudtak betörni annak ellenére, hogy a szoftverfejlesztési költségeket jelentősen csökkentené.

    A fenti okok miatt kezdődött el a kutatása annak, hogy a programok erőforrásigényét elemző eszközökkel meg lehessen határozni. Ennek egyik lehetséges megoldása, hogy a kész, lefordított programot vizsgáljuk. Másik megoldás, hogy a program struktúráit vizsgáljuk magas szinten. Ennek egyik példája a fejlett típusrendszer, amelynek nagy előnye, hogy a program és a program elemzése lényegében ugyanabban a programkódban történik, külső eszköz nélkül. Más megközelítés az a módszer, amelyeket a fordítóprogramok használnak a programok elemzésére, pl. adatfolyam analízis és absztakt interpretáció.

    Doktori dolgozatomban azzal foglalkoztam, hogy funkcionális nyelvekben (Haskell és F#) előforduló adatszerkezetek mérete hogyan határozható meg fordítási időben. Ez az információ közvetlenül segít a memóriahasználat kikövetkeztetésében, és közvetve felhasználható a futási idő elemzéséhez is.

    Alkalmazott módszerek

    Munkám során igyekeztem a legkülönbözőbb területekről a legkorszerűbb technológiákat és kutatási eredményeket felhasználni, így szükségesnek érzem egy szakaszt szentelni a felhasznált eszközök és módszerek rövid bemutatására. A következő bekezdésekben bemutatom, hogy mit nevezünk funkcionális nyelvnek, mik ezeknek a nyelveknek a jellemző típusrendszereik, és milyen programtulajdonságokat lehet ezekkel ellenőrizni. Ezután röviden ismertetem az absztrakt interpretációt is, mint alternatívát. A fenti módszerek implementálására használt beágyazás zárja az alkalmazott módszerek ismeretetését.

    A kutatás során elsősorban tisztán funkcionális nyelvek elemzésével foglalkoztam. Funkcionális nyelvek alatt azokat a programozási nyelveket nevezzük, amelyek támogatják a funkcionális programozási paradigmát. Ez egy olyan deklaratív programozási stílus, amelyben támogatják a mellékhatásmentes függvények használatát, és az olyan adatszerkezeteket, amelyek nem módosíthatóak. Az ilyen nyelvekben a függvények első rendű elemként jelennek meg, és jellemző a magasabb rendű függvények használata, valamint a fejlett típusrendszer is.

    A funkcionális nyelvek között kiemelkedő helyet foglalnak el a tisztán funkcionális nyelvek. Ezek a nyelvekre teljesül a hivatkozási helyfüggetlenség. Ez azt jelenti, hogy ha egy függvényt kétszer meghívok ugyanazzal a paraméterezéssel, az eredmény ugyanaz lesz. Ezek a nyelvek egyáltalán nem támogatnak változókat és állapotokat, valamint a mellékhatásokat (fájlrendszer használat, képernyőkezelés) is közvetett módon oldják meg. Egy ilyen elterjedt megoldás a monádok használata (pl. Haskell), ahol a monádok ábrázolják a külső vagy belső állapottal végezhető műveleteket, és a programunkat ezeknek a műveleteknek a segítségével építhetjük fel anélkül, hogy a hivatkozási helyfüggetlenség sérülne.

    A tisztán funkcionális nyelvek az egyszerű és tiszta elméleti alapok miatt jól tárgyalhatóak, ennek egyik bizonyítéka, hogy a típusrendszerek legnagyobb eredményei is ezekhez a nyelvekhez köthetőek. A tisztán funkcionális nyelvek a gyakran statikus típusosak, azaz ellenőrzik, hogy a függvényeket megfelelő típusú paraméterekkel hívtuk-e meg. Sőt, a legtöbb tisztán funkcionális nyelvek úgy képesek a programok típushelyességét ellenőrizni, hogy a programozónak a függvények típusait nem is kell megadnia, hanem a fordítás része a típuskikövetkeztetés (Hindley–Milner típusrendszer). Ezeknek a nyelveknek egy másik gyakori jellemzője, hogy megenged olyan típusokat, amelyek egy típusparamétertől függenek (ún. polimorf típusok). Ezt a rendszert System F-nek (vagy \(\lambda_{2}\)-nek) nevezzük.

    Ha a típusrendszerben megengedjük azt is, hogy a típusaink ne csak típusparaméterektől, hanem kifejezésektől is függjenek, eljutunk a függő típusokig (\(\lambda\Pi\)). Ennek egy speciális esete a méretkódolt típusok (sized types), ahol a típusainknak nemnegatív egész paraméterei vannak, amelyek az adott típusú argumentum méretét (pl. lista esetében a hosszát) kódolják. Egy másik lehetséges bővítés az, hogy típusparaméternek nem csak típusokat, hanem tetszőleges polimorf típusokat is megengedünk (System \(F_{\omega}\), vagy \(\lambda_{\omega}\)). Ezekben a nyelvekben a típuskikövetkeztetés azonban már eldönthetetlen probléma.

    A típusrendszerek fontosságára mutat rá a Curry-Howard izomorfizmus, amely azt mondja ki, hogy a függvények típusai és a függvények törzse a matematikai logika állításainak és bizonyításainak feleltethetőek meg. Ez arra használható, hogy a függvény típusába bele tudjuk kódolni a függvény bizonyos tulajdonságait is, amennyiben a típusrendszerünk elegendő kifejezőerővel bír. A fenti általánosításokra épül a Coq nyelv típusrendszere (Calculus of (Inductive) Constructions) illetve hasonló kifejezőerővel bír az Agda nyelv is, amely függő típusos (Martin-Löf–féle konstruktív típusrendszer), mely kifejezőereje megegyezik a konstruktív logikával.

    A fenti példa azt mutatja, hogy tetszőleges programtulajdonság vizsgálható és bizonyítható megfelelő típusrendszerrel. A programok statikus elemzésére egy másik módszer a programok absztrakt interpretációja. Ebben a módszerben a program viselkedését közelítjük úgy, hogy tulajdonképpen egy absztrakt állapottéren futtatjuk le. Ezt a megoldás gyakran használják a fordítóprogramok a programok elemzésére (a control-flow és data-flow elemzés mellett).

    Egy ilyen absztakt állapottér lehet a méretek felső korlátja. Ekkor az interpretáló függvényünk listákhoz a listák méretét rendeli. Ez a módszer nem számítja ki a listák konkrét elemeit, csak azok méreteit, ezáltal egy közelítését adja a megoldásnak.

    A fejlett típusrendszerek lehetővé teszik, hogy egy gazdanyelv segítségével megfogalmazzunk egy olyan programozási nyelvet, amelyet a gazdanyelv eszközeivel írunk le és a gazdanyelv típusrendszere ellenőriz. Ennek a megoldásnak az az előnye, hogy nem kell egy programozási nyelvet újraalkotnunk, hiszen a gazda nyelv szintaktikus és szemantikus elemzőjét, de akár a kódgenerátorát is fel tudjuk használni. Másrészt a nyelvet használónak nem kell egy teljesen új nyelvet megtanulnia, hiszen a gazdanyelv eszközei a beágyazott nyelvben is rendelkezésre állhatnak (a beágyazástól függően).

    A fejlett típusrendszerre azért van szükség, hogy a beágyazott nyelv típusrendszerét a gazdarendszer típusain belül kell megfogalmaznunk, amennyiben a nyelv fordítási hibáit valóban a gazdanyelv fordítási idejében akarjuk feltárni.