/* ========================================================================
A MODEL OF THE FULL CHORD ROUTING PROTOCOL IN PROMELA AND C
Pamela Zave
Copyright AT&T Labs, Inc., 2012, 2013.
======================================================================== */
/* ========================================================================
This is a model of the "best" protocol as defined in the CCR paper. It is
derived from pseudocode and text in the Chord papers, as well as other
obvious fixes. It is not correct.
The atomicity of the join attempt is not implementable, but it does not
matter. In the worst case, a join fails when a member has acquired no data
and other members have acquired no pointers to it. In this situation, the
new member can retry the join without repercussions.
======================================================================== */
#define S 4
c_code {
\#include "chordbestccr.c"
}
int succ[S] = 9;
int prdc[S] = 9;
int succ2[S] = 9;
int x, y, z; /* used for passing arguments to C code */
inline joinAttempt(j,m) { /* assumes j is not a member and j != m */
if
:: succ[m] != 9 -> /* m must be a member */
x = m; y = j; z = succ[m]; /* checking between(m,j,succ[m]) */
if
:: c_expr{ between(now.x, now.y, now.z) } && succ[succ[m]] != 9 ->
succ[j] = succ[m];
succ2[j] = succ[succ[m]];
assert c_expr{ valid( now.succ, now.prdc, now.succ2) }
:: else
fi
:: else
fi
}
inline stabilize(s) { /* assumes s is a member */
int newSucc;
newSucc = prdc[succ[s]];
atomic {
if
:: newSucc != 9 -> /* s's successor must have a predecessor */
if
:: succ[newSucc] != 9 -> /* predecessor must be a member */
x = s; y = newSucc; z = succ[s];
if /* checking between(s,prdc[succ[s]],succ[s]) */
:: c_expr { between(now.x, now.y, now.z) } ->
succ[s] = newSucc;
if
:: succ2[s] != succ[newSucc] -> succ2[s] = succ[newSucc];
:: else
fi;
assert c_expr{ valid( now.succ, now.prdc, now.succ2) }
:: else
fi
:: else
fi
:: else
fi;
} /* end atomic */
}
inline notified(t,p) {
if
:: succ[t] != 9 -> /* notified t must be a member */
if
:: prdc[t] == 9 ->
prdc[t] = p;
assert c_expr{ valid( now.succ, now.prdc, now.succ2) }
:: prdc[t] != 9 ->
x = prdc[t]; y = p; z = t; /* checking between(prdc[t],p,t) */
if
:: c_expr{ between(now.x, now.y, now.z) } ->
prdc[t] = p;
assert c_expr{ valid( now.succ, now.prdc, now.succ2) }
:: else
fi
fi
:: else
fi
}
inline failAttempt(f) { /* assumes f is a member */
x = f;
if
:: c_expr { canFailNow( now.x, now.succ, now.prdc, now.succ2 ) } ->
succ[f] = 9; prdc[f] = 9; succ2[f] = 9;
assert c_expr{ valid( now.succ, now.prdc, now.succ2) }
:: else
fi
}
inline reconcile(r) {
if
:: succ[r] != 9 -> /* r must be a member */
if
:: succ[succ[r]] != 9 && succ2[r] != succ[succ[r]] ->
succ2[r] = succ[succ[r]];
assert c_expr{ valid( now.succ, now.prdc, now.succ2) }
:: else
fi
:: else
fi
}
inline update(u) { /* assumes u is a member */
if
:: succ[succ[u]] == 9 && succ2[u] != 9 ->
succ[u] = succ2[u]; succ2[u] = 9;
if
:: succ[succ[u]] != 9 && succ2[u] != succ[succ[u]] ->
succ2[u] = succ[succ[u]]
:: else
fi;
assert c_expr{ valid( now.succ, now.prdc, now.succ2) }
:: else
fi
}
inline flush(f) {
if
:: prdc[f] != 9 -> /* f must have a predecessor */
if
:: succ[prdc[f]] == 9 ->
prdc[f] = 9;
assert c_expr{ valid( now.succ, now.prdc, now.succ2) }
:: else
fi
:: else
fi
}
proctype node (byte n) {
if /* there must be an initial member; 2 is an "arbitrary" choice */
:: n == 2 ->
succ[n] = 2; assert c_expr{ valid( now.succ, now.prdc, now.succ2) }
:: else
fi;
do
:: succ[n] == 9 && n != 0 -> atomic { joinAttempt(n,0) }
:: succ[n] == 9 && n != 1 -> atomic { joinAttempt(n,1) }
:: succ[n] == 9 && n != 2 -> atomic { joinAttempt(n,2) }
:: succ[n] == 9 && n != 3 -> atomic { joinAttempt(n,3) }
:: succ[n] != 9 -> stabilize(n);
atomic { notified(succ[n],n) }
:: succ[n] != 9 -> atomic { failAttempt(n) }
/* can fail if and only if no node is left with no live successor */
:: succ[n] != 9 -> atomic { reconcile(n) }
:: succ[n] != 9 -> atomic { update(n) }
:: succ[n] != 9 -> atomic { flush(n) }
od;
}
init { atomic { run node(0);
run node(1);
run node(2);
run node(3)
} }
/* ========================================================================
======================================================================== */