[Maude] Token Ring 검증

 이 글에서는 Designing Reliables Distributes Systems, 225p에 있는 Token Ring을 maude를 사용해 formal modeling하고 원하는 검증을 진행합니다. 원 프로젝트는 RAFT consensus algorithm을 모델링하는 것이지만, 그 전에 손풀기 느낌으로 좀 더 쉬운 token ring을 모델링합니다.

 

 

 

Token Ring

 In the “token ring” mutual exclusion algorithm, the nodes logically form a “ring” structure, as shown in Figure 13.1 where a node only knows the next node in this ring.

 

 The algorithm works as follows: there is one “token,” and only the node that holds the token may enter its critical section. The node then holds on to the token during its execution in the critical section, and passes the token to the next node in the ring when it exits its critical section. If a node that is not waiting to enter its critical section receives the token, it just passes the token to the next node.

 

 

 

코드

--- module in textbook
mod MESSAGE-CONTENT is
    sort MsgContent . --- message content, application-specific
endm

omod MESSAGE-WRAPPER is
    including MESSAGE-CONTENT .
    op msg_from_to_ : MsgContent Oid Oid -> Msg [ctor] .
endom
---

omod OBJECT-TOKEN-RING is
    including MESSAGE-WRAPPER . --- object들 간의 message 처리

    class Node | state : MutexState, next : Oid . --- 각 Node : state와 next를 가짐.

    sort MutexState .
    ops normal waiting acquire : -> MutexState [ctor] . --- state 정의

    --- prev, current, next
    vars P C N : Oid .

    op token : -> MsgContent [ctor] .

    --- current node가 normal이면 waiting으로 변경
    rl [AccessRequest] :
            < C : Node | state : normal >
        =>  < C : Node | state : waiting > .

    --- message를 받았을 때 current node가 normal이면 다른 state로 바뀌지 않고, next node에게 전달
    rl [SkipToken] :
            (msg token from P to C)     < C : Node | state : normal, next : N >   
        =>  (msg token from C to N)     < N : Node | > .

    --- message를 받았을 때 current node가 waiting이면 acquire로 변경 (critical section에 진입)
    rl [Access] :
            (msg token from P to C)     < C : Node | state : waiting >   
        =>                              < C : Node | state : acquire > .

    --- critical section에서 나감
    --- current node state가 acquire에서 normal로 변경, next node로 message 전달
    rl [Release] :
            < C : Node | state : acquire, next : N >
        =>  < C : Node | state : normal >    (msg token from C to N) .
endom

omod OBJECT-TOKEN-INIT is
    including OBJECT-TOKEN-RING .

    ops a b c d : -> Oid [ctor] .
    op init : -> Configuration .
    
    eq init = (msg token from d to a) --- token이 전달된 상황
    < a : Node | state : normal, next : b >
    < b : Node | state : normal, next : c >
    < c : Node | state : normal, next : d >
    < d : Node | state : normal, next : a > .
endom

***(
    load ./object-token-ring.maude
    set trace on .
)

 

실행

 아래 명령어로 실행할 수 있습니다.

load ./object-token-ring.maude
set trace on .

 

 

 

검증

Normal State 검증

 아래 명령어는 특정 2개의 node의 state가 normal인 상태를 찾는 명령어입니다.

search [1] init =>* C:Configuration
    < O1:Oid : Node | state : normal, next : O1N:Oid >
    < O2:Oid : Node | state : normal, next : O2N:Oid > .

 

 실행 결과, Solution이 나옵니다. 즉, 2개의 node가 normal인 state가 존재함을 알 수 있습니다.

Solution 1 (state 10)
states: 11  rewrites: 11 in 0ms cpu (1ms real) (~ rewrites/second)
C:Configuration --> < c : Node | state : normal, next : d > < d : Node | state : normal, next : a >
O1:Oid --> b
O1N:Oid --> c
O2:Oid --> a
O2N:Oid --> b

 

 

Mutual Exclusion

 아래 명령어는 2개의 node가 acquire인 상태를 찾는 명령어입니다.

search [1] init =>* C:Configuration < C:Oid : Node | state : acquire > < C:Oid : Node | state : acquire > .

 

 실행 결과, No Solution이 나옵니다. 한 번에 2개 이상의 node가 acquire하는 state가 존재하지 않음을 알 수 있습니다.

No solution.
states: 432  rewrites: 865 in 120ms cpu (168ms real) (7208 rewrites/second)

 

 

Critical Section 진입

 아래 명령어는 특정 node의 state가 acquire이 되는 상태를 찾는 명령어입니다.

search [1] init =>* C:Configuration < C:Oid : Node | state : acquire, next : N:Oid > .
search [1] init =>* C:Configuration < a : Node | state : acquire, next : b > .
search [1] init =>* C:Configuration < b : Node | state : acquire, next : c > .
search [1] init =>* C:Configuration < c : Node | state : acquire, next : d > .
search [1] init =>* C:Configuration < d : Node | state : acquire, next : a > .

 

 실행 결과, solution이 나옵니다. 즉, node가 token을 acquire하는 state가 존재함을 알 수 있습니다.

Solution 1 (state 10)
states: 11  rewrites: 11 in 0ms cpu (1ms real) (~ rewrites/second)
C:Configuration --> < b : Node | state : normal, next : c > < c : Node | state : normal, next : d > < d : Node | state : normal, next : a >
C:Oid --> a
N:Oid --> b