실행 중 잠금 정확성 검증기

잠금 클래스

Runtime locking correctness validator는 Ingo Molnar가 시작했고 Arjan van de Ven이 내용을 추가했다.

Validator가 다루는 기본 object는 lock의 class다. Lock class는 실제 instance가 여러 개, 많게는 수만 개 존재하더라도 locking rule 관점에서 논리적으로 같은 lock의 집합이다. 예를 들어 inode struct 안의 lock은 하나의 class이고 각 inode는 그 class에 속한 자기 lock instance를 가진다.

Validator는 lock class의 usage state와 서로 다른 lock class 사이 dependency를 추적한다. Lock usage는 IRQ context와 관련해 lock이 어떻게 쓰였는지를 나타낸다. Lock dependency는 lock order로 이해할 수 있다. L1 -> L2는 task가 L1을 보유한 채 L2 획득을 시도했음을 뜻한다.

Lockdep 관점에서 L1과 L2가 원래부터 관련된 lock일 필요는 없다. Dependency는 그 순서가 한 번이라도 실제로 나타났다는 뜻일 뿐이다. Validator는 usage와 dependency가 올바름을 계속 증명하며, 잘못됐다고 판단하면 splat을 출력한다.

Lock class의 behavior는 모든 instance의 사용 이력을 합쳐 구성한다. Boot 뒤 어떤 class의 첫 instance가 사용되면 class를 등록하고, 이후 instance를 그 class에 mapping한다. 따라서 모든 instance의 usage와 dependency가 class의 이력에 기여한다.

Lock instance가 사라져도 lock class는 곧바로 사라지지 않는다. 다만 static 또는 dynamic lock class의 memory space가 회수되면 class를 제거할 수 있다. Module unload나 workqueue destroy가 그 예다.

lockdep의 기본 단위는 개별 잠금 주소가 아니라 같은 규칙을 따르는 잠금 클래스입니다. inode마다 잠금 인스턴스는 수만 개가 될 수 있지만 모두 같은 초기화 지점과 사용 규약을 공유하면 하나의 클래스로 매핑되어 상태와 의존성을 함께 축적합니다.

`L1 -> L2`는 한 실행 문맥이 L1을 보유한 채 L2를 획득했다는 관찰입니다. 두 잠금이 기능적으로 관련 있다는 뜻은 아니며, lockdep은 관찰된 순서를 방향 그래프의 간선으로 저장해 이후 순환 가능성과 IRQ 상태 규칙을 계속 검사합니다.

.. SPDX-License-Identifier: GPL-2.0

.. include:: ../disclaimer-ita.rst

Validatore di sincronizzazione durante l'esecuzione
===================================================

Classi di blocchi
-----------------

L'oggetto su cui il validatore lavora è una "classe" di blocchi.

Una classe di blocchi è un gruppo di blocchi che seguono le stesse regole di
sincronizzazione, anche quando i blocchi potrebbero avere più istanze (anche
decine di migliaia). Per esempio un blocco nella struttura inode è una classe,
mentre ogni inode sarà un'istanza di questa classe di blocco.

Il validatore traccia lo "stato d'uso" di una classe di blocchi e le sue
dipendenze con altre classi. L'uso di un blocco indica come quel blocco viene
usato rispetto al suo contesto d'interruzione, mentre le dipendenze di un blocco
possono essere interpretate come il loro ordine; per esempio L1 -> L2 suggerisce
che un processo cerca di acquisire L2 mentre già trattiene L1. Dal punto di
vista di lockdep, i due blocchi (L1 ed L2) non sono per forza correlati: quella
dipendenza indica solamente l'ordine in cui sono successe le cose. Il validatore
verifica permanentemente la correttezza dell'uso dei blocchi e delle loro
dipendenze, altrimenti ritornerà un errore.

Il comportamento di una classe di blocchi viene costruito dall'insieme delle sue
istanze. Una classe di blocco viene registrata alla creazione della sua prima
istanza, mentre tutte le successive istanze verranno mappate; dunque, il loro
uso e le loro dipendenze contribuiranno a costruire quello della classe. Una
classe di blocco non sparisce quando sparisce una sua istanza, ma può essere
rimossa quando il suo spazio in memoria viene reclamato. Per esempio, questo
succede quando si rimuove un modulo, o quando una *workqueue* viene eliminata.

사용 상태와 오류 문자열

Validator는 lock class의 사용 이력을 (4 usages × n STATEs + 1) category로 나눈다. 각 STATE에 대해 다음 네 종류를 추적한다.

• STATE context에서 한 번이라도 보유됨
• STATE context에서 readlock으로 한 번이라도 보유됨
• STATE가 enabled인 상태에서 한 번이라도 보유됨
• STATE가 enabled인 상태에서 readlock으로 한 번이라도 보유됨

n개의 STATE는 kernel/locking/lockdep_states.h에 정의되며 현재 hardirq와 softirq를 포함한다. 마지막 한 category는 lock이 한 번이라도 사용됐는지를 나타낸다.

Locking rule 위반 때 usage bit는 오류 message의 중괄호 안에 2 × n STATEs개의 문자로 표시된다. 다음 인위적인 예에서는 같은 lock을 이미 보유한 task가 다시 획득하려 한다.

modprobe/2287 is trying to acquire lock:
 (&sio_locks[i].lock){-.-.}, at: [<c02867fd>] mutex_lock+0x21/0x24

but task is already holding lock:
 (&sio_locks[i].lock){-.-.}, at: [<c02867fd>] mutex_lock+0x21/0x24

각 STATE마다 왼쪽부터 lock usage와 readlock usage를 차례로 나타낸다. 각 위치의 문자는 report 시점까지 관측된 정확한 조합을 요약한다.

주어진 STATE에서 IRQ context 획득 이력과 STATE enabled 상태의 획득 이력을 조합하면 네 경우가 나온다.

'-'가 표시되면 IRQ enabled 이력은 없었다고 추론할 수 있다. 있었다면 '?'가 표시됐을 것이기 때문이다. '+'에도 비슷한 추론을 적용할 수 있다. 아직 사용되지 않은 lock, 예를 들어 한 번도 사용되지 않은 mutex는 오류 원인의 일부가 될 수 없다.

각 잠금 클래스는 hardirq와 softirq 같은 `n`개 상태마다 일반 획득·reader 획득·상태 활성 상태의 일반 획득·상태 활성 상태의 reader 획득이라는 네 사용 비트를 기록하고, 여기에 한 번이라도 사용됐는지를 나타내는 비트를 더합니다.

오류의 `{....}` 표기는 상태별 두 위치를 왼쪽부터 읽습니다. `?`는 IRQ 문맥에서 획득, `-`는 IRQ 문맥에서 획득했지만 IRQ는 비활성, `+`는 IRQ가 활성인 상태에서 획득, `.`은 IRQ를 끈 비 IRQ 문맥 획득을 뜻하며 reader 기록은 대응 위치에 표시됩니다.

Stato
-----

Il validatore traccia l'uso cronologico delle classi di blocchi e ne divide
l'uso in categorie (4 USI * n STATI + 1).

I quattro USI possono essere:

- 'sempre trattenuto nel contesto <STATO>'
- 'sempre trattenuto come blocco di lettura nel contesto <STATO>'
- 'sempre trattenuto con <STATO> abilitato'
- 'sempre trattenuto come blocco di lettura con <STATO> abilitato'

gli `n` STATI sono codificati in kernel/locking/lockdep_states.h, ad oggi
includono:

- hardirq
- softirq

infine l'ultima categoria è:

- 'sempre trattenuto'                                  [ == !unused        ]

Quando vengono violate le regole di sincronizzazione, questi bit di utilizzo
vengono presentati nei messaggi di errore di sincronizzazione, fra parentesi
graffe, per un totale di `2 * n` (`n`: bit STATO). Un esempio inventato::

   modprobe/2287 is trying to acquire lock:
    (&sio_locks[i].lock){-.-.}, at: [<c02867fd>] mutex_lock+0x21/0x24

   but task is already holding lock:
    (&sio_locks[i].lock){-.-.}, at: [<c02867fd>] mutex_lock+0x21/0x24

Per un dato blocco, da sinistra verso destra, la posizione del bit indica l'uso
del blocco e di un eventuale blocco di lettura, per ognuno degli `n` STATI elencati
precedentemente. Il carattere mostrato per ogni bit indica:

   ===  ===========================================================================
   '.'  acquisito con interruzioni disabilitate fuori da un contesto d'interruzione
   '-'  acquisito in contesto d'interruzione
   '+'  acquisito con interruzioni abilitate
   '?'  acquisito in contesto d'interruzione con interruzioni abilitate
   ===  ===========================================================================

Il seguente esempio mostra i bit::

    (&sio_locks[i].lock){-.-.}, at: [<c02867fd>] mutex_lock+0x21/0x24
                         ||||
                         ||| \-> softirq disabilitati e fuori da un contesto di softirq
                         || \--> acquisito in un contesto di softirq
                         | \---> hardirq disabilitati e fuori da un contesto di hardirq
                          \----> acquisito in un contesto di hardirq

Per un dato STATO, che il blocco sia mai stato acquisito in quel contesto di
STATO, o che lo STATO sia abilitato, ci lascia coi quattro possibili scenari
mostrati nella seguente tabella. Il carattere associato al bit indica con
esattezza in quale scenario ci si trova al momento del rapporto.

  +---------------+---------------+------------------+
  |               | irq abilitati | irq disabilitati |
  +---------------+---------------+------------------+
  | sempre in irq |      '?'      |       '-'        |
  +---------------+---------------+------------------+
  | mai in irq    |      '+'      |       '.'        |
  +---------------+---------------+------------------+

Il carattere '-' suggerisce che le interruzioni sono disabilitate perché
altrimenti verrebbe mostrato il carattere '?'. Una deduzione simile può essere
fatta anche per '+'

I blocchi inutilizzati (ad esempio i mutex) non possono essere fra le cause di
un errore.

단일 잠금 상태 규칙

Lock이 irq-safe라는 말은 IRQ context에서 한 번이라도 사용됐다는 뜻이다. irq-unsafe는 IRQ enabled 상태에서 한 번이라도 획득됐다는 뜻이다. Softirq-unsafe lock class는 자동으로 hardirq-unsafe이기도 하다.

각 lock class의 usage에서 hardirq-safe와 hardirq-unsafe는 상호 배타적이고, softirq-safe와 softirq-unsafe도 상호 배타적이다. 각 pair에서는 하나만 설정될 수 있다.

<hardirq-safe> or <hardirq-unsafe>
<softirq-safe> or <softirq-unsafe>

IRQ context에서 사용할 수 있는 irq-safe lock은 IRQ enabled 상태에서 획득된 적이 있어서는 안 된다. 그렇게 사용하면 lock을 획득한 뒤 release하기 전에 interrupt가 들어왔을 때 같은 lock을 두 번째로 획득하려 하므로 deadlock이 생길 수 있다. 이를 lock recursion deadlock이라 한다.

Validator는 이 single-lock state rule을 어긴 lock usage를 발견해 report한다.

한 클래스가 irq-safe라는 것은 실제 IRQ 문맥에서 획득된 적이 있다는 뜻이고, irq-unsafe는 IRQ가 활성인 상태에서 획득된 적이 있다는 뜻입니다. 같은 클래스가 양쪽 상태를 모두 가질 경우 IRQ가 평상시 보유자를 끊고 같은 잠금을 다시 기다리는 재귀 교착이 가능하므로 lockdep이 즉시 모순으로 보고합니다.

Regole dello stato per un blocco singolo
----------------------------------------

Avere un blocco sicuro in interruzioni (*irq-safe*) significa che è sempre stato
usato in un contesto d'interruzione, mentre un blocco insicuro in interruzioni
(*irq-unsafe*) significa che è sempre stato acquisito con le interruzioni
abilitate.

Una classe softirq insicura è automaticamente insicura anche per hardirq. I
seguenti stati sono mutualmente esclusivi: solo una può essere vero quando viene
usata una classe di blocco::

 <hardirq-safe> o <hardirq-unsafe>
 <softirq-safe> o <softirq-unsafe>

Questo perché se un blocco può essere usato in un contesto di interruzioni
(sicuro in interruzioni), allora non può mai essere acquisito con le
interruzioni abilitate (insicuro in interruzioni). Altrimenti potrebbe
verificarsi uno stallo. Per esempio, questo blocco viene acquisito, ma prima di
essere rilasciato il contesto d'esecuzione viene interrotto nuovamente, e quindi
si tenterà di acquisirlo nuovamente. Questo porterà ad uno stallo, in
particolare uno stallo ricorsivo.

Il validatore rileva e riporta gli usi di blocchi che violano queste regole per
blocchi singoli.

복수 잠금 의존성 규칙

같은 lock class를 두 번 획득하면 lock recursion deadlock이 생길 수 있으므로 허용되지 않는다.

두 lock을 서로 반대 순서로 획득하는 것도 허용되지 않는다. L1을 보유한 채 L2를 기다리는 context와 L2를 보유한 채 L1을 기다리는 context가 원을 이루어 영원히 서로를 기다릴 수 있다. 이를 lock inversion deadlock이라 한다.

<L1> -> <L2>
<L2> -> <L1>

Validator는 획득 operation 사이에 다른 locking sequence가 얼마든지 들어 있어도 임의 복잡도의 dependency circle을 찾아낸다.

Usage에 기반한 다음 lock dependency도 어떤 두 lock class 사이에서든 허용되지 않는다.

<hardirq-safe> -> <hardirq-unsafe>
<softirq-safe> -> <softirq-unsafe>

Hardirq-safe lock은 hardirq context에서 획득될 수 있고, 그 context가 hardirq-unsafe lock을 보유한 실행을 interrupt할 수 있다. 그러면 lock inversion deadlock이 생길 수 있다. Softirq-safe lock과 softirq-unsafe lock도 같은 원리다.

Kernel에서 어떤 locking sequence가 관측되든 새 lock을 획득할 때 validator는 새 lock과 현재 보유한 모든 lock 사이에 rule 위반이 있는지 검사한다.

Lock class state가 바뀌면 과거 dependency도 다시 검사한다. 새 hardirq-safe lock이 발견되면 과거에 hardirq-unsafe lock을 획득했는지, 새 softirq-safe lock이면 softirq-unsafe lock을 획득했는지 확인한다. 새 hardirq-unsafe lock이 발견되면 과거에 hardirq-safe lock이 이를 획득했는지, 새 softirq-unsafe lock이면 softirq-safe lock이 이를 획득했는지 확인한다.

실제로 그 interrupt timing이 아직 발생하지 않았어도 검사한다. Interrupt context는 어떤 irq-unsafe 또는 hardirq-unsafe lock 보유 구간도 interrupt할 수 있고, 그 가능성만으로 inversion deadlock이 성립할 수 있기 때문이다.

같은 잠금 클래스를 두 번 획득하는 재귀 경로와 `L1 -> L2`, `L2 -> L1`의 역순 경로는 모두 금지됩니다. 실제 두 CPU가 동시에 그 순서를 실행하지 않았더라도 각각의 순서가 한 번씩 관찰되면 그래프에 순환이 생겨 잠재 교착으로 증명됩니다.

IRQ-safe 클래스에서 IRQ-unsafe 클래스로 향하는 경로도 금지됩니다. IRQ 문맥이 safe 잠금을 보유한 채 unsafe 잠금을 기다리고, 평상시 문맥이 unsafe 잠금을 보유한 상태에서 IRQ에 선점되면 서로를 기다리게 되므로 직접 간선뿐 아니라 임의 길이의 의존성 경로를 검사합니다.

Regole per le dipendenze di blocchi multipli
--------------------------------------------

La stessa classe di blocco non deve essere acquisita due volte, questo perché
potrebbe portare ad uno blocco ricorsivo e dunque ad uno stallo.

Inoltre, due blocchi non possono essere trattenuti in ordine inverso::

 <L1> -> <L2>
 <L2> -> <L1>

perché porterebbe ad uno stallo - chiamato stallo da blocco inverso - in cui si
cerca di trattenere i due blocchi in un ciclo in cui entrambe i contesti
aspettano per sempre che l'altro termini. Il validatore è in grado di trovare
queste dipendenze cicliche di qualsiasi complessità, ovvero nel mezzo ci
potrebbero essere altre sequenze di blocchi. Il validatore troverà se questi
blocchi possono essere acquisiti circolarmente.

In aggiunta, le seguenti sequenze di blocco nei contesti indicati non sono
permesse, indipendentemente da quale che sia la classe di blocco::

   <hardirq-safe>   ->  <hardirq-unsafe>
   <softirq-safe>   ->  <softirq-unsafe>

La prima regola deriva dal fatto che un blocco sicuro in interruzioni può essere
trattenuto in un contesto d'interruzione che, per definizione, ha la possibilità
di interrompere un blocco insicuro in interruzioni; questo porterebbe ad uno
stallo da blocco inverso. La seconda, analogamente, ci dice che un blocco sicuro
in interruzioni software potrebbe essere trattenuto in un contesto di
interruzione software, dunque potrebbe interrompere un blocco insicuro in
interruzioni software.

Le suddette regole vengono applicate per qualsiasi sequenza di blocchi: quando
si acquisiscono nuovi blocchi, il validatore verifica se vi è una violazione
delle regole fra il nuovo blocco e quelli già trattenuti.

Quando una classe di blocco cambia stato, applicheremo le seguenti regole:

- se viene trovato un nuovo blocco sicuro in interruzioni, verificheremo se
  abbia mai trattenuto dei blocchi insicuri in interruzioni.

- se viene trovato un nuovo blocco sicuro in interruzioni software,
  verificheremo se abbia trattenuto dei blocchi insicuri in interruzioni
  software.

- se viene trovato un nuovo blocco insicuro in interruzioni, verificheremo se
  abbia trattenuto dei blocchi sicuri in interruzioni.

- se viene trovato un nuovo blocco insicuro in interruzioni software,
  verificheremo se abbia trattenuto dei blocchi sicuri in interruzioni
  software.

(Di nuovo, questi controlli vengono fatti perché un contesto d'interruzione
potrebbe interrompere l'esecuzione di qualsiasi blocco insicuro portando ad uno
stallo; questo anche se lo stallo non si verifica in pratica)

데이터 계층에 따른 중첩 잠금

Linux kernel에는 같은 lock class의 instance를 둘 이상 획득하는 경우가 조금 있다. 같은 type의 object 사이에 hierarchy가 있을 때 주로 나타난다. Hierarchy 속성이 두 object 사이의 자연스러운 순서를 정의하며 kernel은 각 object의 lock을 항상 그 고정 순서로 잡는다.

Whole-disk block device object와 partition block device object가 nested locking의 예다. Partition은 whole device의 일부이므로 whole disk lock을 partition lock보다 항상 상위에서 획득하면 ordering은 올바르다. 다만 이 ordering rule은 static하지 않으므로 validator가 자연스러운 계층을 자동으로 알아내지는 못한다.

이 올바른 usage model을 validator에 알려 주기 위해 여러 locking primitive에 nesting level을 지정하는 _nested() version이 추가됐다. Block device mutex 예시는 다음과 같다.

enum bdev_bd_mutex_lock_class
{
     BD_MUTEX_NORMAL,
     BD_MUTEX_WHOLE,
     BD_MUTEX_PARTITION
};

mutex_lock_nested(&bdev->bd_contains->bd_mutex,
                  BD_MUTEX_PARTITION);

이 호출은 대상 bdev object가 partition임을 알고 lock을 획득한다. Validator는 nested 방식으로 획득한 lock을 validation 목적상 별도 subclass로 취급한다.

디스크 전체 block device와 그 파티션처럼 같은 클래스 인스턴스 사이에 데이터 자체의 계층이 있으면 상위 객체 뒤에 하위 객체를 잡는 순서가 유효할 수 있습니다. lockdep은 동적 객체 관계를 자동 추론할 수 없으므로 `_nested()` API의 subclass 인자로 이 순서를 알려야 합니다.

`mutex_lock_nested(&bdev->bd_contains->bd_mutex, BD_MUTEX_PARTITION)`은 파티션 잠금을 별도 하위 클래스로 취급하게 합니다. 실제 계층이 틀렸는데 subclass만 지정하면 진짜 교착을 숨기는 거짓 음성과 불필요한 경고인 거짓 양성이 모두 생길 수 있으므로 데이터 규약이 확실할 때만 사용합니다.

Eccezione: dipendenze annidate sui dati portano a blocchi annidati
------------------------------------------------------------------

Ci sono alcuni casi in cui il kernel Linux acquisisce più volte la stessa
istanza di una classe di blocco. Solitamente, questo succede quando esiste una
gerarchia fra oggetti dello stesso tipo. In questi casi viene ereditato
implicitamente l'ordine fra i due oggetti (definito dalle proprietà di questa
gerarchia), ed il kernel tratterrà i blocchi in questo ordine prefissato per
ognuno degli oggetti.

Un esempio di questa gerarchia di oggetti che producono "blocchi annidati" sono
i *block-dev* che rappresentano l'intero disco e quelli che rappresentano una
sua partizione; la partizione è una parte del disco intero, e l'ordine dei
blocchi sarà corretto fintantoche uno acquisisce il blocco del disco intero e
poi quello della partizione. Il validatore non rileva automaticamente questo
ordine implicito, perché queste regole di sincronizzazione non sono statiche.

Per istruire il validatore riguardo a questo uso corretto dei blocchi sono stati
introdotte nuove primitive per specificare i "livelli di annidamento". Per
esempio, per i blocchi a mutua esclusione dei *block-dev* si avrebbe una
chiamata simile a::

  enum bdev_bd_mutex_lock_class
  {
       BD_MUTEX_NORMAL,
       BD_MUTEX_WHOLE,
       BD_MUTEX_PARTITION
  };

  mutex_lock_nested(&bdev->bd_contains->bd_mutex, BD_MUTEX_PARTITION);

In questo caso la sincronizzazione viene fatta su un *block-dev* sapendo che si
tratta di una partizione.

Ai fini della validazione, il validatore lo considererà con una - sotto - classe
di blocco separata.

Nota: Prestate estrema attenzione che la vostra gerarchia sia corretta quando si
vogliono usare le primitive _nested(); altrimenti potreste avere sia falsi
positivi che falsi negativi.

잠금 요구 조건 주석

특정 지점에서 어떤 lock을 보유해야 하는지 annotate하고 검사하는 두 construct는 lockdep_assert_held*(&lock)과 lockdep_*pin_lock(&lock)이다.

lockdep_assert_held* macro family는 특정 시점에 지정한 lock을 보유했는지 assert하고, 그렇지 않으면 WARN()을 만든다. Kernel 전반에서 널리 쓰인다. kernel/sched/core.c의 update_rq_clock()은 rq clock을 안전하게 갱신하려면 rq->lock을 보유해야 함을 다음처럼 검사한다.

void update_rq_clock(struct rq *rq)
{
    s64 delta;

    lockdep_assert_held(&rq->lock);
    [...]
}

lockdep_*pin_lock() family는 현재 rq->lock에만 쓰일 정도로 채택 범위가 좁지만 관심 lock이 실수로 unlock되면 WARN()을 만든다. Upper layer는 lock이 계속 잡혀 있다고 가정하지만 callback 아래쪽 layer가 lock을 잠깐 놓았다 다시 잡아도 된다고 생각해 race를 만드는 code를 debug할 때 특히 유용하다.

lockdep_pin_lock()은 struct pin_cookie를 반환하고 lockdep_unpin_lock()은 이 cookie로 중간에 누군가 lock 상태를 건드리지 않았는지 검사한다. kernel/sched/sched.h의 wrapper는 다음과 같다.

static inline void rq_pin_lock(struct rq *rq,
                               struct rq_flags *rf)
{
    rf->cookie = lockdep_pin_lock(&rq->lock);
    [...]
}

