1 .. SPDX-License-Identifier: GPL-2.0 1 .. SPDX-License-Identifier: GPL-2.0
2 2
3 .. include:: ../disclaimer-ita.rst 3 .. include:: ../disclaimer-ita.rst
4 4
5 Validatore di sincronizzazione durante l'esecu 5 Validatore di sincronizzazione durante l'esecuzione
6 ============================================== 6 ===================================================
7 7
8 Classi di blocchi 8 Classi di blocchi
9 ----------------- 9 -----------------
10 10
11 L'oggetto su cui il validatore lavora è una " 11 L'oggetto su cui il validatore lavora è una "classe" di blocchi.
12 12
13 Una classe di blocchi è un gruppo di blocchi 13 Una classe di blocchi è un gruppo di blocchi che seguono le stesse regole di
14 sincronizzazione, anche quando i blocchi potre 14 sincronizzazione, anche quando i blocchi potrebbero avere più istanze (anche
15 decine di migliaia). Per esempio un blocco nel 15 decine di migliaia). Per esempio un blocco nella struttura inode è una classe,
16 mentre ogni inode sarà un'istanza di questa c 16 mentre ogni inode sarà un'istanza di questa classe di blocco.
17 17
18 Il validatore traccia lo "stato d'uso" di una 18 Il validatore traccia lo "stato d'uso" di una classe di blocchi e le sue
19 dipendenze con altre classi. L'uso di un blocc 19 dipendenze con altre classi. L'uso di un blocco indica come quel blocco viene
20 usato rispetto al suo contesto d'interruzione, 20 usato rispetto al suo contesto d'interruzione, mentre le dipendenze di un blocco
21 possono essere interpretate come il loro ordin 21 possono essere interpretate come il loro ordine; per esempio L1 -> L2 suggerisce
22 che un processo cerca di acquisire L2 mentre g 22 che un processo cerca di acquisire L2 mentre già trattiene L1. Dal punto di
23 vista di lockdep, i due blocchi (L1 ed L2) non 23 vista di lockdep, i due blocchi (L1 ed L2) non sono per forza correlati: quella
24 dipendenza indica solamente l'ordine in cui so 24 dipendenza indica solamente l'ordine in cui sono successe le cose. Il validatore
25 verifica permanentemente la correttezza dell'u 25 verifica permanentemente la correttezza dell'uso dei blocchi e delle loro
26 dipendenze, altrimenti ritornerà un errore. 26 dipendenze, altrimenti ritornerà un errore.
27 27
28 Il comportamento di una classe di blocchi vien 28 Il comportamento di una classe di blocchi viene costruito dall'insieme delle sue
29 istanze. Una classe di blocco viene registrata 29 istanze. Una classe di blocco viene registrata alla creazione della sua prima
30 istanza, mentre tutte le successive istanze ve 30 istanza, mentre tutte le successive istanze verranno mappate; dunque, il loro
31 uso e le loro dipendenze contribuiranno a cost 31 uso e le loro dipendenze contribuiranno a costruire quello della classe. Una
32 classe di blocco non sparisce quando sparisce 32 classe di blocco non sparisce quando sparisce una sua istanza, ma può essere
33 rimossa quando il suo spazio in memoria viene 33 rimossa quando il suo spazio in memoria viene reclamato. Per esempio, questo
34 succede quando si rimuove un modulo, o quando 34 succede quando si rimuove un modulo, o quando una *workqueue* viene eliminata.
35 35
36 Stato 36 Stato
37 ----- 37 -----
38 38
39 Il validatore traccia l'uso cronologico delle 39 Il validatore traccia l'uso cronologico delle classi di blocchi e ne divide
40 l'uso in categorie (4 USI * n STATI + 1). 40 l'uso in categorie (4 USI * n STATI + 1).
41 41
42 I quattro USI possono essere: 42 I quattro USI possono essere:
43 43
44 - 'sempre trattenuto nel contesto <STATO>' 44 - 'sempre trattenuto nel contesto <STATO>'
45 - 'sempre trattenuto come blocco di lettura ne 45 - 'sempre trattenuto come blocco di lettura nel contesto <STATO>'
46 - 'sempre trattenuto con <STATO> abilitato' 46 - 'sempre trattenuto con <STATO> abilitato'
47 - 'sempre trattenuto come blocco di lettura co 47 - 'sempre trattenuto come blocco di lettura con <STATO> abilitato'
48 48
49 gli `n` STATI sono codificati in kernel/lockin 49 gli `n` STATI sono codificati in kernel/locking/lockdep_states.h, ad oggi
50 includono: 50 includono:
51 51
52 - hardirq 52 - hardirq
53 - softirq 53 - softirq
54 54
55 infine l'ultima categoria è: 55 infine l'ultima categoria è:
56 56
57 - 'sempre trattenuto' 57 - 'sempre trattenuto' [ == !unused ]
58 58
59 Quando vengono violate le regole di sincronizz 59 Quando vengono violate le regole di sincronizzazione, questi bit di utilizzo
60 vengono presentati nei messaggi di errore di s 60 vengono presentati nei messaggi di errore di sincronizzazione, fra parentesi
61 graffe, per un totale di `2 * n` (`n`: bit STA 61 graffe, per un totale di `2 * n` (`n`: bit STATO). Un esempio inventato::
62 62
63 modprobe/2287 is trying to acquire lock: 63 modprobe/2287 is trying to acquire lock:
64 (&sio_locks[i].lock){-.-.}, at: [<c02867fd 64 (&sio_locks[i].lock){-.-.}, at: [<c02867fd>] mutex_lock+0x21/0x24
65 65
66 but task is already holding lock: 66 but task is already holding lock:
67 (&sio_locks[i].lock){-.-.}, at: [<c02867fd 67 (&sio_locks[i].lock){-.-.}, at: [<c02867fd>] mutex_lock+0x21/0x24
68 68
69 Per un dato blocco, da sinistra verso destra, 69 Per un dato blocco, da sinistra verso destra, la posizione del bit indica l'uso
70 del blocco e di un eventuale blocco di lettura 70 del blocco e di un eventuale blocco di lettura, per ognuno degli `n` STATI elencati
71 precedentemente. Il carattere mostrato per ogn 71 precedentemente. Il carattere mostrato per ogni bit indica:
72 72
73 === ====================================== 73 === ===========================================================================
74 '.' acquisito con interruzioni disabilitat 74 '.' acquisito con interruzioni disabilitate fuori da un contesto d'interruzione
75 '-' acquisito in contesto d'interruzione 75 '-' acquisito in contesto d'interruzione
76 '+' acquisito con interruzioni abilitate 76 '+' acquisito con interruzioni abilitate
77 '?' acquisito in contesto d'interruzione c 77 '?' acquisito in contesto d'interruzione con interruzioni abilitate
78 === ====================================== 78 === ===========================================================================
79 79
80 Il seguente esempio mostra i bit:: 80 Il seguente esempio mostra i bit::
81 81
82 (&sio_locks[i].lock){-.-.}, at: [<c02867fd 82 (&sio_locks[i].lock){-.-.}, at: [<c02867fd>] mutex_lock+0x21/0x24
83 |||| 83 ||||
84 ||| \-> softirq disab 84 ||| \-> softirq disabilitati e fuori da un contesto di softirq
85 || \--> acquisito in 85 || \--> acquisito in un contesto di softirq
86 | \---> hardirq disab 86 | \---> hardirq disabilitati e fuori da un contesto di hardirq
87 \----> acquisito in 87 \----> acquisito in un contesto di hardirq
88 88
89 Per un dato STATO, che il blocco sia mai stato 89 Per un dato STATO, che il blocco sia mai stato acquisito in quel contesto di
90 STATO, o che lo STATO sia abilitato, ci lascia 90 STATO, o che lo STATO sia abilitato, ci lascia coi quattro possibili scenari
91 mostrati nella seguente tabella. Il carattere 91 mostrati nella seguente tabella. Il carattere associato al bit indica con
92 esattezza in quale scenario ci si trova al mom 92 esattezza in quale scenario ci si trova al momento del rapporto.
93 93
94 +---------------+---------------+----------- 94 +---------------+---------------+------------------+
95 | | irq abilitati | irq disabi 95 | | irq abilitati | irq disabilitati |
96 +---------------+---------------+----------- 96 +---------------+---------------+------------------+
97 | sempre in irq | '?' | '-' 97 | sempre in irq | '?' | '-' |
98 +---------------+---------------+----------- 98 +---------------+---------------+------------------+
99 | mai in irq | '+' | '.' 99 | mai in irq | '+' | '.' |
100 +---------------+---------------+----------- 100 +---------------+---------------+------------------+
101 101
102 Il carattere '-' suggerisce che le interruzion 102 Il carattere '-' suggerisce che le interruzioni sono disabilitate perché
103 altrimenti verrebbe mostrato il carattere '?'. 103 altrimenti verrebbe mostrato il carattere '?'. Una deduzione simile può essere
104 fatta anche per '+' 104 fatta anche per '+'
105 105
106 I blocchi inutilizzati (ad esempio i mutex) no 106 I blocchi inutilizzati (ad esempio i mutex) non possono essere fra le cause di
107 un errore. 107 un errore.
108 108
109 Regole dello stato per un blocco singolo 109 Regole dello stato per un blocco singolo
110 ---------------------------------------- 110 ----------------------------------------
111 111
112 Avere un blocco sicuro in interruzioni (*irq-s 112 Avere un blocco sicuro in interruzioni (*irq-safe*) significa che è sempre stato
113 usato in un contesto d'interruzione, mentre un 113 usato in un contesto d'interruzione, mentre un blocco insicuro in interruzioni
114 (*irq-unsafe*) significa che è sempre stato a 114 (*irq-unsafe*) significa che è sempre stato acquisito con le interruzioni
115 abilitate. 115 abilitate.
116 116
117 Una classe softirq insicura è automaticamente 117 Una classe softirq insicura è automaticamente insicura anche per hardirq. I
118 seguenti stati sono mutualmente esclusivi: sol 118 seguenti stati sono mutualmente esclusivi: solo una può essere vero quando viene
119 usata una classe di blocco:: 119 usata una classe di blocco::
120 120
121 <hardirq-safe> o <hardirq-unsafe> 121 <hardirq-safe> o <hardirq-unsafe>
122 <softirq-safe> o <softirq-unsafe> 122 <softirq-safe> o <softirq-unsafe>
123 123
124 Questo perché se un blocco può essere usato 124 Questo perché se un blocco può essere usato in un contesto di interruzioni
125 (sicuro in interruzioni), allora non può mai 125 (sicuro in interruzioni), allora non può mai essere acquisito con le
126 interruzioni abilitate (insicuro in interruzio 126 interruzioni abilitate (insicuro in interruzioni). Altrimenti potrebbe
127 verificarsi uno stallo. Per esempio, questo bl 127 verificarsi uno stallo. Per esempio, questo blocco viene acquisito, ma prima di
128 essere rilasciato il contesto d'esecuzione vie 128 essere rilasciato il contesto d'esecuzione viene interrotto nuovamente, e quindi
129 si tenterà di acquisirlo nuovamente. Questo p 129 si tenterà di acquisirlo nuovamente. Questo porterà ad uno stallo, in
130 particolare uno stallo ricorsivo. 130 particolare uno stallo ricorsivo.
131 131
132 Il validatore rileva e riporta gli usi di bloc 132 Il validatore rileva e riporta gli usi di blocchi che violano queste regole per
133 blocchi singoli. 133 blocchi singoli.
134 134
135 Regole per le dipendenze di blocchi multipli 135 Regole per le dipendenze di blocchi multipli
136 -------------------------------------------- 136 --------------------------------------------
137 137
138 La stessa classe di blocco non deve essere acq 138 La stessa classe di blocco non deve essere acquisita due volte, questo perché
139 potrebbe portare ad uno blocco ricorsivo e dun 139 potrebbe portare ad uno blocco ricorsivo e dunque ad uno stallo.
140 140
141 Inoltre, due blocchi non possono essere tratte 141 Inoltre, due blocchi non possono essere trattenuti in ordine inverso::
142 142
143 <L1> -> <L2> 143 <L1> -> <L2>
144 <L2> -> <L1> 144 <L2> -> <L1>
145 145
146 perché porterebbe ad uno stallo - chiamato st 146 perché porterebbe ad uno stallo - chiamato stallo da blocco inverso - in cui si
147 cerca di trattenere i due blocchi in un ciclo 147 cerca di trattenere i due blocchi in un ciclo in cui entrambe i contesti
148 aspettano per sempre che l'altro termini. Il v 148 aspettano per sempre che l'altro termini. Il validatore è in grado di trovare
149 queste dipendenze cicliche di qualsiasi comple 149 queste dipendenze cicliche di qualsiasi complessità , ovvero nel mezzo ci
150 potrebbero essere altre sequenze di blocchi. I 150 potrebbero essere altre sequenze di blocchi. Il validatore troverà se questi
151 blocchi possono essere acquisiti circolarmente 151 blocchi possono essere acquisiti circolarmente.
152 152
153 In aggiunta, le seguenti sequenze di blocco ne 153 In aggiunta, le seguenti sequenze di blocco nei contesti indicati non sono
154 permesse, indipendentemente da quale che sia l 154 permesse, indipendentemente da quale che sia la classe di blocco::
155 155
156 <hardirq-safe> -> <hardirq-unsafe> 156 <hardirq-safe> -> <hardirq-unsafe>
157 <softirq-safe> -> <softirq-unsafe> 157 <softirq-safe> -> <softirq-unsafe>
158 158
159 La prima regola deriva dal fatto che un blocco 159 La prima regola deriva dal fatto che un blocco sicuro in interruzioni può essere
160 trattenuto in un contesto d'interruzione che, 160 trattenuto in un contesto d'interruzione che, per definizione, ha la possibilitÃ
161 di interrompere un blocco insicuro in interruz 161 di interrompere un blocco insicuro in interruzioni; questo porterebbe ad uno
162 stallo da blocco inverso. La seconda, analogam 162 stallo da blocco inverso. La seconda, analogamente, ci dice che un blocco sicuro
163 in interruzioni software potrebbe essere tratt 163 in interruzioni software potrebbe essere trattenuto in un contesto di
164 interruzione software, dunque potrebbe interro 164 interruzione software, dunque potrebbe interrompere un blocco insicuro in
165 interruzioni software. 165 interruzioni software.
166 166
167 Le suddette regole vengono applicate per quals 167 Le suddette regole vengono applicate per qualsiasi sequenza di blocchi: quando
168 si acquisiscono nuovi blocchi, il validatore v 168 si acquisiscono nuovi blocchi, il validatore verifica se vi è una violazione
169 delle regole fra il nuovo blocco e quelli già 169 delle regole fra il nuovo blocco e quelli già trattenuti.
170 170
171 Quando una classe di blocco cambia stato, appl 171 Quando una classe di blocco cambia stato, applicheremo le seguenti regole:
172 172
173 - se viene trovato un nuovo blocco sicuro in i 173 - se viene trovato un nuovo blocco sicuro in interruzioni, verificheremo se
174 abbia mai trattenuto dei blocchi insicuri in 174 abbia mai trattenuto dei blocchi insicuri in interruzioni.
175 175
176 - se viene trovato un nuovo blocco sicuro in i 176 - se viene trovato un nuovo blocco sicuro in interruzioni software,
177 verificheremo se abbia trattenuto dei blocch 177 verificheremo se abbia trattenuto dei blocchi insicuri in interruzioni
178 software. 178 software.
179 179
180 - se viene trovato un nuovo blocco insicuro in 180 - se viene trovato un nuovo blocco insicuro in interruzioni, verificheremo se
181 abbia trattenuto dei blocchi sicuri in inter 181 abbia trattenuto dei blocchi sicuri in interruzioni.
182 182
183 - se viene trovato un nuovo blocco insicuro in 183 - se viene trovato un nuovo blocco insicuro in interruzioni software,
184 verificheremo se abbia trattenuto dei blocch 184 verificheremo se abbia trattenuto dei blocchi sicuri in interruzioni
185 software. 185 software.
186 186
187 (Di nuovo, questi controlli vengono fatti perc 187 (Di nuovo, questi controlli vengono fatti perché un contesto d'interruzione
188 potrebbe interrompere l'esecuzione di qualsias 188 potrebbe interrompere l'esecuzione di qualsiasi blocco insicuro portando ad uno
189 stallo; questo anche se lo stallo non si verif 189 stallo; questo anche se lo stallo non si verifica in pratica)
190 190
191 Eccezione: dipendenze annidate sui dati portan 191 Eccezione: dipendenze annidate sui dati portano a blocchi annidati
192 ---------------------------------------------- 192 ------------------------------------------------------------------
193 193
194 Ci sono alcuni casi in cui il kernel Linux acq 194 Ci sono alcuni casi in cui il kernel Linux acquisisce più volte la stessa
195 istanza di una classe di blocco. Solitamente, 195 istanza di una classe di blocco. Solitamente, questo succede quando esiste una
196 gerarchia fra oggetti dello stesso tipo. In qu 196 gerarchia fra oggetti dello stesso tipo. In questi casi viene ereditato
197 implicitamente l'ordine fra i due oggetti (def 197 implicitamente l'ordine fra i due oggetti (definito dalle proprietà di questa
198 gerarchia), ed il kernel tratterrà i blocchi 198 gerarchia), ed il kernel tratterrà i blocchi in questo ordine prefissato per
199 ognuno degli oggetti. 199 ognuno degli oggetti.
200 200
201 Un esempio di questa gerarchia di oggetti che 201 Un esempio di questa gerarchia di oggetti che producono "blocchi annidati" sono
202 i *block-dev* che rappresentano l'intero disco 202 i *block-dev* che rappresentano l'intero disco e quelli che rappresentano una
203 sua partizione; la partizione è una parte del 203 sua partizione; la partizione è una parte del disco intero, e l'ordine dei
204 blocchi sarà corretto fintantoche uno acquisi 204 blocchi sarà corretto fintantoche uno acquisisce il blocco del disco intero e
205 poi quello della partizione. Il validatore non 205 poi quello della partizione. Il validatore non rileva automaticamente questo
206 ordine implicito, perché queste regole di sin 206 ordine implicito, perché queste regole di sincronizzazione non sono statiche.
207 207
208 Per istruire il validatore riguardo a questo u 208 Per istruire il validatore riguardo a questo uso corretto dei blocchi sono stati
209 introdotte nuove primitive per specificare i " 209 introdotte nuove primitive per specificare i "livelli di annidamento". Per
210 esempio, per i blocchi a mutua esclusione dei 210 esempio, per i blocchi a mutua esclusione dei *block-dev* si avrebbe una
211 chiamata simile a:: 211 chiamata simile a::
212 212
213 enum bdev_bd_mutex_lock_class 213 enum bdev_bd_mutex_lock_class
214 { 214 {
215 BD_MUTEX_NORMAL, 215 BD_MUTEX_NORMAL,
216 BD_MUTEX_WHOLE, 216 BD_MUTEX_WHOLE,
217 BD_MUTEX_PARTITION 217 BD_MUTEX_PARTITION
218 }; 218 };
219 219
220 mutex_lock_nested(&bdev->bd_contains->bd_mut 220 mutex_lock_nested(&bdev->bd_contains->bd_mutex, BD_MUTEX_PARTITION);
221 221
222 In questo caso la sincronizzazione viene fatta 222 In questo caso la sincronizzazione viene fatta su un *block-dev* sapendo che si
223 tratta di una partizione. 223 tratta di una partizione.
224 224
225 Ai fini della validazione, il validatore lo co 225 Ai fini della validazione, il validatore lo considererà con una - sotto - classe
226 di blocco separata. 226 di blocco separata.
227 227
228 Nota: Prestate estrema attenzione che la vostr 228 Nota: Prestate estrema attenzione che la vostra gerarchia sia corretta quando si
229 vogliono usare le primitive _nested(); altrime 229 vogliono usare le primitive _nested(); altrimenti potreste avere sia falsi
230 positivi che falsi negativi. 230 positivi che falsi negativi.
231 231
232 Annotazioni 232 Annotazioni
233 ----------- 233 -----------
234 234
235 Si possono utilizzare due costrutti per verifi 235 Si possono utilizzare due costrutti per verificare ed annotare se certi blocchi
236 devono essere trattenuti: lockdep_assert_held* 236 devono essere trattenuti: lockdep_assert_held*(&lock) e
237 lockdep_*pin_lock(&lock). 237 lockdep_*pin_lock(&lock).
238 238
239 Come suggerito dal nome, la famiglia di macro 239 Come suggerito dal nome, la famiglia di macro lockdep_assert_held* asseriscono
240 che un dato blocco in un dato momento deve ess 240 che un dato blocco in un dato momento deve essere trattenuto (altrimenti, verrÃ
241 generato un WARN()). Queste vengono usate abbo 241 generato un WARN()). Queste vengono usate abbondantemente nel kernel, per
242 esempio in kernel/sched/core.c:: 242 esempio in kernel/sched/core.c::
243 243
244 void update_rq_clock(struct rq *rq) 244 void update_rq_clock(struct rq *rq)
245 { 245 {
246 s64 delta; 246 s64 delta;
247 247
248 lockdep_assert_held(&rq->lock); 248 lockdep_assert_held(&rq->lock);
249 [...] 249 [...]
250 } 250 }
251 251
252 dove aver trattenuto rq->lock è necessario pe 252 dove aver trattenuto rq->lock è necessario per aggiornare in sicurezza il clock
253 rq. 253 rq.
254 254
255 L'altra famiglia di macro è lockdep_*pin_lock 255 L'altra famiglia di macro è lockdep_*pin_lock(), che a dire il vero viene usata
256 solo per rq->lock ATM. Se per caso un blocco n 256 solo per rq->lock ATM. Se per caso un blocco non viene trattenuto, queste
257 genereranno un WARN(). Questo si rivela partic 257 genereranno un WARN(). Questo si rivela particolarmente utile quando si deve
258 verificare la correttezza di codice con *callb 258 verificare la correttezza di codice con *callback*, dove livelli superiori
259 potrebbero assumere che un blocco rimanga trat 259 potrebbero assumere che un blocco rimanga trattenuto, ma livelli inferiori
260 potrebbero invece pensare che il blocco possa 260 potrebbero invece pensare che il blocco possa essere rilasciato e poi
261 riacquisito (involontariamente si apre una sez 261 riacquisito (involontariamente si apre una sezione critica). lockdep_pin_lock()
262 restituisce 'struct pin_cookie' che viene usat 262 restituisce 'struct pin_cookie' che viene usato da lockdep_unpin_lock() per
263 verificare che nessuno abbia manomesso il bloc 263 verificare che nessuno abbia manomesso il blocco. Per esempio in
264 kernel/sched/sched.h abbiamo:: 264 kernel/sched/sched.h abbiamo::
265 265
266 static inline void rq_pin_lock(struct rq *rq 266 static inline void rq_pin_lock(struct rq *rq, struct rq_flags *rf)
267 { 267 {
268 rf->cookie = lockdep_pin_lock(&rq->loc 268 rf->cookie = lockdep_pin_lock(&rq->lock);
269 [...] 269 [...]
270 } 270 }
271 271
272 static inline void rq_unpin_lock(struct rq * 272 static inline void rq_unpin_lock(struct rq *rq, struct rq_flags *rf)
273 { 273 {
274 [...] 274 [...]
275 lockdep_unpin_lock(&rq->lock, rf->cook 275 lockdep_unpin_lock(&rq->lock, rf->cookie);
276 } 276 }
277 277
278 I commenti riguardo alla sincronizzazione poss 278 I commenti riguardo alla sincronizzazione possano fornire informazioni utili,
279 tuttavia sono le verifiche in esecuzione effet 279 tuttavia sono le verifiche in esecuzione effettuate da queste macro ad essere
280 vitali per scovare problemi di sincronizzazion 280 vitali per scovare problemi di sincronizzazione, ed inoltre forniscono lo stesso
281 livello di informazioni quando si ispeziona il 281 livello di informazioni quando si ispeziona il codice. Nel dubbio, preferite
282 queste annotazioni! 282 queste annotazioni!
283 283
284 Dimostrazione di correttezza al 100% 284 Dimostrazione di correttezza al 100%
285 ------------------------------------ 285 ------------------------------------
286 286
287 Il validatore verifica la proprietà di chiusu 287 Il validatore verifica la proprietà di chiusura in senso matematico. Ovvero, per
288 ogni sequenza di sincronizzazione di un singol 288 ogni sequenza di sincronizzazione di un singolo processo che si verifichi almeno
289 una volta nel kernel, il validatore dimostrerà 289 una volta nel kernel, il validatore dimostrerà con una certezza del 100% che
290 nessuna combinazione e tempistica di queste se 290 nessuna combinazione e tempistica di queste sequenze possa causare uno stallo in
291 una qualsiasi classe di blocco. [1]_ 291 una qualsiasi classe di blocco. [1]_
292 292
293 In pratica, per dimostrare l'esistenza di uno 293 In pratica, per dimostrare l'esistenza di uno stallo non servono complessi
294 scenari di sincronizzazione multi-processore e 294 scenari di sincronizzazione multi-processore e multi-processo. Il validatore può
295 dimostrare la correttezza basandosi sulla sola 295 dimostrare la correttezza basandosi sulla sola sequenza di sincronizzazione
296 apparsa almeno una volta (in qualunque momento 296 apparsa almeno una volta (in qualunque momento, in qualunque processo o
297 contesto). Uno scenario complesso che avrebbe 297 contesto). Uno scenario complesso che avrebbe bisogno di 3 processori e una
298 sfortunata presenza di processi, interruzioni, 298 sfortunata presenza di processi, interruzioni, e pessimo tempismo, può essere
299 riprodotto su un sistema a singolo processore. 299 riprodotto su un sistema a singolo processore.
300 300
301 Questo riduce drasticamente la complessità de 301 Questo riduce drasticamente la complessità del controllo di qualità della
302 sincronizzazione nel kernel: quello che deve e 302 sincronizzazione nel kernel: quello che deve essere fatto è di innescare nel
303 kernel quante più possibili "semplici" sequen 303 kernel quante più possibili "semplici" sequenze di sincronizzazione, almeno una
304 volta, allo scopo di dimostrarne la correttezz 304 volta, allo scopo di dimostrarne la correttezza. Questo al posto di innescare
305 una verifica per ogni possibile combinazione d 305 una verifica per ogni possibile combinazione di sincronizzazione fra processori,
306 e differenti scenari con hardirq e softirq e a 306 e differenti scenari con hardirq e softirq e annidamenti vari (nella pratica,
307 impossibile da fare) 307 impossibile da fare)
308 308
309 .. [1] 309 .. [1]
310 310
311 assumendo che il validatore sia corretto al 311 assumendo che il validatore sia corretto al 100%, e che nessun altra parte
312 del sistema possa corromperne lo stato. Ass 312 del sistema possa corromperne lo stato. Assumiamo anche che tutti i percorsi
313 MNI/SMM [potrebbero interrompere anche perc 313 MNI/SMM [potrebbero interrompere anche percorsi dove le interruzioni sono
314 disabilitate] sono corretti e non interferi 314 disabilitate] sono corretti e non interferiscono con il validatore. Inoltre,
315 assumiamo che un hash a 64-bit sia unico pe 315 assumiamo che un hash a 64-bit sia unico per ogni sequenza di
316 sincronizzazione nel sistema. Infine, la ri 316 sincronizzazione nel sistema. Infine, la ricorsione dei blocchi non deve
317 essere maggiore di 20. 317 essere maggiore di 20.
318 318
319 Prestazione 319 Prestazione
320 ----------- 320 -----------
321 321
322 Le regole sopracitate hanno bisogno di una qua 322 Le regole sopracitate hanno bisogno di una quantità **enorme** di verifiche
323 durante l'esecuzione. Il sistema sarebbe diven 323 durante l'esecuzione. Il sistema sarebbe diventato praticamente inutilizzabile
324 per la sua lentezza se le avessimo fatte davve 324 per la sua lentezza se le avessimo fatte davvero per ogni blocco trattenuto e
325 per ogni abilitazione delle interruzioni. La c 325 per ogni abilitazione delle interruzioni. La complessità della verifica è
326 O(N^2), quindi avremmo dovuto fare decine di m 326 O(N^2), quindi avremmo dovuto fare decine di migliaia di verifiche per ogni
327 evento, il tutto per poche centinaia di classi 327 evento, il tutto per poche centinaia di classi.
328 328
329 Il problema è stato risolto facendo una singo 329 Il problema è stato risolto facendo una singola verifica per ogni 'scenario di
330 sincronizzazione' (una sequenza unica di blocc 330 sincronizzazione' (una sequenza unica di blocchi trattenuti uno dopo l'altro).
331 Per farlo, viene mantenuta una pila dei blocch 331 Per farlo, viene mantenuta una pila dei blocchi trattenuti, e viene calcolato un
332 hash a 64-bit unico per ogni sequenza. Quando 332 hash a 64-bit unico per ogni sequenza. Quando la sequenza viene verificata per
333 la prima volta, l'hash viene inserito in una t 333 la prima volta, l'hash viene inserito in una tabella hash. La tabella potrÃ
334 essere verificata senza bisogno di blocchi. Se 334 essere verificata senza bisogno di blocchi. Se la sequenza dovesse ripetersi, la
335 tabella ci dirà che non è necessario verific 335 tabella ci dirà che non è necessario verificarla nuovamente.
336 336
337 Risoluzione dei problemi 337 Risoluzione dei problemi
338 ------------------------ 338 ------------------------
339 339
340 Il massimo numero di classi di blocco che il v 340 Il massimo numero di classi di blocco che il validatore può tracciare è:
341 MAX_LOCKDEP_KEYS. Oltrepassare questo limite i 341 MAX_LOCKDEP_KEYS. Oltrepassare questo limite indurrà lokdep a generare il
342 seguente avviso:: 342 seguente avviso::
343 343
344 (DEBUG_LOCKS_WARN_ON(id >= MAX_LOCKDEP 344 (DEBUG_LOCKS_WARN_ON(id >= MAX_LOCKDEP_KEYS))
345 345
346 Di base questo valore è 8191, e un classico s 346 Di base questo valore è 8191, e un classico sistema da ufficio ha meno di 1000
347 classi, dunque questo avviso è solitamente la 347 classi, dunque questo avviso è solitamente la conseguenza di un problema di
348 perdita delle classi di blocco o d'inizializza 348 perdita delle classi di blocco o d'inizializzazione dei blocchi. Di seguito una
349 descrizione dei due problemi: 349 descrizione dei due problemi:
350 350
351 1. caricare e rimuovere continuamente i moduli 351 1. caricare e rimuovere continuamente i moduli mentre il validatore è in
352 esecuzione porterà ad una perdita di class 352 esecuzione porterà ad una perdita di classi di blocco. Il problema è che ogni
353 caricamento crea un nuovo insieme di classi 353 caricamento crea un nuovo insieme di classi di blocco per tutti i blocchi di
354 quel modulo. Tuttavia, la rimozione del mod 354 quel modulo. Tuttavia, la rimozione del modulo non rimuove le vecchie classi
355 (vedi dopo perché non le riusiamo). Dunque 355 (vedi dopo perché non le riusiamo). Dunque, il continuo caricamento e
356 rimozione di un modulo non fa altro che aum 356 rimozione di un modulo non fa altro che aumentare il contatore di classi fino
357 a raggiungere, eventualmente, il limite. 357 a raggiungere, eventualmente, il limite.
358 358
359 2. Usare array con un gran numero di blocchi c 359 2. Usare array con un gran numero di blocchi che non vengono esplicitamente
360 inizializzati. Per esempio, una tabella has 360 inizializzati. Per esempio, una tabella hash con 8192 *bucket* dove ognuno ha
361 il proprio spinlock_t consumerà 8192 class 361 il proprio spinlock_t consumerà 8192 classi di blocco a meno che non vengano
362 esplicitamente inizializzati in esecuzione 362 esplicitamente inizializzati in esecuzione usando spin_lock_init() invece
363 dell'inizializzazione durante la compilazio 363 dell'inizializzazione durante la compilazione con __SPIN_LOCK_UNLOCKED().
364 Sbagliare questa inizializzazione garantisc 364 Sbagliare questa inizializzazione garantisce un esaurimento di classi di
365 blocco. Viceversa, un ciclo che invoca spin 365 blocco. Viceversa, un ciclo che invoca spin_lock_init() su tutti i blocchi li
366 mapperebbe tutti alla stessa classe di bloc 366 mapperebbe tutti alla stessa classe di blocco.
367 367
368 La morale della favola è che dovete sempre 368 La morale della favola è che dovete sempre inizializzare esplicitamente i
369 vostri blocchi. 369 vostri blocchi.
370 370
371 Qualcuno potrebbe argomentare che il validator 371 Qualcuno potrebbe argomentare che il validatore debba permettere il riuso di
372 classi di blocco. Tuttavia, se siete tentati d 372 classi di blocco. Tuttavia, se siete tentati dall'argomento, prima revisionate
373 il codice e pensate alla modifiche necessarie, 373 il codice e pensate alla modifiche necessarie, e tenendo a mente che le classi
374 di blocco da rimuovere probabilmente sono lega 374 di blocco da rimuovere probabilmente sono legate al grafo delle dipendenze. Più
375 facile a dirsi che a farsi. 375 facile a dirsi che a farsi.
376 376
377 Ovviamente, se non esaurite le classi di blocc 377 Ovviamente, se non esaurite le classi di blocco, la prossima cosa da fare è
378 quella di trovare le classi non funzionanti. P 378 quella di trovare le classi non funzionanti. Per prima cosa, il seguente comando
379 ritorna il numero di classi attualmente in uso 379 ritorna il numero di classi attualmente in uso assieme al valore massimo::
380 380
381 grep "lock-classes" /proc/lockdep_stat 381 grep "lock-classes" /proc/lockdep_stats
382 382
383 Questo comando produce il seguente messaggio:: 383 Questo comando produce il seguente messaggio::
384 384
385 lock-classes: 385 lock-classes: 748 [max: 8191]
386 386
387 Se il numero di assegnazioni (748 qui sopra) a 387 Se il numero di assegnazioni (748 qui sopra) aumenta continuamente nel tempo,
388 allora c'è probabilmente un problema da qualc 388 allora c'è probabilmente un problema da qualche parte. Il seguente comando può
389 essere utilizzato per identificare le classi d 389 essere utilizzato per identificare le classi di blocchi problematiche::
390 390
391 grep "BD" /proc/lockdep 391 grep "BD" /proc/lockdep
392 392
393 Eseguite il comando e salvatene l'output, quin 393 Eseguite il comando e salvatene l'output, quindi confrontatelo con l'output di
394 un'esecuzione successiva per identificare even 394 un'esecuzione successiva per identificare eventuali problemi. Questo stesso
395 output può anche aiutarti a trovare situazion 395 output può anche aiutarti a trovare situazioni in cui l'inizializzazione del
396 blocco è stata omessa. 396 blocco è stata omessa.
397 397
398 Lettura ricorsiva dei blocchi 398 Lettura ricorsiva dei blocchi
399 ----------------------------- 399 -----------------------------
400 400
401 Il resto di questo documento vuole dimostrare 401 Il resto di questo documento vuole dimostrare che certi cicli equivalgono ad una
402 possibilità di stallo. 402 possibilità di stallo.
403 403
404 Ci sono tre tipi di bloccatori: gli scrittori 404 Ci sono tre tipi di bloccatori: gli scrittori (bloccatori esclusivi, come
405 spin_lock() o write_lock()), lettori non ricor 405 spin_lock() o write_lock()), lettori non ricorsivi (bloccatori condivisi, come
406 down_read()), e lettori ricorsivi (bloccatori 406 down_read()), e lettori ricorsivi (bloccatori condivisi ricorsivi, come
407 rcu_read_lock()). D'ora in poi, per questi tip 407 rcu_read_lock()). D'ora in poi, per questi tipi di bloccatori, useremo la
408 seguente notazione: 408 seguente notazione:
409 409
410 W o E: per gli scrittori (bloccatori esclu 410 W o E: per gli scrittori (bloccatori esclusivi) (W dall'inglese per
411 *Writer*, ed E per *Exclusive*). 411 *Writer*, ed E per *Exclusive*).
412 412
413 r: per i lettori non ricorsivi (r dall'ing 413 r: per i lettori non ricorsivi (r dall'inglese per *reader*).
414 414
415 R: per i lettori ricorsivi (R dall'inglese 415 R: per i lettori ricorsivi (R dall'inglese per *Reader*).
416 416
417 S: per qualsiasi lettore (non ricorsivi + 417 S: per qualsiasi lettore (non ricorsivi + ricorsivi), dato che entrambe
418 sono bloccatori condivisi (S dall'ingle 418 sono bloccatori condivisi (S dall'inglese per *Shared*).
419 419
420 N: per gli scrittori ed i lettori non rico 420 N: per gli scrittori ed i lettori non ricorsivi, dato che entrambe sono
421 non ricorsivi. 421 non ricorsivi.
422 422
423 Ovviamente, N equivale a "r o W" ed S a "r o R 423 Ovviamente, N equivale a "r o W" ed S a "r o R".
424 424
425 Come suggerisce il nome, i lettori ricorsivi s 425 Come suggerisce il nome, i lettori ricorsivi sono dei bloccatori a cui è
426 permesso di acquisire la stessa istanza di blo 426 permesso di acquisire la stessa istanza di blocco anche all'interno della
427 sezione critica di un altro lettore. In altre 427 sezione critica di un altro lettore. In altre parole, permette di annidare la
428 stessa istanza di blocco nelle sezioni critich 428 stessa istanza di blocco nelle sezioni critiche dei lettori.
429 429
430 Dall'altro canto, lo stesso comportamento indu 430 Dall'altro canto, lo stesso comportamento indurrebbe un lettore non ricorsivo ad
431 auto infliggersi uno stallo. 431 auto infliggersi uno stallo.
432 432
433 La differenza fra questi due tipi di lettori e 433 La differenza fra questi due tipi di lettori esiste perché: quelli ricorsivi
434 vengono bloccati solo dal trattenimento di un 434 vengono bloccati solo dal trattenimento di un blocco di scrittura, mentre quelli
435 non ricorsivi possono essere bloccati dall'att 435 non ricorsivi possono essere bloccati dall'attesa di un blocco di scrittura.
436 Consideriamo il seguente esempio:: 436 Consideriamo il seguente esempio::
437 437
438 TASK A: TASK B: 438 TASK A: TASK B:
439 439
440 read_lock(X); 440 read_lock(X);
441 write_lock(X); 441 write_lock(X);
442 read_lock_2(X); 442 read_lock_2(X);
443 443
444 L'attività A acquisisce il blocco di lettura 444 L'attività A acquisisce il blocco di lettura X (non importa se di tipo ricorsivo
445 o meno) usando read_lock(). Quando l'attività 445 o meno) usando read_lock(). Quando l'attività B tenterà di acquisire il blocco
446 X, si fermerà e rimarrà in attesa che venga 446 X, si fermerà e rimarrà in attesa che venga rilasciato. Ora se read_lock_2() è
447 un tipo lettore ricorsivo, l'attività A conti 447 un tipo lettore ricorsivo, l'attività A continuerà perché gli scrittori in
448 attesa non possono bloccare lettori ricorsivi, 448 attesa non possono bloccare lettori ricorsivi, e non avremo alcuno stallo.
449 Tuttavia, se read_lock_2() è un lettore non r 449 Tuttavia, se read_lock_2() è un lettore non ricorsivo, allora verrà bloccato
450 dall'attività B e si causerà uno stallo. 450 dall'attività B e si causerà uno stallo.
451 451
452 Condizioni bloccanti per lettori/scrittori su 452 Condizioni bloccanti per lettori/scrittori su uno stesso blocco
453 ---------------------------------------------- 453 ---------------------------------------------------------------
454 Essenzialmente ci sono quattro condizioni bloc 454 Essenzialmente ci sono quattro condizioni bloccanti:
455 455
456 1. Uno scrittore blocca un altro scrittore. 456 1. Uno scrittore blocca un altro scrittore.
457 2. Un lettore blocca uno scrittore. 457 2. Un lettore blocca uno scrittore.
458 3. Uno scrittore blocca sia i lettori ricorsiv 458 3. Uno scrittore blocca sia i lettori ricorsivi che non ricorsivi.
459 4. Un lettore (ricorsivo o meno) non blocca al 459 4. Un lettore (ricorsivo o meno) non blocca altri lettori ricorsivi ma potrebbe
460 bloccare quelli non ricorsivi (perché potr 460 bloccare quelli non ricorsivi (perché potrebbero esistere degli scrittori in
461 attesa). 461 attesa).
462 462
463 Di seguito le tabella delle condizioni bloccan 463 Di seguito le tabella delle condizioni bloccanti, Y (*Yes*) significa che il
464 tipo in riga blocca quello in colonna, mentre 464 tipo in riga blocca quello in colonna, mentre N l'opposto.
465 465
466 +---+---+---+---+ 466 +---+---+---+---+
467 | | W | r | R | 467 | | W | r | R |
468 +---+---+---+---+ 468 +---+---+---+---+
469 | W | Y | Y | Y | 469 | W | Y | Y | Y |
470 +---+---+---+---+ 470 +---+---+---+---+
471 | r | Y | Y | N | 471 | r | Y | Y | N |
472 +---+---+---+---+ 472 +---+---+---+---+
473 | R | Y | Y | N | 473 | R | Y | Y | N |
474 +---+---+---+---+ 474 +---+---+---+---+
475 475
476 (W: scrittori, r: lettori non ricorsivi, R 476 (W: scrittori, r: lettori non ricorsivi, R: lettori ricorsivi)
477 477
478 Al contrario dei blocchi per lettori non ricor 478 Al contrario dei blocchi per lettori non ricorsivi, quelli ricorsivi vengono
479 trattenuti da chi trattiene il blocco di scrit 479 trattenuti da chi trattiene il blocco di scrittura piuttosto che da chi ne
480 attende il rilascio. Per esempio:: 480 attende il rilascio. Per esempio::
481 481
482 TASK A: TASK B: 482 TASK A: TASK B:
483 483
484 read_lock(X); 484 read_lock(X);
485 485
486 write_lock(X); 486 write_lock(X);
487 487
488 read_lock(X); 488 read_lock(X);
489 489
490 non produce uno stallo per i lettori ricorsivi 490 non produce uno stallo per i lettori ricorsivi, in quanto il processo B rimane
491 in attesta del blocco X, mentre il secondo rea 491 in attesta del blocco X, mentre il secondo read_lock() non ha bisogno di
492 aspettare perché si tratta di un lettore rico 492 aspettare perché si tratta di un lettore ricorsivo. Tuttavia, se read_lock()
493 fosse un lettore non ricorsivo, questo codice 493 fosse un lettore non ricorsivo, questo codice produrrebbe uno stallo.
494 494
495 Da notare che in funzione dell'operazione di b 495 Da notare che in funzione dell'operazione di blocco usate per l'acquisizione (in
496 particolare il valore del parametro 'read' in 496 particolare il valore del parametro 'read' in lock_acquire()), un blocco può
497 essere di scrittura (blocco esclusivo), di let 497 essere di scrittura (blocco esclusivo), di lettura non ricorsivo (blocco
498 condiviso e non ricorsivo), o di lettura ricor 498 condiviso e non ricorsivo), o di lettura ricorsivo (blocco condiviso e
499 ricorsivo). In altre parole, per un'istanza di 499 ricorsivo). In altre parole, per un'istanza di blocco esistono tre tipi di
500 acquisizione che dipendono dalla funzione di a 500 acquisizione che dipendono dalla funzione di acquisizione usata: esclusiva, di
501 lettura non ricorsiva, e di lettura ricorsiva. 501 lettura non ricorsiva, e di lettura ricorsiva.
502 502
503 In breve, chiamiamo "non ricorsivi" blocchi di 503 In breve, chiamiamo "non ricorsivi" blocchi di scrittura e quelli di lettura non
504 ricorsiva, mentre "ricorsivi" i blocchi di let 504 ricorsiva, mentre "ricorsivi" i blocchi di lettura ricorsivi.
505 505
506 I blocchi ricorsivi non si bloccano a vicenda, 506 I blocchi ricorsivi non si bloccano a vicenda, mentre quelli non ricorsivi sì
507 (anche in lettura). Un blocco di lettura non r 507 (anche in lettura). Un blocco di lettura non ricorsivi può bloccare uno
508 ricorsivo, e viceversa. 508 ricorsivo, e viceversa.
509 509
510 Il seguente esempio mostra uno stallo con bloc 510 Il seguente esempio mostra uno stallo con blocchi ricorsivi::
511 511
512 TASK A: TASK B: 512 TASK A: TASK B:
513 513
514 read_lock(X); 514 read_lock(X);
515 read_lock(Y); 515 read_lock(Y);
516 write_lock(Y); 516 write_lock(Y);
517 write_lock(X); 517 write_lock(X);
518 518
519 Il processo A attende che il processo B esegua 519 Il processo A attende che il processo B esegua read_unlock() so Y, mentre il
520 processo B attende che A esegua read_unlock() 520 processo B attende che A esegua read_unlock() su X.
521 521
522 Tipi di dipendenze e percorsi forti 522 Tipi di dipendenze e percorsi forti
523 ----------------------------------- 523 -----------------------------------
524 Le dipendenze fra blocchi tracciano l'ordine c 524 Le dipendenze fra blocchi tracciano l'ordine con cui una coppia di blocchi viene
525 acquisita, e perché vi sono 3 tipi di bloccat 525 acquisita, e perché vi sono 3 tipi di bloccatori, allora avremo 9 tipi di
526 dipendenze. Tuttavia, vi mostreremo che 4 sono 526 dipendenze. Tuttavia, vi mostreremo che 4 sono sufficienti per individuare gli
527 stalli. 527 stalli.
528 528
529 Per ogni dipendenza fra blocchi avremo:: 529 Per ogni dipendenza fra blocchi avremo::
530 530
531 L1 -> L2 531 L1 -> L2
532 532
533 Questo significa che lockdep ha visto acquisir 533 Questo significa che lockdep ha visto acquisire L1 prima di L2 nello stesso
534 contesto di esecuzione. Per quanto riguarda l' 534 contesto di esecuzione. Per quanto riguarda l'individuazione degli stalli, ci
535 interessa sapere se possiamo rimanere bloccati 535 interessa sapere se possiamo rimanere bloccati da L2 mentre L1 viene trattenuto.
536 In altre parole, vogliamo sapere se esiste un 536 In altre parole, vogliamo sapere se esiste un bloccatore L3 che viene bloccato
537 da L1 e un L2 che viene bloccato da L3. Dunque 537 da L1 e un L2 che viene bloccato da L3. Dunque, siamo interessati a (1) quello
538 che L1 blocca e (2) quello che blocca L2. Di c 538 che L1 blocca e (2) quello che blocca L2. Di conseguenza, possiamo combinare
539 lettori ricorsivi e non per L1 (perché blocca 539 lettori ricorsivi e non per L1 (perché bloccano gli stessi tipi) e possiamo
540 combinare scrittori e lettori non ricorsivi pe 540 combinare scrittori e lettori non ricorsivi per L2 (perché vengono bloccati
541 dagli stessi tipi). 541 dagli stessi tipi).
542 542
543 Con questa semplificazione, possiamo dedurre c 543 Con questa semplificazione, possiamo dedurre che ci sono 4 tipi di rami nel
544 grafo delle dipendenze di lockdep: 544 grafo delle dipendenze di lockdep:
545 545
546 1) -(ER)->: 546 1) -(ER)->:
547 dipendenza da scrittore esclusivo 547 dipendenza da scrittore esclusivo a lettore ricorsivo. "X -(ER)-> Y"
548 significa X -> Y, dove X è uno sc 548 significa X -> Y, dove X è uno scrittore e Y un lettore ricorsivo.
549 549
550 2) -(EN)->: 550 2) -(EN)->:
551 dipendenza da scrittore esclusivo 551 dipendenza da scrittore esclusivo a bloccatore non ricorsivo.
552 "X -(EN)->" significa X-> Y, dove 552 "X -(EN)->" significa X-> Y, dove X è uno scrittore e Y può essere
553 o uno scrittore o un lettore non r 553 o uno scrittore o un lettore non ricorsivo.
554 554
555 3) -(SR)->: 555 3) -(SR)->:
556 dipendenza da lettore condiviso a 556 dipendenza da lettore condiviso a lettore ricorsivo. "X -(SR)->"
557 significa X -> Y, dove X è un let 557 significa X -> Y, dove X è un lettore (ricorsivo o meno) e Y è un
558 lettore ricorsivo. 558 lettore ricorsivo.
559 559
560 4) -(SN)->: 560 4) -(SN)->:
561 dipendenza da lettore condiviso a 561 dipendenza da lettore condiviso a bloccatore non ricorsivo.
562 "X -(SN)-> Y" significa X -> Y , d 562 "X -(SN)-> Y" significa X -> Y , dove X è un lettore (ricorsivo
563 o meno) e Y può essere o uno scri 563 o meno) e Y può essere o uno scrittore o un lettore non ricorsivo.
564 564
565 Da notare che presi due blocchi, questi potreb 565 Da notare che presi due blocchi, questi potrebbero avere più dipendenza fra di
566 loro. Per esempio:: 566 loro. Per esempio::
567 567
568 TASK A: 568 TASK A:
569 569
570 read_lock(X); 570 read_lock(X);
571 write_lock(Y); 571 write_lock(Y);
572 ... 572 ...
573 573
574 TASK B: 574 TASK B:
575 575
576 write_lock(X); 576 write_lock(X);
577 write_lock(Y); 577 write_lock(Y);
578 578
579 Nel grafo delle dipendenze avremo sia X -(SN)- 579 Nel grafo delle dipendenze avremo sia X -(SN)-> Y che X -(EN)-> Y.
580 580
581 Usiamo -(xN)-> per rappresentare i rami sia pe 581 Usiamo -(xN)-> per rappresentare i rami sia per -(EN)-> che -(SN)->, allo stesso
582 modo -(Ex)->, -(xR)-> e -(Sx)-> 582 modo -(Ex)->, -(xR)-> e -(Sx)->
583 583
584 Un "percorso" in un grafo è una serie di nodi 584 Un "percorso" in un grafo è una serie di nodi e degli archi che li congiungono.
585 Definiamo un percorso "forte", come il percors 585 Definiamo un percorso "forte", come il percorso che non ha archi (dipendenze) di
586 tipo -(xR)-> e -(Sx)->. In altre parole, un pe 586 tipo -(xR)-> e -(Sx)->. In altre parole, un percorso "forte" è un percorso da un
587 blocco ad un altro attraverso le varie dipende 587 blocco ad un altro attraverso le varie dipendenze, e se sul percorso abbiamo X
588 -> Y -> Z (dove X, Y, e Z sono blocchi), e da 588 -> Y -> Z (dove X, Y, e Z sono blocchi), e da X a Y si ha una dipendenza -(SR)->
589 o -(ER)->, allora fra Y e Z non deve esserci u 589 o -(ER)->, allora fra Y e Z non deve esserci una dipendenza -(SN)-> o -(SR)->.
590 590
591 Nella prossima sezione vedremo perché definia 591 Nella prossima sezione vedremo perché definiamo questo percorso "forte".
592 592
593 Identificazione di stalli da lettura ricorsiva 593 Identificazione di stalli da lettura ricorsiva
594 ---------------------------------------------- 594 ----------------------------------------------
595 Ora vogliamo dimostrare altre due cose: 595 Ora vogliamo dimostrare altre due cose:
596 596
597 Lemma 1: 597 Lemma 1:
598 598
599 Se esiste un percorso chiuso forte (ciclo fort 599 Se esiste un percorso chiuso forte (ciclo forte), allora esiste anche una
600 combinazione di sequenze di blocchi che causa 600 combinazione di sequenze di blocchi che causa uno stallo. In altre parole,
601 l'esistenza di un ciclo forte è sufficiente a 601 l'esistenza di un ciclo forte è sufficiente alla scoperta di uno stallo.
602 602
603 Lemma 2: 603 Lemma 2:
604 604
605 Se non esiste un percorso chiuso forte (ciclo 605 Se non esiste un percorso chiuso forte (ciclo forte), allora non esiste una
606 combinazione di sequenze di blocchi che causin 606 combinazione di sequenze di blocchi che causino uno stallo. In altre parole, i
607 cicli forti sono necessari alla rilevazione de 607 cicli forti sono necessari alla rilevazione degli stallo.
608 608
609 Con questi due lemmi possiamo facilmente affer 609 Con questi due lemmi possiamo facilmente affermare che un percorso chiuso forte
610 è sia sufficiente che necessario per avere gl 610 è sia sufficiente che necessario per avere gli stalli, dunque averli equivale
611 alla possibilità di imbattersi concretamente 611 alla possibilità di imbattersi concretamente in uno stallo. Un percorso chiuso
612 forte significa che può causare stalli, per q 612 forte significa che può causare stalli, per questo lo definiamo "forte", ma ci
613 sono anche cicli di dipendenze che non causera 613 sono anche cicli di dipendenze che non causeranno stalli.
614 614
615 Dimostrazione di sufficienza (lemma 1): 615 Dimostrazione di sufficienza (lemma 1):
616 616
617 Immaginiamo d'avere un ciclo forte:: 617 Immaginiamo d'avere un ciclo forte::
618 618
619 L1 -> L2 ... -> Ln -> L1 619 L1 -> L2 ... -> Ln -> L1
620 620
621 Questo significa che abbiamo le seguenti dipen 621 Questo significa che abbiamo le seguenti dipendenze::
622 622
623 L1 -> L2 623 L1 -> L2
624 L2 -> L3 624 L2 -> L3
625 ... 625 ...
626 Ln-1 -> Ln 626 Ln-1 -> Ln
627 Ln -> L1 627 Ln -> L1
628 628
629 Ora possiamo costruire una combinazione di seq 629 Ora possiamo costruire una combinazione di sequenze di blocchi che causano lo
630 stallo. 630 stallo.
631 631
632 Per prima cosa facciamo sì che un processo/pr 632 Per prima cosa facciamo sì che un processo/processore prenda L1 in L1 -> L2, poi
633 un altro prende L2 in L2 -> L3, e così via. A 633 un altro prende L2 in L2 -> L3, e così via. Alla fine, tutti i Lx in Lx -> Lx+1
634 saranno trattenuti da processi/processori dive 634 saranno trattenuti da processi/processori diversi.
635 635
636 Poi visto che abbiamo L1 -> L2, chi trattiene 636 Poi visto che abbiamo L1 -> L2, chi trattiene L1 vorrà acquisire L2 in L1 -> L2,
637 ma prima dovrà attendere che venga rilasciato 637 ma prima dovrà attendere che venga rilasciato da chi lo trattiene. Questo perché
638 L2 è già trattenuto da un altro processo/pro 638 L2 è già trattenuto da un altro processo/processore, ed in più L1 -> L2 e L2 ->
639 L3 non sono -(xR)-> né -(Sx)-> (la definizion 639 L3 non sono -(xR)-> né -(Sx)-> (la definizione di forte). Questo significa che L2
640 in L1 -> L2 non è un bloccatore non ricorsivo 640 in L1 -> L2 non è un bloccatore non ricorsivo (bloccabile da chiunque), e L2 in
641 L2 -> L3 non è uno scrittore (che blocca chiu 641 L2 -> L3 non è uno scrittore (che blocca chiunque).
642 642
643 In aggiunta, possiamo trarre una simile conclu 643 In aggiunta, possiamo trarre una simile conclusione per chi sta trattenendo L2:
644 deve aspettare che L3 venga rilasciato, e cosà 644 deve aspettare che L3 venga rilasciato, e così via. Ora possiamo dimostrare che
645 chi trattiene Lx deve aspettare che Lx+1 venga 645 chi trattiene Lx deve aspettare che Lx+1 venga rilasciato. Notiamo che Ln+1 è
646 L1, dunque si è creato un ciclo dal quale non 646 L1, dunque si è creato un ciclo dal quale non possiamo uscire, quindi si ha uno
647 stallo. 647 stallo.
648 648
649 Dimostrazione della necessità (lemma 2): 649 Dimostrazione della necessità (lemma 2):
650 650
651 Questo lemma equivale a dire che: se siamo in 651 Questo lemma equivale a dire che: se siamo in uno scenario di stallo, allora
652 deve esiste un ciclo forte nel grafo delle dip 652 deve esiste un ciclo forte nel grafo delle dipendenze.
653 653
654 Secondo Wikipedia[1], se c'è uno stallo, allo 654 Secondo Wikipedia[1], se c'è uno stallo, allora deve esserci un ciclo di attese,
655 ovvero ci sono N processi/processori dove P1 a 655 ovvero ci sono N processi/processori dove P1 aspetta un blocco trattenuto da P2,
656 e P2 ne aspetta uno trattenuto da P3, ... e Pn 656 e P2 ne aspetta uno trattenuto da P3, ... e Pn attende che il blocco P1 venga
657 rilasciato. Chiamiamo Lx il blocco che attende 657 rilasciato. Chiamiamo Lx il blocco che attende Px, quindi P1 aspetta L1 e
658 trattiene Ln. Quindi avremo Ln -> L1 nel grafo 658 trattiene Ln. Quindi avremo Ln -> L1 nel grafo delle dipendenze. Similarmente,
659 nel grafo delle dipendenze avremo L1 -> L2, L2 659 nel grafo delle dipendenze avremo L1 -> L2, L2 -> L3, ..., Ln-1 -> Ln, il che
660 significa che abbiamo un ciclo:: 660 significa che abbiamo un ciclo::
661 661
662 Ln -> L1 -> L2 -> ... -> Ln 662 Ln -> L1 -> L2 -> ... -> Ln
663 663
664 , ed ora dimostriamo d'avere un ciclo forte. 664 , ed ora dimostriamo d'avere un ciclo forte.
665 665
666 Per un blocco Lx, il processo Px contribuisce 666 Per un blocco Lx, il processo Px contribuisce alla dipendenza Lx-1 -> Lx e Px+1
667 contribuisce a quella Lx -> Lx+1. Visto che Px 667 contribuisce a quella Lx -> Lx+1. Visto che Px aspetta che Px+1 rilasci Lx, sarÃ
668 impossibile che Lx in Px+1 sia un lettore e ch 668 impossibile che Lx in Px+1 sia un lettore e che Lx in Px sia un lettore
669 ricorsivo. Questo perché i lettori (ricorsivi 669 ricorsivo. Questo perché i lettori (ricorsivi o meno) non bloccano lettori
670 ricorsivi. Dunque, Lx-1 -> Lx e Lx -> Lx+1 non 670 ricorsivi. Dunque, Lx-1 -> Lx e Lx -> Lx+1 non possono essere una coppia di
671 -(xR)-> -(Sx)->. Questo è vero per ogni ciclo 671 -(xR)-> -(Sx)->. Questo è vero per ogni ciclo, dunque, questo è un ciclo forte.
672 672
673 Riferimenti 673 Riferimenti
674 ----------- 674 -----------
675 675
676 [1]: https://it.wikipedia.org/wiki/Stallo_(inf 676 [1]: https://it.wikipedia.org/wiki/Stallo_(informatica)
677 677
678 [2]: Shibu, K. (2009). Intro To Embedded Syste 678 [2]: Shibu, K. (2009). Intro To Embedded Systems (1st ed.). Tata McGraw-Hill
Linux® is a registered trademark of Linus Torvalds in the United States and other countries.
TOMOYO® is a registered trademark of NTT DATA CORPORATION.