20160531

동시성 프로그램의 이해
hierarchy of SW coverage criteria
– SW coverage criteria에서 가장 강력한 coverage인 complete value coverage(CVC)를 테스팅하는 것이 model checking 기법이다. Model checking 기법은 각 변수의 모든 가능한 값을 대상으로 프로그램을 검증한다. 매우 많은 프로그램 상태가 발생하고, 따라서 작은 프로그램도 model checking하기는 쉽지 않다. Model checking 기법은 큰 오버헤드를 유발하지만, 제약 조건을 준다면 가능한 상태의 수가 크게 줄어들게 된다.
overview of the spin architecture.PNG
– Model checking 도구에는 Spin이 있다. Promela로 쓰인 시스템 정의와 LTL로 정의된 요구사항을 Spin에 입력으로 주면,  Spin에 시스템 정의와 요구사항을 점검하는 소스 코드를 생성한다. 소스 코드를 빌드해 실행함으로써 요구사항을 위반하는 반례가 있는지 확인할 수 있다.
– Spin은 프로그램을 테스팅하기 위한 플랫폼이므로, 간단하게 프로그램 테스팅을 표현하는 것에 목표를 둔다(고성능이 목표가 아님). Promela는 C와 유사하지만, 포인터, 실수 타입, 함수가 없다. 프로세스들은 전역 변수, 메시지 채널을 사용해 통신한다. 여러 개의 쓰레드가 있을 때, Spin은 한 번에 한 개의 쓰레드를 실행하며 모든 interleaving을 탐색한다.

overview of the promela.PNG
– run 연산을 사용해 프로세스를 실행할 수 있다. 함수명 앞에 active[2]는 두 개의 같은 쓰레드를 생성함을 의미한다. 프로세스의 생성과 실행은 동시에 일어나지 않을 수 있음에 유의해야 한다. 한 개의 statement는 atomic하게 실행된다. statement 실행 중간에 interleaving이 발생하지는 않는다.
process creation example.PNG
– Promela는 long, float 등의 타입을 지원하지 않는다. 배열은 1차원 배열만 사용 가능하다. 2차원 배열을 사용하고 싶다면 record를 사용하면 된다.

variables and types.PNG

– Promela는 유한한 상태 모델만 지원한다. 프로세스는 최대 255개까지 생성 가능하다. 각 프로세스는 유한한 코드를 갖는다. 각 변수는 유한한 데이터 타입을 갖는다. 모든 메시지 채널은 255의 크기를 갖는다. 무한한 상태(실수)를 다루는 model checker도 있지만, Spin은 유한한 상태를 다룬다 (정수)

finite state model.PNG

– Promela의 statement는 현재 실행 가능하거나(executable) 실행 불가능하다(blocked). x+3>0;은 while(!(x+3>0)); 와 같다. 조금 더 간단히 설명해, 1;이라는 statement가 있으면 프로세스가 계속해서 실행될 수 있지만, 0;이라는 statement가 있으면 프로세스가 멈춘다. “active proctype inv() { assert( x== 0);}”를 사용하면 모든 경우에 x==0임을 확인한다. active는 프로세스를 생성하고, 그것이 실행되는 시점은 언제가 되어도 괜찮기 때문이다. 따라서 모든 경우에 x==0임을 확인할 수 있다.

basic statements.PNG

expression statements.PNG

– Promela는 goto, if, do 등을 사용할 수 있다. 그리고 non-deterministic selection도 지원한다. Verification을 위한 model checking에서는 프로그램 크기가 클 수 없다 (goto를 지원하는 이유?) Non-deterministic selection이란, if 문에 조건을 만족하는 statement가 여러 개 있을 때 non-deterministic하게 임의로 실행하는 것. do는 Promela에서 사용되는 while 루프이다. if 문이 있을 때 두 가지 조건을 모두 만족하지 않으면 프로세스는 실행되지 않고 멈춘다. 따라서 else문을 항상 써주는 것이 좋다.

program execution control.PNG
– spin -a 명령어를 사용해 process analyze 결과를 만들어낼 수 있다 (pan.c). 이렇게 만들어진 c 코드를 컴파일해 assertion이 위반되는지 확인하면 된다.
SPIN critical section example.PNG
– 위 예제에서 assertion violation이 발생하게 되는데, “!lock -> lock=true;”이 한 개의 statement가 아니기 때문에 발생한다. ->는 세미콜론과 같아서, 위 statement는 !lock과 lock=true의 조합이다.
– atomic을 사용하면 assertion violation이 발생하지 않는다. “atomic{!lock -> lock=true;}”
– assertion violation이 발생하는 경우에는 assertion violation이 발생할 때까지만 state를 생성하고 state transition한다. assertion violation이 발생하지 않는 경우에는 모든 state를 생성한다. 그럼에도 불구하고 assertion violation이 발생하지 않는 경우의 state 수가 더 적다. 그 이유는 atomic을 사용해 두 개의 상태를 묶었기 때문이다.
– 모든 statement를 atomic으로 묶는다면 state는 적게 생성되겠지만, 실제 프로그램을 제대로 반영하지 못한다는 문제점이 있음.
– Promela 코드에 deadlock이 있으면 Spin이 이를 탐지한다.
– Promela에서 timeout은 모든 코드가 실행되었을 때 실행된다. assert(0)가 없으면 Spin이 trail을 출력해주지 않음. 따라서 assert(0)를 사용.
– DXUSAFE는 send, receive를 하지 않음을 표현. -m은 몇 개의 step을 실행할 것인지 표현. -c는 몇 개의 violation을 찾을 때 멈출 것인지 결정 -c1은 한 개의 violation을 찾으면 멈추는 것. -c0는 violation을 찾아도 멈추지 않는 것. 일반적으로는 -c1 옵션을 주어, 한 개의 violation만 찾아도 멈추도록 한다.
– Spin에 대한 자세한 내용은 http://spinroot.com/spin/Man/index.html에서 확인할 수 있다.

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

누적 방문자 수
  • 103,571 hits
%d bloggers like this: