Nuprl Definition : Paxos-spec9-body

Paxos-spec9-body(es;T;f;acceptors;leaders;Input;...;...;...;...;...;...;...) ==
((((||acceptors|| = ((2 * f) + 1))

(0 < ||leaders||))

no_repeats(Id;acceptors)

(||filter(

a.deq-member(IdDeq;a;failset);acceptors)||

f))

(

(tag1a = tag2a)))

let 1a = restricted-baseclass(acceptors;[tagpaxos; tag1a];Id

;p.0

(snd(p))) in
let 1b = restricted-baseclass(acceptors;[tagpaxos; tag1b];Id

(?

T);q.(0

(snd(fst(q))))

((

isl(snd(q)))

(0

(fst(outl(snd(q))))))) in
let 2a = restricted-baseclass(acceptors;[tagpaxos; tag2a];Id

T;q.0

(fst(snd(q)))) in
let 2b = restricted-baseclass(acceptors;[tagpaxos; tag2b];Id

;q.0

(fst(snd(q)))) in
     let Collect = Collect(f + 1 vs's from 1b
                            with maximum num= fst(vs)
                            return <num,n,outl(vs).2> for which
                            n=outl(snd(vs)).1 is maximum
                            or <num,-1,prior Input> if all isr(snd(vs)))) in
     let Proposal =

tr.let b,b',v = tr in
if b' <z b then inl <b, v> else inr

fi [Collect] in
let NoProposal =

tr.let b,b',v = tr in
if b

z b' then inl b else inr

