raft.pml

//
// Simplified model of the MongoDB Raft consensus algorithm in Promela.
//


// The number of servers.
#define N 3
#define Quorum 2

// State constraints.
#define maxTerm 3
#define maxLogLen 3

// Define constants to represent server states.
mtype {Secondary, Primary}

typedef Log{
    byte elems[maxLogLen]
    byte length = 0
}

//
// Global variables.
//
byte globalCurrentTerm = 0;
byte state[N];
Log slog[N] // the log of each server.

// The term of the last entry in a log, or -1 if empty.
#define LogTerm(lg) ((lg.length > 0) -> lg.elems[(lg.length-1)] : -1)

// Can i receive a log entry from j.
inline CanAppendLog(i, j){
    (state[i] == Secondary) &&
    (j != i) && // can't get log from yourself.
    (slog[j].length > 0) &&
    (slog[j].length > slog[i].length) && // their log must be longer than yours.
    (// if your log is empty, you can always sync logs.
     (slog[i].length == 0) ||
     // their log has the same entry as the one in your last log slot.
     (slog[j].elems[slog[i].length - 1] == slog[i].elems[slog[i].length - 1]));
}

// Can node i rollback entries against node j
inline CanRollbackOplog(i, j){
    (state[i] == Secondary) &&
    (j != i) && // can't rollback against yourself.
    (slog[j].length > 0) && 
    (slog[i].length > 0) &&
    // i's log is not a prefix of j's log.
    ((slog[i].length > slog[j].length) ||
     (slog[i].elems[(slog[i].length-1)] != slog[j].elems[(slog[i].length-1)])) &&
    // Last term of j's log is greater than i's
    LogTerm(slog[j]) > LogTerm(slog[i])
}

// Append an element to a log.
inline Append(lg, elem){
    lg.elems[lg.length] = elem;
    lg.length = lg.length + 1;
}

// Can server i vote for server j.
inline CanVoteFor(i, j){
    // Same log terms, but j is longer.
    ((LogTerm(slog[i]) == LogTerm(slog[j])) && 
     (slog[j].length >= slog[i].length)) ||
    // Different log terms, j has larger term.
    (LogTerm(slog[j]) > LogTerm(slog[i]));
}

// Set the states of all servers to the given state in a single atomic step.
inline SetAllStates(s){
    d_step{
        int inc;
        for(inc : 0 .. (N-1)){
            state[inc] = s;
        }
    }
}

inline printState(){
    int s, ind;
    printf("state: ");
    for(s : 0 .. (N-1)){
        // printf("servers: %e ", state[s]);
        printf("%e,", state[s]);
    }
    printf(" | ");
    for(s : 0 .. (N-1)){
        printf("s%d: [", s);
        for(ind : 0 .. (maxLogLen-1)){
        // printf("servers: %e ", state[s]);
            printf("%d,", slog[s].elems[ind]);
        }
        printf("], ", s);
    }
    printf("\n\n");
}

proctype ServerProcess(byte sid) {
    do
    // Select some arbitrary other server.
    ::  atomic {
        int other;
        select (other : 0 .. (N-1));
        skip;
        // assert (slog[0].length + slog[1].length + slog[2].length) < 9;
    if  
        // BecomePrimaryByMagic
        :: atomic {
            (state[sid] == Secondary && globalCurrentTerm < maxTerm) -> 

            // Check vote quorum.
            byte v, voters = 0;
            for(v : 0 .. (N-1)){
                if  
                :: CanVoteFor(v, sid) -> voters++;    
                :: else -> skip
                fi
            }

            // Become leader if eligible.
            if  
            :: (voters >= Quorum) ->
                d_step{
                    printf("BecomePrimaryByMagic(%d, term=%d)\n", sid, globalCurrentTerm + 1)
                    printState();
                    // Revert all other servers to secondary state and then become primary.
                    SetAllStates(Secondary)
                    state[sid] = Primary
                    globalCurrentTerm++;
                }
            :: else -> skip;
            fi
        }

        // AppendOplog
        :: d_step {
            CanAppendLog(sid, other) ->
            printf("AppendOplog(%d, from=%d)\n", sid, other);
            // Append one log entry.
            byte newEntry = slog[other].elems[slog[sid].length];
            Append(slog[sid], newEntry);
            printState();
        }

        // RollbackOplog
        :: d_step{
            CanRollbackOplog(sid, other) ->
            printf("RollbackOplog(%d, against=%d)\n", sid, other);
            // Roll back one entry.
            slog[sid].elems[(slog[sid].length - 1)] = 0;
            slog[sid].length = slog[sid].length - 1;
            printState()
            // assert false;
        }

        // ClientWrite
        :: d_step {
            (state[sid] == Primary && slog[sid].length < maxLogLen) ->
            printf("ClientWrite(%d, term=%d)\n", sid, globalCurrentTerm)
            slog[sid].elems[slog[sid].length] = globalCurrentTerm
            slog[sid].length = slog[sid].length + 1 // append to your own log.
            printState();
        }

        // RollbackOplog
        // TODO.

        // Continue if no branches were executable.
        :: else -> skip
    fi;
    } // make the entire switch statement atomic.
    od
}

init {
    // Initialize server state and start each process.
    atomic{
        SetAllStates(Secondary);
        int i;
        for(i : 0 .. (N-1)){
            run ServerProcess(i);
        }
    }
}