20160614

동시성 프로그램의 이해
– 운영체제의 커널은 테스팅하기가 어렵다. 코드가 복잡하고, 멀티 쓰레드이며, 유닛 테스팅이 어렵고, 테스팅 툴이 부족하다. 유닛 테스팅을 하려면 해당 유닛이 실행되기 위한 환경을 제공해야 한다. 하지만 monolithic kernel에서 하나의 유닛만 떼어내기가 힘들다. 커널은 고성능이어야 하며, 정확해야 한다. 따라서 지금까지 커널 테스팅을 위해 printk를 사용하고 있다.
– Model checking을 사용하면 커널을 테스팅할 수 있다. 하지만 model checking은 실제 코드와 추상화된 모델 사이에 간극이 있다는 문제가 있다.

summary of MOKERT.PNG
– 프로그램을 자동으로 intrument하여 translation script를 만들어내고, 이를 통해 model을 만들어낸다(modex 활용). Translation script는 model을 구성하는데 참고는 되지만, 자동화가 되는 것은 아님. 사람의 도움이 필요하다. 이렇게 만든 모델을 사용해 프로그램이 올바른지 확인한다. Counter example이 발생하면, counter example이 발생하도록 instrument하여 해당 버그를 확인한다.
– 이렇게 구성한 model이 완벽히 원래의 소스 코드를 반영하지는 않지만, 아무것도 없는 것보다는 낫다. C의 제어문은 자동으로 Promela 코드로 변환되지만, 그 외의 표현은 해당 표현에 맞는 Promela 코드를 테이블로 제시해주어야 한다.
– Model의 counter example이 발생한다고 해도, 이것이 실제로 소스 코드의 버그를 의미하지 않을 수 있다. Model이 틀릴 수 있기 때문이다.

case 1 data race proc directory.PNG
– 위 코드에서 directory entry를 읽는 도중에 해당 directory entry를 지우게 되면(context switch) 버그가 발생한다.

case 1 data race proc directory result.PNG

– 다음 코드에서는 counter example이 실제 커널에서는 발생하지 않는다. ext2_readdir과 ext2_rmdir이 실제로는 lock에 의해 각각 감싸여있기 때문이다. 이는 model이 실제 소스 코드를 제대로 반영하지 못하는 경우이다.

case 2 model refinement.PNG

Advertisements
Tagged with: , , , , ,
Posted in 1) Memo

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

누적 방문자 수
  • 98,786 hits
%d bloggers like this: