20160602

동시성 프로그램의 이해
– Spin에서 “active proctype inv() { assert( x== 0);}”는 모든 경우에 x==0임을 확인하는 코드이다.
– Spin에서는 메시지 채널을 사용해 프로세스 사이에 통신한다. Spin은 다양한 타입의 메시지 채널을 제공한다. Buffered, non-buffered, 다양한 메시지 타입, 다양한 메시지 처리 연산 등이 있다.
– 다음 코드에서 첫 번째 프로세스는 (0, 10), (1, 20)을 전송한다. 두 번째 프로세스는 (0,10)을 받고, 그 다음으로 (1, 20)을 받는다. ch?1, bt는 패턴이 일치하는 경우만 데이터를 받는다. 첫 번째 값이 1이어야만 bt가 받아짐.

chan ch1 = [2] of {bit, byte};
ch1!0,10;ch1!1,20
ch1?b,bt;ch?1,bt

operations on channels.PNG
– ch?[x,y]는 메시지를 받아오지 않고, polling만 한다. ch?<x,y>는 메시지를 메시지 큐에서 삭제하지 않고 복사해온다. ch!!x,y는 increasing order로 메시지를 전송한다. ch!3, ch!5, ch!1로 메시지로 보냈다면 메시지 큐에 sender – 1 – 5 – 3 – receiver 순서로 들어간다. ch!!3, ch!!5, ch!!1 연산으로 메시지를 보낸다면 메시지 큐에 sender – 5 – 3 – 1 – receiver 순서로 들어간다. ch?x로 메시지를 받아올 때 버퍼에 쌓인 순서대로 메시지를 받아온다. 하지만 ch??x는 메시지를 받아올 때 버퍼에서 랜덤하게 받아온다 (가능한 모든 경우를). 위 연산들을 사용할 때 유의해야 한다. 예상치 못한 부작용이 있을 수 있음.
– Model checking technique에서는 모든 가능한 경우를 보고자 함. 모든 가능한 상황을 만들고자 함. 모든 non-deterministic 선택에서 분기해서 모든 경우를 확인해보게 됨. 평행 세계라고 생각하면 됨. Model checking technique의 단점은 메모리 소모가 많다는 것.

faulty data transfer protocol.PNG
– 위 프로그램은 프로토콜을 Promela로 구현한 것. timeout은 모든 프로세스가 block되었을 때 호출됨. 위 코드에서 데이터를 받았을 때 간단하게 W?data->skip을 하는데, 추상화된 프로토콜을 테스팅하는 것이 목적이기 때문에 자세한 구현은 하지 않는다.
– 위 코드에는 deadlock이 있다. M?data->W!data에서 데이터를 보내면 W?data->skip에서 데이터를 보낸다. 하지만 그 다음으로 Wproc()은 데이터를 보내지 않는다. 따라서 Mproc()은 계속해서 대기한다. 마찬가지로 Wproc()도 계속해서 대기한다.

– 다음 Promela 코드에서 실행 결과 x는 1, 2, 3 중 무엇이 될 수도 있다. Promela 코드에서 if문은 조건에 따라 실행하기 위한 것이 아니라, non-determinism을 제공하기 위한 것.

if
::x=1;
::x=2;
::x=3;
fi

– Promela는 함수를 제공하지 않지만, proctype을 제공하므로 이를 함수처럼 사용할 수 있다. 채널을 사용해 인자값을 주고, 반환값을 받아올 수 있다. Eratosthenes의 체도 Promela로 구현할 수 있으며, 이 코드를 이해하면 대부분의 Promela 코드를 이해할 수 있다. “end:” 레이블은 해당 위치의 코드가 무한히 돌아도 괜찮다는 것을 표현하는 레이블이다. 그렇지 않으면 Spin에 의해 비정상적 상태로 탐지될 수 있다.

– 다음과 같은 코드를 사용해, 메시지가 받아지지 않았을 때 else 구문을 실행하도록 할 수 있다. 하지만 예상치 못한 문제가 발생할 수 있으므로 추천하지 않는다.

if
:: ch?msg1 -> …
:: ch?msg2 ->
:: else -> … /* use empty(ch) instead*/
fi

– 다음 코드에서는 if 가 조건 확인을 위해 사용됨. x==0이면 else는 spawning되지 않음.

/* necessity of else */
/* in C, if(x==0) y=10; */
if
:: x == 0 -> y = 10
:: else /* i.e., x != 0 */
fi

– Promela에서 goto와 break는 statement가 아니다. Promela의 모든 statement는 state transition을 일으킨다.
– Promela에서 inline 함수를 만들 수는 있지만, 반환값은 없다.
– 다음과 같은 방식으로 다차원 배열을 만들 수 있다.

typedef array {byte y[3];}
array x[2];
x[2].y[1] = 10;

– Promela는 다음과 같은 다양한 연산자를 지원한다. 특이한 점은 scoping rule을 깨고 remote reference를 지원한다는 것이다. 다른 프로세스의 변수를 참조할 수 있다. 메모리 사용량을 줄이기 위한 구현이다.

more usages of various operators.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

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