Nuprl Definition : RSC_non_blocking
RSC_non_blocking(Cmd;locs;f;es) ==
e:E. n:
.
(loc(e) 
locs
(
c:Cmd. <n, c> RSC_Propose(Cmd)(e))
(slow:bag(Id)
((bag-size(slow) = f)
sub-bag(Id;slow;locs)
(r:
. (RSC-slow-round(Cmd;es;n;r;slow) RSC-slow-round(Cmd;es;n;r + 1;slow)))))
(e':E. c':Cmd. <n, c'> RSC_Decided(Cmd)(e')))
Definitions occuring in Statement :
RSC_Propose: RSC_Propose(Cmd),
RSC_Decided: RSC_Decided(Cmd),
classrel: v X(e),
es-loc: loc(e),
es-E: E,
Id: Id,
nat: ,
all: x:A. B[x],
exists: x:A. B[x],
squash: T,
implies: P Q,
and: P Q,
pair: <a, b>,
product: x:A 
B[x],
add: n + m,
natural_number: $n,
int: ,
equal: s = t,
bag-member: x bs,
sub-bag: sub-bag(T;as;bs),
bag-size: bag-size(bs),
bag: bag(T)
FDL editor aliases :
RSC_non_blocking
RSC\_non\_blocking(Cmd;locs;f;es) ==
\mforall{}e:E. \mforall{}n:\mBbbZ{}.
(loc(e) \mdownarrow{}\mmember{} locs
{}\mRightarrow{} (\mexists{}c:Cmd. <n, c> \mmember{} RSC\_Propose(Cmd)(e))
{}\mRightarrow{} (\mdownarrow{}\mexists{}slow:bag(Id)
((bag-size(slow) = f)
\mwedge{} sub-bag(Id;slow;locs)
\mwedge{} (\mexists{}r:\mBbbN{}. (RSC-slow-round(Cmd;es;n;r;slow) \mwedge{} RSC-slow-round(Cmd;es;n;r + 1;slow)))))
{}\mRightarrow{} (\mdownarrow{}\mexists{}e':E. \mexists{}c':Cmd. <n, c'> \mmember{} RSC\_Decided(Cmd)(e')))
Date html generated:
2012_02_20-PM-04_02_00
Last ObjectModification:
2012_02_02-PM-01_59_30
Home
Index