Péter Bereczky, Dániel Horpácsi, Simon Thompson: Program Equivalence in the Erlang Actor Model

Computers, https://doi.org/10.3390/computers13110276

A modern szoftverek életútja nem ér véget a megírásukkal: folyamatosan javítják, bővítik, optimalizálják és átalakítják őket. Ezek az átalakítások történhetnek kézzel (például kódrészletek átszervezésével) vagy automatikusan (például a fordítóprogram vagy refaktoráló eszközök segítségével). Lényeges azonban, hogy ezek a módosítások ne változtassák meg a program viselkedését – hiszen egy apró eltérés is hibákat okozhat.

A gyakorlatban az átalakítások helyességét többnyire teszteléssel ellenőrzik, ám ez nem mindig elég: bizonyos esetekben a hibák rejtve maradhatnak. Megbízhatóbb módszer, ha matematikai alapokra támaszkodunk, vagyis a programozási nyelv formális szemantikáját (pontos, matematikai leírását) használjuk. Erre építve meghatározható a programekvivalencia fogalma: két program akkor ekvivalens, ha ugyanúgy viselkednek a külvilág számára, még akkor is, ha belső működésük vagy kommunikációs felépítésük eltér.

A kutatók most a Core Erlang nyelv – az Erlang nyelv egy leegyszerűsített, köztes változata – működését írták le részletesen, a párhuzamos programfutásra koncentrálva. A Core Erlang egy olyan programozási nyelv, amelyben az egymással párhuzamosan futó programrészek üzeneteket küldhetnek egymásnak, és ezeket az üzeneteket speciális jelekkel (például exit vagy link jel) kísérhetik.

Az új leírás pontosan meghatározza, hogyan zajlik az üzenetküldés és -fogadás, mégpedig az Erlang/OTP 23 hivatalos szabványához igazodva. Ez azért fontos, mert így a nyelv viselkedését matematikai pontossággal lehet modellezni, és bizonyítani lehet, ha két program ugyanazt csinálja, még akkor is, ha belül másképp van megírva.

A kutatók példákat is hoztak arra, mikor számít két program egyenértékűnek: például ha csak a folyamatok azonosítóját nevezzük át, vagy ha olyan „csendes” műveleteket hajtunk végre, amelyek nem változtatják meg a kimenetet.

A módszert egy konkrét helyzetben is kipróbálták: megmutatták, hogy bizonyos feltételek mellett egy lista feldolgozása sorban (lépésről lépésre) és párhuzamosan (egyszerre több részen dolgozva) is ugyanazt az eredményt adhatja. Ez a megközelítés segíthet abban, hogy a jövőben biztonságosan lehessen átalakítani vagy optimalizálni a párhuzamos programokat anélkül, hogy új hibák kerülnének a rendszerbe.