이 게시글은 크티스텔 바이어의 Principles of Model Checking을 학습한 내용을 정리한 것입니다.
소프트웨어 검증의 필요성
소프트웨어를 개발할 때, 30~50%의 비용은 소프트웨어를 테스트하는데 소모된다. 그만큼, 소프트웨어가 버그가 없는지 확인하는 과정은 제품을 출시함에 있어 매우 중요한 과정이다.
왜냐하면, 소프트웨어에서 버그는 빨리 찾을 수록 미래에 발생할 수 있는 어마어마한 비용을 절감할 수 있기 때문이다. 실제로 소프트웨어의 결함을 고치는데 사용되는 비용은 maintenance 과정에서 버그픽스가 이루어질 경우 design phase에서에 비하여 약 500배의 비용이 소모된다고 한다. 이러한 비용적 측면에서, 소프트웨어를 미리 철저하게 검증하는 과정이 중요함은 너무나 명실상부하다.
소프트웨어에서 발생하는 버그의 50%는 프로그래밍, 즉 코드를 작성하는 과정에서 발생한다. 그리고 이 중 15%만이 초기의 design stages에서 검출된다. 즉 나머지 대부분의 버그들은 testing과정에서 발견하게 되는 것이다. unit testing을 시작할 때, 1000개의 코드 라인 당 20개의 결함이 발견되는 것이 일반적이다. system testing 과정에서는 1000개의 코드 라인 당 6개, 그리고 실제 출시되는 소프트웨어에서는 1000개의 라인 당 1개의 결함이 발견되는 것이 보통이다.
소프트웨어에서 발생하는 에러의 특징은 특정한 모듈에 집중되어 있다는 점이다. 절반 정도의 모듈은 결함이 없고, 약 80%의 결함이 매우 작은 비중의 모듈에서 발생한다.(약 20%)
하드웨어 검증의 필요성
하드웨어 디자인에서 에러를 방지하는 것 또한 매우 중요하다.
하드웨어는 특성상 고객에게 배송된 이후 결함을 수정하기 매우 어려우며, 그 비용 또한 비싸다.
소프트웨어처럼 패치나 업데이트를 통해 결함 수정을 제공할 수 없기 때문이다.
그 예시로, 인텔의 Pentium II에서 발생한 결함 때문에 Intel은 $ 475 million의 손해를 입었다.
이러한 문제를 방지하기 위해, 일반적으로 하드웨어를 디자인하는데 있어 실제로 디자인하는 시간은 전체의 27% 정도이며, 나머지는 에러를 찾고 방지하는데 사용된다.
하드웨어를 검증하는 테크닉으로는 Emulation, simulation, 그리고 structural analysis가 존재한다.
Structural analysis는 synthesis, timing analysis, 그리고 equivalence checking이라는 테크닉으로 이루어진다.
Emulation은 테스팅의 일종으로, 회로에 일련의 자극을 제공하고 생성된 출력을 칩 사양에 규정된 예상 출력과 비교하는 방식으로 이루어진다. 하지만 모든 case를 사람이 예상하기는 쉽지 않기 때문에, 잠재적으로 발견하지 않은 오류가 존재할 수 있다.
Simulation을 사용하면, 해당 회로의 모델이 구축되고 시뮬레이션된다. 모델은 일반적으로 Verilog, VHDL과 같은 언어를 사용하여 구성된다. 이후 특정한 자극을 주어 chip model의 execution path를 조사하는 방식으로 이루어진다. 이 자극은 인간에 의해 주어질수도 있고, 자동화된 수단에 의해 주어질 수 있다. 만약 시뮬레이터의 결과값과 specification에서 정의된 값이 다르다면, 에러가 존재한다는 것을 알 수 있다. 시뮬레이션은 테스팅과 매우 유사하지만, 이는 model에 적용된다는 점에서 다르다. 하지만 테스팅과 같이, 모든 케이스를 전부 확인하는 것은 불가능에 가깝다는 문제점을 가지고 있다.
Model Checking
앞서 언급한 것과 같이, construction에서 보다 더 많은 노력과 시간이 verificaiton에서 이루어진다.
따라서 자연스럽게 verification에 사용되는 노력을 줄이면서, coverage를 상승시키려는 노력이 계속되고 있다.
Formal methods는 design process에서 검증 과정을 초기 통합하여 더 효율적인 verification 기술을 제공하며, 시간을 단축시킨다.
쉽게말하면, formal methods는 ICT 시스템을 분석하는데 수학적인 모델을 적용하는 방식이다. 해당 방식의 목표는 수학적인 엄밀함을 통해 시스템의 정확성을 보장하는 것이다. 이 formal methods에 대한 연구는 매우 유망한 검증 기술의 발달로 이루어졌고, 자동으로 검증 과정을 수행하는 강력한 소프트웨어 tool과 결합되었다.
조사에 따르면, 해당 툴은 formal verification procedures는 Ariane-5 미사일, Mars Pathfinder, Intel의 Pentium II 등의 결함을 발견하였다.
Model checking이란 검증 기술 중 하나로, 시스템의 가능한 모든 states를 brute-force 방식으로 탐색하는 검증 방식이다. 이는 알고리즘과 데이터 구조의 개선, 그리고 컴퓨터 성능의 증가로 인해 점점 더 현실적이고, 큰 설계에 적용 가능해지고 있다.
Model checking을 통해 생성된 결과의 correctness, 데드락에 도달할 수 있는지의 여부 등을 확인할 수 있다. Model checking에서 검증 상황은 항상 정확하고 모호해야하지 않기 때문에, 이를 검증하는 과정은 informal documentation의 모호성과 모순점을 발견하는 단계가 되기도 한다.
Model Checking의 과정
Model Checking은 다음과 같은 과정으로 이루어진다.
Model phase
- 고려 중인 시스템을 모델 체커의 모델 설명 언어를 사용하여 모델링한다.
- 모델의 최초 타당성 검사와 빠른 평가를 위해 모델은 몇 가지 시뮬레이션을 수행한다.
- property specification language를 사용하여 property를 formalize한다.Running phase
- system model의 property를 검증하기 위하여 model checker를 실행한다.Analysis phase
- Property가 만족된 경우 -> 다음 propery를 체크한다.
- Propery가 만족되지 않은 경우(테스트가 실패한 경우) ->
- 반례를 simulation으로 분석한다.
- 모델, 디자인, propery를 refine한다.
- 전체 과정을 반복한다.
- out of memory인 경우 -> 모델을 reduce한 후 다시 시도한다.
이러한 step들에 더하여, 전체 검증 과정은 계획되어야하고, 감독되어야하며 조직되어야한다. 이를 verification organiztion이라고 한다.
Modeling
모델 검사에 필요한 input은 고려 중인 시스템의 모델과 체크될 property의 formal characterization이다.
system의 model은 정확하고, 모호하지 않은 방식으로 설명되며 일반적으로 유한 상태 오토마타를 사용하여 표현된다.
Model checking의 장점과 단점
Model checking의 장점
- Model checking은 굉장히 광범위하게 적용될 수 있는 검증 방식으로, 임베디드 시스템, 소프트웨어, 그리고 하드웨어 디자인에 적용될 수 있다.
- partial verification을 지원한다. 즉 properties들이 개별적으로 체크될 수 있다.
- 오류가 exposed될 가능성에 취약하지 않다.
- property가 invalidated된 경우 진단 정보를 제공한다.
Model checking의 단점
- 주로 제어 집중적인 프로그램에 적합하며, 데이터 집약적인 프로그램에는 적합하지 않다.(일반적으로 데이터는 무한한 domain을 범주로 하기 때문)
- infinite-state system이나 추상 데이터 타입에 대한 추론의 경우 model checking이 효과적으로 작동하지 않는다.
Concurrent System의 모델링
Transition System
특정 상태에서 다른 상태로의 전이를 모델링하는, 엣지가 있는 일종의 그래프 형태로 표현된다. 이는 시스템의 동작을 설명하는 모델로 주로 사용된다. 아래와 같은 요소들을 통해 정의될 수 있다.
아래와 같이 간단한 예시를 들 수 있다.
위 예시에서 space S = {pay, select, soda, beer}이 된다. 또한, initial state I={pay}임을 알 수 있다. 또한 Labeling function의 경우 L(pay) = ∅, L(soda) = L(beer) = {paid, drink}, L(select) = {paid}로 표현할 수 있다.
Direct Predecessors and Successors
TS = (S, Act, ->, I, AP, L)로 정의하면, 집합 S에 속하는 원소 s와 Act에 속하는 α에 대해 다음과 같이 정의할 수 있다.
Terminal State
Post(s) = ∅ 을 만족하는 state s에 대해 이를 terminal이라고 한다.
Deterministic Transition System
다음과 같이 정의된다.
즉, 시작 State가 1개 이하, 그리고 모든 state에 대하여 direct α- usccessors의 원소가 1개 이하인 경우가 Deterministic한 TS가 된다.
Executions
위에서 정의한 TS는 굉장히 직관적인 레벨에서의 정의였다. 이후부터는 execution(run)이라는 개념을 바탕으로 formalize 된 정의를 제공한다. Execution은 nondeterminism의 가능한 해결 방안을 모색하는 과정에서 도출되었다.
일반적으로 말하는 Execution of transition system은 initial, maximal execution fragment이다.
Execution Fragment
TS = (S, Act, ->, I, AP, L) 에 대하여, finite execution fragment는 state로 종료되는, state와 action의 반복되는 sequence로 정의된다.
n이 0 이상이면, 우리는 n을 execution frament의 길이라고 부른다. n이 유한하지 않은 경우, 우리는 이를 infinite execution fragment라고 한다.
당연하지만, infinite execution의 홀수 길이의 prefix들은 모두 finite execution이 된다.
이 fragment들은 다음과 같이 표현할 수 있다.
Maximal and Initial Execution Fragment
finite execution fragment 중 terminal state로 종료되는 경우, 그리고 대상이 infinite execution fragment인 경우 우리는 이를 maximal execution fragment라고 한다.
마찬가지로, fragment가 initial state로 시작되는 경우 우리는 이를 initial execution fragment라고 한다.
Reachable State
다음과 같은 조건을 만족하는 state에 대해 reachable하다고 한다.
Modeling Hardware and Software Systems
Sequential Hardware Circuits
input이 x, output이 y, 그리고 register r이 존재하는 circuit을 가정하자. control function for output variable y는 다음과 같이 주어진다.
circuit의 구조와 이를 바탕으로 구성한 transition system은 아래와 같다.
transition system TS = (S, Act, -> I, AP, L)은 sequential hardware circuit을 다음과 같이 모델링한다.
우선, state space S를 다음과 같이 정의한다.S = Eval(x1, .... xn, r1, .....rk)
여기서 Eval이란 input variable x의 evaluation과 register rj의 evaluation으로 나타내어지며, 이 집합은 { 0, 1 }n+k 집합과 동일하게 정의될 수 있다. 이 집합은 단순하게, x1...xn과 r1...rk가 각각 0 또는 1이 될 수 있기 때문에, 위와 같이 나타내어 지는 것이다. 처음 n개의 요소들은 input bit를 나타내는데, 임의로 지정된다는 특징이 있다. 따라서, set of inital state는 아래와 같이 정의된다.
여기서 c는 register의 값을 의미한다.
Data-Dependent System
data-dependant system의 executable action은 일반적으로 conditional-branching에 의해 이루어진다. 예를 들면 다음과 같다.
이러한 프로그램을 TS로 모델링 할 때, transition의 조건을 생략될 수 있으며, 조건 분기는 nondeterminism으로 대체될 수 있다. 하지만 일반적으로 이는 매우 추상적인 transition system을 결과로 가지게 되며, 매우 적은 소수의 properties 만이 검증될 수 있다. 그에 대한 대안으로, conditional transitions가 사용되며 resulting hraph가 transition system으로 unfold 될 수 있다.
Data-Dependent System의 예시
앞서 살펴보았던 음료 자판기를 떠올려보자. 우리는 이 자판기에 soda와 beer가 얼마나 남았는지 세는 기능을 추가했다고 가정 할 것이다. 그리고 이 자판기는 음료수가 남아있지 않은 경우, 코인을 다시 돌려주는 기능을 수행한다. 예시를 간단하게 설명하기 위하여 start와 select라는 두 가지의 location만이 존재한다고 가정한다. 이 때, conditional transition은 다음과 같이 정의할 수 있다.
Labels of conditional transition은 g : α 라는 형태로 이루어진다. 여기서 g는 Boolean condition이며, 알파는 action에 해당한다.
그러나 node로 표현된 locations와 conditional transitions로 표현된 edge로 구성된 graph는 transition system이 아니다. 왜냐하면 edge가 조건문으로 주어져있기 때문이다. 하지만 우리는 이 그래프를 'unfolding'하는 과정을 통해 transition system을 도출해낼 수 있다.
다음과 같은 proposition을 가정해보자.
x와 x'을 활용한 Boolean condition, 그리고 dom(y) = {red, green}에 해당하는 변수 y를 사용하여 Boolean condition을 만들었다. 여기서 dom(x)는 정의되지 않았는데, 임의의 수 일수도 있으며 set일 수도 있다.
Program graph는 digraph로, edge가 변수들에 대한 condition과 action으로 labeled 되어 존재한다. action의 effect는 다음과 같이 formalized 될 수 있다.
이는 변수의 evaluation이 action의 수행에 따라 어떻게 변화하는지를 가리킨다. 예를 들어, aciton이 x:=y+5와 같이 정의 될 경우, x의 evalution이 17이며 y의 evalution이 -2라고 가정하면 아래와 같다.
즉 Effect(α, n) 은 x에 3을, y에 -2를 assign하는 evaluation이 된다.
program graph에서 node는 locations라고 부르며, conditional transition이 가능하기 때문에 control function을 가지고 있다.
Progam Graph(PG)
program graph는 다음과 같은 tuple로 정의된다. (Loc, Act,Effect, →, Loc0, g0)
action은 Effect(α, ·)에 따라 변수의 evaluation 값을 변화시킨다. 만약 더 이상 transition이 불가능 할 경우, 시스템은 중단된다.
이 PG를 이전에 보았던 자판기 예시를 통해 살펴보자
set of variables는 다음과 같다. Var = {nsoda, nbeer}
각각의 변수의 domain은 {0,1, ..., max}로 정의하고, set Loc of locations는 {start, select}, Loc0 = {start}로 정의한다.
Effect는 다음과 같이 정의한다.
여기서 η[nsoda := nsoda−1] 는 η'(nsoda) = η(nsoda)−1 와 nsoda와 다른 모든 변수에 대해 η'(x) = η(x) 가 성립하는 η'의 shorthand에 해당한다. g0 = (nsoda = max ∧ nbeer = max ).이다.
이러한 정보를 활용해 transition system을 만드는 방법은 다음과 같다.
우선, control component로 구성되는 state는 location of the program graph, 그리고 evaluation η of variables로 구성된다. 따라서 staet는 <l, η> 라는 pair로 구성된다.
Initial state는 initial locations으로, initial condition g0를 만족한다.
program graph로 정의된 properties를 formulate하기 위하여, proposition의 set AP는 Loc에 속하는 l과 Boolean conditions for variables로 구성된다. 예를 들어, 다음과 같은 proposition이 존재한다고 가정한다.
이는 x, y는 정수형의 변수, 그리고 locations는 naturals로 formualted될 수 있다.
PG를 TS로 변환시키는 방법을 공식화 한 것은 아래와 같다.
여기서 분수 형태로 되어 있는 수식은 SOS-notation이라고 부르며, 윗 부분은 premise, 아래 부분은 conclustion을 의미한다.
Parallelism and Communication
위에서 simple suquential computer program을 transition system으로 변환하는 방식에 대해 살펴보았다. 하지만 실제로는 대부분의 하드웨어와 소프트웨어가 parallel로 작동한다. 따라서 우리는 parallel system에서 transition systems를 도출하기 위한 방법에 대해 살펴 볼 필요가 있다. 해당 테크닉에는 parallel로 작동하는 transition system 간 communication이 없는 간단한 경우와 message가 transferred될 수 있는 복잡한 경우까지 존재한다. 또한 이 메세지는 동기적일수도, 비동기적일 수도 있다.
TS = TS1 || TS2 || ... || TSn 라고 정의할 때, 우리의 목표는 ||를 새롭게 정의하는 것이다.
위 TS는 여러개의 transition system이 병렬적으로 작동하는 방식을 표현한 것이다.
우선, ||를 commutative와 associative로 정의하자. 참고로, 각각의 TSi들은 또 다른 TS들의 결합으로 이루어져 있을 수 있다.
Concurrency and Interleaving
interleaving은 parallel system에서 보편적으로 채용되는 패러다임이다. 이 모델에서, system은 set of independent components로 이루어진다. 이로인해 concurrency는 interleaving으로 표현되며 이는 nondeterministic choice이다.
P 와 Q라는 nonterminating processes가 존재한다고 하면, 아래와 같은 3개의 실행 예시를 들 수 있을 것이다.
concurrency의 interleaving 표현은 priori unknown 전략을 가지고 concurrently하게 동작하는 프로세스들을 연결하는 스케쥴러가 존재한다는 생각에 착안하여 이루어진다.
아래와 같은 예시를 통해 살펴보겠다.
신호등이 두개가 존재하며, 각각 빨간불과 초록불이 켜질 수 있다. 따라서 위와 같은 4개의 state가 존재할 수 있을 것이다. |||의 경우 interleaving operator를 의미한다.
위 interleaving의 justification에서 중요한 것은, 각각의 액션이 임의의 순서에 따라 연속적으로 작동할 때 effect와 액션이 identical하다는 것이다. 이는 수식으로 나타내면 다음과 같다.
이러한 사실은 두 개의 독립된 변수의 assignments 예시를 살펴보면 쉽게 이해할 수 있다.
x=0이고 y=7일 때, action 이후 x=1, y=5가 된다. 이는 assignments가 concurrently하게 진행되었는지, 혹은 일정한 순서에 따라 진행되었는지와 관계 없다.
이제, interleaving을 transition으로 어떻게 정의할 것인지의 문제가 남았다. 아래와 같이 정의할 수 있따.
Communication via Shared Variables
interleaving operator의 경우 각각의 processor가 서로와 독립된 작업을 비동기적으로 처리하는 경우 사용된다. 그러나 이러한 operator는 너무나 간소화 된 것으로, 대부분의 parallel system과 맞지 않는다.
위 예시에서 문제점은, actions α 와 β가 shared variable x에 접근하며 경쟁하고 있다는 사실이다. 하지만 transition system의 interleaving operator는 Cartesian product를 암묵적으로 수행한다. 따라서 local states가 x=6인지, x=4가 배타적인 이벤트로 존재하는지 식별할 방법이 없다.
shard variable을 가지는 parallel programs를 다루기 위해, 우리는 interleaving operator를 program graph 수준으로 정의할 필요가 있다(직접적으로 transition systems으로 하지 않고). interleaving program graphs of PG1 and PG2는 PG1|||PG2로 정의할 수 있다.
PG1와 PG2는 Var1와 Var2의 교집합을 shard variable로 가지며, 여집합을 각각의 local variable로 가진다.
실제로 PG1과 PG2를 정의한 후, 이를 transition system으로 나타낸 예시는 아래와 같다.
shared variable이 중요한 이유는, local variable과 달리 여러 program graph로 이루어진 PG의 action에 매우 큰 영향을 미치기 때문이다. 그래서 이런 program graph에서 shared variable에 영향을 미치는 action을 critical하다고 한다.
우리는 PG1과 PG2의 결합으로 이루어진 PG를 통해 얻은 TS(PG1|||PG2)에서 nondeterminism은 다음과 같은 의미를 가질 수 있다.
1. PG1과 PG2 내부의 nondeterminism
2. PG1와 PG2의 noncritical action의 interleaving
3. PG1와 PG2의 critical actions 간 경쟁의 결정(concurrency)
위 statement에서 effect를 정리하면 아래와 같다.
다음으로, 아래와 같이 정의된 PG1과 PG2가 있다고 가정해보자.
위 그래프는 bianry semaphore y를 공유하고 있다. y=0이라는 것은 critical section으로의 접근이 lock 되었음을 의미한다. 이해를 돕기 위해 y를 제외한 local variable과 shared variable은 없다고 가정한다. 또한, critical section의 내부와 외부에서 발생하는 activities가 없다고 가정한다.
location of PGi를 정의하면, noncrit_i, wait_i , crit_i의 세 가지가 존재할 것이다. 이는 각각 noncritial section, critical section으로 진입하기 위해 대기하는 상태, critical section을 의미한다.
PG1|||PG2로 정의된 program graph는 9개의 location을 가진다. 이는 의도하지 않은 상황인 <crit_1, crit_2> 도 포함한 것이다.
여기서 reachable한 state는 8개로, 아래와 같다.
따라서 transition system으로 변환하면 아래와 같다.
<w1, w2, y=1> state의 경우 두 process가 하나의 자원을 두고 경쟁하는 상황을 의미한다. 이를 해결하기 위해서는 다양한 스케줄링 전략이 적용될 수 있다.
이러한 상황에서의 대표적인 예시로, Peterson's Mutual Exclusion Algorithm을 들 수 있다.
위 예시에서, b1과 b2는 bool 타입 변수, x는 dom(x) = {1,2}인 변수이며 모두 shared variable이다. x는 어떤 프로세스가 critical section에 들어갈 수 있는지 결정하며, x=i이면 P_i가 임계 영역에 들어갈 수 있음을 의미한다. 프로세스 p1은 wait_1 location에 진입할 때 x:=2를 수행하여 p2가 critical section에 진입할 수 있도록 한다. 대칭적으로, p2는 wait를 시작할 때 x를 1로 설정하여 p1이 진입할 수 있게 한다. 변수 bi는 P_i가 어떤 location에 위치했는지에 대한 더 자세한 정보를 제공한다. 아래 그림을 통해 PG1, PG2의 동작 방식과 P1의 수도코드를 살펴볼 수 있다.
Peterson's mutual exclusion algorithm으로 구성한 Transition system은 아래와 같다.
위 프로그램에서, b1 :=true, x:=2와 b2:=true, x:=1은 쪼개질 수 없는 action, 즉 indivisible(atomic) action이다 이는 program text에서 barchkets < and >로 표현된다. 하지만 만약 b에 true를 할당하는 행위와 x에 값을 할당하는 행위가 순차적으로 이루어진다면, 이는 mutual exclusion을 보장하지 않는다. 아래 예시를 통해 살펴볼 수 있다.
여기서 req_i는 P_i가 x:= ... 와 b_i:= true의 중간 location에 위치하고 있음을 의미한다.
Handshaking
handshaking이란 interact하려는 concurrent process들이 이를 동기적인 방식으로 처리해야 함을 의미한다. 즉 프로세스들이 interact하려면 양쪽이 모두 같은 시간에 interaction에 참여해야 함을 의미한다.
hand shaking 기호는 H가 p1과 p2 액션의 교집합일 때, 언더바H를 생략하여 표기할 수 있다.
또한 handshake actions가 공집합인 경우, 이를 interleaving으로 대체하여 표기할 수 있다.
Handshaking은 commutative하지만, 일반적으로 associative하지 않다.
다만 모든 프로세스가 synchronize한 경우 associative하다.
아래와 같은 Booking System에서 handshaking에 대한 예시를 살펴볼 수 있다.
그림으로 나타낸 예시는 다음과 같다.
여기서 Arbiter란 handshaking 과정을 조절하기 위해 도입한 새로운 process로 binary semaphore와 유사한 기능을 한다.
Channel Systems
channel system이란 process들이 channel을 통해 communicate하는 parallel systems을 말한다.
FIFO인 버퍼를 통해 통신한다. 여기서는 폐쇄된 채널 시스템, 즉 외부가 아닌 내부의 프로세스들과 통신하는 모델을 가정한다.
다음과 같이 조건부 전이 또는 통신 동작 중 하나를 가진다.
c!v는 값 v를 버퍼 뒤에 넣으며 c?x는 버퍼의 앞부분에서 요소를 가져와 x에 할당한다.
채널에서의 communication action은 위와 같이 정의된다.
각 채널은 용량과 도메인을 가지며, c가 비트만 전송할 수 있는 채널인 경우 dom(c) ={0,1}이 된다. 채널에서 메세지를 전송하고 수신하는데는 지연시간이 존재하며, 동일한 메시지를 보내고 읽는 것은 반드시 다른 시점에서 발생하며 이를 비동기식 메시지 전달이라고 한다. 따라서 채널 시스템을 통해 동기식 및 비동기식 메시지 전달 모두를 모델링할 수 있다.
왼쪽의 기호는 conditional transition을 의미하는 것으로, 앞서 g:a와 같이 guard와 action의 조건문으로 전이를 표현한 것과 유사하다. 여기서는 communication actions로 labeling된다. 따라서 다음과 같다.
guard가 만족되었다고 가정하자,
만약 cap(c) = 0 이라면 P_i는 value v를 channel c로 전송할 것이다.
그리고 이 과정은 P_ j가 receive action을 제공할 수 있는 경우에만 가능하다.
이 경우, c!v와 c?x가 동시에 진행될 수 있다. 이 경우 P_i와 P_ j 의 메세지 통신이 발생하는 것이다.
주의할 점은, handshaking은 동기적인 목적으로 수행되는 것이지 data 통신을 위한 것이 아니다.
다음으로 비 동기 메세지 통신에 관해 살펴본다.
cap(c) > 0 이라고 가정할 때, P_i는 다음과 같은 conditional transition을 수행할 수 있다.
이후 p_ j 가 다음을 수행한다
다만 buffer of c 가 비어있지 않기 때문에, 맨 앞의 element v가 x에 할당된다(이는 atomic하게 진행된다) 이를 요약하면 아래와 같다.
Channel System을 활용한 Transition System Semantics는 다음과 같다.
여기서 채널의 evaluation은 '채널이 비어있다', '가득찼다'와 같은 값을 가질 수 있다.
NanoPromela
앞선 내용들은 reactive system을 모델링 하기 위한 수학적 기반에 해당한다. 그러나 이러한 시스템을 검증하기 위한 자동화된 도구를 구축하기 위해서는 분석 대상인 시스템의 동작을 지정하기 위한 더 간단한 형식을 도출해낼 수 있어야 한다. 또한 이러한 specification language는 비전문가도 사용할 수 있을 정도로 쉽게 간단해야하며 언어 명령의 의미를 모호하지 않게 나타내는 formal semantics가 필요하다.
이 섹션에서는 유명한 모델 체커 SPIN의 input language인 Promela에 대한 내용을 담고 있다. Promela는 shared variable을 통한 통신과 동기적 혹은 버퍼링된 FIFO 채널을 통한 메시지 전달을 지원한다. Promela의 formal semantics는 채널 시스템을 통해 제공되며, 이후 transition system으로 unfold 될 수 있다.
Promela는 'guared command language'를 사용하여 Process Pi의 단계별 동작을 지정한다. 이 언어는 고전적인 명령형 프로그래밍 언어의 여러 기능(변수 할당, 조건 부 및 반복 명령, 순차적 구성)을 포함하며, 프로세스가 채널로부터 메세지를 보내고 받을 수 있는 통신 동작 및 원하지 않는 interleaving을 방지하는 atomic regions을 포함한다. guared command는 PG와 채널 시스템의 엣지 레이블로 사용된다.
nanoPromela는 Promela의 기본 요소에 중점을 둔 fragment로, 변수 선언과 같은 세부 사항을 추상화하며 추상 데이터 유형(배열, 리스트)이나 동적 프로세스 생성과 같은 advanced 개념을 생략한다. nanoPromela 프로그램은 프로세스 P1...Pn의 단계별 동작을 나타내는 문장들과 프로그램 변수의 초기값에 대한 boolean condition으로 구성된다.
nanoPromela program은 다음과 같이 적을 수 있다.
프로세스 Pi의 단계별 동작을 형식화하는 문장의 주요 element는 atomic command 인 skip, 변수 할당 x:=expr, communication actions c?x 와 c!expr, conditional commands (if-then-else) 그리고 (while) 루프로 구성된다. 표준화된 if-then-else 구조나 while 루프 대신 nanoPromela는 nondeterministic한 decision을 지원하며 조건부 및 반복 명령에서 유한한 수의 guarded command를 지정할 수 있다.
nanoPromela의 프로그램 P의 변수는 타입(integer, Boolean, char, real)을 가질 수 있으며, Pi 프로세스의 전역 변수이거나 지역 변수일 수 있다. 채널에 대한 데이터 도메인을 지정해야하며 미리 정의된 용량의 동기적 또는 FIFO-채널로 선언되어야 한다. 우리는 P에 나타나는 변수의 집합을 Var로 가정하고 변수 이름 x에 대한 도메인을 dom(x) 집합으로 표기한다. 또한 Promela 프로그램 선언 부분에서 채널의 타입을 지정한다. 여기서는 간단히 채널 c의 유형( dom(c))와 용량 (cap(c))로 표기한다.
guard란 변수의 값에 대한 condition을 부과하는 Boolean Statement에 해당한다. 즉 가드는 변수 값의 조건으로 취급하며 Cond(Var)의 요소로 간주된다.
위 그림은 nanoPromela 프로세스의 동작을 지정하는 statement이다. 여기서 x는 Var내의 변수, expr은 식, 그리고 c는 임의의 용량을 갖는 채널을 의미한다. 할당 x:=expr에서 변수 x와 식 expr의 유형 일치가 필요하며 메시지 전달 동작 c?x및 c!expr에 대해 dom(c) ⊆ dom(x) 및 expr의 유형이 c의 도메인에 해당하는 것을 요구한다. if-then-else 문과 do-od 문의 g_i는 가드를 의미한다. 여기서 g_i ∈ Cond(Var) 라고 가정한다.
Command의 작관적 의미에 대해 formal semantics를 제공하기 전에 명령어의 의미에 대해 informal한 explanation을 살펴보면 다음과 같다.
skip은 변수의 값이나 채널의 내용에 영향을 주지 않고 한 단계에서 종료되는 프로세스를 나타낸다.
assignment의 의미는 말 그대로 값을 할당함을 의미한다.
stmt1; stmt2는 순차적인 구성을 나타내며, stmt1이 먼저 실행되고 종료되면 stmt2가 실행된다.
atomic region은 atomic{stmt} 형태의 statement를 통해 구현된다. atomic region은 stmt의 실행이 다른 프로세스의 활동과 interleaving되지 않는 atomic step으로 진행됨을 의미한다.
if-fi나 do-od로 구성된 문장은 표준 if-then-else와 while 루프의 일반화에 해당한다.
conditional commands의 직관적인 의미를 살펴보면 다음과 같다.
다음 문장을 예시로 한다. if :: g_1 ⇒ stmt_1 ... :: g_n ⇒ stmt_n fi
이 문장은 가드 gi가 현재 상태에서 만족되는 문장 stmt_i 사이에서의 nondeterministic 한 choice를 나타낸다. 우리는 guard의 evaluation, 가능한 가드 명령 사이의 선택 및 선택된 첫 번째 statement의 atomic한 실행을 atomic unit으로 실행하는 test-and-set semantics로 가정한다. Atomic unit으로 실행된다는 것은 concurrent porcesses들의 action이 interleaved될 수 없음을 의미한다.
만일 g_1, ... g_n중 어떠한 가드도 충족되지 않는다면 if-fi 명령과 while loop가 블록된다. 이러한 블록은 병렬로 실행되는 다른 프로세스들의 context에서 볼 수 있어서 다른 프로세스가 shared variable의 값을 변경하여 하나 이상의 가드가 최종적으로 true로 평가될 수 있는 상황에서 block이 해제될 수 있다. 예를 들어
위에서 y가 0이면 y에 0이 아닌 값을 다른 프로세스가 할당할 때까지 대기한다.
일반적인 명령형 프로그래밍 언어의 표준 if-then-else 명령인 "if g then stmt_1 else stmt_2 if"는 다음과 같이 얻을 수 있다.
반면 "if g then stem_t if"와 같은 else 옵션이 없는 문장은 다음과 같이 모델링 될 수 있다.
비슷한 방식으로 do-od- 명령은 while 루프를 일반화한다. 하나 이상의 가드가 충족될 때까지 본문을 반복적으로 실행함을 지정한다. 즉, 다음과 같은 형태의 문장이 된다.
guard g_i가 현재 구성에서 참인 경우에만 수행되는 guarded command gi=>stmt_i의 nondeterministic한 선택의 반복 실행을 나타낸다. conditional commands와 달리, 모든 가드가 위배된 경우 do-od 루프는 .state에서 block되지 않는다.
대신, 현재 상태에서 g1,....g_n이 성립하지 않는다면 while 루프는 중단된다. 실제로, 단일 가드 루프인 do :: g=> stmt od는 몸체가 stmt이고 종료 조건이 ¬g인 보통의 while 루프 "while g do stmt od"와 동일한 효과를 가진다. (Promela와 달리, loop는 break라는 명령으로 중단시킬 수 없다)
두 개의 프로세스에 대한 Peterson 상호 배제 알고리즘(45p)은 nanoPromela로 다음과 같이 표시될 수 있다.두 개의 Boolean variable b1, b2와 dom(x) = {1,2} 도메인을 갖는 변수 x와 crit1, crit2 두 개의 Boolean variable을 다룬다.프로세스의 noncritical section에서의 활동은 skip 동작으로 모델링 된다. critical section에서는 assignment crit_i := true를 사용한다. 초기 상태에서는 b1=b2=crit1=crit2=false이며 x는 임의의 값이다. 이후 P1의 nanoPromela 코드는 다음과 같이 주어진다.
두 번째 프로세스 모델링에 사용되는 문장도 유사하다.다만 요청동작은 b1 := true 와 x := 2의 두 가지 할당으로 나뉘는데 위에서는 이를 묶어 atomic하다고 가정했다. 그러나 atomic 영역을 제외한 경우, 상호 배제 속성을 보장하기 위해 b1:=true, x := 2의 순서를 사용해야 한다. 따라서 다음과 같다.
자판기 예제를 고려하여 nanoPromela 시스템의 동작을 살펴보면 다음과 같다.
시작 시점에는 두 옵션이 모두 활성화된다. 첫 번째 옵션은 사용자가 동전을 넣는 것으로, skip 명령으로 모델링된다. if-fi 명령의 첫 두 옵션은 사용자가 소다 혹은 맥주를 선택하는 경우를 나타내며, 각각 소다와 맥주가 자판기에 남아있어야 한다. if-fi의 하위 명령의 세 번째 가드 명령은 더 이상 소다나 맥주가 없는 경우를 의미하며 기계가 초기 상태로 돌아간다. 시작 위치에서 활성화 될 수 있는 두 번째 옵션은 소다와 맥주 병을 max로 채워 넣는 것이다.
Semantic 측면에서 변수와 채널을 가진 nanoPromela 문장의 opertional semantics는 Program Graph로 제공된다. 프로그램 P = [P1|....|Pn] 의 프로세스 P1,...P2에 대한 프로그램 그래프 PG1, .... PGn은 (Var, Chan) 상에서 채널 시스템을 형성한다. 그 후 채널 시스템에 대한 transition system sematics는 transition system TS(P)를 생성하며, P의 단계별 동작을 형식화한다.
nanoPromela의 문장 stmt와 관련된 프로그램 그래프는 stmt를 실행할 때의 제어 흐름을 형식화한다.
즉 하위 statement들은 location의 역할을 한다. termination을 모델링하기 위해 특별한 location인 exit가 도입된다.
대략적으로 어떤 가드 명령 g => stmt는 stmt의 첫 번째 동작을 나타내는 α에 대한 레이블 g:α를 가진 엣지에 해당한다. 예를 들어 다음과 같은 문장에 대해서,
cond cmd를 본다면 프로그램 그래프로서 두 개의 edge가 존재한다. 하나는 가드 x >1과 y= x+y 동작이 exit로 가는 것이며 다른 하나는 가드 true와 x :=0 동작이 y :=x 문장의 위치로 가는 것이다. y := x는 deterministic이므로 가드 true와 y : = x 동작이 exit로 가는 단일 엣지가 있음을 알 수 있다. 다음으로 반복문을 살펴보면,
여기서 do-od 루프는 본문이 실행된 후에 제어를 stmt로 돌리는 것으로 모델링 되어 있다. 따라서 loop에서는 세 개의 나가는 edge가 존재한다. 하나는 가드 x>1과 y := x+y동작이 loop 위치로 돌아가는 것이며, 두 번째는 가드 y<x와 x:=0 동작이 y := x; loop 문장의 위치로 가는 것이다. 세 번째 edge는 루프가 종료되는 경우를 다루며 가드 ¬(x > 1)∧ ¬(y<x)를 가지고 변수에 어떠한 영향도 주지 않는 동작이 exit location으로 lead하게 된다.
'개인학습' 카테고리의 다른 글
OAuth (0) | 2023.10.23 |
---|---|
MVC 패턴 (1) | 2023.09.14 |
Linear-time Temporal Logic guided Greybox Fuzzing 정리 (0) | 2023.09.05 |