180 lines
8 KiB
Org Mode
180 lines
8 KiB
Org Mode
* Modello A
|
||
Sono stati usati tre template per rappresentare un sender, un link wd
|
||
un receiver
|
||
| sender = Sender();
|
||
| receiver = Receiver();
|
||
| link = Link();
|
||
| system sender, receiver, link;
|
||
** Sender
|
||
Lo stato iniziale dell'automata e` /wait/ che simula l'attesa
|
||
dell'arrivo di un pacchetto che viene processato nell'intervallo [1;2]
|
||
del clock /sc/.
|
||
Lo stato successivo e` /send_pkg/ che invia il pacchetto sul canale di
|
||
sincronizzazione urgente /ML/. Il sender passa allo stato /wait_ack/
|
||
che simula l'attesa di un pacchetto sul canale di sincronizzazione
|
||
urgente /LM/ e resetta il clock /sc/.
|
||
Viene simulata la verifica dell'ack in un intervallo di tempo [2;4] e
|
||
successivamente l'automa torna allo stato iniziale resettando il clock
|
||
/sc/.
|
||
# \includepdf{sender_A.jpg}
|
||
[[./sender_A.jpg]]
|
||
** Receiver
|
||
Il receiver e` simmetrico al sender. Dallo stato iniziale di /wait/
|
||
viene simulato l'arrivo di un pacchetto sul canale di sincronizzazione
|
||
urgente /LR/ che permette al receiver di resettare il clock /rc/ e
|
||
avanzare nello stato /recv_pkg/, simulando la preparazione del
|
||
pacchetto in un intervallo di tempo [2;4].
|
||
La transizione dallo stato /done_pkg/ a /send_ack/ simula la generazione
|
||
di un pacchetto di ack in un intervallo di tempo [2;4] ed tornare allo
|
||
stato iniziale dopo aver inviato il pacchetto nel canale di
|
||
sincronizzazione urgente /RL/.
|
||
[[./receiver_A.jpg]]
|
||
** Link
|
||
Il link e` modellato come un canale perfetto senza perdite. Lo stato
|
||
interno /idle/ simula l'attesa di un pacchetto da parte del receiver o
|
||
del sender. Lo stato /received_pkg/ simula l'arrivo di un pacchetto da
|
||
parte del sender sul canale /ML/ che viene processato e spedito al
|
||
receiver sul canale /LR/. Simmetricamente le stesse operazioni di
|
||
attesa, processing e invio avvengono con i pacchetti di ack di cui si
|
||
simula l'arrivo nello stato /received_ack/ dal canale di trasmissione
|
||
/RL/ e l'invio verso il sender dallo stato /resend_ack/ attraverso il
|
||
canale di trasmissione /LM/. Per il processing dei pacchetti
|
||
l'intervallo di tempo e` sempre [2;4].
|
||
[[./link_A.jpg]]
|
||
** Proprieta`
|
||
Sono state verificate tre proprieta` TCTL sul modello:
|
||
- Assenza di deadlock
|
||
| A[] (not deadlock)
|
||
che viene rispettata e indica che la traccia del sistema e` infinita
|
||
- Il sender ricevera` sempre un ack
|
||
| AF sender.received_ack
|
||
| A<> sender.received_ack
|
||
la proprieta` risulta vera in quanto il link non ha perdite.
|
||
- Il receiver ricevera` sempre un pacchetto
|
||
| AF receiver.recv_pkg
|
||
| A<> receiver.recv_pkg
|
||
e` una proprieta` rispettata in quando non ci sono constraint sul
|
||
tempo di attesa del pacchetto.
|
||
** Tempo attesa
|
||
Il tempo di attesa viene calcolato attraverso il simulatore di Uppaal.
|
||
E` stato inserito un clock che viene resettato ogni qualvolta viene
|
||
inviato un pacchetto e una volta processato l'ack.
|
||
L'intervallo di tempo che intercorre dall'invio del messaggio alla
|
||
recezione del suo ack e` [11, 22).
|
||
* Modello B
|
||
E` stato riutilizzato il sistema A e modificato il link per simulare
|
||
la possibilita` di perdita o corruzione di un pacchetto.
|
||
** Link
|
||
Come si denota dall'immagine il link e` simile a quello del modello A
|
||
eccezion fatta per la possibilita` di procedere non
|
||
deterministicamente dagli spazi /received_pkg/ e /received_ack/ verso
|
||
/loss/
|
||
[[./link_B.jpg]]
|
||
Mostriamo un trace in cui il link perde un pacchetto di ack inviato
|
||
dal sender e il sistema va in deadlock.
|
||
Dalla figura possiamo notare la transizione che simula la perdita,
|
||
ovvero l'arco /received_ack/ → /loss/.
|
||
[[./trace_B.jpg]]
|
||
\includepdf{trace_B2.jpg}
|
||
** Proprieta`
|
||
Sono state verificate quattro proprieta` TCTL sul modello:
|
||
- Assenza di deadlock
|
||
| A[] (not deadlock)
|
||
che non e` rispettata
|
||
- Il sender compiera` sempre del progresso
|
||
| sender.waitACK –> (sender.receivedACK)
|
||
la proprieta` non risulta vera in quanto il link ha perdite
|
||
- Il receiver ricevera` sempre un pacchetto
|
||
| AF receiver.recv_pkg
|
||
| A<> receiver.recv_pkg
|
||
che come per la proprieta` precedente non puo` risultare vera
|
||
- Il receiver puo` ricevere un pacchetto
|
||
| EF receiver.recv_pkg
|
||
| E<> receiver.recv_pkg
|
||
la proprieta` risulta vera perche` il link in alcuni path riesce ad
|
||
inviare il pacchetto (non avvengono perdite sul canale)
|
||
** Tempo attesa
|
||
Non si devono fare modifiche al modello rispetto al precedente per
|
||
stabilire il tempo che intercorre dall'invio di un messaggio
|
||
all'arrivo dell'ack. Bisogna pero` notare che in caso di deadlock
|
||
l'ack non arriva mai al mittente e quindi effettivamente possiamo
|
||
calcolare solo il tempo di ricezione minimo, ovvero 11 cicli del clock.
|
||
* Modello C
|
||
E` stato riutilizzato il sistema B e modificati sender e receiver per
|
||
simulare la possibilita` di recovery in seguito alla perdita o
|
||
corruzione di uno o piu` pacchetti.
|
||
Vengono anche mantenute due flag binarie globali, /ack/ e /frame/ per
|
||
tenere traccia dei pacchetti inviati e degli ack ricevuti.
|
||
|
||
** Receiver
|
||
Di seguito viene mostrato il receiver del modello C. Rispetto al
|
||
Modello B il receiver utilizza una flag binaria locale /r_frame/ per tenere
|
||
traccia degli pacchetti gia` ricevuti e processati.
|
||
[[./receiver_C.jpg]]
|
||
** Sender
|
||
Il sender e` stato modellato raddopiando il numero di posti e archi,
|
||
escludendo per lo stato iniziale, in modo da poter processare nella
|
||
parte destra i frame di tipo 0 e nella parte sinistra i frame di
|
||
tipo 1.
|
||
Inoltre sono stati aggiunti due timer che, nel momento in cui
|
||
l'automa e` fermo su /wait_ack/ allo scadere del timeout, permettono
|
||
di spostarsi nello spazio /lost/ e riprovare l'invio del pacchetto.
|
||
Si nota subito che i due timer sono indipendenti l'uno dall'altro e vi
|
||
e` la possibilita` di modellare i sender senza duplicare il numero di
|
||
spazi.
|
||
[[./sender_2t.jpg]]
|
||
[[./sender_1t.jpg]]
|
||
La variabile che regola il timeout e` un numero intero uguale o
|
||
maggiore del piu` grande fra i seguenti valore:
|
||
- il massimo tempo necessario all'invio di un pacchetto che il sender non ha processato
|
||
- il massimo tempo necessario all'invio di un pacchetto che il sender ha gia`
|
||
processato
|
||
Se non si rispetta questo constraint il sistema va in deadlock.
|
||
Nel modello utilizzato lo spazio /is_dup/ e /done_pkg/ del receiver
|
||
hanno lo stesso invariante e il timeout /TOUT/ ha valore minimo 16.
|
||
\begin{comment}
|
||
Ho calcolato il timeout considerando i seguenti cammini
|
||
# Perdita per sender
|
||
Link: received_pkg -> resend_pkg = 4
|
||
Receiver: recv_pkg -> done_pkg = 4
|
||
Receiver: done_pkg -> send_ack = 4
|
||
Link: received_ack -> resend_ack = 4
|
||
|
||
# Perdita per receiver
|
||
Link: received_pkg -> resend_pkg = 4
|
||
Receiver: recv_pkg -> is_dup = 4
|
||
Receiver: is_dup -> send_ack = 4
|
||
Link: received_ack -> resend_ack = 4
|
||
\end{comment}
|
||
** Proprieta`
|
||
Sono state verificate cinque proprieta` TCTL sul modello:
|
||
- In caso di perdita il sender o il receiver tentano nuovamente di
|
||
inviare il pacchetto
|
||
| link.loss --> (sender.send_pkg || sender.send_pkg1 || receiver.send_ack)
|
||
questa proprieta` e` rispttata.
|
||
- Assenza di deadlock
|
||
| A[] (not deadlock)
|
||
questa proprieta` e` rispettata.
|
||
- Nonostante una perdita nel link, il sender o il receiver riceveranno
|
||
il pacchetto
|
||
| link.loss --> (sender.send_pkg || receiver.send_ack)
|
||
la proprieta` e` rispettata
|
||
- Il receiver ricevera` sempre un pacchetto
|
||
| sender.wait_ack || sender.wait_ack1 --> (sender.received_ack || sender.received_ack1)
|
||
questa proprieta` non risulta vera dato che ci possono essere delle
|
||
perdite nel canale
|
||
- C'e` almeno un caso in cui l'ack ricevuto e` quello atteso
|
||
| E<> (ack == expected)
|
||
questa proprieta` risulta vera e conferma la correttezza del meccanismo di
|
||
recovery loss.
|
||
** Tempo attesa
|
||
In questo modello se si considera l'intervallo di tempo che intercorre
|
||
dal primo tentativo di invio alla ricezione dell'ack, non e` possibile
|
||
calcolare il valore massimo dell'intervallo.
|
||
Questo perche` non e` possibile prevedere quanti tentativi saranno
|
||
necessari per un corretto invio.
|
||
Se invece si decide di resettare il clock ad ogni tentativo di invio,
|
||
ovvero di calcolare l'intervallo di tempo che intercorre fra un
|
||
pacchetto inviato in una situazione in cui il link non avra` perdite
|
||
fino all'invio del relativo ack, allora si puo` considerare il modello
|
||
equivalente al modello A, e quindi l'intervallo e` il medesimo.
|