20160607

동시성 프로그램의 이해
– 실제 프로그램과 model checking language 사이에는 차이가 있다. 변환하는 과정에서 오류가 있다면? Model-based testing에서 실제 프로그램을 model checking language로 얼마나 정확하게 변환하느냐는 중요한 문제이다.
– Spin에서 statements를 atomic으로 묶으면 interleaving 없이 실행하게 된다. atomic block 중에 일부 statement가 block되면 atomicity를 잃게 된다(중요).
atomic.PNG
d_step을 사용해 여러 개의 statements를 indivisible step으로서 실행할 수 있다. d_step은 d_step block 내부의 statements는 모두 deterministic해야 하고, block되면 안 된다. atomic의 경우에는 atomic block 안에서 다른 곳에 메시지를 보낼 수 있고, 다른 곳에서 메시지를 받을 수도 있다. 그러면 atomicity는 깨지지만, 그 시점부터 계속해서 실행되게 된다. 하지만 d_step은 이를 허용하지 않는다.
d_step.PNG
– atomic, d_step의 차이점 (http://spinroot.com/spin/Man/d_step.html)

A d_step sequence is executed as if it were one single indivisible statement. It is comparable to an atomic sequence, but it differs from such sequences on the following three points:
* No goto jumps into or out of a d_step sequence are allowed.
* The sequence is executed deterministically. If non-determinism is present, it is resolved in a fixed and deterministic way, for instance, by always selecting the first true guard in every selection and repetition structure.
* It is an error if the execution of any statement inside the sequence can block. This means, for instance, that in most cases send and receive statements cannot be used inside d_step sequences.

atomic vs d_step.PNG

– atomic, d_step의 차이점을 그림으로 표현하면 다음과 같다. d_step의 중간 상태에서 밖으로 나갈 수도 없고, 밖에서 들어올 수도 없고, non-determinism도 허용하지 않는다. d_step을 사용하면 상태도 줄어들고, 가능한 transition도 줄어서 메모리 사용량이 크게 줄어들게 된다. 하지만 atomic, d_step의 남용은 테스팅의 효과성을 떨어뜨린다.

atomic_vs_d_step.PNG
– 두 개의 atomic block 중 하나는 sender, 다른 하나는 receiver일 때, sender는 atomicity를 잃지만 receiver는 atomicity를 잃지 않는다.
– “{guard1; } unless {guard2; }”를 사용해 예외 처리를 할 수 있다. unless 앞에 나오는 구문이 try, 뒤에 나오는 구문이 catch라고 생각하면 된다(Java에 비유).
– 테스팅할 때 fairness를 가정해주는 것도 중요하다. Model checking은 모든 가능한 interleaving scenario를 보여주지만, 실제로는 발생하지 않을 interleaving도 있다. 예를 들어, 다음과 같은 그림에서 한 개의 프로세스만 계속 실행될 수도 있다. 첫 번째 열만 계속해서 실행되는 경우. 하지만 스케쥴링은 공정하게 발생하므로, 그런 경우는 일어나지 않는다.
all possible scheduling.PNG
– Spin에서는 보장해주는 최소한의 fairness를 강제하는 weak fairness를 옵션으로 줄 수 있다.
weak fairness strong fairness.PNG
– Strong fairness는 한 번이라도 실행되는 상태는 반드시 프로세서를 사용할 수 있다. 하지만 Weak fairness는 충분히 긴 시간 실행되는 상태만 프로세서를 사용할 수 있다. Strong fairness의 state set이 weak fairness의 것보다 더 작다. Strong fairness가 만족되면 weak fairness가 만족됨.
다음 코드에서 proctype A는 infinitely long하게 실행되므로, weak fairness가 보장되면 반드시 실행됨.

int
active proctype A() {
x=10
}

하지만 다음 코드는 infinitely often하게 실행되므로, weak fairness 보장에서는 실행되지 않을 수 있음. strong fairness에서는 반드시 실행됨.

int
active proctype A() {
x==10 -> x++;
}

strong fairness weak fairness example.PNG
– 첫 번째 예제에서는 x=2, x=3이 한 개의 프로세스 안에 있으므로 fairness와 무관. 따라서 fairness가 있는지 없는지 무관하게 조건이 만족되지 않을 수 있음 (중요!). fairness는 한 개 이상의 프로세스에서만 적용된다.
– 두 번째 예제에서는 fairness가 없다면 조건이 만족되지 않을 수 있음. Weak fairness가 적용된다면 조건이 만족됨. 따라서 strong fairness가 적용되면 조건이 만족됨.
– 세 번째 예제에서는 B가 infinitely long하게 실행되지 않는다. Weak fairness가 적용되었을 때 조건이 만족되지 않을 수 있다.

– 병렬 프로그램을 정의할 때, 요구사항이 있고, 자연어로 된 요구사항을 표현할 프로그래밍 언어가 필요하다. LTL을 사용하면 다음과 같이 요구사항을 정의할 수 있다. G와 []는 always, F와 <>는 eventually이다. X 또는 O는 next이다. 이들을 temporal operator라 한다.
LTL examples.PNG

visualizing LTL formula.PNG
– 맨 마지막 formula는 만족하지 않음.
practical patterns of specification.PNG
– p – p – p – p 의 실행에서, weak until pUq는 만족하지만 strong until pUq는 만족하지 않는다. Strong until에서는 반드시 q가 등장해야 한다.

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

누적 방문자 수
  • 96,190 hits
%d bloggers like this: