From 161d269d279b9c77640e8658d794d503db8ad8a2 Mon Sep 17 00:00:00 2001 From: Peizhao Ou Date: Tue, 25 Mar 2014 11:52:46 -0700 Subject: [PATCH] add Commit point clear construct --- benchmark/chase-lev-deque-bugfix/deque.c | 2 +- .../cliffc-hashtable/.cliffc_hashtable.h.swp | Bin 40960 -> 0 bytes benchmark/cliffc-hashtable/cliffc_hashtable.h | 82 +++++++++++------- benchmark/cliffc-hashtable/main.cc | 2 +- grammer/spec_compiler.jj | 30 +++++++ .../codeGenerator/CodeGenerator.java | 16 ++++ .../codeGenerator/CodeVariables.java | 80 ++++++++++++++++- .../codeGenerator/SemanticsChecker.java | 17 ++-- .../specExtraction/CPClearConstruct.java | 23 +++++ .../CPDefineCheckConstruct.java | 2 +- 10 files changed, 213 insertions(+), 41 deletions(-) delete mode 100644 benchmark/cliffc-hashtable/.cliffc_hashtable.h.swp create mode 100644 src/edu/uci/eecs/specCompiler/specExtraction/CPClearConstruct.java diff --git a/benchmark/chase-lev-deque-bugfix/deque.c b/benchmark/chase-lev-deque-bugfix/deque.c index 11e5e99..c9fc8a9 100644 --- a/benchmark/chase-lev-deque-bugfix/deque.c +++ b/benchmark/chase-lev-deque-bugfix/deque.c @@ -30,7 +30,7 @@ int take(Deque *q) { /** @Begin @Commit_point_define_check: t > b - @Label: Take_Point_1 + @Label: Take_Point1 @End */ int x; diff --git a/benchmark/cliffc-hashtable/.cliffc_hashtable.h.swp b/benchmark/cliffc-hashtable/.cliffc_hashtable.h.swp deleted file mode 100644 index a868efd725e96c2c7ab3b96e294aa623c84fddd0..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 40960 zcmeI533QxSmFFv@p<7{TXx4#Y^4TG=Buld8gb=*Nj%>$@*R~V|NJ6Dl^~tKZR3)lP zw&jEX2{d62+d!WL5@^CQVOYWjVAy5|oUrzRX4rd9m}xi+^!)z!z4t9u zC0P#iIej?t$v>+4zPH|Y-+k{c@746isqq8R(?%{V@b8g@!ejp1#)%7_-#+W^#X?~| zuAZ7LH5z)g+`r0+;fqJ&xZE09C|5_~%EA(fZwdu&XwApv;qq);J{C8J%Z<7DYAtSV zn2zh^*|}2l*oJbgIx|xqo-MUz+okDR>>m`92P3mf)Uo<_l>)02=s|&n_RR1l4=-G} zX>_CBp0{>Q^yojivPZ(zN2?TArNAl$Rw=MbfmI5uQec$=s}xwJ!0#&s+Vg)@cpja5 zkniBj{ok`X{{E5w{$l_46&>&U{P(8+`#4`fDCZCS^IQDiTRYxA*gwC~|2@YyDCB=g z$NN9)c>jm~ebxVc(An-o$nU=vw)ywRI^O%otAAE0uu6ed3anCKl>)02Sf#)!1y(7r zN`X}htWsc=0>76OC{+rD3+UM?>C^cCgZ}@$KQ0tL1O5(t0K6Hz4BP;Yf-Ar-FbK{A zYr(_7FCI}Sd<%RMybb(0cr~~QJQpm2A@IG27Yet7Tfpe1&kNZ2V22rFbd8Gj|0EN@bP_cFZd*QC%6N=3>3iz@Obbz@DT7d3@IN1 zuLH+H8SDa=f-PV@_zlLG{{_ARJ^)?|THrdc6Kn-rzcdS>Tyq z9Gne43jc_Q7QJ2O^pmBpukXC5bi7opDZ(RamySm5MkA`uMAdfGjGwbmZN{yr6xHJs z_Hw4tjM}rMc62OWj9Rrud!%4RR9n%(EBEgoiW=?NxOt-5ilgfnS}LNw(5$;G6h0D- zx1$r)S}j_buaw$UI2%*;$+j!y%JiXH;wp=y@Gu3*$XQ5u+T+oB(>VJK{A^n5Z%ILs|O5e6E(zi|aZHpxesb)&GR_q>8RXMA5Il}kQJNGQ=pIn@e zr*eI>C()oQB$vQ-E1`S4xsV~KI;KiQB&#IbeF{5+{zDJZBsa+LW=aCSoQ4ES9=a?N zC`b4nNZ_8i9`5TR!M46+gCr=fnj4aM5OIaG4dkf9Ju=c{g_Wu)gj%G~cc^>MiBlaanw{ zS}$nu&vSyH+^)y1)<`soWS}QV2uTG5QyY0!L4H(c7NZiP$BB-)IV9YCqgpo+c3#wq zo7GaSda5*CtySBLLs6>{ort5>Y-6ETiDpa3W5i$!vZ|y~jVC@VE;=zA*Ok;l=~TM4 zNzG_25=+-?)G1XBS0XDY2)4A0qt)Zc*##O)w)tjbK5n)bqsC03Z^PhV0TQ-aT@*qZ zwBxz?8gg`No2gkZ&Bc*sh5wJKu;R2MpC_X#Q4-4?mFg8M zXDamG4VT(hZAOg~bqGGc$p7js=5@Kh^XzWB8WaLG;QHc{#UTwFc z#`N`ZxjkgntcCtw?wNSm$5UHE_Q8v5A#Jrh%NT~1&1p?B61pZ;q8a48(bh^5LC2`C zKgpXcKq7r>wxFJ}34)y@GKxqb_>2FGzl!tCDkS8){_;c%T))XCdy!Q{3+g9*UMK!U<}<@v)l)HF*ROYr)`ks{WQwu3S|m<6xWHr-iRrb; zZ`Zi1tJhN2M$sZEd7~@2vsBTl+D$ZVR(N%_CBIhhv(>8>+Q{ai5|x_G(xQ8>`3gt3 zn=HiBwMO|^VE*Zt!m66{bg9B;GOKs}S{sZ~G*?xY+Ksttd8?RWaQoE>6|4bjY4U{h zty9rpv?*E-%~XoYv!{GZ22puhr;L7uzFgtapw&xarEydVEElrFcAC+yqphgFRCm2a zs2H~)Z0L~|mtYg=3w>kxZ5z+^?vP0ZriP7)$ULU_WBtE;Y+Wn5f?aA< zMcl=6NMMtvBW^bLmX2FiE*yc&_sOCr>P(!6bl#dM`=on5wHo9c0yg{;(MgKgrK ztrIVi$#Wz_63()w&Bi4rzttI4+!E{3IJu}Td)nOSc-(BM84P`nsE&RMEiIH8I2a;4>8 z#T}X2m0ESWqaM#ZLhYs#8Y}k-=eQW4?wtsFWW}j3W3{+g2+YZ%y{bT#b_v{%f z?%g@DcXH=t`*#=j()5|Ss_OAd`u~OKpkwH*(*J{h{B!8?Zw0Rhw}F>~o52`(B=`Y3 zy!8C9f)9cBf%k%!fER!TumeQk$LR9+fKPxAgPXxKz`p_aqQk!nyb@duHiAckZ=kc^ z3tkUi18xR2@C@)6@LlwE>Ga~>w zsQ;IN)qkrLSf#)!1y(7rN`X}htWsbF6!81QZbJwAMvNZLS|sH^sN&u*FdNsfwMYqT zH|9C`IJ{j?iZXB%wcqc@jMT!O(wIlF8bViMmuW^a8HPiaBI+Nnm(k7>dm>t(S;W(N z(M=CFqA~^*bRJAUM^P^^c=So58gwN*ZVfXpiy9YOC!G?HC$|of0f_8|n!Em7E?~UT6?*Pt*eCx|1Ckhz=NH=JGY3lT z@~pa#X>ka}l##MQQnn)65!B%%Ym$IInPJ`R_bq3Z>7N=fd+rpJl9gF$Fb$qGYRX2i zo5797c23Y0lsWh&G(30@$m#t67hK@`5v_4g2BJ%&$wLP&o0vq2h&D%4t_!~7eb!*p z)JJAwdQvP^D*eNl_m?!QhyZ~usx~Ry+oaXAHT`Leuw2`hG+lJT1xCic-nFl|a(b8+ z>Pl4QE2|r_nn{2Y#;|y$fi8<~2(On>nIO0H?)t*qG}BE_F%P7w+z4DAQ6iqLfQ^{;U8q(H6xg5upxPoQZ*>p=4b5Y6m zVil=Rj{VXxy&vEm-)T&};%)945mkm8C+lpj+jMYM*_#n17BP3QcK>Ly0ta;=|h9RD3P zUiv?7-olXg|KH*lydR?DzYUbZg)!+31l|Dt0=yQ;9&i&_4;~B70bfGzzYE+7j)R@x5#Y<{ z`yT}F1#bpNfqeRxf-PVT_yxNCz2GfCwtznco5172W5A=qBfx{f{n$f31Ktnb22O#? zfc*78#V7w2@G0;La1D3@_(y#2KLTF|e+}Lb{xkUZ;9Br3@JuiX#)16yPXs^2AOBJC zPVfS73|t2`fhU7sFgQN|cY`;8JHas^KmB&F4O{|-!DGRX&!&Cg9`Jf_3h1oE6<`cp z3f6+3G2TB0KLY;%?gRe?yd9hb*Mn`q_`-O?q|4sRkQ$i7WLh*Ins@eT%BH@#B3p)j zTP#^;S#5bMKHo8x%i2RkMK?xA@GvaF+~m&)tXAAMZ`^pj9XDr~&71Riv8JWII`h5Q zR=}^Psl4u|jYH`wGZY;>R6MYAa%^w$(EeRopXHgF8f5pRhIvAf^w`#5%fes2Tu~6*jqUz52;+avDLC=siLr5e2&gmAbP==bM6`jqa zzYurRwpbiHbZ}R3VkcB(zvJnfY>GCA5C(B#pgGic!!Qu3^BvUh%aAfpe#)Q;wu{o5 zl&#w2_3w62`mAGzwSjO{(W)J7-W(bq`lv2+&cDo*iq>TM6D<1)Pg%Qr&$vv@`IYdr z^DUF}0r18W^GrkGoWYu8S+?kAiZh*XZcB_{pyc80+Gv@ieWV2;f?Io{ZrQhw{NGi zh?XczGVT4=-{b96UK^D z_`#>3ws+R&JUsntsu>+msX+s1gI405O_tpZlMmFXH19+59|C zXDWW_H?ygG21tcq5@dO>SKdy^9i}mjU)j{XoV`LibpxON9?aM-YW+6z@qug~pln{t z9AyvJ^>9;uUZg)W>Hc6JWTksZsu&|SjA%X*d$HQf4yV2%Y`Wx$JOYG z2QYTOH$x{OF8v=hv+yW%J^BB``TH-U-+vUm7bpf`5nK;;gY955kS*YUqU*l}ycygD z-T>|ZuK>qE30wg#0t4Vz==>ob;8T45IJgbeKo!h_GEjWL7H|Q$AKm|Z-~-?-;5fJr zTnTo7CxVB9f4~;-EpQ)rBbWo%gDTLufTx3BVGH;P_#yZK_&9hGxEVYjjDbf2#s9w+ zD0ZM9D6anr;M3RuWEXfTXoBm3V*0NFlVAcI1P=ip#V*hWisx4h|0lpl!A)Qv__yGH zK>T+B#pz!QCcxR?XXx^O3*H6(Be)B^3j7D~O7Jr9Qcwlb{T~c|h+h9!;0|yrI00sW zV)RGB2p9tY#8|%#Tn#P;8v92A`(Zm4>ZGV8QVZ*4nq;|7<^eB-)k+)!yN%C$anurMyl4VuqxK?!F z%85y~Di~tplcjPyD&di^perJxDD5&t6A`^KC(6Kx!oN_jYm10t?j)BrA|l?X6sePL&cQMdGD3LJgv z0M%_gIm5qlKOOVY^4S|QIXveas{W?ATL+oTPli&s@y zwzC`58!d$H+kn2>ezEt~H`z`Go3-ql`7Gg$I+$S@+l=P-pJEu1m;VI z+ub%;Hi{ajs`H;*DdxhC%clAtyTo_%i*hD&{Wcg6X zhAr&J8-#4*UxLYD8#WNk5$9`kk&;YTZxiPw<>WOTwR1c1u^MN6-s(FMHbBV;LtSF| z)X(7Ta>1&DbQ-spb_}?_7;!c9Fm#EVOnL7e7@m&Vhmb#pw#-h{!n*ckI2Q<2B;<~9 zF(nZ{g7F4@VTUBr`^`%_QmsfK>bL^YyV^}Y9;Fb4NTOd75pO;Z{5f)4^crX;6}}!9 zT#sbX9*dF~?Ftc#gihAd7;r1nn1Sxa%{uQCNpFFO?%0vIZX`OiKsaV!t3j~0+sT#j zMA^{++C|*ICqiy(XndMhrGyK_rk5zlMXArlC4x8^PAgX>O6ZcVq=ByGnU^dufO{`@ zm<5Ou+KIo$qKGr?ro`^LOVQedT5EGfWAW(HpHDxD_aS5w|J3ipB;M3(5@%xNZFZh6 zz?iZ9*E5L`>KRY{?`jfLDpNSOrrP!)FC0&I@*oj92pdT=tu1jY-`udcbS^Cx=itRM zpYs)?K`wjb!B?z&RxwIsQY$MdkrEPc*ba{)cXS>wvv)}4tn)q~-k4|{VXRg7J0KgO z`^W-l<~lYd+972uFo|K*B}~4$qO9(mZz5~N&e+d4M{B%U29E2rvn*{P_qAw!HhWjL zbeWn@Yf5lN@4O$jhuz!zn7i!WeHoL{QYOZPoNCX?Tu)1Tg->e>&v)ekn8TgVY3IRb zYO~~xZp#e2@d*r;8{`aC{HQMPfchOfGJ5zI9PK-tPI@?=b=w);m+~-?`t(k_Fm3oN zrgS?lzS#biZ5JOimUlZ(ySdBasY1x@XIzK7FPULVrKz2xe0Bo-_R}l%|H+t~E&Gfn zSH_dN)Z7Z^|2Ikh%jo~VMz{YJ_#${a&{=@H!F6B=DE|Lm@IG)mI0mM{LGU3iMqNjffd=h*NECT88SA$1^U!$MDAKVR| z4bBJWg0G^Ve*nA#ybx4D30woRvHrhCH~$&97kmWV3GM(VK?xiN7lC207W@YN{j=bm z;LYIm;055h;6^YDc7Xx#6cB+QquYNNya~J(yc8S*PXmty=YR)+Poe974BP^Cg2#hD z0gnPYqkj*050Kvfr(hh&=l^gZU;p2O`@ma46U>1c*a|KIPX!l&e`b6?0bT;;!FAvo za3RpxkAfBc3$rVzddx1CgI=x!Tk^u>4Gs`-G;5ZeZ(&B-bkcrj^3bkBn}dO}&G}W1 zwkiCt9NY2Ri2XE*Kbu+$WK@ZXsLU*>shc7@XBRjk<-~%o-D;)MogrdSQD8E45;5f> zq|!Zirt|^7l$#SmY7jb|{;ZEi2cip{nPiyH7L~-RAmfOFw??JfI*M4tCw{a{#AiPw z)Se+5ni$+SW*$g{pi3A?hph3!EK%irprUH?$}{5D4&ds^4zEC8-f6fmUT8VARA$7r z)1H0Ig2tIfhPr)v?>eJwAIFtMdPajGgNvG6I#@NUq?);^j24PAo40b^i20M0Hne0=$Y>~W1tZfr z0xJ&{74IJsYwP+7LVYo)b5c~iXrYT2h~r&%^(^0I-&j8rTcPj?k zAu}*U@Yz~M&ohj&45w^zBd`5pPm_y}B|Oq2POc|=Wn&3bKMAb~3?-S7^Rv1U71{P- zvYM^7*F<9q!nON3bQ^&W5*CMK0-J5G%7_wy$4T`tv_s|{ja@`8)DNClCzjAq0!Mfn zn%A=#OR0>P^+MDouUW@a1&Ua*caxG%2r0fNhP_28Ig|AU_UU){9Stbj#@ib zG9)xE)wq`!kffom)MSqP5phi>k%*XYva>JrYv=9=D0@$K*7+0G-V8($f#5mmDe5Rm zdLTWo-5E_yfpgwFz4a=Xy;5FTtZAWn1!bht&M;JFZBsX#_GXUwPUn^d!Mk_|@A2cd z4Vkc9zLbBcjP_;}yk*TEZks%njj>&7*n;tr@-z^MT@j0=nU^q-;j6R2b}lx+GUh|V zmH519-0spbI}jElMFP`%XOqXlCleqmUdhQATz@izIinQ)F&h@e_yMnAux~1YIp=&u zZ0i<)j;C2$hu=%f@|iVxZo=T{7EMf^vbbWsE3(edmg-02BDOjr{}m)_ol+#tpl^U1 zHg{OMS~o+ZRgsAs?qO>rR>iKhNlLWuW`69lDKf7o8*r008Yij*e``{5s}4h8W=cum z4pXH%Yy&Y{olmTlUO`A~WjRxsERqwtG{Ya*c69_h@{o*^7EbLfl&VsJG#CW`w*@bF;*J=jq^J%38tTBqo^raCphE;^ByLW6UrlLqkchf7igMf(JA( zxv5G}PkLn!<6s)&Cg<{Sk_5S(JP-0)xAiDz_@2c1B#~C$rQ#B$0a2kO>g*j)lq3jq zS&i@{HdZGA>z9+jN#d}#4G-`@Ifn{@z;;EnBe|PtpYNS@udi>PYD%^Y;pj%czp>+L zS=6`}Lxz7k?d)sm!&IKSBOkVK1j$GS7~OFgA3RC)mgXQ5R_JNcx*5*8NQT1+V_4If zpf2KJ9o_@8(jx#BNT%5(`Jc9p4Pcgpv>+iN8v#el&}iqO@avBIqE5@Yy@9=#zpSE- zI7si8&^=>ZHKS`q);S~0I&(8w9=9`5a0OMkV5chg(?pYO=_*K79Gw;=LVw(BtF~}? zxT`J*#%gt}En>!m9P-8RT>~0!j_DSTNrYO$G$uwh4W$3CLGk;JF3Ly$uX-g={{Oqc zHQ-6$|Dn&{2juI2BapBEPN10oM*#WqZv@u>>G+QV-$j@I1h^BN0P@?*XTJ^T4!^U2 z{Po`ip9b#%cY`~@i@^)QB-jr6!CByo==qBCm(N~j{m%mb2mStM;DbOu`#%S-2Gd|8 zcoI;Y|L4)=btm5mFb*CDzK5>9-8fmKwvVdh-3>Gwgf$tOZFVv_2N}3 zS$wz4ns=|-Ha$cd9ZsX35#@HBl_nDH2%1UQ@Mcoxqmfq~BOAL8_t=3YQ7?O1jv3pd9&88h$XqBFftQ$sC3y2E?2;#{JIOmGx!?xCQ<`M8(RY>SwCBKO$$3oG6U;;z zOUoIZxYTx18%1^4TOGoZ!BZN&r$ec>V|=STCUxhA7&*S#L)_ z5+n5nza%TQLEQXYspZ(Zq}a6Pt1dc-h=-bX)NJabk{JxN4w70H9_>P$CbG2o&gO}; zv-sU|4=#07&RP{hFY%zkJx@oXS>seO%EouiLxucP`4@;goDDV;D#g^%a_;k&sl3`70ZL2hneS#;nZx^rXpb; znvb={QKG!eewc>HD#*2p77R0*nr9Ilunk;d%`tLJ!=J~@l6yIeTGcTP-E-S~&RbDLWwbXiPDnXc5z94lY)V7Hn!UN4JrhDC?g zuw4RIhO>;QHY=pWlOVAtxr1=&luDLU^|My0&e`aSnn}6VI5A?Fe7VIu5hdZRO)n)k zzISV>vHayGD`p5kv|&@Ry$y8Tqd?mHqN%=5AdCnk%nBlU8p+;-iL z^Sh7x^i-Nnm{qc3dwW_!lai?!${XrS082^U1`q+NO5 zPPZL?zhJ8AQfb2I4fIGA-X$86NT!oy#;ZZs3#r0)U#rZ@UQZPL1~bR{`_ITY=#4+N zF@(MRIjoY~DZ0ueWDe=byhONjQ`_~_N{cwKtS+UyuQXk9oN36dL?or0+)+A{EE0!o z#e+pj9Z}qyZLM8ptkC*y`;2HE?6*!Wf-noj<&HZ~n5!cM+-Yy`lv^$D%Iw;QKd%`+ z>cZ5%!wX!j;STZ+MSKYd8(9e3D-^3C5bewMj<5!I!;$elVqMgiJ3Od`!N4cx(hAOgxoXn_$%RlcVG|B_*-NHRi2v7FZ|VOp z_PXSK==|>nw}L6K2W$f8gYTp7e+7I2+yg!hbobxuz^lQ{parf2hru>*3D6mUCxgd; zpI{$QY{2`#n}O~KXo4cR1Pp-)=#Ie0g2#Xd0o@nyW$=0MH{e6ycJNZr05xzBYzCKr zbHO>_4}okAA-3Qhe0~*pCHOPY27AC0!9QYC_$l}V(7l4M0Q%j47l4~U3pBts@WQCFTizR8#o*M7(2t)fZ`2q1G-OOKhSRgJQe<f@h}YrqX)AJ_vFQ=q#A zbg#gdz&pU(zygpRVgQ^C&H~@Y?(h+C7q}kGf`cFe-^A{qvjlg5=YU<{{|-!1#@uE@F<_ zpUwWUSlV*=RF)jhX4VE5O@`%@UF*uUmX1}0t(^IUsEQgatWHzURt*>BW0RW6>=Y<- z5+s)sxxna^h<#T++9!Rp-IbRD=}PV%r7?oGC~`$)DgV*Vr1H9Hs{i7qN~X zMGFG|a*mqdl5zdC&DNUGhNUe0i9-P?@BA=%=MQD-8XYO!nGp+#;e#|B(hk)z1SVB8 ziG39vX(c?3O|+$9JFAt(H#RIhX@~u}G}_>a&QCV@#E#Y2-1Vo=s4DckJGwJOAq*tT zfci!&c1q2VdDe_qr5U_q)+z)o5h{-OIO6h@NGnyh_0A0=oPH)p6sbR_*%5@ES`L;w zzsLp7MuB7w@j;7@)h-)}OQ42n2keuD1u(2+?y(<^&W5D=rO&+*>V~1+Z;HH8G(85n zj)K+^?IFTyy8-K=rX5GK%e0d#thah`Vw}bIAaz3F{yL!6ENAzRMLK2Fkw0YUEI`M1 zMnfrA#aJ!Op6PGx7AuC2Iu+C|%{i-upWqteOl#~ckf~9-8VmZBlZyKzNvHN0;Ym** ziejQnY9cn>U12@S8qJm!3en(om9a^>k||v?GJPNxqD@ad-;_923{PL73+-nbFfYel zbK&T-Jq|{xV4wK*t(D3w1Z0Ztkkq zhl3r8{km*w?0~uA-S%dlqH3Sp%DNUBb-TrI4@OtYFe@?vOQ)9-o=I|Zf~{Wl6!wUb zk&$3}31#aB8MSStiiC-38t2q?+Zgsb^B)K*9tv7vYHP7JA{m#7d2)7QM=Gi_7h}fw zs1eQNcm6Ol@MMrny-bm@RFjb*)&`YBq2Bq-j#-9!`zd+HnLDDSMhZaYz7l>Ltf zY+S~H-RDxHcYXVT{GNxY0Ub)0JFCJTC;rdW3o zQX%a49d(Y$NF$4?nQZJ$S35->U)=;BEwF^kh;YpA8%nR#OWL_LnHAf^daT?T#+YeV zxj&O%9+5iSxd|h!d!YcJ8#1RXoKH#})(trNK?Qe^eF6Cwd`>b(_+5iE%v?p3C+kEm zv>OF>csu{2ebQ`)w__X9=M5WNAP?i@E})8rx1+;yH(c_BWIOh{OYivE6B^)tc*afX zBe_fH`t25={4)h@52&g>|C|tc+ivka6WblKW*%A2Y|gC@lKX$y4&L|U`Jp18q4V%erpTe>t_kfC ztM&^j`3Ab@w2=?`0kTZFTEco>^^~a~7)p~4$`riMT?Lj#M@#ZZ|3~dF{M`Hhn_jh3 z{J&xVJ`COt>Og1y9|gXS{{8`=-}1W{DAxZzbn}ma4}re~F99uZId};8C-iTf;g{a7 zSpVC=NpKiE89V`e5#9T9;2xkm{+ZcSbh)T zB{OrKSBM(=^&IE#vMsq^%d7#~cbJ{SKB(1ZYhjJgHdnH5J~`^0c(UCNCTo+V3&n-{ zbc0`cGI6Zohz2uHDT!P;%OY=Stuw+(6j~dQS?+nT-?}a$h|T2dg67P9r44_nh83eC z%ea1YM`5kz7_*|Ba1Vub6IzAXWy;NX7+|;SUGsuj-DW_LZb7?qJ8n~S zwD~oCU>U7U!jCy@27B+Kqf46F)*E9k&tW}nZq^3f@op!6%zVF;$<3Fmu{F`rSzcmq z`z;Rft}@q~Q(VNG(ropx3G}Z0I4mr0*gx+c7x3N zZ45+OEv*-c7;!e+4C&n9BxE+GFrj1vWJ9%r;Ymklg=FQDA&X2P!~qUvT`S{F@a!O} z`swJ#+LB)742d@DeauX3EM~bCkfD6W?`y0P&{6@)^QC&V%&88UACMNqqb8~OdCvJo z21(Z@1K^$VtRqKe!WW#4}-0t3mb!v+7itmi}iW^Zl|PrF109%uP#ePm!DlvBs(qCOXTr3mC64yr}63 zjm7hpJjlx&c`Y~X^?ejE)+Bw{nwXho>%5j8NAA_Ld^J(QA1D)$#w^3& zKN%V-UX$AHmRb`%mpJik1K}F&<*a{=Lm*htt!p8gHes?e>6(a^BdYPNv!`Q}<_99` xWotyJ{0s{B&0f)hlJRofp!y_2e3dr5`kreiQ_Eh!NK2dd?N@Q#hPtot{{dfcJ+uG- diff --git a/benchmark/cliffc-hashtable/cliffc_hashtable.h b/benchmark/cliffc-hashtable/cliffc_hashtable.h index 5c32ca0..3cef980 100644 --- a/benchmark/cliffc-hashtable/cliffc_hashtable.h +++ b/benchmark/cliffc-hashtable/cliffc_hashtable.h @@ -151,27 +151,7 @@ class cliffc_hashtable { return res; } } - - @Interface_cluster: - Read_interface = { - Get, - PutIfAbsent, - RemoveAny, - RemoveIfMatch, - ReplaceAny, - ReplaceIfMatch - } - - Write_interface = { - Put, - PutIfAbsent(COND_PutIfAbsentSucc), - RemoveAny, - RemoveIfMatch(COND_RemoveIfMatchSucc), - ReplaceAny, - ReplaceIfMatch(COND_ReplaceIfMatchSucc) - } @Happens_before: - //Write_interface -> Read_interface Put->Get Put->Put @End @@ -222,6 +202,7 @@ friend class CHM; kvs_data* resize(cliffc_hashtable *topmap, kvs_data *kvs) { //model_print("resizing...\n"); + /**** FIXME: miss ****/ kvs_data *newkvs = _newkvs.load(memory_order_acquire); if (newkvs != NULL) return newkvs; @@ -244,6 +225,7 @@ friend class CHM; if (newsz < oldlen) newsz = oldlen; // Last check cause the 'new' below is expensive + /**** FIXME: miss ****/ newkvs = _newkvs.load(memory_order_acquire); //model_print("hey1\n"); if (newkvs != NULL) return newkvs; @@ -255,15 +237,19 @@ friend class CHM; kvs_data *cur_newkvs; // Another check after the slow allocation + /**** FIXME: miss ****/ if ((cur_newkvs = _newkvs.load(memory_order_acquire)) != NULL) return cur_newkvs; // CAS the _newkvs to the allocated table kvs_data *desired = (kvs_data*) NULL; kvs_data *expected = (kvs_data*) newkvs; + /**** FIXME: miss ****/ + //model_print("release in resize!\n"); if (!_newkvs.compare_exchange_strong(desired, expected, memory_order_release, memory_order_relaxed)) { // Should clean the allocated area delete newkvs; + /**** FIXME: miss ****/ newkvs = _newkvs.load(memory_order_acquire); } return newkvs; @@ -272,6 +258,7 @@ friend class CHM; void help_copy_impl(cliffc_hashtable *topmap, kvs_data *oldkvs, bool copy_all) { MODEL_ASSERT (get_chm(oldkvs) == this); + /**** FIXME: miss ****/ kvs_data *newkvs = _newkvs.load(memory_order_acquire); int oldlen = oldkvs->_size; int min_copy_work = oldlen > 1024 ? 1024 : oldlen; @@ -285,7 +272,7 @@ friend class CHM; copyidx = _copy_idx.load(memory_order_relaxed); while (copyidx < (oldlen << 1) && !_copy_idx.compare_exchange_strong(copyidx, copyidx + - min_copy_work, memory_order_release, memory_order_relaxed)) + min_copy_work, memory_order_relaxed, memory_order_relaxed)) copyidx = _copy_idx.load(memory_order_relaxed); if (!(copyidx < (oldlen << 1))) panic_start = copyidx; @@ -309,6 +296,7 @@ friend class CHM; kvs_data* copy_slot_and_check(cliffc_hashtable *topmap, kvs_data *oldkvs, int idx, void *should_help) { + /**** FIXME: miss ****/ kvs_data *newkvs = _newkvs.load(memory_order_acquire); // We're only here cause the caller saw a Prime if (copy_slot(topmap, idx, oldkvs, newkvs)) @@ -332,7 +320,9 @@ friend class CHM; // Promote the new table to the current table if (copyDone + workdone == oldlen && topmap->_kvs.load(memory_order_relaxed) == oldkvs) { + /**** FIXME: miss ****/ kvs_data *newkvs = _newkvs.load(memory_order_acquire); + /**** CDSChecker error ****/ topmap->_kvs.compare_exchange_strong(oldkvs, newkvs, memory_order_release, memory_order_relaxed); } @@ -423,7 +413,8 @@ friend class CHM; /** @Begin @Interface: Get - @Commit_point_set: Get_Success_Point1 | Get_Success_Point2 | Get_Success_Point3 + //@Commit_point_set: Get_Point1 | Get_Point2 | Get_Point3 | Get_ReadKVS + @Commit_point_set: Get_Point1 | Get_Point2 | Get_Point3 @ID: getKeyTag(key) @Action: TypeV *_Old_Val = (TypeV*) spec_table_get(map, key); @@ -443,7 +434,14 @@ friend class CHM; TypeV* get(TypeK *key) { slot *key_slot = new slot(false, key); int fullhash = hash(key_slot); + /**** CDSChecker error ****/ kvs_data *kvs = _kvs.load(memory_order_acquire); + /** + //@Begin + @Commit_point_define_check: true + @Label: Get_ReadKVS + @End + */ slot *V = get_impl(this, kvs, key_slot, fullhash); if (V == NULL) return NULL; MODEL_ASSERT (!is_prime(V)); @@ -453,7 +451,7 @@ friend class CHM; /** @Begin @Interface: Put - @Commit_point_set: Write_Success_Point + @Commit_point_set: Put_Point @ID: getKeyTag(key) @Action: # Remember this old value at checking point @@ -612,6 +610,7 @@ friend class CHM; MODEL_ASSERT (idx >= 0 && idx < kvs->_size); // Corresponding to the volatile read in get_impl() and putIfMatch in // Cliff Click's Java implementation + /**** CDSChecker error & hb violation ****/ slot *res = (slot*) kvs->_data[idx * 2 + 3].load(memory_order_acquire); /** @Begin @@ -674,8 +673,17 @@ friend class CHM; // Together with key() preserve the happens-before relationship on newly // inserted keys static inline bool CAS_key(kvs_data *kvs, int idx, void *expected, void *desired) { - return kvs->_data[2 * idx + 2].compare_exchange_strong(expected, + bool res = kvs->_data[2 * idx + 2].compare_exchange_strong(expected, desired, memory_order_relaxed, memory_order_relaxed); + /** + # If it is a successful put instead of a copy or any other internal + # operantions, expected != NULL + @Begin + @Potential_commit_point_define: res + @Label: Write_Key_Point + @End + */ + return res; } /** @@ -686,6 +694,7 @@ friend class CHM; // inserted values static inline bool CAS_val(kvs_data *kvs, int idx, void *expected, void *desired) { + /**** CDSChecker error & HB violation ****/ bool res = kvs->_data[2 * idx + 3].compare_exchange_strong(expected, desired, memory_order_acq_rel, memory_order_relaxed); /** @@ -713,12 +722,11 @@ friend class CHM; @Begin @Commit_point_define: K == NULL @Potential_commit_point_label: Read_Key_Point - @Label: Get_Success_Point_1 + @Label: Get_Point1 @End */ slot *V = val(kvs, idx); - if (K == NULL) { //model_print("Key is null\n"); return NULL; // A miss @@ -731,7 +739,7 @@ friend class CHM; @Begin @Commit_point_define: true @Potential_commit_point_label: Read_Val_Point - @Label: Get_Success_Point_2 + @Label: Get_Point2 @End */ return (V == TOMBSTONE) ? NULL : V; // Return this value @@ -745,11 +753,12 @@ friend class CHM; key_slot == TOMBSTONE) { // Retry in new table // Atomic read can be here + /**** FIXME: miss ****/ kvs_data *newkvs = chm->_newkvs.load(memory_order_acquire); /** @Begin @Commit_point_define_check: newkvs == NULL - @Label: Get_Success_Point_3 + @Label: Get_Point3 @End */ return newkvs == NULL ? NULL : get_impl(topmap, @@ -769,7 +778,14 @@ friend class CHM; slot *key_slot = new slot(false, key); slot *value_slot = new slot(false, value); + /**** FIXME: miss ****/ kvs_data *kvs = _kvs.load(memory_order_acquire); + /** + //@Begin + @Commit_point_define_check: true + @Label: Put_ReadKVS + @End + */ slot *res = putIfMatch(this, kvs, key_slot, value_slot, old_val); // Only when copy_slot() call putIfMatch() will it return NULL MODEL_ASSERT (res != NULL); @@ -840,6 +856,7 @@ friend class CHM; // Here it tries to resize cause it doesn't want other threads to stop // its progress (eagerly try to resize soon) + /**** FIXME: miss ****/ newkvs = chm->_newkvs.load(memory_order_acquire); if (newkvs == NULL && ((V == NULL && chm->table_full(reprobe_cnt, len)) || is_prime(V))) { @@ -862,7 +879,7 @@ friend class CHM; !(V == NULL && expVal == TOMBSTONE) && (expVal == NULL || !valeq(expVal, V))) { /** - @Begin + //@Begin @Commit_point_define: expVal == TOMBSTONE @Potential_commit_point_label: Read_Val_Point @Label: PutIfAbsent_Fail_Point @@ -871,14 +888,14 @@ friend class CHM; @End */ /** - @Begin + //@Begin @Commit_point_define: expVal != NULL && val_slot == TOMBSTONE @Potential_commit_point_label: Read_Val_Point @Label: RemoveIfMatch_Fail_Point @End */ /** - @Begin + //@Begin @Commit_point_define: expVal != NULL && !valeq(expVal, V) @Potential_commit_point_label: Read_Val_Point @Label: ReplaceIfMatch_Fail_Point @@ -893,7 +910,7 @@ friend class CHM; # The only point where a successful put happens @Commit_point_define: true @Potential_commit_point_label: Write_Val_Point - @Label: Write_Success_Point + @Label: Put_Point @End */ if (expVal != NULL) { // Not called by a table-copy @@ -919,6 +936,7 @@ friend class CHM; // Help along an existing table-resize. This is a fast cut-out wrapper. kvs_data* help_copy(kvs_data *helper) { + /**** FIXME: miss ****/ kvs_data *topkvs = _kvs.load(memory_order_acquire); CHM *topchm = get_chm(topkvs); // No cpy in progress diff --git a/benchmark/cliffc-hashtable/main.cc b/benchmark/cliffc-hashtable/main.cc index 3e52744..7e7a305 100644 --- a/benchmark/cliffc-hashtable/main.cc +++ b/benchmark/cliffc-hashtable/main.cc @@ -55,8 +55,8 @@ IntWrapper *k0, *k1, *k2, *k3, *k4, *k5; IntWrapper *v0, *v1, *v2, *v3, *v4, *v5; void threadA(void *arg) { - table->put(k3, v3); table->put(k1, v4); + table->put(k3, v3); //table->put(k2, v2); //table->put(k3, v3); /* diff --git a/grammer/spec_compiler.jj b/grammer/spec_compiler.jj index 37749aa..43faebf 100644 --- a/grammer/spec_compiler.jj +++ b/grammer/spec_compiler.jj @@ -66,6 +66,13 @@ @Label: ... @End + // Commit point clear (just as a normal commit point, but it is used to + // clear all commit points) + @Begin + @Commit_point_clear: ... + @Label: ... + @End + e) Entry point construct @Begin @Entry_point @@ -122,6 +129,7 @@ import edu.uci.eecs.specCompiler.specExtraction.InterfaceConstruct; import edu.uci.eecs.specCompiler.specExtraction.PotentialCPDefineConstruct; import edu.uci.eecs.specCompiler.specExtraction.CPDefineConstruct; import edu.uci.eecs.specCompiler.specExtraction.CPDefineCheckConstruct; +import edu.uci.eecs.specCompiler.specExtraction.CPClearConstruct; import edu.uci.eecs.specCompiler.specExtraction.ConditionalInterface; import edu.uci.eecs.specCompiler.specExtraction.SequentialDefineSubConstruct; import edu.uci.eecs.specCompiler.specExtraction.InterfaceDefineConstruct; @@ -373,6 +381,8 @@ SKIP : { | +| + | } @@ -885,6 +895,7 @@ Construct ParseSpec() : LOOKAHEAD(2) res = Potential_commit_point_define() | LOOKAHEAD(2) res = Commit_point_define() | LOOKAHEAD(2) res = Commit_point_define_check() | + LOOKAHEAD(2) res = Commit_point_clear() | LOOKAHEAD(2) res = Entry_point() | LOOKAHEAD(2) res = Class_begin() | LOOKAHEAD(2) res = Class_end() | @@ -1120,6 +1131,25 @@ CPDefineConstruct Commit_point_define() : } } +CPClearConstruct Commit_point_clear() : +{ + CPClearConstruct res; + String label, condition; + ArrayList content; +} +{ + + { res = null; } + + (content = C_CPP_CODE(null) { condition = stringArray2String(content); }) +