static inline void rq_unpin_lock(struct rq *rq,
                                 struct rq_flags *rf)
{
    [...]
    lockdep_unpin_lock(&rq->lock, rf->cookie);
}

Locking requirement를 comment로 남기는 것도 정보가 되지만 annotation의 runtime check는 locking problem debug에 매우 값지고 code를 읽을 때도 같은 수준의 detail을 전달한다. 어느 쪽을 쓸지 망설여진다면 annotation을 우선한다.

`lockdep_assert_held*()` 계열은 해당 지점에서 지정 잠금을 보유해야 한다는 실행 중 계약입니다. 단순 주석과 달리 규약 위반 시 `WARN()`을 내며, `kernel/sched/core.c`의 runqueue clock 갱신처럼 호출자가 잠금을 잡아야 하는 내부 함수의 전제 조건을 코드로 검증합니다.

`lockdep_pin_lock()`이 반환한 `struct pin_cookie`를 `lockdep_unpin_lock()`에 넘기면 callback 아래쪽이 잠금을 몰래 풀었다 다시 잡는 행위까지 감지할 수 있습니다. 상위 계층이 임계 구역의 연속성을 기대하는 경우 단순 ‘종료 시 보유 여부’보다 강한 검사가 됩니다.

Annotazioni
-----------

Si possono utilizzare due costrutti per verificare ed annotare se certi blocchi
devono essere trattenuti: lockdep_assert_held*(&lock) e
lockdep_*pin_lock(&lock).

Come suggerito dal nome, la famiglia di macro lockdep_assert_held* asseriscono
che un dato blocco in un dato momento deve essere trattenuto (altrimenti, verrà
generato un WARN()). Queste vengono usate abbondantemente nel kernel, per
esempio in kernel/sched/core.c::

  void update_rq_clock(struct rq *rq)
  {
	s64 delta;

	lockdep_assert_held(&rq->lock);
	[...]
  }

dove aver trattenuto rq->lock è necessario per aggiornare in sicurezza il clock
rq.

L'altra famiglia di macro è lockdep_*pin_lock(), che a dire il vero viene usata
solo per rq->lock ATM. Se per caso un blocco non viene trattenuto, queste
genereranno un WARN(). Questo si rivela particolarmente utile quando si deve
verificare la correttezza di codice con *callback*, dove livelli superiori
potrebbero assumere che un blocco rimanga trattenuto, ma livelli inferiori
potrebbero invece pensare che il blocco possa essere rilasciato e poi
riacquisito (involontariamente si apre una sezione critica). lockdep_pin_lock()
restituisce 'struct pin_cookie' che viene usato da lockdep_unpin_lock() per
verificare che nessuno abbia manomesso il blocco. Per esempio in
kernel/sched/sched.h abbiamo::

  static inline void rq_pin_lock(struct rq *rq, struct rq_flags *rf)
  {
	rf->cookie = lockdep_pin_lock(&rq->lock);
	[...]
  }

  static inline void rq_unpin_lock(struct rq *rq, struct rq_flags *rf)
  {
	[...]
	lockdep_unpin_lock(&rq->lock, rf->cookie);
  }

I commenti riguardo alla sincronizzazione possano fornire informazioni utili,
tuttavia sono le verifiche in esecuzione effettuate da queste macro ad essere
vitali per scovare problemi di sincronizzazione, ed inoltre forniscono lo stesso
livello di informazioni quando si ispeziona il codice. Nel dubbio, preferite
queste annotazioni!

정확성 폐쇄성과 성능

Validator는 kernel lifetime 동안 한 번이라도 발생한 단순하고 독립적인 single-task locking sequence 각각에 대해 수학적 closure를 만든다. 이 component sequence들을 어떤 조합과 timing으로 실행해도 어떤 종류의 lock-related deadlock도 만들 수 없음을 100% 확실하게 증명한다.

복잡한 multi-CPU, multi-task locking scenario가 실제로 발생할 필요는 없다. 단순 component locking chain이 어느 task나 context에서든 한 번씩만 나타나면 validator가 correctness를 증명할 수 있다. 원래라면 CPU 세 개 이상과 task, IRQ context, timing의 매우 희귀한 조합이 필요한 deadlock도 부하가 적은 single-CPU system에서 검출할 수 있다.

따라서 locking QA의 복잡성이 크게 낮아진다. 현실적으로 불가능한 모든 CPU interaction과 모든 hardirq·softirq nesting 조합을 일으키는 대신, kernel의 단순 single-task dependency를 가능한 한 많이 한 번씩 실행하면 된다.

O(N²) 검사를 줄이는 chain cache

위 rule을 lock 획득과 IRQ-enable event마다 모두 검사하면 runtime overhead가 너무 커져 system을 사실상 쓸 수 없을 정도로 느리게 만든다. 검사 complexity는 O(N²)이므로 lock class가 수백 개만 있어도 event마다 수만 번 검사해야 한다.

Lockdep은 주어진 locking scenario, 즉 lock을 차례로 획득한 unique sequence를 한 번만 검사해 해결한다. Held lock의 단순 stack을 유지하고 lock chain마다 unique한 가벼운 64-bit hash를 계산한다.

Chain을 처음 validate하면 hash를 lock-free 방식으로 조회할 수 있는 hash table에 넣는다. 나중에 같은 chain이 다시 발생하면 hash table을 보고 다시 validate하지 않는다.

lockdep의 100% 증명은 실제 커널에서 한 번이라도 관찰된 단일 실행 흐름의 잠금 순서 집합에 대한 수학적 폐쇄성을 뜻합니다. 가능한 모든 CPU 타이밍을 재현하지 않아도 관찰된 간선을 조합한 그래프에 순환이 없으면 그 집합 안에서는 어떤 배치로도 교착이 생기지 않습니다.

따라서 품질 검증의 핵심은 복잡한 동시 실행을 우연히 재현하는 것이 아니라 가능한 코드 경로와 IRQ·softirq 문맥의 단순 잠금 순서를 각각 한 번 이상 실행하는 것입니다. 검증기는 잠금 획득 fast path에 연결되지만 이미 확인한 체인은 캐시해 반복 비용을 줄입니다.

Dimostrazione di correttezza al 100%
------------------------------------

Il validatore verifica la proprietà di chiusura in senso matematico. Ovvero, per
ogni sequenza di sincronizzazione di un singolo processo che si verifichi almeno
una volta nel kernel, il validatore dimostrerà con una certezza del 100% che
nessuna combinazione e tempistica di queste sequenze possa causare uno stallo in
una qualsiasi classe di blocco. [1]_

In pratica, per dimostrare l'esistenza di uno stallo non servono complessi
scenari di sincronizzazione multi-processore e multi-processo. Il validatore può
dimostrare la correttezza basandosi sulla sola sequenza di sincronizzazione
apparsa almeno una volta (in qualunque momento, in qualunque processo o
contesto). Uno scenario complesso che avrebbe bisogno di 3 processori e una
sfortunata presenza di processi, interruzioni, e pessimo tempismo, può essere
riprodotto su un sistema a singolo processore.

Questo riduce drasticamente la complessità del controllo di qualità della
sincronizzazione nel kernel: quello che deve essere fatto è di innescare nel
kernel quante più possibili "semplici" sequenze di sincronizzazione, almeno una
volta, allo scopo di dimostrarne la correttezza. Questo al posto di innescare
una verifica per ogni possibile combinazione di sincronizzazione fra processori,
e differenti scenari con hardirq e softirq e annidamenti vari (nella pratica,
impossibile da fare)

.. [1]

   assumendo che il validatore sia corretto al 100%, e che nessun altra parte
   del sistema possa corromperne lo stato. Assumiamo anche che tutti i percorsi
   MNI/SMM [potrebbero interrompere anche percorsi dove le interruzioni sono
   disabilitate] sono corretti e non interferiscono con il validatore. Inoltre,
   assumiamo che un hash a 64-bit sia unico per ogni sequenza di
   sincronizzazione nel sistema. Infine, la ricorsione dei blocchi non deve
   essere maggiore di 20.

