Nuprl Definition : Paxos-spec10-body

Paxos-spec10-body(es;T;f;acceptors;leaders;Input;...;...;...;...;...;...;...) ==
  let ks1a = Rcvs(tag1a) on links(tagpaxos) from leaders to acceptors in
   let ks2a = Rcvs(tag2a) on links(tagpaxos) from leaders to acceptors in
   let ks1b = Rcvs(tag1b) on links(tagpaxos) from acceptors to leaders in
   let ks2b = Rcvs(tag2b) on links(tagpaxos) from acceptors to leaders in
   ((((||acceptors|| = ((2 * f) + 1))

(0 < ||leaders||))

no_repeats(Id;acceptors)

(||filter(

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

f))

(

e:E. ((kind(e)

ks1a)

(valtype(e)

r

)))

(

e:E. ((kind(e)

ks1b)

(valtype(e)

r (

(?

T)))))

(

e:E. ((kind(e)

ks2a)

(valtype(e)

r (

T))))

(

e:E. ((kind(e)

ks2b)

(valtype(e)

r (

))))

(

(tag1a = tag2a))

(

(tag1b = tag2b))

(

e:E(Input)
((loc(e)

leaders)

(

((

isrcv(e))

((tag(e) = tag1b)

(tag(e) = tag2b)))))))

let 1a = Val(ks1a) in
      let 1b = Val(ks1b) in
      let 2a = Val(ks2a) in
      let 2b = Val(ks2b) in
      let Collect = es-collect-opt-max(es;
                                       1b;
                                       Input;
                                       f + 1;
                                       vs.fst(vs);
                                       vs.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(es;

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

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

) in
      let NewBallot = es-rec-combined-interface1-1
                        (es;

x,d,s.paxos-new-ballot(||leaders||; x; d; s);
                         NoProposal+2b+es-parameter-class
                                         (es;

i.list-index(IdDeq;leaders;i);
                                          Input);
                         Decide) in
      Vote(v)| (kind = k1)

1b|(kind = k2
s.t. destination(lnk(k2)) = source(lnk(k1))

destination(lnk(k1)) = source(lnk(k2)) )

(<fst(fst(x)), snd(x)> where x from AcceptOrReject)(v)| (kind = k1)

2b|(kind = k2 s.t. destination(lnk(k2)) = source(lnk(k1))

destination(lnk(k1)) = source(lnk(k2)) )

(

k

ks2a.es-interface-at(es; Proposal; source(lnk(k)))

Val([k]):

T)

(Decide
        = (snd(fst(p)) where p from es-interface-pair-prior
                                      (es;
                                       Proposal;
                                       es-collect-filter(es;
                                                         2b;
                                                         f + 1;
                                                         vt.fst(vt);
                                                         vt.snd(vt))
                                       ) such that (fst(fst(p)) =

snd(p))))

(

k

ks1a.es-interface-at(es; NewBallot; source(lnk(k)))

Val([k]):

)

Definitions : nil: [], cons: [car / cdr], lnk: lnk(k), lsrc: source(l), nat:

, es-propagate-iff1: X

Y:T, isrcv: isrcv(k), assert:

b, Knd: Knd, set: {x:A| B[x]} , l_all: (

x

L.P[x]), pi2: snd(t), pi1: fst(t), natural_number: $n, add: n + m, eq_int: (i =

j), mapfilter-class: (f[v] where v from X such that P[v]), es-interface: Temporary AbsInterface(es;A), equal: s = t, and: P

Q, product: x:A

B[x], ldst: destination(l), eq_id: a = b, band: p

q, pair: <a, b>, map-class: (f[v] where v from X), bool:

, unit: Unit, union: left + right, id-deq: IdDeq, list-index: list-index(d;L;x), lambda:

x.A[x], es-interface-union: X+Y, length: ||as||, paxos-new-ballot: paxos-new-ballot(n; np_or_2b_or_firstballot; d; prevb), let: let, it:

, inr: inr x , inl: inl x , lt_int: i <z j, ifthenelse: if b then t else f fi , es-tagged-true-class: Tagged_tt(X), minus: -n, le_int: i

z j, spread: spread def, imax: imax(a;b), spreadn: spread3, es-filter-image: f[X], Id: Id, or: P

Q, not:

A, es-loc: loc(e), l_member: (x

l), es-E-interface: E(X), all:

x:A. B[x], subtype_rel: A

r B, implies: P

Q, es-E: E, deq-member: deq-member(eq;x;L), filter: filter(P;l), le: A

B, no_repeats: no_repeats(T;l), less_than: a < b, multiply: n * m, int:

, links-from-to: links(tg) from srclocs to dstlocs, rcvs-on: Rcvs(tg) on links
FDL editor aliases : Paxos-spec10-body

Paxos-spec10-body(es;T;f;acceptors;leaders;Input;Decide;tag1a;tag1b;tag2a;tag2b;tagpaxos;failset) == let ks1a = Rcvs(tag1a) on links(tagpaxos) from leaders to acceptors in let ks2a = Rcvs(tag2a) on links(tagpaxos) from leaders to acceptors in let ks1b = Rcvs(tag1b) on links(tagpaxos) from acceptors to leaders in let ks2b = Rcvs(tag2b) on links(tagpaxos) from acceptors to leaders in ((((||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{} (\mforall{}e:E. ((kind(e) \mmember{} ks1a) {}\mRightarrow{} (valtype(e) \msubseteq{}r \mBbbN{}))) \mwedge{} (\mforall{}e:E. ((kind(e) \mmember{} ks1b) {}\mRightarrow{} (valtype(e) \msubseteq{}r (\mBbbN{} \mtimes{} (?\mBbbN{} \mtimes{} T))))) \mwedge{} (\mforall{}e:E. ((kind(e) \mmember{} ks2a) {}\mRightarrow{} (valtype(e) \msubseteq{}r (\mBbbN{} \mtimes{} T)))) \mwedge{} (\mforall{}e:E. ((kind(e) \mmember{} ks2b) {}\mRightarrow{} (valtype(e) \msubseteq{}r (\mBbbN{} \mtimes{} \mBbbB{})))) \mwedge{} (\mneg{}(tag1a = tag2a)) \mwedge{} (\mneg{}(tag1b = tag2b)) \mwedge{} (\mforall{}e:E(Input). ((loc(e) \mmember{} leaders) \mwedge{} (\mneg{}((\muparrow{}isrcv(e)) \mwedge{} ((tag(e) = tag1b) \mvee{} (tag(e) = tag2b))))))) \mwedge{} let 1a = Val(ks1a) in let 1b = Val(ks1b) in let 2a = Val(ks2a) in let 2b = Val(ks2b) in let Collect = es-collect-opt-max(es; 1b; Input; f + 1; vs.fst(vs); vs.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(es; \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 es-prior-class-when(es; MaxReserve; 2a; -1)) in let Accept = Tagged\_tt(AcceptOrReject) in let MaxAccept = accum-class(es; bv1,bv2.if fst(bv1) <z fst(bv2) then bv2 else bv1 fi ; bv.bv; Accept) in let Vote = es-prior-class-when(es; (inl bv where bv from MaxAccept); 1a; inr \mcdot{} ) in let NewBallot = es-rec-combined-interface1-1 (es; \mlambda{}x,d,s.paxos-new-ballot(||leaders||; x; d; s); NoProposal+2b+es-parameter-class(es; \mlambda{}i.list-index(IdDeq;leaders;i); Input ); Decide) in Vote(v)| (kind = k1) \mLeftarrow{}{}\mRightarrow{} 1b|(kind = k2 s.t. destination(lnk(k2)) = source(lnk(k1)) \mwedge{}\msubb{} destination(lnk(k1)) = source(lnk(k2)) ) \mwedge{} (<fst(fst(x)), snd(x)> where x from AcceptOrReject)(v)| (kind = k1) \mLeftarrow{}{}\mRightarrow{} 2b|(kind = k2 s.t. destination(lnk(k2)) = source(lnk(k1)) \mwedge{}\msubb{} destination(lnk(k1)) = source(lnk(k2)) ) \mwedge{} (\mforall{}k\mmember{}ks2a.es-interface-at(es; Proposal; source(lnk(k))) \mLeftarrow{}{}\mRightarrow{} Val([k]):\mBbbN{} \mtimes{} T) \mwedge{} (Decide = (snd(fst(p)) where p from es-interface-pair-prior(es; Proposal; es-collect-filter(es; 2b; f + 1; vt.fst(vt); vt.snd(vt)) ) such that (fst(fst(p)) =\msubz{} snd(p)))) \mwedge{} (\mforall{}k\mmember{}ks1a.es-interface-at(es; NewBallot; source(lnk(k))) \mLeftarrow{}{}\mRightarrow{} Val([k]):\mBbbN{}) Date html generated: 2010_08_28-PM-01_58_40 Last ObjectModification: 2010_07_15-PM-02_27_24 Home Index