Verificare formală - Proiect 2

(Enunt alternativ)

Să se modeleze şi verifice în SMV un protocol care asigură coerenţa memoriilor cache, pentru un sistem compus din următoarele module: două procesoare, două memorii cache (una pentru fiecare procesor), o memorie principală şi o magistrală la care sunt conectate cele trei memorii.

Pentru a realiza un model abstractizat şi simplificat al sistemului se va ţine seama de următoarele indicaţii. (Corectitudinea simplificărilor descrise se poate argumenta formal; pentru moment, le vom accepta ca atare.)

Procesorul execută un şir infinit de instrucţiuni de următoarele trei tipuri: citire din memorie, scriere în memorie, alte instrucţiuni fără acces la memorie.
Memoria cache are capacitatea de un singur cuvânt. (Întrucât toate liniile memoriei cache funcţionează la fel, pe baza simetriei este suficientă modelarea uneia din ele.)
Memoria principală are capacitatea de două cuvinte (adrese), ambele corespunzând aceleiaşi (unicei) linii din memoria cache. (E suficientă modelarea unei adrese arbitrare de memorie şi a unei alte adrese care reprezintă ``orice altceva'').
Se face abstracţie completă de valoarea înscrisă într-un cuvânt de memorie, şi implicit de numărul de biţi. (Protocolul modelat este independent de valoarea datelor din memorie. Trebuie modelată şi verificată doar folosirea în permanenţă a ultimei valori actuale, nu şi valoarea numerică propriu-zisă).

Sistemul funcţionează în felul următor: fiecare din procesoare trimite memoriei cache proprii comenzi de citire/scriere în funţie de instrucţiunile executate. Memoria cache răspunde imediat dacă poate satisface cererea. Altfel, execuţia procesorului este blocată temporar (stall), şi memoria cache emite pe magistrală o cerere pentru satisfacerea comenzii procesorului. Magistrala este partajată şi răspunde nedeterminist, dar echitabil (fair) cererilor emise de cele două memorii cache. Comenzile emise pe magistrală sunt monitorizate de către memoria principală (care nu emite niciodată cereri), precum şi de memoria cache care nu este activă în ciclul respectiv; ambele îşi actualizează datele şi/sau starea proprie în mode corespunzător. Protocolul este de tip snoopy: memoria cache pasivă poate prelua o dată emisă pe magistrală (anticipând o posibilă utilizare de către procesorul propriu), cu condiţia ca această acţiune să nu compromită integritatea datelor proprii.

Cererile emise de o memorie cache pe magistrală pot fi de citire, scriere sau invalidare (aceasta informează ceilalţi parteneri din sistem că se doreşte actualizarea adresei respective). Se consideră că toate componentele sistemului reacţionează la o cerere transmisă pe magistrală în acelaşi ciclu în care a fost făcută.

Starea unei linii (unui cuvânt) din memoria cache poate fi: a) consistentă cu valoarea din memoria principală; b) modificată (conţine singura copie curentă, valoarea din memoria principală nemaifiind actuală); c) invalidă (nu conţine valoarea curentă a vreunei adrese de memorie).

Se vor specifica şi verifica următoarele proprietăţi:

Cele două memorii cache nu pot avea niciodată valori inconsistente pentru aceeaşi adresă.
Valoarea curentă a unui cuvânt de memorie nu se "pierde" niciodată.
Executia niciunui procesor nu este blocată la infinit.

Se vor preda prin e-mail fişierul SMV (comentat inteligibil) şi rezultatele rulării. Se va preda de asemenea, fie pe hârtie, fie prin e-mail (format ASCII, PDF sau PostScript) o notă explicând principalele decizii de modelare şi de formulare a specificaţiilor.

Marius Minea