Prestazione
-----------

Le regole sopracitate hanno bisogno di una quantità **enorme** di verifiche
durante l'esecuzione. Il sistema sarebbe diventato praticamente inutilizzabile
per la sua lentezza se le avessimo fatte davvero per ogni blocco trattenuto e
per ogni abilitazione delle interruzioni. La complessità della verifica è
O(N^2), quindi avremmo dovuto fare decine di migliaia di verifiche per ogni
evento, il tutto per poche centinaia di classi.

Il problema è stato risolto facendo una singola verifica per ogni 'scenario di
sincronizzazione' (una sequenza unica di blocchi trattenuti uno dopo l'altro).
Per farlo, viene mantenuta una pila dei blocchi trattenuti, e viene calcolato un
hash a 64-bit unico per ogni sequenza. Quando la sequenza viene verificata per
la prima volta, l'hash viene inserito in una tabella hash. La tabella potrà
essere verificata senza bisogno di blocchi. Se la sequenza dovesse ripetersi, la
tabella ci dirà che non è necessario verificarla nuovamente.

lockdep 키 고갈 진단

Validator가 추적할 수 있는 lock class는 최대 MAX_LOCKDEP_KEYS개다. 이 수를 넘으면 다음 warning이 발생한다.

DEBUG_LOCKS_WARN_ON(id >= MAX_LOCKDEP_KEYS)

현재 기본 MAX_LOCKDEP_KEYS는 8191이고 일반 desktop system의 lock class는 1,000개보다 적다. 따라서 이 warning은 보통 lock class leak이나 lock initialization 누락을 뜻한다.

반복되는 module load와 unload

Validator를 실행한 채 module을 반복 load·unload하면 lock class leak이 생긴다. Load할 때마다 module lock의 새 class set을 만들지만 unload는 과거 class를 제거하지 않는다. Lock class 재사용이 어려운 이유는 아래 설명과 같다. 반복하면 class 수가 결국 maximum에 도달한다.

대규모 lock array의 초기화 누락

명시적으로 초기화하지 않은 lock을 많이 포함한 array 같은 structure도 원인이 된다. Bucket마다 spinlock_t가 있는 8192-bucket hash table에서 각 spinlock을 runtime에 명시적으로 초기화하지 않으면 lock class 8192개를 소비한다.

Compile-time initializer인 __SPIN_LOCK_UNLOCKED()만 쓰지 말고 loop에서 각 lock에 spin_lock_init()을 호출하면 8192개 lock이 모두 하나의 lock class에 들어간다. 교훈은 lock을 항상 명시적으로 초기화하라는 것이다.

Lock class를 재사용하도록 validator를 고치자는 주장이 나올 수 있다. 그러나 제거할 class가 lock-dependency graph에 연결돼 있을 가능성을 고려해 필요한 변경을 검토하면 말보다 구현이 훨씬 어렵다는 점을 알 수 있다.

Leak 찾기

현재 사용 중인 lock class 수와 maximum은 다음 명령으로 확인한다.

grep "lock-classes" /proc/lockdep_stats

lock-classes:                          748 [max: 8191]

할당 수가 시간에 따라 계속 늘어나면 leak일 가능성이 높다. Leaking lock class는 다음 명령으로 찾을 수 있다.

grep "BD" /proc/lockdep

명령 결과를 저장하고 나중 결과와 비교해 새로 늘어난 class를 찾는다. 같은 output은 runtime lock initialization을 빠뜨린 위치를 찾는 데도 도움이 된다.

동적 잠금 클래스를 계속 등록하고 해제하지 않으면 `MAX_LOCKDEP_KEYS`에 도달해 lockdep이 꺼질 수 있습니다. 모듈 언로드나 workqueue 제거처럼 메모리 수명이 끝날 때 클래스 키도 회수되어야 하며, 정적 키와 동적 키의 수명 규칙을 어기면 검증 능력 자체를 잃습니다.

`/proc/lockdep_stats`의 `lock-classes` 증가를 반복 작업 전후로 비교하고 `/proc/lockdep`에서 의심 이름을 찾으면 누수된 클래스를 좁힐 수 있습니다. `DEBUG_LOCKS_WARN_ON(id >= MAX_LOCKDEP_KEYS)` 경고는 교착 보고가 아니라 검증기 자원 고갈 신호로 해석해야 합니다.

Risoluzione dei problemi
------------------------

Il massimo numero di classi di blocco che il validatore può tracciare è:
MAX_LOCKDEP_KEYS. Oltrepassare questo limite indurrà lokdep a generare il
seguente avviso::

	(DEBUG_LOCKS_WARN_ON(id >= MAX_LOCKDEP_KEYS))

Di base questo valore è 8191, e un classico sistema da ufficio ha meno di 1000
classi, dunque questo avviso è solitamente la conseguenza di un problema di
perdita delle classi di blocco o d'inizializzazione dei blocchi. Di seguito una
descrizione dei due problemi:

1. caricare e rimuovere continuamente i moduli mentre il validatore è in
   esecuzione porterà ad una perdita di classi di blocco. Il problema è che ogni
   caricamento crea un nuovo insieme di classi di blocco per tutti i blocchi di
   quel modulo. Tuttavia, la rimozione del modulo non rimuove le vecchie classi
   (vedi dopo perché non le riusiamo). Dunque, il continuo caricamento e
   rimozione di un modulo non fa altro che aumentare il contatore di classi fino
   a raggiungere, eventualmente, il limite.

2. Usare array con un gran numero di blocchi che non vengono esplicitamente
   inizializzati. Per esempio, una tabella hash con 8192 *bucket* dove ognuno ha
   il proprio spinlock_t consumerà 8192 classi di blocco a meno che non vengano
   esplicitamente inizializzati in esecuzione usando spin_lock_init() invece
   dell'inizializzazione durante la compilazione con __SPIN_LOCK_UNLOCKED().
   Sbagliare questa inizializzazione garantisce un esaurimento di classi di
   blocco. Viceversa, un ciclo che invoca spin_lock_init() su tutti i blocchi li
   mapperebbe tutti alla stessa classe di blocco.

   La morale della favola è che dovete sempre inizializzare esplicitamente i
   vostri blocchi.

Qualcuno potrebbe argomentare che il validatore debba permettere il riuso di
classi di blocco. Tuttavia, se siete tentati dall'argomento, prima revisionate
il codice e pensate alla modifiche necessarie, e tenendo a mente che le classi
di blocco da rimuovere probabilmente sono legate al grafo delle dipendenze. Più
facile a dirsi che a farsi.

Ovviamente, se non esaurite le classi di blocco, la prossima cosa da fare è
quella di trovare le classi non funzionanti. Per prima cosa, il seguente comando
ritorna il numero di classi attualmente in uso assieme al valore massimo::

	grep "lock-classes" /proc/lockdep_stats

Questo comando produce il seguente messaggio::

	lock-classes:                          748 [max: 8191]

Se il numero di assegnazioni (748 qui sopra) aumenta continuamente nel tempo,
allora c'è probabilmente un problema da qualche parte. Il seguente comando può
essere utilizzato per identificare le classi di blocchi problematiche::

	grep "BD" /proc/lockdep

Eseguite il comando e salvatene l'output, quindi confrontatelo con l'output di
un'esecuzione successiva per identificare eventuali problemi. Questo stesso
output può anche aiutarti a trovare situazioni in cui l'inizializzazione del
blocco è stata omessa.

재귀 reader 잠금

이후 문서는 특정 종류의 dependency cycle과 deadlock 가능성이 동치임을 증명한다. Locker는 writer, non-recursive reader, recursive reader 세 종류다.

따라서 N은 r 또는 W이고 S는 r 또는 R이다. Recursive reader는 같은 lock instance의 다른 reader critical section 안에서도 획득할 수 있어 한 lock의 read-side critical section을 중첩할 수 있다. Non-recursive reader는 같은 상황에서 획득을 시도하면 self-deadlock을 일으킨다.

