Architektúry a zobrazenia, ASM
návrh programu má dve casti:
- UNITY programy a dôkazy (formálnost)
- popis architektúr, mapovanie programov na architektúry
Zobrazenia na Asynchrónne-Shared-Memory architektúry
ASM:
- pevne daná mnozina procesorov a pamätí
- s kazdou pamätou je asociovaná mnozina procesov, ktoré z nej môzu cítat a mnozina procesov, ktoré do nej môzu zapisovat
Zobrazenie:
- priradí kazdý príkaz nejakému procesu
- priradí (alokuje) kazdú premennú pamäti
- špecifikuje “control flow” pre všetky procesy (postupnost udávajúca ako sú príkazy v danom procesore vykonávané)
Celé to musí splnat:
- všetky premenné na lavej strane kazdého príkazu alokovaného k procesoru sú v pamätiach, do ktorých môze tento zapisovat (okrem indexov polí) a kazdá premenná na pravej strane (a všetky indexy na lavej strane) sú v pamätiach, ktoré môzu cítat
- control flow musí byt taký, ze kazdý príkaz alokovaný ku procesoru je vykonaný nekonecne vela krát