 |
Mihai Budiu -- mihaib+@cs.cmu.edu
http://www.cs.cmu.edu/~mihaib/
octombrie 2001
Pe data de 8 august 2000 pe lista de e-mail numită ``Linux kernel'', care este folosită de către cei care meșteresc la nucleul sistemului de operare Linux pentru a comunica între ei, a apărut un mesaj care descria o serie de potențiale probleme (bug-uri) din nucleu, trimis de Dawson Engler, un proaspăt profesor la universitatea Stanford. Pe această listă se vehiculează adesea rapoarte de defecțiuni, așa că unul în plus nu pare ceva deosebit. Mesajul cu pricina însă conținea nu una, două, sau chiar zece erori, ci peste 160! Și mai interesant, toate aceste potențiale erori au fost descoperite automat, folosind un program care studiază codul și caută inadvertențe. În final nu toate rapoartele s-au dovedit a fi defecțiuni, dar multe dintre ele erau într-adevăr bug-uri importante.
Acest mesaj de poștă electronică este probabil cea mai ``vizibilă'' aplicare a unei tehnologii încă relativ imature, dar care face progrese remarcabile, numită verificare formală. Verificarea formală este folosită pe scară relativ largă, dar mai ales de către proiectanții de hardware; multe din circuitele procesoarelor moderne au fost certificate ca fiind corecte folosind verificarea formală. O cercetare febrilă se desfășoară pentru a adapta metodele dezvoltate pentru hardware și la analiza programelor; software-ul are însă o natură substanțial diferită de a hardware-ului, și probabil va fi nevoie de inventarea unor tehnici noi.
În acest articol voi descrie pe scurt metodele folosite de echipa de la Stanford condusă de Dawson Engler pentru a descoperi erori în programe, și unele din rezultatele lor foarte interesante despre natura erorilor în nucleul Linux.
Un aforism spune că orice program are cel puțin un bug și este cu cel puțin o linie prea lung. Aplicînd această regulă în mod repetat putem deduce că orice program poate fi optimizat pînă este redus la o singură linie de cod, care este eronată.
Chiar dacă sistemul de operare Linux este lăudat pentru robustețea sa deosebită, nu este scutit de imperfecțiuni. Profitînd de disponibilitatea surselor C ale programului, cercetătorii de la Stanford au testat o nouă metodologie pentru a descoperi bug-uri pe 21 de versiuni diferite ale nucleului, începînd de la versiunea 1.0, din ianuarie 1994, pînă la versiunea 2.4.7, din primăvara acestui an. Trebuie menționat dintru început că sistemul de la Stanford nu descoperă toate bug-urile, ci numai anumite tipuri de bug-uri, relativ simple; voi discuta metodologia folosită ceva mai încolo. Vom considera că bug-urile descoperite de acest sistem sunt reprezentative pentru toate bug-urile în general, cel puțin în anumite aspecte ale distribuțiilor statistice. E de rețiunt deci că rezultatele pe care le prezint în continuare se referă la un subset al tuturor bug-urilor, care poate nu este reprezentativ.
Codul Linux e structurat din mai multe părți relativ independente; putem factoriza codul însă în două mari clase: nucleul propriu-zis, și driverele. Driverele sunt mici programe care fac parte din nucleu și care interfațează nucleul cu dispozitivele periferice. Datorită popularității PC-ului, există literalmente mii de periferice diferite, fiecare avînd nevoie de un driver separat1. Ca atare, majoritatea codului Linux se află în drivere. Cantitatea de cod din drivere variază între 50 și 70 la sută din întregul sistem.
Între versiunile 1.0 și 2.4.1 codul sistemului Linux a crescut de aproximativ 16 ori, de la 105 mii de linii de cod la 1,6 milioane2 Cel mai mult au crescut driverele, datorită faptului că din ce în ce mai mulți fabricanți de hardware au publicat informații despre periferice sau chiar au contribuit cu cod. Alte subsisteme care au crescut sensibil între timp sunt sistemele de fișiere și codul pentru protocoalele de rețea.
În total, în cele 21 de versiuni de nucleu sistemul de la Stanford a detectat peste 1000 de bug-uri distincte. (Unele dintre bug-uri se manifestă în mai multe versiuni diferite de nucleu.) Numărul de bug-uri este practic direct proporțional cu mărimea codului: nucleele mai mari aveau mai multe erori.
Bug-urile sunt însă departe de a fi uniform distribuite. După cum ne așteptăm, cele mai multe bug-uri sunt în drivere, pentru că driverele ocupă atît de mult din cod. Putem normaliza numărul de bug-uri în două feluri: împărțim la numărul de linii, pentru a vedea la cîte linii avem un bug, sau putem împărți la numărul de locuri în care același tip de bug s-ar fi putut manifesta. De exemplu, dacă un bug care constă în lipsa verificării unui cod de eroare după apelul unei funcții care poate eșua, densitatea de bug-uri este numărul de locuri în care nu verificăm eroarea împărțit la numărul de locuri în care apelăm funcții care pot returna erori.
Chiar dacă normalizăm numărul de bug-uri, driverele stau însă destul de rău: densitatea de bug-uri în drivere este între 3 și 7 ori mai mare decît în nucleul propriu-zis. Driverele sunt folosite doar de cei care au perifericele corespunzătoare, spre deosebire de nucleu, care e folosit practic de toată lumea. Ca atare, driverele sunt mai puțin testate, deci este de așteptăt să aibă mai multe bug-uri.
Înțelepciunea populară spune că cu cît un program e mai ``bătrîn'', cu atît are mai puține bug-uri; acest lucru este verificat și de datele despre Linux: fișierele cele mai vechi au cele mai puține bug-uri. La nivel de funcție, funcțiile mai lungi tind să aibă o densitate mai mare de bug-uri, ceea ce confirmă regula că programul trebuie spart în bucățele mici și independente, pentru a stăvili complexitatea.
Dacă facem un grafic al distribuției erorilor în raport cu fișierele în care apar, graficul este foarte neuniform: cele mai multe fișiere au cam 1 bug, pe cînd cîteva fișiere sunt responsabile pentru majoritatea bug-urilor. Foarte adesea, programatorii au copiat un fragment de program eronat în mai multe locuri, multiplicînd apariția unui singur bug.
Privind la versiuni succesive ale sistemului de operare, se poate observa în care versiune apare un bug și în care dispare. Folosind aceste date, se poate calcula durata medie de viață a unui bug în cod. În pofida numărului mare de persoane care contribuie la Linux, durata medie de viață este relativ ridicată: un bug supraviețuiește cam un an și opt luni înainte de a fi corectat.
O ultimă statistică pe care o voi prezenta compară densitatea de bug-uri din Linux cu cea dintr-un alt sistem de operare dezvoltat open-source: OpenBSD. Programatorii sistemului OpenBSD sunt foarte mîndri de faptul că periodic inspectează manual întregul cod, cu scopul de a detecta erori (în engleză această procedură se numește code audit). Ca atare, ei spun că OpenBSD este cel mai sigur sistem de operare. În mod surprinzător, densitatea de bug-uri în Linux este mai mică, fiind undeva între 1,2 și 6 ori (cercetătorii au calculat cîte un raport pentru fiecare tip de bug pe care l-au analizat, de aceea prezintă mai multe numere diferite). Acest lucru demonstrează că într-adevăr o comunitate mai mare de programatori este mai eficace în a detecta probleme (Linux este mai popular decît OpenBSD) .
Care este metodologia prin care aceste bug-uri au fost depistate? Cum au putut cercetătorii să găsească probleme în bucăți de cod pe care nici măcar nu le pot executa (de exemplu, este limpede că nu pot rula toate driverele, pentru că nu au la-ndemînă toate perifericele posibile)?
Există două metode diferite de a depana un program: metode dinamice și metode statice.
Testarea este o metodă dinamică: programul este pornit, i se dau niște date de intrare, și comportarea lui este observată; eventual se poate folosi un debugger pentru a urmări evoluția programului în timp și pentru a-i putea inspecta măruntaiele. Testarea este relativ ușor de înțeles și folosit, dar are mai multe probleme, mai ales în contextul depanării unui sistem de operare:
Ca atare, grupul de la Stanford folosește metode statice. Metodele statice constau în analiza unui program înainte de a fi lansat în execuție, independent de datele de intrare. Cea mai familiară dintre aceste metode este chiar compilarea: un compilator modern verifică tot felul de proprietăți ale programului, și rejectează programele care nu respectă criteriile de corectitudine. Alteori compilatorul poate da avertismente asupra unor construcții care pot genera probleme la execuție, cum ar fi de pildă variabile neinițializate.
Metodele statice sunt extrem de puternice: ele pot raționa despre comportarea unui program oricare ar fi datele sale de intrare. Compilatoarele de astăzi efectuează analize extrem de sofisticate asupra codului, pe care apoi îl optimizează. Multe dintre optimizări pot fi aplicate numai în anumite condiții; de exemplu, o atribuire poate fi eliminată dacă rezultatul ei nu mai este folosit în restul programului. Pentru a demonstra că atribuirea este inutilă, compilatorul analizează codul și demonstrează că, orice cărare prin program va urma execuția, rezultatul atribuirii nu mai este folosit.
În general astfel de demonstrații nu pot fi făcute: teoria calculabilității arată că chestiuni de genul acesta sunt nedecidabile. De aceea, compilatoarele sunt conservatoare: aplică optimizări numai cînd sunt absolut sigure că sunt corecte, și cîteodată nu aplică optimizări corecte pentru că nu pot demonstra legalitatea lor. Cît de greu este de demonstrat o proprietate, depinde de mulți factori, dar în primul rînd de limbajul de programare care este compilat. La ora actuală se desfășoară o cercetare extrem de febrilă în domeniul limbajelor de programare, scopul căreia este proiectarea unor limbaje mai restrictive. În astfel de limbaje anumite tipuri de erori devin imposibile; limbajele trebuie să rămînă însă suficient de flexibile pentru a exprima în mod natural calcule arbitrar de complicate.
Pentru că limbajul C în care este scris nucleul de Linux este un limbaj relativ primitiv, cercetătorii de la Stanford au făcut un compromis: au extins compilatorul de C cu informații specifice nucleului Linux. Această metodologie dă și numele proiectului: meta-compilare.
Un exemplu va clarifica cel mai bine tehnica folosită.
Pentru a preveni accesele concurente la unele structuri de date importante, nucleele folosesc regiuni critice. Intrarea unui program într-o regiune critică este permisă numai după achiziționarea unei încuietori (lock). Un singur program poate obține o încuietoare, care-i permite accesul în regiunea critică; la terminarea regiunii critice, programul eliberează încuietoarea. Dacă un program accesează încuietoarea cînd un altul este în regiunea critică, este blocat pînă cînd posesorul încuietorii iese din regiune și eliberează încuietoarea.
De exemplu, funcțiile lock_kernel() și unlock_kernel() încuie și respectiv descuie anumite porțiuni din nucleu. Aceste operații sunt implementate în două funcții obișnuite. Dar felul în care aceste funcții sunt folosite este foarte specific: de exemplu, de fiecare dată cînd se folosește lock, trebuie să urmeze eventual unlock (altfel nimeni nu mai poate intra în regiunea critică, și calculatorul probabil se va bloca). De asemenea, nimeni nu poate face de două ori la rînd lock, fără a face între timp și un unlock: a doua oară programul s-ar bloca din cauză că se află deja în regiunea critică.
Metacompilarea exploatează acest gen de informație, care nu ține de limbajul de programare, ci de aplicația care este programată. Proiectul MC le permite programatorilor să scrie extensii ale compilatorului care încorporează astfel de informații.
MC folosește compilatorul de C numit gcc (Gnu C Compiler), care este compilatorul folosit în mod tradițional pentru a compila nucleul Linux; acest compilator este disponibil, ca și Linux, cu codul său sursă. Cercetătorii de la Stanford au definit un limbaj foarte simplu, pe care l-au numit Metal. Compilatorul extins cu Metal poartă numele de xgcc (eXtended gcc). Iată un exemplu de program complet scris în Metal, care verifică folosirea corectă a instrucțiunilor de încuiere:
{ #include "linux-includes.h" }
// descriem un automat finit: state machine
sm verifica_lock {
// Pattern-uri de cautat in cod
pat incuie = { lock_kernel(); }
pat descuie = { unlock_kernel(); }
// stari; prima stare e starea initiala
descuiat: incuie ==> incuiat
| descuie ==> { err("descuiere dubla"); }
;
incuiat: descuie ==> descuiat
| incuie ==> { err("incuiere dubla"); }
// acest pattern indica sfirsitul functiei
| $end_of_path$ ==> { err("functia se termina incuiata"); }
;
}
Programele Metal sunt compilate și transformate în programe C și apoi executabile, care sunt apoi legate dinamic de compilatorul gcc. Cînd xgcc este executat pentru a compila nucleul, extensiile scrise în Metal sunt executate una cîte una. Fiecare extensie analizează fiecare funcție compilată și o verifică.
Programele Metal descriu automate finite. Programul de mai sus descrie automatul din figura 1.
|
Acest automat finit este executat în mod abstract de către compilator pe program, pe fiecare procedură în mod separat. În mod conceptual, compilatorul execută fiecare cărare posibilă din procedură și face tranzițiile indicate de automat cînd întîlnește pattern-urile indicate. Dacă vreuna din cărări cauzează intrarea în starea de eroare, xgcc generează un mesaj de eroare.
Observați că acest automat ignoră cele mai multe operațiuni din program, și este interesat numai de apelurile funcțiilor lock_kernel() și unlock_kernel().
Să ilustrăm funcționarea automatului pe o procedură fictivă, al cărei schelet este următorul:
f() {
lock_kernel();
...
p = malloc(10);
if (!p)
return OUT_OF_MEMORY;
...
unlock_kernel();
return OK;
}
Această procedură obține încuietoarea după care încearcă să aloce 10 octeți. Dacă alocarea eșuează, returnează un cod de eroare. Altfel procedura face tot felul de calcule, descuie nucleul, și returnează un cod OK.
Execuția poate urma două cărări prin această procedură, ilustrate în figura 2: amîndouă intră pe la început, dar una iese în caz de eroare din procedură, pe cînd a doua descuie lacătul înainte de a ieși. Cu litere cursive în figura 2 am indicat starea curentă a automatului finit cînd parcurge cărările respective. Observați că pe cărarea roșie automatul ajunge la sfîrșitul procedurii și se află în starea ``încuiat''; ultima regulă din programul Metal va semnaliza în acest caz o eroare.
 |
În realitate xgcc nu parcurge toate cărările posibile, ci calculează simultan toate stările în care se poate afla automatul în fiecare punct din program folosind o metodă numită interpretare abstractă. Sper să pot consacra un articol special interpretării abstracte și altor tehnici de verificare formală, așa că nu voi mai discuta aici despre ea.
Toate analizele descrise în Metal sunt strict intraprocedurale, adică analizează fiecare funcție separat3.
Aceasta este și una dintre limitările cele mai mari ale acestei scheme. Vom ilustra falibilitatea ei printr-un alt exemplu. Să presupunem că funcția f() de mai sus este apelată în următorul fragment de cod:
...
eroare = f();
if (eroare == OUT_OF_MEMORY)
unlock_kernel();
...
Atunci de fapt codul funcției f nu era eronat, pentru că pînă la urmă ambele cărări duc la o descuiere.
Astfel, analizele descrise în Metal sunt incomplete, și pot genera alarme false, numite falsuri pozitive. (Un fals negativ este o eroare reală care nu este semnalată). xgcc poate fi folosit cu succes dacă cei care programează folosesc o disciplină și un stil de programare consistent. De exemplu, în general programatorii vor considera codul funcție f de mai sus ca fiind defectuos, pentru că este asimetric: uneori descuiem în f(), alteori în apelantul lui f.
În proiecte atît de mari ca Linux, disciplina în programare este absolut esențială. Contributorilor le este bine-cunoscută atitudinea cvasi-dictatorială a lui Linus Torvalds în această privință: el va rejecta programe perfect funcționale dacă nu este mulțumit cu stilul de programare. Cu siguranță că această disciplină de fier contribuie în mod substanțial la calitatea ridicată a nucleului Linux.
Cele aproximativ 1000 de bug-uri menționate mai sus au fost detectate folosind 8 programe Metal, toate în jurul a 100 de linii de cod fiecare. Alte extensii scrise pentru xgcc au avut rezultate mixte: deși generau erori, multe dintre ele erau falsuri pozitive. Din păcate, fiecare mesaj trebuie să fie inspectat manual pentru a decide dacă este o eroare adevărată sau nu. Ca atare, extensiile Metal sunt utile mai ales dacă generează relativ puține alarme false, altfel efortul necesar pentru verificarea mesajelor devine repede prohibitiv.
În mod interesant, nici unul dintre programatorii de la Stanford din proiectul MC nu este expert în nucleul Linux. Ca atare, pentru a valida mesajele xgcc, ei trebuia sa scruteze codul pentru a înțelege ce se întîmplă de fapt. Din această activitate le-a venit o idee foarte interesantă, care este subiectul unuia din cele mai recent articole pe care le-au scris, și care vor fi prezentate în luna octombrie la conferința ``Symposium on Operating System Priciples''.
xgcc este atît de bun pe cît sunt extensiile scrise. Dacă știi ce fel de bug să cauți, îl poți găsi (de exemplu, trebuie să știi că lock/unlock se folosesc împreună în felul indicat). Cînd cercetătorii de la Stanford validau erorile, căutau exemple similare în cod, pentru a vedea cum trebuie făcute de fapt lucrurile.
De aici s-a născut ideea lor cea mai interesantă: avem la dispoziție aproape două milioane de linii de cod. De ce să nu folosim acest cod pentru a extrage automat regulile de programare? De exemplu, dacă în cod funcțiile lock și unlock apar mereu împreună, și în ordinea asta, înseamnă că asta e o regulă care trebuie respectată.
Bine, dar dacă în program sunt bug-uri? Atunci regula va fi încălcată. Pentru a infera reguli, vom căuta în program construcții care apar foarte frecvent, chiar dacă nu apar întotdeauna. Dacă în 999 de cazuri din 1000 lock este urmat de unlock, dar în 1 la mie nu, considerăm că am dat peste o regulă importantă.
A fost făcută o listă de tipuri de reguli care trebuie căutate în cod (de exemplu, <A> este mereu urmat de <B>, unde <A> și <B> trebuie descoperite), și apoi codul a fost analizat exhaustiv pentru a obține posibile reguli (de exemplu, <A> este lock() și <B> este unlock()). Fiecare regulă a fost apoi analizată statistic, și regulile au fost apoi sortate în raport cu deviația de la distribuția uniformă. Apoi regulile cele mai promițătoare au fost transformate în programe Metal.
Ingeniozitatea cercetătorilor însă nu s-a oprit aici. Dacă suntem nefamiliari cu nucleul, tot nu știm dacă regulile acestea trebuie sau nu să fie respectate. Analizînd regulile, cercetătorii au observat că folosirea unei anumite construcții în cod implică faptul că programatorul are o anumită credință despre cum trebuie să arate codul. De exemplu, dacă un programator compară un pointer cu zero, înseamnă că programatorul se așteaptă că acel pointer să poată avea valoarea zero.
Cercetătorii au definit apoi niște reguli simple care arată cum se propagă credințele prin program și care dintre credințe sunt contradictorii. Voi ilustra din nou acest lucru cu un exemplu simplu:
char* p = f();
b = *p; /* credinta: p nu poate fi zero */
...
if (p == 0) /* credinta: p poate fi zero */
...
În acest fragment de program, pointerul p este dereferențiat (se citește valoarea la care punctează). Asta înseamnă că programatorul nu se așteaptă ca în acest punct valoarea pointerului să fie zero. Dar, ceva mai departe în program, pointerul este comparat cu zero. Programatorul nu ar fi făcut această comparație dacă nu s-ar fi așteptat să reușească cițeodată. Aceste două credințe (că p nu poate fi zero, respectiv că p poate fi zero) sunt contradictorii. Una dintre ele trebuie să fie o eroare!
Folosind această metodă au fost construite noi teste care au descoperit alte cîteva sute de bug-uri în Linux.
În acest articol am prezentat proiectul numit Meta-compilare, care augumentează compilatorul cu informații specifice programului compilat. Compilatorul folosește aceste informații pentru a detecta posibile erori în program. Tipul proprietăților care se pot verifica folosind această schemă este destul de restrîns: fiecare procedură din programul de analizat este redusă la un automat finit a cărui traiectorie este urmărită pentru a vedea dacă trece prin stări de eroare. Am văzut de asemenea o schemă ingenioasă prin care codul este analizat pentru a extrage reguli de stil de programare în mod automat; cazuri în care regulile de stil sunt încălcate sunt potențiale erori de programare. Aceste exemple constituie o aplicare a tehnicilor de verificare formală pentru analiza automată a programelor.