차이는 recursive reader가 현재 write lock holder에게만 block되지만 non-recursive reader는 write lock waiter에게도 block될 수 있다는 점에서 생긴다.

표기 `W` 또는 `E`는 배타 writer, `r`은 비재귀 shared reader, `R`은 재귀 shared reader입니다. `S`는 두 reader 종류를 합친 집합이고 `N`은 writer와 비재귀 reader처럼 다른 획득을 막을 수 있는 비재귀 locker 집합입니다.

재귀 reader는 현재 writer 보유자에게는 막히지만 writer 대기자만으로는 막히지 않습니다. 이미 read lock을 가진 Task A가 두 번째 read를 얻을 때 Task B의 writer 대기가 있어도 재귀 reader라면 진행하며, 비재귀 reader라면 자신이 놓아야 할 첫 read 때문에 스스로 교착될 수 있습니다.

Lettura ricorsiva dei blocchi
-----------------------------

Il resto di questo documento vuole dimostrare che certi cicli equivalgono ad una
possibilità di stallo.

Ci sono tre tipi di bloccatori: gli scrittori (bloccatori esclusivi, come
spin_lock() o write_lock()), lettori non ricorsivi (bloccatori condivisi, come
down_read()), e lettori ricorsivi (bloccatori condivisi ricorsivi, come
rcu_read_lock()). D'ora in poi, per questi tipi di bloccatori, useremo la
seguente notazione:

    W o E: per gli scrittori (bloccatori esclusivi) (W dall'inglese per
           *Writer*, ed E per *Exclusive*).

    r: per i lettori non ricorsivi (r dall'inglese per *reader*).

    R: per i lettori ricorsivi (R dall'inglese per *Reader*).

    S: per qualsiasi lettore (non ricorsivi + ricorsivi), dato che entrambe
       sono bloccatori condivisi (S dall'inglese per *Shared*).

    N: per gli scrittori ed i lettori non ricorsivi, dato che entrambe sono
       non ricorsivi.

Ovviamente, N equivale a "r o W" ed S a "r o R".

Come suggerisce il nome, i lettori ricorsivi sono dei bloccatori a cui è
permesso di acquisire la stessa istanza di blocco anche all'interno della
sezione critica di un altro lettore. In altre parole, permette di annidare la
stessa istanza di blocco nelle sezioni critiche dei lettori.

Dall'altro canto, lo stesso comportamento indurrebbe un lettore non ricorsivo ad
auto infliggersi uno stallo.

La differenza fra questi due tipi di lettori esiste perché: quelli ricorsivi
vengono bloccati solo dal trattenimento di un blocco di scrittura, mentre quelli
non ricorsivi possono essere bloccati dall'attesa di un blocco di scrittura.
Consideriamo il seguente esempio::

    TASK A:            TASK B:

    read_lock(X);
                       write_lock(X);
    read_lock_2(X);

L'attività A acquisisce il blocco di lettura X (non importa se di tipo ricorsivo
o meno) usando read_lock(). Quando l'attività B tenterà di acquisire il blocco
X, si fermerà e rimarrà in attesa che venga rilasciato. Ora se read_lock_2() è
un tipo lettore ricorsivo, l'attività A continuerà perché gli scrittori in
attesa non possono bloccare lettori ricorsivi, e non avremo alcuno stallo.
Tuttavia, se read_lock_2() è un lettore non ricorsivo, allora verrà bloccato
dall'attività B e si causerà uno stallo.

reader·writer 차단 행렬

같은 lock instance의 reader와 writer 사이에는 네 가지 blocking condition이 있다. Writer는 다른 writer를 block하고, reader는 writer를 block한다. Writer는 recursive와 non-recursive reader를 모두 block한다. Reader는 다른 recursive reader를 block하지 않지만 함께 존재할 수 있는 writer waiter 때문에 non-recursive reader는 block할 수 있다.

표에서 Y는 row의 locker가 column의 locker를 block함을 뜻하고 N은 block하지 않음을 뜻한다.

Recursive read lock은 current write lock holder에게는 block되지만 write lock waiter만으로는 block되지 않는다. Task A가 read_lock(X)을 가진 상태에서 Task B가 write_lock(X)을 기다려도 Task A의 두 번째 recursive read_lock(X)은 기다릴 필요가 없다. 같은 operation이 non-recursive라면 B가 실제 lock을 얻지 못했더라도 waiter가 두 번째 read를 block해 deadlock이 된다.

하나의 lock instance도 어떤 acquisition function을 사용했는지, 더 정확히는 lock_acquire()의 read parameter 값에 따라 exclusive write lock, non-recursive read lock, recursive read lock 세 형태로 획득될 수 있다.

이후 설명에서는 write lock과 non-recursive read lock을 합쳐 non-recursive lock, recursive read lock을 recursive lock이라 부른다. Recursive lock끼리는 서로 block하지 않는다. Non-recursive lock끼리는 두 non-recursive read lock인 경우까지 서로 block한다. Non-recursive lock과 대응 recursive lock은 서로를 block할 수 있다.

Task A는 Task B가 Y를 read_unlock()하기를 기다리고 Task B는 Task A가 X를 read_unlock()하기를 기다리므로 둘 다 진행할 수 없다.

차단 행렬에서 writer는 W·r·R을 모두 막고, reader는 writer와 비재귀 reader를 막지만 재귀 reader는 막지 않습니다. 같은 잠금 인스턴스라도 어떤 acquisition API와 `lock_acquire()`의 `read` 값으로 잡았는지에 따라 세 역할 중 하나가 됩니다.

두 잠금 X와 Y에서 Task A가 X reader를 보유하고 Y writer를 기다리며 Task B가 Y reader를 보유하고 X writer를 기다리면 reader가 재귀 가능하더라도 원형 대기는 해소되지 않습니다. 재귀성은 같은 잠금의 reader 중첩을 허용할 뿐 서로 다른 잠금의 역순 획득을 안전하게 만들지 않습니다.

Condizioni bloccanti per lettori/scrittori su uno stesso blocco
---------------------------------------------------------------
Essenzialmente ci sono quattro condizioni bloccanti:

1. Uno scrittore blocca un altro scrittore.
2. Un lettore blocca uno scrittore.
3. Uno scrittore blocca sia i lettori ricorsivi che non ricorsivi.
4. Un lettore (ricorsivo o meno) non blocca altri lettori ricorsivi ma potrebbe
   bloccare quelli non ricorsivi (perché potrebbero esistere degli scrittori in
   attesa).

Di seguito le tabella delle condizioni bloccanti, Y (*Yes*) significa che il
tipo in riga blocca quello in colonna, mentre N l'opposto.

    +---+---+---+---+
    |   | W | r | R |
    +---+---+---+---+
    | W | Y | Y | Y |
    +---+---+---+---+
    | r | Y | Y | N |
    +---+---+---+---+
    | R | Y | Y | N |
    +---+---+---+---+

    (W: scrittori, r: lettori non ricorsivi, R: lettori ricorsivi)

Al contrario dei blocchi per lettori non ricorsivi, quelli ricorsivi vengono
trattenuti da chi trattiene il blocco di scrittura piuttosto che da chi ne
attende il rilascio. Per esempio::

	TASK A:			TASK B:

	read_lock(X);

				write_lock(X);

	read_lock(X);

non produce uno stallo per i lettori ricorsivi, in quanto il processo B rimane
in attesta del blocco X, mentre il secondo read_lock() non ha bisogno di
aspettare perché si tratta di un lettore ricorsivo. Tuttavia, se read_lock()
fosse un lettore non ricorsivo, questo codice produrrebbe uno stallo.

Da notare che in funzione dell'operazione di blocco usate per l'acquisizione (in
particolare il valore del parametro 'read' in lock_acquire()), un blocco può
essere di scrittura (blocco esclusivo), di lettura non ricorsivo (blocco
condiviso e non ricorsivo), o di lettura ricorsivo (blocco condiviso e
ricorsivo). In altre parole, per un'istanza di blocco esistono tre tipi di
acquisizione che dipendono dalla funzione di acquisizione usata: esclusiva, di
lettura non ricorsiva, e di lettura ricorsiva.

In breve, chiamiamo "non ricorsivi" blocchi di scrittura e quelli di lettura non
ricorsiva, mentre "ricorsivi" i blocchi di lettura ricorsivi.

I blocchi ricorsivi non si bloccano a vicenda, mentre quelli non ricorsivi sì
(anche in lettura). Un blocco di lettura non ricorsivi può bloccare uno
ricorsivo, e viceversa.

Il seguente esempio mostra uno stallo con blocchi ricorsivi::

	TASK A:			TASK B:

	read_lock(X);
				read_lock(Y);
	write_lock(Y);
				write_lock(X);

Il processo A attende che il processo B esegua read_unlock() so Y, mentre il
processo B attende che A esegua read_unlock() su X.

의존성 간선과 strong path

Lock dependency는 두 lock의 획득 순서를 기록한다. Locker가 세 종류이므로 이론상 dependency는 아홉 종류지만 deadlock detection에는 네 종류면 충분함을 보일 수 있다.

L1 -> L2는 같은 runtime context에서 L1을 보유한 뒤 L2를 획득한 이력을 lockdep이 봤다는 뜻이다. Deadlock detection에서 필요한 것은 L1을 보유한 상태로 L2에서 block될 수 있는지다. 즉 L1이 무엇을 block하는지와 무엇이 L2를 block하는지만 중요하다.

따라서 L1 쪽에서는 recursive reader와 non-recursive reader가 같은 type을 block하므로 합칠 수 있다. L2 쪽에서는 writer와 non-recursive reader가 같은 type에게 block되므로 합칠 수 있다.

두 lock 사이에는 dependency가 여러 개 있을 수 있다. Task A가 read_lock(X) 뒤 write_lock(Y)을 획득하고 Task B가 write_lock(X) 뒤 write_lock(Y)을 획득했다면 graph에는 X -(SN)-> Y와 X -(EN)-> Y가 모두 존재한다.

TASK A:
read_lock(X);
write_lock(Y);

TASK B:
write_lock(X);
write_lock(Y);

-(xN)->은 -(EN)-> 또는 -(SN)-> edge를 뜻한다. 같은 방식으로 -(Ex)->, -(xR)->, -(Sx)-> 표기를 사용한다.

Path는 graph에서 연속으로 이어진 dependency edge의 series다. Strong path는 path의 어떤 인접한 두 edge도 -(xR)-> 다음 -(Sx)-> 조합이 아닌 path로 정의한다.

다르게 말하면 X -> Y -> Z가 path에 있고 X에서 Y로 이동한 edge가 -(SR)-> 또는 -(ER)->라면 Y에서 Z로 이동하는 edge는 -(SN)-> 또는 -(SR)->일 수 없다. 다음 절에서 이 조건이 왜 strong이라 불리는지 증명한다.

세 locker 유형의 조합은 아홉 가지지만 교착 판정에는 출발점이 exclusive인지 shared인지와 도착점이 recursive인지 non-recursive인지의 네 간선 `ER`, `EN`, `SR`, `SN`이면 충분합니다. 같은 두 클래스 사이에도 실행 경로에 따라 여러 종류의 간선이 동시에 존재할 수 있습니다.

strong path는 인접 간선 사이에 ‘도착점이 recursive인 간선’과 ‘다음 출발점이 shared인 간선’의 완화 조합이 나타나지 않는 경로입니다. 즉 경로의 각 중간 잠금에서 앞 실행자는 다음 실행자의 보유 형태 때문에 실제로 차단될 수 있어야 합니다.

Tipi di dipendenze e percorsi forti
-----------------------------------
Le dipendenze fra blocchi tracciano l'ordine con cui una coppia di blocchi viene
acquisita, e perché vi sono 3 tipi di bloccatori, allora avremo 9 tipi di
dipendenze. Tuttavia, vi mostreremo che 4 sono sufficienti per individuare gli
stalli.

Per ogni dipendenza fra blocchi avremo::

  L1 -> L2

Questo significa che lockdep ha visto acquisire L1 prima di L2 nello stesso
contesto di esecuzione. Per quanto riguarda l'individuazione degli stalli, ci
interessa sapere se possiamo rimanere bloccati da L2 mentre L1 viene trattenuto.
In altre parole, vogliamo sapere se esiste un bloccatore L3 che viene bloccato
da L1 e un L2 che viene bloccato da L3. Dunque, siamo interessati a (1) quello
che L1 blocca e (2) quello che blocca L2. Di conseguenza, possiamo combinare
lettori ricorsivi e non per L1 (perché bloccano gli stessi tipi) e possiamo
combinare scrittori e lettori non ricorsivi per L2 (perché vengono bloccati
dagli stessi tipi).

Con questa semplificazione, possiamo dedurre che ci sono 4 tipi di rami nel
grafo delle dipendenze di lockdep:

1) -(ER)->:
            dipendenza da scrittore esclusivo a lettore ricorsivo. "X -(ER)-> Y"
            significa X -> Y, dove X è uno scrittore e Y un lettore ricorsivo.

2) -(EN)->:
            dipendenza da scrittore esclusivo a bloccatore non ricorsivo.
            "X -(EN)->" significa X-> Y, dove X è uno scrittore e Y può essere
            o uno scrittore o un lettore non ricorsivo.

3) -(SR)->:
            dipendenza da lettore condiviso a lettore ricorsivo. "X -(SR)->"
            significa X -> Y, dove X è un lettore (ricorsivo o meno) e Y è un
            lettore ricorsivo.

4) -(SN)->:
            dipendenza da lettore condiviso a bloccatore non ricorsivo.
            "X -(SN)-> Y" significa X -> Y , dove X è un lettore (ricorsivo
            o meno) e Y può essere o uno scrittore o un lettore non ricorsivo.

Da notare che presi due blocchi, questi potrebbero avere più dipendenza fra di
loro. Per esempio::

	TASK A:

	read_lock(X);
	write_lock(Y);
	...

	TASK B:

	write_lock(X);
	write_lock(Y);

Nel grafo delle dipendenze avremo sia X -(SN)-> Y che X -(EN)-> Y.

Usiamo -(xN)-> per rappresentare i rami sia per -(EN)-> che -(SN)->, allo stesso
modo -(Ex)->, -(xR)-> e -(Sx)->

Un "percorso" in un grafo è una serie di nodi e degli archi che li congiungono.
Definiamo un percorso "forte", come il percorso che non ha archi (dipendenze) di
tipo -(xR)-> e -(Sx)->. In altre parole, un percorso "forte" è un percorso da un
blocco ad un altro attraverso le varie dipendenze, e se sul percorso abbiamo X
-> Y -> Z (dove X, Y, e Z sono blocchi), e da X a Y si ha una dipendenza -(SR)->
o -(ER)->, allora fra Y e Z non deve esserci una dipendenza -(SN)-> o -(SR)->.

Nella prossima sezione vedremo perché definiamo questo percorso "forte".

재귀 reader 교착과 strong cycle

두 lemma를 증명한다. Lemma 1은 closed strong path, 즉 strong circle이 있으면 deadlock을 만드는 locking sequence 조합이 존재한다는 명제다. Strong circle은 deadlock detection의 충분조건이다.

Lemma 2는 closed strong path가 없으면 deadlock을 만들 수 있는 locking sequence 조합도 없다는 명제다. Strong circle은 deadlock detection의 필요조건이다.

두 lemma를 합치면 closed strong path는 deadlock의 필요충분조건이고 deadlock 가능성과 동치다. Deadlock을 만들지 않는 dependency circle도 있으므로, deadlock 가능한 chain을 구별해 strong이라 부른다.

충분조건 증명: strong circle이면 deadlock을 구성할 수 있다

L1 -> L2 -> ... -> Ln -> L1인 strong circle이 있다고 하자. 이는 L1 -> L2, L2 -> L3, ..., Ln-1 -> Ln, Ln -> L1 dependency가 있다는 뜻이다.