fi [Collect] in
let MaxReserve = es-interface-accum(

mx,x.imax(mx;x);0;1a) in
     let AcceptOrReject = (let bv,m = bvm in
                             <bv
                            , m

z fst(bv)
                            > where bvm from (MaxReserve'?-1) when 2a) in
     let Accept = Tagged_tt(AcceptOrReject) in
     let MaxAccept = accum-class(bv1,bv2.if fst(bv1) <z fst(bv2)
                                 then bv2
                                 else bv1
                                 fi ;
                                 bv.bv;
                                 Accept) in
     let Vote = ((inl bv  where bv from MaxAccept)'?inr

) when 1a in
Vote

i,x.<i, snd(fst(x)), snd(x)>

1b@

x.[fst(x)]

AcceptOrReject

i,x.<i, fst(fst(x)), snd(x)>

2b@

x.[fst(x)]

Proposal

i,x.<i, x>

2a@

x.acceptors

(Decide
       = (snd(fst(p)) where p from Proposal;
                                   Collect(f + 1 vt's from 2b
                                           with maximum fst(vt)
                                           such that snd(vt)) such that ...))

(

NewBallot:EClass(

)
(NewBallot

i,x.<i, x>

1a@

x.acceptors

(

n:E(NewBallot). (loc(n) = (round-robin(leaders) NewBallot(n))))

(

e':E(NewBallot)
(((

e:E(NoProposal)
(e'

loc e

(NoProposal(e) = NewBallot(e'))))

(

e:E(2b)
(e'

loc e

(2b(e) = <NewBallot(e'), ff>)

x<e.

x

Decide)))

(

n:E(NewBallot)
(e'

loc n

(NewBallot(e') < NewBallot(n))))))

(

e:E(Input)
((

n:E(Input). (

(n <loc e)))

(

n:E(NewBallot). e

loc n )))

(

nb1,nb2:E(NewBallot).
((nb1 <loc nb2)

((NewBallot(nb1) < NewBallot(nb2))

((

e:E(NoProposal)
((nb1

loc e

e

loc nb2 )

(NoProposal(e) = NewBallot(nb1))))

(

e:E(2b)
((nb1

loc e

e

loc nb2 )

(2b(e) = <NewBallot(nb1), ff>)

x<e.

x

Decide))))))))

Definitions : in-eclass: e

X, assert:

b, not:

A, alle-lt:

e<e'.P[e], bfalse: ff, eclass-val: X(e), pair: <a, b>, bool:

, nat:

, product: x:A

B[x], equal: s = t, and: P

Q, es-le: e

loc e' , es-E-interface: E(X), exists:

x:A. B[x], or: P

Q, less_than: a < b, es-locl: (e <loc e'), implies: P

Q, all:

x:A. B[x], round-robin: round-robin(L), apply: f a, es-loc: loc(e), Id: Id, lambda:

x.A[x], unit: Unit, union: left + right, es-propagation-rule-iff: A

f

B@g, Message: Message, eclass: EClass(A[eo; e]), pi2: snd(t), pi1: fst(t), natural_number: $n, add: n + m, es-collect-filter: Collect(size v's from X with maximum num[v] such that P[v]), es-interface-pair-prior: X;Y, eq_int: (i =

j), mapfilter-class: (f[v] where v from X such that P[v]), nil: [], cons: [car / cdr], it:

, inr: inr x , inl: inl x , map-class: (f[v] where v from X), es-prior-class-when: (X'?d) when Y, let: let, lt_int: i <z j, ifthenelse: if b then t else f fi , accum-class: accum-class(a,x.f[a; x]; x.base[x]; X), es-tagged-true-class: Tagged_tt(X), minus: -n, le_int: i

z j, spread: spread def, imax: imax(a;b), es-interface-accum: es-interface-accum(f;x;X), spreadn: spread3, es-filter-image: f[X], es-collect-opt-max: es-collect-opt-max, le: A

B, int:

, restricted-baseclass: restricted-baseclass(locs;h;T;v.P[v]), outl: outl(x), isl: isl(x), id-deq: IdDeq, deq-member: deq-member(eq;x;L), filter: filter(P;l), length: ||as||, no_repeats: no_repeats(T;l), multiply: n * m
FDL editor aliases : Paxos-spec9-body

Paxos-spec9-body(es;T;f;acceptors;leaders;Input;Decide;tag1a;tag2a;tag1b;tag2b;tagpaxos;failset) == ((((||acceptors|| = ((2 * f) + 1)) \mwedge{} (0 < ||leaders||)) \mwedge{} no\_repeats(Id;acceptors) \mwedge{} (||filter(\mlambda{}a.deq-member(IdDeq;a;failset);acceptors)|| \mleq{} f)) \mwedge{} (\mneg{}(tag1a = tag2a))) \mwedge{} let 1a = restricted-baseclass(acceptors;[tagpaxos; tag1a];Id \mtimes{} \mBbbZ{};p.0 \mleq{} (snd(p))) in let 1b = restricted-baseclass(acceptors;[tagpaxos; tag1b];Id \mtimes{} \mBbbZ{} \mtimes{} (?\mBbbZ{} \mtimes{} T);q.(0 \mleq{} (snd(fst(q)))) \mwedge{} ((\muparrow{}isl(snd(q))) {}\mRightarrow{} (0 \mleq{} (fst(outl(snd(q))))))) in let 2a = restricted-baseclass(acceptors;[tagpaxos; tag2a];Id \mtimes{} \mBbbZ{} \mtimes{} T;q.0 \mleq{} (fst(snd(q)))) in let 2b = restricted-baseclass(acceptors;[tagpaxos; tag2b];Id \mtimes{} \mBbbZ{} \mtimes{} \mBbbB{};q.0 \mleq{} (fst(snd(q)))) in let Collect = Collect(f + 1 vs's from 1b with maximum num= fst(vs) return <num,n,outl(vs).2> for which n=outl(snd(vs)).1 is maximum or <num,-1,prior Input> if all isr(snd(vs)))) in let Proposal = \mlambda{}tr.let b,b',v = tr in if b' <z b then inl <b, v> else inr \mcdot{} fi [Collect] in let NoProposal = \mlambda{}tr.let b,b',v = tr in if b \mleq{}z b' then inl b else inr \mcdot{} fi [Collect] in let MaxReserve = es-interface-accum(\mlambda{}mx,x.imax(mx;x);0;1a) in let AcceptOrReject = (let bv,m = bvm in <bv, m \mleq{}z fst(bv)> where bvm from (MaxReserve'?-1) when 2a) in let Accept = Tagged\_tt(AcceptOrReject) in let MaxAccept = accum-class(bv1,bv2.if fst(bv1) <z fst(bv2) then bv2 else bv1 fi ; bv.bv; Accept) in let Vote = ((inl bv where bv from MaxAccept)'?inr \mcdot{} ) when 1a in Vote \mLeftarrow{}{}\mlambda{}i,x.<i, snd(fst(x)), snd(x)>{}\mRightarrow{} 1b@\mlambda{}x.[fst(x)] \mwedge{} AcceptOrReject \mLeftarrow{}{}\mlambda{}i,x.<i, fst(fst(x)), snd(x)>{}\mRightarrow{} 2b@\mlambda{}x.[fst(x)] \mwedge{} Proposal \mLeftarrow{}{}\mlambda{}i,x.<i, x>{}\mRightarrow{} 2a@\mlambda{}x.acceptors \mwedge{} (Decide = (snd(fst(p)) where p from Proposal; Collect(f + 1 vt's from 2b with maximum fst(vt) such that snd(vt)) such that (fst(fst(p)) =\msubz{} snd(p)))) \mwedge{} (\mexists{}NewBallot:EClass(\mBbbN{}) (NewBallot \mLeftarrow{}{}\mlambda{}i,x.<i, x>{}\mRightarrow{} 1a@\mlambda{}x.acceptors \mwedge{} (\mforall{}n:E(NewBallot). (loc(n) = (round-robin(leaders) NewBallot(n)))) \mwedge{} (\mforall{}e':E(NewBallot) (((\mexists{}e:E(NoProposal). (e' \mleq{}loc e \mwedge{} (NoProposal(e) = NewBallot(e')))) \mvee{} (\mexists{}e:E(2b). (e' \mleq{}loc e \mwedge{} (2b(e) = <NewBallot(e'), ff>) \mwedge{} \mforall{}x<e.\mneg{}\muparrow{}x \mmember{}\msubb{} Decide))) {}\mRightarrow{} (\mexists{}n:E(NewBallot). (e' \mleq{}loc n \mwedge{} (NewBallot(e') < NewBallot(n)))))) \mwedge{} (\mforall{}e:E(Input). ((\mforall{}n:E(Input). (\mneg{}(n <loc e))) {}\mRightarrow{} (\mexists{}n:E(NewBallot). e \mleq{}loc n ))) \mwedge{} (\mforall{}nb1,nb2:E(NewBallot). ((nb1 <loc nb2) {}\mRightarrow{} ((NewBallot(nb1) < NewBallot(nb2)) \mwedge{} ((\mexists{}e:E(NoProposal) ((nb1 \mleq{}loc e \mwedge{} e \mleq{}loc nb2 ) \mwedge{} (NoProposal(e) = NewBallot(nb1)))) \mvee{} (\mexists{}e:E(2b) ((nb1 \mleq{}loc e \mwedge{} e \mleq{}loc nb2 ) \mwedge{} (2b(e) = <NewBallot(nb1), ff>) \mwedge{} \mforall{}x<e.\mneg{}\muparrow{}x \mmember{}\msubb{} Decide)))))))) Date html generated: 2010_08_30-AM-01_01_02 Last ObjectModification: 2010_08_23-PM-02_34_17 Home Index