wwnr 모니터 | Linux 6.18.37

요약·해설과 원문, 전문 번역을 서로 분리했습니다. API 이름, symbol, source path는 원문 표기를 사용합니다.

1. 요약·해설

원문의 핵심 논리와 kernel programming 관점의 보충 설명입니다. 아래의 전문 번역과는 별도로 작성했습니다.

요약·해설

monitor_wwnr.rst:1-45

per-task wwnr 오토마톤과 TASK_UNINTERRUPTIBLE 설정 및 schedule 사이의 IRQ 반례, reactor 시험 목적을 설명합니다.

2. 영어 원문 전체

번역 기준이 된 Linux v6.18.37 원문입니다. 줄 번호는 이 버전의 파일 좌표입니다.

원문 전체 펼치기

1 Monitor wwnr

2 ============

4 - Name: wwrn - wakeup while not running

5 - Type: per-task deterministic automaton

6 - Author: Daniel Bristot de Oliveira <[email protected]>

8 Description

9 -----------

11 This is a per-task sample monitor, with the following

12 definition::

14 |

15 |

16 v

17 wakeup +-------------+

18 +--------- | |

19 | | not_running |

20 +--------> | | <+

21 +-------------+ |

22 | |

23 | switch_in | switch_out

24 v |

25 +-------------+ |

26 | running | -+

27 +-------------+

29 This model is broken, the reason is that a task can be running

30 in the processor without being set as RUNNABLE. Think about a

31 task about to sleep::

33 1: set_current_state(TASK_UNINTERRUPTIBLE);

34 2: schedule();

36 And then imagine an IRQ happening in between the lines one and two,

37 waking the task up. BOOM, the wakeup will happen while the task is

38 running.

40 - Why do we need this model, so?

41 - To test the reactors.

43 Specification

44 -------------

45 Grapviz Dot file in tools/verification/models/wwnr.dot

3. 한국어 전문 번역

영어 원문의 문단 순서와 의미를 유지한 전체 번역입니다. 코드, 함수명, symbol과 URL은 원문 표기를 유지합니다.

설명과 상태 전이

1-28

`wwnr` 문서의 Name 줄에는 `wwrn - wakeup while not running`이라고 적혀 있다. Daniel Bristot de Oliveira가 작성한 per-task 결정적 오토마톤 예제이며, 원문의 이름 철자는 원문 보존 영역에 그대로 둔다.

wwnr 상태 전이

startnot_running (initial)

wakeupnot_running self-loop

switch_inrunning

switch_outnot_running

원문의 ASCII 오토마톤을 초기 상태와 세 event의 방향이 드러나도록 다시 구성했다.

wwnr 오토마톤

현재 stateevent다음 state

`not_running``wakeup``not_running`

`not_running``switch_in``running`

`running``switch_out``not_running`

task별 실행 상태와 scheduling event의 전이를 정리한다.

Monitor wwnr
============

- Name: wwrn - wakeup while not running
- Type: per-task deterministic automaton
- Author: Daniel Bristot de Oliveira <[email protected]>

Description
-----------

This is a per-task sample monitor, with the following
definition::

               |
               |
               v
    wakeup   +-------------+
  +--------- |             |
  |          | not_running |
  +--------> |             | <+
             +-------------+  |
               |              |
               | switch_in    | switch_out
               v              |
             +-------------+  |
             |   running   | -+
             +-------------+

깨진 모델인 이유

29-42

이 모델은 task가 `RUNNABLE`로 설정되지 않은 채 processor에서 실행 중일 수 있다는 사실을 표현하지 못하므로 깨져 있다.

잠들려는 task가 먼저 `set_current_state(TASK_UNINTERRUPTIBLE);`를 실행하고 다음 줄에서 `schedule();`을 호출한다고 하자.

1:      set_current_state(TASK_UNINTERRUPTIBLE);
2:      schedule();

두 줄 사이에 IRQ가 발생해 task를 깨우면, task는 여전히 실행 중인데 wakeup이 일어난다. 이 반례 때문에 모델은 실제 kernel 동작을 올바르게 설명하지 못한다.

그럼에도 이 모델은 reactor를 시험하기 위해 필요하다.

wwnr 반례

TASK_UNINTERRUPTIBLE 설정아직 CPU에서 실행 중

IRQ 발생현재 task wakeup

schedule() 전running 상태에서 wakeup 관찰

모델 위반reactor 시험에 활용

state 설정과 실제 context switch 사이의 interrupt가 모델의 가정을 깨뜨린다.

This model is broken, the reason is that a task can be running
in the processor without being set as RUNNABLE. Think about a
task about to sleep::

  1:      set_current_state(TASK_UNINTERRUPTIBLE);
  2:      schedule();

And then imagine an IRQ happening in between the lines one and two,
waking the task up. BOOM, the wakeup will happen while the task is
running.

- Why do we need this model, so?
- To test the reactors.

명세 위치

43-45

Graphviz Dot 명세 파일은 `tools/verification/models/wwnr.dot`에 있다. 원문의 `Grapviz` 철자는 원문 보존 영역에 그대로 유지한다.

Specification
-------------
Grapviz Dot file in tools/verification/models/wwnr.dot