먼저 한 CPU 또는 task가 L1 -> L2에서 L1을 획득하게 하고, 다른 CPU 또는 task가 L2 -> L3에서 L2를 획득하게 하는 식으로 배치한다. 그러면 Lx -> Lx+1의 모든 Lx를 서로 다른 CPU 또는 task가 보유한다.

L1 holder가 L2 획득을 시도할 때 L2는 이미 다른 CPU 또는 task가 보유한다. Strong 정의 때문에 L1 -> L2와 L2 -> L3는 -(xR)-> 뒤 -(Sx)-> 조합이 아니다. 즉 앞 dependency의 L2가 누구에게나 block되는 non-recursive locker이거나 뒤 dependency의 L2가 누구든 block하는 writer다. 따라서 L1 holder는 L2를 얻지 못하고 L2 holder의 release를 기다린다.

같은 결론을 이어가면 L2 holder는 L3 holder를 기다리고 모든 Lx holder는 Lx+1 holder를 기다린다. Ln+1은 L1이므로 circular waiting이 완성되고 누구도 진행하지 못해 deadlock이 된다.

필요조건 증명: deadlock이면 strong circle이 존재한다

Lemma 2는 deadlock scenario가 있다면 dependency graph에 반드시 strong circle이 있다는 명제와 동치다.

Deadlock에는 circular waiting이 존재한다. N개의 CPU 또는 task P1...Pn이 있고 P1은 P2가 보유한 lock을, P2는 P3가 보유한 lock을 기다리며, 마지막 Pn은 P1이 보유한 lock을 기다린다.

Px가 기다리는 lock을 Lx라 하자. P1은 Ln을 보유하면서 L1을 기다리므로 dependency graph에 Ln -> L1이 있다. 같은 방식으로 L1 -> L2, L2 -> L3, ..., Ln-1 -> Ln이 있어 Ln -> L1 -> L2 -> ... -> Ln circle이 만들어진다.

각 Lx에서 Px는 Lx-1 -> Lx dependency를 만들고 Px+1은 Lx -> Lx+1 dependency를 만든다. Px가 Px+1의 Lx release를 실제로 기다리므로 Px+1 쪽 Lx가 reader이고 Px 쪽 Lx가 recursive reader인 조합은 불가능하다. Recursive 여부와 상관없이 reader는 recursive reader를 block하지 않기 때문이다.

따라서 Lx-1 -> Lx와 Lx -> Lx+1은 -(xR)-> 뒤 -(Sx)-> pair일 수 없다. Circle의 모든 lock에 같은 사실이 성립하므로 이 circle은 strong이다.

충분성 증명은 strong cycle `L1 -> L2 -> ... -> Ln -> L1`의 각 Li를 서로 다른 실행 주체가 먼저 보유하게 구성합니다. strong 조건 때문에 Li를 가진 주체는 Li+1의 보유자에게 실제로 막히며 마지막 Ln의 대기는 다시 L1로 돌아와 어느 주체도 진행할 수 없습니다.

필요성 증명은 실제 교착에 반드시 원형 대기 P1...Pn이 있다는 사실에서 시작합니다. 각 Px가 기다리는 잠금을 Lx라 두면 의존성 그래프에 `Ln -> L1 -> ... -> Ln`이 생기고, 실제로 서로 차단 중이므로 완화되는 reader 조합이 들어갈 수 없어 그 순환은 strong cycle입니다.

Identificazione di stalli da lettura ricorsiva
----------------------------------------------
Ora vogliamo dimostrare altre due cose:

Lemma 1:

Se esiste un percorso chiuso forte (ciclo forte), allora esiste anche una
combinazione di sequenze di blocchi che causa uno stallo. In altre parole,
l'esistenza di un ciclo forte è sufficiente alla scoperta di uno stallo.

Lemma 2:

Se non esiste un percorso chiuso forte (ciclo forte), allora non esiste una
combinazione di sequenze di blocchi che causino uno stallo. In altre parole, i
cicli forti sono necessari alla rilevazione degli stallo.

Con questi due lemmi possiamo facilmente affermare che un percorso chiuso forte
è sia sufficiente che necessario per avere gli stalli, dunque averli equivale
alla possibilità di imbattersi concretamente in uno stallo. Un percorso chiuso
forte significa che può causare stalli, per questo lo definiamo "forte", ma ci
sono anche cicli di dipendenze che non causeranno stalli.

Dimostrazione di sufficienza (lemma 1):

Immaginiamo d'avere un ciclo forte::

    L1 -> L2 ... -> Ln -> L1

Questo significa che abbiamo le seguenti dipendenze::

    L1   -> L2
    L2   -> L3
    ...
    Ln-1 -> Ln
    Ln   -> L1

Ora possiamo costruire una combinazione di sequenze di blocchi che causano lo
stallo.

Per prima cosa facciamo sì che un processo/processore prenda L1 in L1 -> L2, poi
un altro prende L2 in L2 -> L3, e così via. Alla fine, tutti i Lx in Lx -> Lx+1
saranno trattenuti da processi/processori diversi.

Poi visto che abbiamo L1 -> L2, chi trattiene L1 vorrà acquisire L2 in L1 -> L2,
ma prima dovrà attendere che venga rilasciato da chi lo trattiene. Questo perché
L2 è già trattenuto da un altro processo/processore, ed in più L1 -> L2 e L2 ->
L3 non sono -(xR)-> né -(Sx)-> (la definizione di forte). Questo significa che L2
in L1 -> L2 non è un bloccatore non ricorsivo (bloccabile da chiunque), e L2 in
L2 -> L3 non è uno scrittore (che blocca chiunque).

In aggiunta, possiamo trarre una simile conclusione per chi sta trattenendo L2:
deve aspettare che L3 venga rilasciato, e così via. Ora possiamo dimostrare che
chi trattiene Lx deve aspettare che Lx+1 venga rilasciato. Notiamo che Ln+1 è
L1, dunque si è creato un ciclo dal quale non possiamo uscire, quindi si ha uno
stallo.

Dimostrazione della necessità (lemma 2):

Questo lemma equivale a dire che: se siamo in uno scenario di stallo, allora
deve esiste un ciclo forte nel grafo delle dipendenze.

Secondo Wikipedia[1], se c'è uno stallo, allora deve esserci un ciclo di attese,
ovvero ci sono N processi/processori dove P1 aspetta un blocco trattenuto da P2,
e P2 ne aspetta uno trattenuto da P3, ... e Pn attende che il blocco P1 venga
rilasciato. Chiamiamo Lx il blocco che attende Px, quindi P1 aspetta L1 e
trattiene Ln. Quindi avremo Ln -> L1 nel grafo delle dipendenze. Similarmente,
nel grafo delle dipendenze avremo L1 -> L2, L2 -> L3, ..., Ln-1 -> Ln, il che
significa che abbiamo un ciclo::

	Ln -> L1 -> L2 -> ... -> Ln

, ed ora dimostriamo d'avere un ciclo forte.

Per un blocco Lx, il processo Px contribuisce alla dipendenza Lx-1 -> Lx e Px+1
contribuisce a quella Lx -> Lx+1. Visto che Px aspetta che Px+1 rilasci Lx, sarà
impossibile che Lx in Px+1 sia un lettore e che Lx in Px sia un lettore
ricorsivo. Questo perché i lettori (ricorsivi o meno) non bloccano lettori
ricorsivi. Dunque, Lx-1 -> Lx e Lx -> Lx+1 non possono essere una coppia di
-(xR)-> -(Sx)->. Questo è vero per ogni ciclo, dunque, questo è un ciclo forte.

참고 자료

• Deadlockhttps://en.wikipedia.org/wiki/Deadlock

Shibu, K. (2009). Intro To Embedded Systems (1st ed.). Tata McGraw-Hill.

이탈리아어 원문은 교착의 원형 대기 개념을 설명하는 이탈리아어 Wikipedia 항목과 K. Shibu의 임베디드 시스템 입문서를 참고 자료로 제시합니다.

Riferimenti
-----------

[1]: https://it.wikipedia.org/wiki/Stallo_(informatica)

[2]: Shibu, K. (2009). Intro To Embedded Systems (1st ed.). Tata McGraw-Hill