20160609

동시성 프로그램의 이해
review model checking.PNG
motivation for temporal logic.PNG
– Linear time temporal logic(LTL)은 시간을 상태의 무한한 연속으로 모델링한다(LTL models time as a sequence of states, extending infinitely into the future). LTL에서 x가 항상 2인 상태를 [](x==2)로 표현할 수 있다. LTL을 사용하지 않는다면 x==2@s0, x==2@s1, x==2@s2…와 같은 식으로 모델링해야 한다. LTL 식에서 단항 연산자가 먼저 결합하고, 그 외의 연산자들은 순서대로 결합한다.
– Model에서의 path는 상태의 무한한 연속으로 정의한다. 한 개의 프로그램 모델에서 무한하게 많은 state sequence가 발생할 수 있다. 그리고 각 sequence는 무한히 길다. 한 개의 state sequence pi를 볼 때, pi_i는 해당 sequence 내의 i번째 state에서 시작하는 path이다 (state i에서 실행하는 sequence가 아님!)
semantics of LTL.PNG
– Temporal operator가 없는 경우(위 슬라이드에서 Basic)에는 해당 실행 sequence 중에 첫 번째 상태(s1)만을 고려한다.

visualizing LTL formula
– 네 번째 sequence에서 pUq는 참이다. Sequence가 첫 상태가 pUq를 만족하기 때문
– 다섯 번째 sequence에서 <>(pUq)는 참이다. Sequence내에 pUq를 만족하는 경우가 있기 때문이다.
– 여섯 번째 sequence에서 [](pUq)는 거짓이다.

– (<>b1) -> (<>b2)를 사용해 correlation을 표현할 수 있다.
– sigma ㅑ [] p는 execution path sigma의 모든 상태가 p임을 의미한다. 한 개의 실행 경로만 보는 것. s0 ㅑ []p는 s0에서 시작하는 모든 path가 p임을 의미한다.

summary of practical patterns.PNG
– G F p는 p 상태가 일어나는 것이 항상 보장된다는 것. F G p는 임의의 시점 이후로 p가 되는 사건이 반드시 일어난다는 것.
– G (F p)는 여러 개의 formula로 분해할 수 있다. G (F p)인지 확인하려면 실행 sequence의 모든 상태에서 F p임을 확인하면 된다.
– F (G p)이면 F p이지만, F p라고 해서 F (G p)인 것은 아니다. q – q – q – p – q – p – p – p… 는 F(G p)이고, F p이다. 하지만 q – p – q – q – q … 는 F p만 만족한다.

– LTL을 사용해서 mutual exclusion을 모델링하고, 모델이 만족하거나 만족하지 않음을 확인할 수 있다. 우선 mutual exclusion의 요구사항은 다음과 같다.
mutual exclusion example.PNG
– 두 개의 프로세스의 상태를 다음과 같이 모델링할 수 있다. non-critical state n, trying to enter its critical state t, critical section c로 모델링한다.
1st model.PNG
– Safety, liveness를 만족함을 LTL로 확인할 수 있음. Non-blocking을 만족하지만 이는 CTL로 표현할 수 있음. 한 가지 문제는 한 프로세스가 critical section에 들어가지 못하고, 계속해서 대기하는 상태가 발생할 수 있다는 것이다.
1st model for mutual exclusion.PNG
– 상태를 다음과 같이 재정의하면 이 문제를 해결할 수 있다.
2nd model for mutual exclusion.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

누적 방문자 수
  • 88,534 hits
%d bloggers like this: