MINIX in ASM

Il professor Boerger ha analizzato, in un suo articolo, il kernel Minix tramite le Abstract State Machine (ASM). Una sorta di pseudocodice su dati astratti che permette di avere una visione globale su sistemi molto complessi e nè facilita l’estensione delle funzionalità.
Di seguito riporto un sunto in italiano.

O.S. Kernel in ASM

Il tempo del sistema è tenuto contando i cicli di clock(tick clock). Questo compito è affidato ad un task, che quando si verifica un tick di clock riceve un messaggio di interruzione e registra il time attuale del sistema. Registrare il passare del tempo consente di eseguire operazioni centrali del
kernel quali: notifica allarme dei processi, operazioni che consentono di cambiare lo stato di un processo(processing switching) e lo swapping. Il task che si occupa di processare i compiti relativi al tick di clock è modellato da una ASM chiamata ExecClockISR. Ad ogni occorrenza di una interruzione per tick di clock viene seguita un passo della ExecClockISR ASM,a sua volta descritto da tre azioni, in successione:

• DeSchedule : descrive la politica di scheduling per i processi utente. Se un processo è da troppo tempo in esecuzione(RunTooLong) ed un altro è presente in lista pronti; il processo corrente viene inserito in fondo alla lista pronti utente. la procedura viene eseguita ad interruzioni disabilitate
  
• ManageTimedFeatures : aggiorna il time del sistema a quella corrente(now) e chiama le componenti relative alla notifica dei processi sospesi,in swap e zombie.
  
• ReSchedule : settare 'cur_proc'(currp) e 'proc_ptr'(tabella dei processi),rispettivamente l'identificatore al processo corrente e il puntatore alla tabella dei processi Se il sistema è inattivo 'cur_proc' e 'proc_ptr' vengono settati ad un valore speciale IDLE, per identificare lo stato di inattività. Per impostare il processo corrente controlla se è presente un processo nelle liste pronti, in ordine di priorità, verifica : quella dei task, dei processi server e di quelli utente.Se è in esecuzione il task per il controllo del ciclo di clock, 'cur_proc' = CLOCKTASK. Viene settato anche il puntatore al processo bill_ptr che conta i cicli di clock
  della CPU.
  

ExecClockISR =
if HwClockTick then
DeSchedule
step ManageTimedFeatures
step ReSchedule

Nota. Scrivere questa regola come un turbo-ASM sequenziale riflette che la sua azione è considerata "atomica" L'uso della tecnica di locking farà si che riusciamo mappare un passo della ASM, visto come l'esecuzione di tre sottomacchine, in una sequenza di azioni protette da LOCK e UNLOCK, per ottenere la mutua esclusione nelle zone critiche, visto che siamo in uniprocessor, basterà disabilitare prima di una sezione critica.

Processi.
Distinguiamo tre tipi di processi:

• user(utente)
  
• system (di sistema)
  
• device (dispositivi)

abbiamo anche 2 tipi di processi speciali: idleProcess e nullProcess
Quindi :
Process = DeviceProcess
U SystemProcess U UserProcess U{idleProcess,nullProcess}
RealProcess = Process\{idleProcess,
nullProcess}

Ogni processo ha un suo stato interno(registri,pc,psw,etc) il quale viene salvato al momento del DeSchedule (stato da running a ready) e ripristinato quando viene chiamata la sottomacchina ReSchedule.
Ogni processo è schedulato per un certo quanto di tempo. Il valore dell'intervallo di tempo associato al processo è memorizzata nella locazione timeQuant(currp) che decresce quando il processo è in esecuzione
In caso che un processo è da troppo tempo in esecuzione RunTooLong passa dalla testa della coda readyq(kind(currp)) alla coda.
Gli accessi alla coda pronti e l'aggiornamento di stato di processi sono e devono essere fatti in mutua
esclusione. La coppia di macchine LOCK ed UNLOCK consentono di eseguire operazioni senza interruzioni..

DeSchedule =
SaveState //salvo stato processo in esecuzione
Lock //disabilità interruzioni
seq
status(currp) := ready //setta lo stato di currp a ready
HandleProcessQuantum(currp) //se scade il quanto di tempo commuta contesto
seq
UnLock //abilità interruzioni
where
HandleProcessQuantum(p) =
if p ∈ UserProcess then // solo per i processi utente
timeQuant(p) := timeQuant(p) − 1 //decrementa il quanto
if RunTooLong(p) then //se è da troppo tempo in esecuzione
RemoveHead(readyq(kind(p))) //rimuove dalla testa
seq
Enqueue(p, readyq(kind(p))) // e mette in coda
RunTooLong(p) = (timeQuant(p) − 1 minUserTimeQuant)

ReSchedule =
ScheduleNext //seleziona nuovo processo in esecuzione
seq
RestoreState(currp) //ripristina lo stato del processo
where
ScheduleNext =
prevp := currp //prevp prende proc precedente
let p = selectLowLevelScheduler(readyq) /*preleva proc da mandare in esecuzione,per
priorità,dalla lista pronti*/
if p = undef then //se non ci sono processi in coda pronti
currp := idleProc /*si assegna a currp il processo speciale per identificare lo stato di inattività del sistema */
else
currp := p //altrimenti si manda il prcesso in esecuzione
status(p) := running // modifica stato in runnung

Quando non ci sono processi nelle liste pronti idleProcess viene schedulato.Può essere visto come un processo che fa attesa attiva finchè non si verifica un INT (while true do Skip).

ManageTimedFeatures =
now := now + ticklength //aggiona ora corrente
Wake(clockDriver) // sveglia il task swap driver
seq
Wake(deZombifier) // sveglia task che elimina i proc. zombie

ManageTimedFeatures aggiorna l'ora corrente aggiungendogli ticklength e sveglia i i task che gestiscono i processi sospesi in swap e il kill dei zombie(Wow come Resident Evil), rispattevamente chiamando le sottomacchine ExecSwapper ed ExecDeZombifier.

2 ExecCLOCKD RIVER
ManageTimedFeatures sveglia attraverso la regola wake la sottomacchina ExecClockDriver, inizializzata a sleep.
ExecClockDriver chiama le 2 sottomacchine:

• UpdateStorageTimes: aggiorna il time dei processi presenti in disco ed
  esegue la macchina ExecSwapper
  
• ResumeAlarmedProcesses: i processi con
  tempo di attesa con tempo di attesa alarmTime(p) superiore a now vengono svegliati,cioè inseriti in lista pronti.

e si rimette a “dormire”.

ExecClockDriver =
Lock
seq
UpdateStorageTimes
Wake(swapper) //sveglia la macchina ExecSwapper
ResumeAlarmedProcesses
UnLock
PutToSleep(clockDriver) // ritono a 'dormire'

UpdateStorageTimes =
forall p ∈ Process
if status(p) = swappedout then //per ogni proc residente in disco
swappedOutTime(p) := swappedOutTime(p) + 1 // inc. tempo di permanenza fuori swap
else
residencyTime(p) := residencyTime(p) + 1 // incr. tempo permanenza nel disco

ResumeAlarmedProcesses =
let alarmed = { p ∈ RealProcess | alarmTime(p) ≤ now }
if alarmed ≠ Ø then
forall p ∈ alarmed //se ci sono processi da svegliare
alarmTime(p) := undef //azzera allarme
MakeReady(p) //metti il processo in coda pronti

MakeReady(p) =
Lock
seq
Enqueue(p, readyq(kind(p))) //mette il processo p nella sua lista pronti
status(p) := ready // cambia lo stato del processo
seq UnLock

3 La componente DeZombifica
La macchina ExecDeZombifier in attesa su un semaforo, quando viene svegliata, cerca tutti i processi terminati ma che non hanno rilasciato le risorse poichè condividevano le risorse con i loro figli ora(now) terminati

ExecDeZombifier =
Lock seq
KillAllZombies
UnLock
PutToSleep(deZombifier) //torna a 'dormire'
where

KillAllZombies =
letdeadzs = { z ∈ zombies | children(z ) ≠ Ø} //zombie senza figli
zombies := zombies \ deadzs //aggiorno insieme dei proc zombie
forall z ∈ deadzs
parent(z ) := undef //kill zombie senza figli

children è una funzione derivata da parent, children(p) = {q | parent(q) = p}, che ha sua volta è una funzione dinamica.


4 La componente Swapper.

La sotto macchina ASM ExecSwapper ha il compito di effettuare lo swap dei
processi user tra memoria e disco,e viceversa. Nello stato iniziale fa attesa
passiva su un semaforo.
ExecSwapper = DiskSwap step PutSwapperToSleep


4.1 La Componente DiskSwap
La macchina astratta DiskSwap usa una funzione nextProcessToSwapIn per determinare il prossimo processo p da swappare, quello con il massimo valore di swappedOutTime.
Successivamente, calcola la memoria richiesta dal processo s = memSize(p) è verifica se il sistema può soddisfare tale richiesta, attraverso la funzione CanAllocateInStore(s).
Se la condizione è vera si chiama la sottomacchina SwapProcessIntoStore(p, s), che swappa il processo in memoria.
Altrimenti si cerca un candidato in memoria di dimensione s per lo swapOut, se è presente si fa lo swapIn del processo p.

DiskSwap =
if nextProcessToSwapIn ≠ undef then
let p = nextProcessToSwapIn // p proc. per swap in
let s = memSize(p) // determina memory size di p
if CanAllocateInStore(s) then // posso allocare p in mem.?
Trigger(SwapProcessIntoStore(p, s)) // si, faccio lo swapIn
else
let cand = swapOutCandidate(s) //no, prendo proc. per swap out
if cand ≠ undef then //se c'è un candidato
Trigger(SwapProcessOut(cand, start, size)) //faccio lo swapOut di cand
step
SwapProcessIn(p, s) // e faccio lo swapIn del proc.p

where
nextProcessToSwapIn = // il proc. In disco conpermanenza massima
p(swappedOutTime(p) = max{swappedOutTime(q) | status(q) = swappedout})

swapOutCandidate(s) = //proc. Da più tempo in mem. Condimensione maggiore di s
p ∈UserProcess with status(p) = ready memSize(p) ≥ s

residencyTime = max{residencyTime(q) |
q ∈ UserProcess and status(p) ≠ swappedout}

CanAllocateInStore(s) = forsome h ∈ holes s ≤ size(h)


4.2 Storage Management Background
Il Gestore del disco fa l'assunsione che la memoria principale è composta da una sequenza di unita primarie di immagazzinamento(Primary Storage Units, es.byte o parole), mem:PSU*, e che ogni pocesso p occupa ne una sotto sequenza contigua(regione di memoria).
La memoria mem(p) associata al processo p è la sotto sequenza compresa tra memStart(p), l'indirizzo base di p e memSize(p), la dimensione. Quindi la regione di memoria di p è :
[mem(memStart(p)), . . . ,mem(memStart(p) + memSize(p) − 1)]

L'intera memoria è partiziona in regioni occupate da processi. Le restanti sottosequenze di memoria non allocate hai processi sono chiamati buchi(holes). La funzione CanAllocateInStore(s) cerca un buco di dimenzione almeno s.
CanAllocateInStore(s) = forsome ∈ holes s ≤ size(h)

Quando viene chiamato SwapProcessIntoStore(p, s) siamo sicuri che c'è un
hole che soddisfa la dimensione s richiesta dal processo p.
Viene assegnato l'indirizzo di partenza del processo in corrispondenza del
hole AllocateFromHole(s), il quale restituisce il buco h sufficiente a contenere s.
Successivamente si invia la richiesta allo swap disk driver ExecSwapDiskDriver e si mette in attesa dell'esito. Infine, il processo swappato viene messo in coda pronti MakeReady(p) e i suoi
attributi aggiornati .
SwapProcessIntoStore(p, s) =
let h = AllocateFromHole(s) in memStart(p) := start(h) //x ind. Base del proc p
step
RequestSwapIn(p, memStart(p)) //invia richiesta di swapIn al ExecSwapDiskDriver
step
swapDiskDriver_donesema.Wait //attesa esito
step
Delete(p, SwappedOut) // processo non più in disco
status(p) := ready // cambia lo stato in ready
UpdateRelocationReg // aggiornamento registri
residencyTime(p) := 0 //inizializza attributi
swappedOutTime(p) := 0
MakeReady(p) //inserisce coda pronti

RequestSwapIn scrive nel buffer swapReqBuffer la richiesta di swapIn passando come parametro il processo da swappare e il suo indirizzo base in memoria.
Successivamente si sveglia disk driver ExecSwapDiskDriver-
RequestSwapIn(p, loadpt) =
swapDiskMsg_sema.Wait //stato iniziale in attesa
step
swapReqBuff := SWAPIN(< p, loadpt >) //scrive sul buffer la richiesta
step
swapDiskMsg_sema.Signal //sveglia ExecSwapDiskDriver
Wake(swapDiskDriver)

La regola AllocateFromHole, protetto dalla coppia LOCK ed UNLOCK, sceglie un hole che soddisfa la richiesta di dimensione s. Associa tale regione al processo p ed infine calcella hole(buco) scelto dalla collezioni di holes.
AllocateFromHole(s) =
Lock
seq
choose h ∈ holes with s ≤ size(h) //si sceglie un hole che soddisfa la richiesta
Insert((start(h), s), usermem) /*il nuovo segmento di mem. viene aggiunta alla collezione di mem. riservata ai proc. Utente*/
result:= (start(h), s) // restituisce la coppia(ind.base,dim.)
Delete(h, holes) //elimino h dalla collezione holes
if size(h) − s > 0 then //se il buco è più di s
Insert((start(h) + s, size(h) − s), holes) //se ne crea un'altro con differenza
seq
UnLock

Visto che il processo padre condivide il codice con i processi figli, di conseguenza quando il processo padre è salvato nel disco(swapout), i figli perdono il riferimento al codice del padre, quindi dovranno passare in uno stato di attesa.
SwapProcessOut(p, st, sz ) = // p proc., ind. St,dimensione sz
SwapProcessOutOfStore(p, st, sz ) // swapOut processo p
step
if children(p)≠Ø and IsCodeOwner(p) then //se ha figli con codice condiviso
BlockProcessDescendants(p) //mette in attesa i figli di p

where
BlockProcessDescendants(p) =
forall q ∈ child⁺(p) //per ogni figlio q del processo p;
Insert(q, blockswaiting(p)) //si inserisce nell'insieme discendenti bloccati di p
status(q) := waiting //stato impostato in attesa
MakeUnready(q) //e rimosso dalla lista pronti

SwapProcessOutOfStore(p, st, sz ) esegue la computazione inversa di SwapProcessIntoStore(p, sz ). La regola RequestSwapOut fa richiesta, per mezzo di un buffer, al processo driver swap disk,il cui compito è quello di gestisce il trasferimento mem-disco e viceversa, che la regione p deve essere 'swappata' in discola regione di memoria che era occupata dal processo p viene aggiunta nella collezioni di buchi(holes)
Gli attributi del processo swappato nel disco vengono aggiornati e il processo viene messo stato di attesa(non pronto)
SwapProcessOutOfStore(p, st, sz ) =
RequestSwapOut(p, st, st + sz ) // invia richiesta di swapOut al ExecSwapDiskDriver
step
swapDiskDriver_donesema.Wait // attesa esito
step
Insert(p, SwappedOut) // processo in disco
status(p) := swappedOut // cambio lo stato
residencyTime(p) := 0 //inizializza attributi
swappedOutTime(p) := 0
FreeMainStore(st, sz ) // libera la memoria che era occupata da p
MakeUnready(p) // rimuovo processo dalla coda pronti

La sottomacchina MakeUnready estrae il processo r, passato come parametro, dalla relativa lista pronti.
MakeUnready(r) =
let q = readyq(schedlev(r)) //q è la coda relativa a r
if q ≠[] then //q non è vuota
if r = head(readyq)then //se è il processo corrente
Delete(r , q) //elimina dalla lista q
seq
ReSchedule // manda un nuovo proc. In esecuzione
else
Delete(r , q) //altrimenti elimina dalla lista q

La regola FreeMainStore elimina la regione passata come parametro, ed unifica buchi adiacenti.
FreeMainStore(region) =
Lock
seq
FreeMainStoreBlock(region) //elimina regione dalla mem.
seq
MergeAdjacentHoles //unifica holes adiacenti
seq
UnLock

where
FreeMainStoreBlock(region) =
Delete(region, usermem) //elimina region dalla memoria associata all'utente
Insert(region, holes) //e la inserisce nella colleizone di holes

MergeAdjacentHoles =
forall h1, h2 ∈ holes //per ogni coppia di buchi adiacenti
if start(h1) + size(h1) = start(h2) then
Delete(h1, holes) //li elimino dalla collezione di holes
Delete(h2, holes) //e ne aggiungo uno dato dalla somma h1+h2
Insert((min{start(h1), start(h2)}, size(h1) + size(h2)), holes)

RequestSwapOut è la funzione simile di RequestSwapIn. Cambia solo il valore inserito nel buffer
RequestSwapOut(p, s, e) =
swapDiskMsg_sema.Wait //stato iniziale in attesa
step
swapReqBuff := SWAPOUT(< p, s, e >) //scrive sul buffer la richiesta
step
swapDiskMsg_sema.Signal
Wake(swapDiskDriver) //sveglia ExecSwapDiskDriver

Nel caso in cui un processo padre entra in swap(swapin, in memoria principale), i fogli devono essere svegliati e messi in stato di pronto.
SwapProcessIn(p, s) =
SwapProcessIntoStore(p, s) // swapIn processo p dim. s
step
if children(p)≠Ø and IsCodeOwner(p) then //se p ha figli con codice condiviso
ReadyProcessDescendants(p) //sveglia i figli di p

where
ReadyProcessDescendants(p) =
forall q ∈ blockswaiting(p)//per ogni discendente q di p in attesa;
Delete(q, blockswaiting) //si elimina dall'insieme dei discendenti bloccati di p
status(q) := ready //stato impostato in pronto
MakeReady(q) //q aggiunto in lista pronti

Il processo relativo alla gestione delle fasi di swap(swap disk driver), è definita dalla macchina ExecSwapDiskDriver che compie le seguenti azioni: Se nel buffer è presente una richiesta pendente, viene processata da una sottomacchina HandleRequest, che a secondo del tipo di richiesta effettua operazioni di : swapin, wapout,elimina e crea un nuovo processo.
ExecSwapDiskDriver =
let rq= Read(swapReqBuff)
if rq ≠ NullSwap then //se il buffer delle richieste non è vuoto
HandleRequest(rq)// processa la richiesta
swapDiskDriver donesema.Signal //e sveglia chi era in attesa su questo sem.
PutToSleep(swapDiskDriver) //torna in Wait

where
HandleRequest(rq) =
case swapReqBuff of
SwapOut(p, start, end) → dmem(p) := [mem(start), . . . ,mem(end)]
SwapIn(p, ldpt) → forall ldpt ≤ ldpt + memSize(dmem(pdo) do mem(i):= dmem(p)(i)
DelProc(p) → dmem(p) := undef
NewProc(p, img) → dmem(p) := img

dmem = memoria del disco
mem = memoria principale
Le regole di lettura(READ) e scrittura(WRITE) usano il semaforo swapDiskMsg_sema per la sincronizzazione tra il swap disk process e il swapper process.
Write(rq) =
swapDiskMsg_sema.Wait
step
swapReqBuff := rq //scrive rq nel buffer delle richieste
step
swapDiskMsg_sema.Signal

Read =
step
SwapDiskMsg_sema.Wait
step
result:= swapReqBuff //ritorna il buffer delle richieste
swapReqBuff := Nullswap
sstep
swapDiskMsg_sema.Signal

5 Lo Scheduler
La regola principale per le operazioni di scheduling è definita dalla ASM ScheduleNext già descritta in precedenza. In questo paragrafo viene mostrato il raffinamento della funzione
selectLowLevelScheduler , e le definizioni di SaveState e RestoreState..

5.1 SelectLowLevelScheduler
La funzione SelectLowLevelScheduler è utilizzata per selezionare un processo, rispetto alla priorità su tre code rispettivamente ai tre tipi di processi. I processi device hanno massima priorità e quelli user minima. Ogni coda è gestita tramite una politica FIFO(round robin scheduler), il raffinamento corrispondente per la gestione delle code in ASM è definita da:
Enqueue =InsertAtEnd and Dequeue = RemoveHead

readyq, logicamente è un unica lista, ma è definita come una locazione derivata dalla concatenazione delle tre readyq(i) per device(dispositivi), system(sistema) e user(utente) con i=1,2,3. La concatenazione è ordinata a secondo della priorità. La testa della lista
punta al processo con priorità più alta. readyq può essere definite nel seguente modo:
readyq = readyq(1).ready(2).readyq(3)

5.2 Definizione di SaveState e RestoreState.
La sotto macchina saveState è utilizzata per salvare lo stato della macchina. In dettaglio, salva l'ip,l'insieme dei registri,lo stack e la process status word nel descrittore del processo corrente presente nella tabella dei processi
SaveState =
if currp ≠ nullProcess then
ip(currp) := ip
regs(currp) := regs
stack(currp) := stack
statwd(currp) := statwd

RestoreState esegue l'operazione inversa, cioè ripristina lo stato del processo caricando i valori dal descrittore di processo in tabella dei processi al nuovo processo in esecuzione
RestoreState =
if currp ≠ idleProcess then
ip := ip(currp)
regs := regs(currp)
stack := stack(currp)
statwd := statwd(currp)

6 Semaphores and Lock/Unlock Mechanism
semacount, è un semaforo con contatore. Il contatore rappresenta il numero di processi che simultaneamente vogliono accedere ad una sezione critica. SIGNAL incrementa il contatore di 1 e WAIT lo sottrae 1. Se il contatore prende valori negativi significa che c'è già un processo in sezione critica., quindi nel caso di WAIT il processo corrente sarà inserito nella coda di attesa del semaforo salvando lo stato e viene eseguito un'altro processo.
Wait =
Lock
seq
let newcount = semacount − 1 //decrementa contatore
semacount := newcount
if newcount < 0 then // se contaore negativo
Enqueue(currp, waiters) // inserisce nella coda del semaforo currp
status(currp) := waiting // e lo stato passa in attesa
SaveState(currp) // e si commuta contesto
MakeUnready(currp) seq ReSchedule
seq
UnLock

SIGNAL aggiunge uno al contatore. Se il contatore è ancora negativo vuol dire che c'è almeno un processo in coda d'attesa del semaforo; di conseguenza il processo in attesa viene messo in esecuzione.
Signal =
Lock
seq
let newcount = semacount + 1 //decrementa contatore
semacount := newcount
if newcount ≤ 0 then // se contaore non è positivo
let cand = head(waiters) //prendo il primo processo in coda
status(cand) := ready // e lo sveglio, và in stato di pronto
MakeReady(cand) //viene inserito in lista pronti
Delete(cand, waiters) //eliminato dalla coda del sem.
seq
UnLock

Si usano le macro:

• Wake(device) = device_sema.Signal
• PutToSleep(device) = device_sema.Wait
  

per le operazioni di SIGNAL E WAIT su un semaforo legato ad un device.

Daniele Licari