From 3833bb98cb3a8255344e442b66b0fa2175ed8e32 Mon Sep 17 00:00:00 2001 From: Yu-Ting Shi Date: Sat, 29 Jun 2024 02:52:18 +0800 Subject: [PATCH 1/6] Add new subsection "Memory consistency model" --- concurrency-primer.tex | 68 ++++++++++++++++++++++++++++++++++++++--- images/hw-relaxed.pdf | Bin 0 -> 71764 bytes images/hw-seq-cst.pdf | Bin 0 -> 13771 bytes images/hw-tso.pdf | Bin 0 -> 19746 bytes images/race-free.pdf | Bin 0 -> 7059 bytes images/race.pdf | Bin 0 -> 4553 bytes 6 files changed, 64 insertions(+), 4 deletions(-) create mode 100644 images/hw-relaxed.pdf create mode 100644 images/hw-seq-cst.pdf create mode 100644 images/hw-tso.pdf create mode 100644 images/race-free.pdf create mode 100644 images/race.pdf diff --git a/concurrency-primer.tex b/concurrency-primer.tex index 37aee7f..ae136ca 100644 --- a/concurrency-primer.tex +++ b/concurrency-primer.tex @@ -1090,6 +1090,66 @@ \section{Do we always need sequentially consistent operations?} \section{Memory orderings} +\subsection{Memory consistency models} + +When a program is compiled and executed, it doesn't always follow the written order. The system may change the sequence and optimize it to simulate line-by-line execution, as long as the final result matches the expected outcome. + +This requires an agreement between the programmer and the system (hardware, compiler, etc.), ensuring that if the rules are followed, the execution will be correct. Correctness here means defining permissible outcomes among all possible results, known as Memory Consistency Models. These models allow the system to optimize while ensuring correct execution. + +Memory Consistency Models operate at various levels. For example, when machine code runs on hardware, processors can reorder and optimize instructions, and the results must match expectations. Similarly, when converting high-level languages to assembly, compilers can rearrange instructions while ensuring consistent outcomes. Thus, from source code to hardware execution, agreements must ensure the expected results. + +One can envision hardware that achieves sequential consistency as follows: each thread has direct access to shared memory, and memory processes only one read or write operation at a time. This naturally ensures sequential consistency. + +\subsubsection{Sequential consistency (SC)} + +In the 1970s, Leslie Lamport proposed the most common memory consistency model, Sequential Consistency (SC), defined as follows: + +\begin{quote} +A multiprocessor system is sequentially consistent if the result of any execution is the same as if the operations of all the processors were executed in some sequential order, and the operations of each individual processor appear in this sequence in the order specified by its program. +\end{quote} + +On modern processors, ensuring sequential consistency involves many optimization constraints, which slow down program execution. If some conventions are relaxed, such as not guaranteeing program order within each processing unit, performance can be further improved. + +A memory consistency model is a conceptual convention. This means the program's execution results must conform to this model. However, when a program is compiled and run on computer hardware, there is significant flexibility in adjusting the execution order. As long as the execution results match the predefined convention, the actual order can vary depending on the circumstances. + +It is important to note that sequential consistency does not imply a single order or a single result for the program. On the contrary, sequential consistency only requires that the program appears to execute in some interleaved order on a single thread, meaning a sequentially consistent program can still have multiple possible results. + +To enhance the understanding of sequential consistency, consider the following simple example. Two threads write to and read from two shared variables \monobox{x} and \monobox{y}, both initially set to \monobox{0}. + +\begin{ccode} +int x = 0; +int y = 0; + +// Thread 1 // Thread 2 +x = 1; r1 = y; +y = 1; r2 = x; +\end{ccode} + +If this program satisfies sequential consistency, then for Thread 1, \monobox{x = 1} must occur before \monobox{y = 1}, and for Thread 2, \monobox{r1 = y} must occur before \monobox{r2 = x}. For the entire program, the following six execution orders are possible: + +\begin{verbatim} +| x = 1 | x = 1 | x = 1 | +| y = 1 | r1 = y(0) | r1 = y(0) | +| r1 = y(1) | y = 1 | r2 = x(1) | +| r2 = x(1) | r2 = y(1) | y = 1 | ++-------------------+-------------------+-------------------+ +| r1 = y(0) | r1 = y(0) | r1 = y(0) | +| x = 1 | x = 1 | r2 = x(0) | +| y = 1 | r2 = x(1) | x = 1 | +| r2 = x(1) | y = 1 | y = 1 | +\end{verbatim} + +Observing these orders, we see that none result in \monobox{r1 = 1} and \monobox{r2 = 0}. Thus, sequential consistency only allows the outcomes \monobox{(r1, r2)} to be \monobox{(1, 1)}, \monobox{(0, 1)}, and \monobox{(0, 0)}. With this convention, software can expect that \monobox{(1, 0)} will not occur, and hardware can optimize as long as it ensures the result \monobox{(1, 0)} does not appear. + +We can imagine sequentially consistent hardware as the figure \ref{hw-seq-cst} shows: each thread can directly access shared memory, and memory processes one read or write operation at a time, naturally ensuring sequential consistency. In fact, there are multiple ways to implement sequentially consistent hardware. It can even include caches and be banked, as long as it ensures that the results behave the same as the aforementioned model. + +\centering +\includegraphics[keepaspectratio,width=0.7\linewidth]{images/hw-seq-cst} +\captionof{figure}{The memory model of sequentially consistent hardware.} +\label{hw-seq-cst} + +\subsection{C11/C++11 atomics} + By default, all atomic operations, including loads, stores, and various forms of \textsc{RMW}, are considered sequentially consistent. However, this is just one among many possible orderings. @@ -1136,7 +1196,7 @@ \section{Memory orderings} let's look at what these orderings are and how we can use them. As it turns out, almost all of the examples we have seen so far do not actually need sequentially consistent operations. -\subsection{Acquire and release} +\subsubsection{Acquire and release} We have just examined the acquire and release operations in the context of the lock example from \secref{lock-example}. You can think of them as ``one-way'' barriers: an acquire operation permits other reads and writes to move past it, @@ -1201,7 +1261,7 @@ \subsection{Acquire and release} } \end{cppcode} -\subsection{Relaxed} +\subsubsection{Relaxed} Relaxed atomic operations are useful for variables shared between threads where \emph{no specific order} of operations is needed. Although it may seem like a niche requirement, such scenarios are quite common. @@ -1243,7 +1303,7 @@ \subsection{Relaxed} a \textsc{CAS} loop is performed to claim a job. All of the loads can be relaxed as we do not need to enforce any order until we have successfully modified our value. -\subsection{Acquire-Release} +\subsubsection{Acquire-Release} \cc|memory_order_acq_rel| is used with atomic \textsc{RMW} operations that need to both load-acquire \emph{and} store-release a value. A typical example involves thread-safe reference counting, @@ -1293,7 +1353,7 @@ \subsection{Acquire-Release} experts-only construct we have in the language. \end{quote} -\subsection{Consume} +\subsubsection{Consume} Last but not least, we introduce \cc|memory_order_consume|. Imagine a situation where data changes rarely but is frequently read by many threads. diff --git a/images/hw-relaxed.pdf b/images/hw-relaxed.pdf new file mode 100644 index 0000000000000000000000000000000000000000..a9a0c2ccae1ad63a9ef443ca5c06247c7153a74c GIT binary patch literal 71764 zcmcHhWmuJ6*9HnpcekW;x1@9^(xoDu0wNMiKtLL#L+Ox`R8YD_N*X~zTDn2$RQ5oh z`~AM(`#82gadEAA%^2gX35%AZGLHbSC^pN&;@4qpAqIYirxy0uw{Btc={y*@HOyFMAHt*z)wL_df zw*&uPO488m5Yq%G1OzoUyKlZYqqSkll}uCjy__SldE{w7S)5nT$s7c~BSwS&a`B#C zsgc24?M-%zipNwh+vaNtY}_|!9+|oEEW!tl{g2=6;PIK_zib<#nEg;M+UPA#gMZu9 zqj_WY*WNOG;>G;$Vz0K|BzWFI@c-KnSDcNSHv2Sv{I$|gz1lp3DeZkCYkKhe+`Yp3 z^wO!R8^(HOaj&`FrvJLJY1UzrxD zr;)cF+T7_n-CylZVRsdA^2OY{lly6E$t}d^X=2{E~nk9Rs7+`+M%~m|tBr zPk+4kJv&$*?uejpZi}Ipp<&zGU;TH9C8o`P z{`@}Q?QHTouAN9xa;2PS9+Gaq@K)<)3xxV=cjvl_FfN5MPcKx;m%`wx=vQwjitS~)}yhf z7fC7LBqbMs`u&6H@!p<=yI|9ESl)OJ-G^*wSzE}+$n8ZpXw%%k^$!-ms%iGU{G^c~ zA@Wnx#(z^CwxqL{+V`|b`C#m;6@@v}&Q-RiAfUU&?!#%)=usP5M<>}pBxKX4mLfRh zxxU<+G$H)as{2*Nqp!1{UYyUh1TJ>Qe67qDtNIc}y=XB}ZrvG0U1Q!B5{yG3V)rem zsb050gE-~#Y?JSZ%cdwp(*0BzLYzbp33k87=eti({&=kV|_FVmtu^v0(*63^_9Nb_GV zWbzB;Z5HX|mHVv!nr~bGF7a$bjQr13%~R)v_Og5B4(C-)^Q~i={TY%;eHUjz-VJaAVC(X(?m1*Q`b^aB^NcL@yZ;gr z5>j%yO;3E7qe-;`m9g*f4(;nl-%E|h2++~dzs+)ePrE85v+(fClSP6}(`N6}R-Iap zUB-qtHx$sldg6G#k#j%z7)+a{m94YFjBFx)j# z1cP^s%B`@BRnkOCnm(+oYC(BpyG5vcxH4JwnB};_TBop@@rdJLC3^~Slh5zeenNo= zhrz5Cs35zga60c5YRTn@vZ*D@-Y>W5xBvO>zxkh9Q?KTz^ZD&5F7LMfEqF&WRd^i+ z+aaU>!NfR6bXTIDu}qh^t#RVNO)<6B-;=;KtO;c#iOFgpU3~q|?qa8^PqALnE5)a8 z#9c#P48azAuX}#5P9hoJ`mZ1eIOd8@=oHt~)HF9YTVgf){Jt(=p;&*}9!9c|2`3?$ z{zks2v+s1R^SZ@M{j(C1bctu2=Sy|2s}ep9sQ(==5zqa$mjr!=@^OqxbTU2;8Tk*A z6~l;C;+f!Z;ITGlX3{sz7HHDfQ{Ipd8p^#LK`-uo@^O6q$JRu}lhp{?e`SI{2ws~1 z@fi1!341vlx&AcKr?4|m+<(orkZPsPOlQfV)C(y`QVxbCKiiqCir_gS{(W|6c`V~~ zq_$O3s8^)JbURwHC+hmmoFXog@%-DK82>7xIi~x!G_$SovH%5GI~8}6dPJD`4-yh7 z&x5_?-r*m_oqJGQtnM`s7wf+hahw)A^Xf|$2rrNLw|^BVhd#{Kxw7ds)j7^cbb7+! zPDTWZDL+W$HlW$;CybyEOuhNId|OqyC!PZql@~wE1$MDbuqx~ZTFl+SKC6!{w_&cw+O{c3&gBcs3 zcMN1m9&b-!{66{f+sn)SlgF;bRP_@{x2@Xe`}uwC+1@d9QrI&u7TU2eI2w?59)5yz zVM*R-`s}I4>EB-S%V)G{e!2Imp|zgtABQCIUG*)TpZ8~|O|Cwi%lH4?hmqN6{%h-U z#6>BKKCnz3TMxfnA%Ql#$x4p13uqpxJfVV6xy`FFVK{AAF~Sbxgr2U;Jqb2AIex2O zGbuQ9+8sEqumcI*DfFFeQ78nDs~NBYn8V`&I`XdDt@|Vby4elS{{}>q<81BZit37qwnVxV6`#Y>p?8f!Nq=PMi z82#jmMGWC}CcxeCrI*z#OO3+3fV*S-bKu~Mr^Zl(8T?$UU zLbGbb-wEfl>Q5yrUfmddXM;nGUHQi0btn-NY_wJfBi2$+I&d$!V*}f#c%n3o*fB0-hv7GvxYZ(A6 zU{Q>bQBazinrJuGoi@jKDp;=YT=e;CZUaH~3^vU-$?%DL?;j8qe?$HB>649W&(-W4 zvuWojYDttj+}F)f#1i+s0t^55U(j{6BmgrA7!poRe|ljU{f!x_hjn%1)tfoHT69L^ zMeW1MsX!}J*U}mU@bdfjZ~9vvPEg&cMIE7qvp`Xaeg5Oqi_U1;^VLk>qn|&Ty^eRb zr)nB%pOIX>;Pf?@R+4I?(YV=*gZ0<{?KPsC_Ihg!YMXuJib!wXyonX(=O1*C`@0=> ze*OC8hktgu4||E7LFetA*p%B>t(7Kv|3<|1iaagl2k|LayTb8WzJr!*@~0Fy0gX*f zB+Pfrs!9K@i90Gfy8Kh+sOzH+a`Dc)3mv^ld}%yrf9IPPmOo@Rl1{4r-&kIfpnF{Y zkvgz}BG*s;7iXvQe})2@CA!!V@u-^N>WT9~NHAAOO)2c!j1_2C^NN4_(I?-_KbdHo zt`X4M+7CCse=w9eyf}5eI5=3>O|z4JzK7~5WKeE(7V%i*3N2p&UCT~@X0CtP_r#kxI5$d}BM5qn;vY-4RX(onv#h$tzvV*-60b zXv@5}h~a9KdJ6kJP~^k;VOl!4WZ>4pv9l@44E< z)YrPx0ZU*U$IhxH^JkwdL{RX-TKaD;eu)x#pnNsXT2z@IyjzTF&(SqXM8ATFDi_@!>QmXZ8Vbk<^3=U@nN-Wu?!qaQw{W zbkDjgo#{3{#_{-Y8tjzLL!G?4R2+X_+6c3JKSk1=x8W5$yHGn9%3>89k&`g0zB%kt zFHg?}0MdHVwtE zKi;a4oc)A$ck9-zyGguJ&1~waL75@ARPr)#a0o6-w6X&NM>H~}pET8PE&xPF7qqOL zo1;tnTi3hZdF(Doc^&ncQC$_7MNXqe52EYyF*1L$E&;+)T^{c5&{cp=g+HZv_6sD!R=@o z|2`l)?oI^j>V$xX++u~?w#M(58abz?|1Bv*_9KNzJRi;5&@VCoh@b2(3hhq{TKB|` z4g$K(RSav*&pQ%xn!C2ssT+b*LT}ZpSD-O-)=*jW@T}Nd^AB zy)2q6$HCUb>&9LY+d;qI!rmuNMh5i=4)q=h#M+!#5zN$FHDDEL?(%`HnFfmD!4^D` zW6|{kE}5WKILY&PI@n4PzidFy)s+>)yl^MzX8N^aVuQv#O_#OpX$)WJ8;pot<@Y zdh{yF77jFvOx!sGzt6>q*04c?8_&)a zy^JCn7T#J{f0%?nYV@~SLu2onyi8q)S;6@RY<2mT-Ov;h9f4kLH6=a((bDEc5>rdn{ga(Cd8$Dg5 z%l5BAYSdcpOxF#{0hI#0fEJ{b@^``LVqa)Ovw&8QWUg)V_f%jkd3MQ}J*Hsh?)lr% zkNt999j*kibmsf-jJDlY@5>H6*+mNs#2(@lOI; zVfzvG3N-D{uqA=R(@|2|{`YM_<}o~7p;Or4TZ_p++>WHY+Bg3V zITvukU>YpO)npFRJO@tkZxHEDw_yRZ1Mig@*}?Q+MhLpX!gNZVT!Fp7v43Fie?MjG z+Xa@Bt?)9MQlRzg*QXaJyRTs*OTX|eHLA-B1U_2nFj21m?p_I?yy1NHE3oXolRmLG znRl<`VeE4#-v4`Z(E`{g0k^Uq^plVAjuz_&2K~c@e-~8Tb#)*iSNMv#Zj5qO1Xrm7 z9=)*yVElg*;5Y!J7bpi!@$7rug6N4?5;@+ddxS1OXPf@_{Nn;>-`N}L6!%pC;7I?7fu!pjYD;EG($rc*ZtCD9?Yv_G@beR^Jf^F_+VNoeH*}t)$^lm zAw%rH>r2s9^G2OfIdbji&!^RXeZG-TxH2Xm3=H=zjS0X!HA5hdQxz zegX+^#QEAqHgXnbA30l}69`Do?xdoQ)8sr4x2Eg%VIpiIzRX|9lw0?*4y6^=*x<0> zAnsP!^b5kES49V#a$n!RAA>K$Ey6WS1(?13oy&4hAUa-8y0}p9)tj21lz|ckH7J#b ziLG&Qb(PI=2I{z=A!D6YS1b}TG{0|vt#_vlMaERqI zmA3j02Y9U+Mnx&@?Ew_npcD#VljBVNZLc^(Rb3KM?{%2(-wvW1J&ePeNaw9fuy(Wi9!&85Z-sXP(Lz%MXTel$LZ0+ap= zx!xKvu$E)+02MK__IW5u@`yxUU@V(7oz%gE^KGdCrkr1a8i zp?YB7ZL!sE6XrAh)GmgqdqO}j&F)DUxC;FN&a^ntC5N+^=`XU&^KCEDReI+~-Wyby zwFKCxX5&t3pIw|*K%JQ;LDa2z4E-+0yNT#sOCM6=GG6v$^po(@nX_@gPZoD&6|92; zRjey34PQgU0SK;adqw8*V)*OVpGVtM65&1ben9TU$OeOz?#NTQO;xQmlF~a zW?7c|`};#J0iIG+QzObXflDQbOUXY6xJu$vs3rTr&oANwoj`-*a3nMl*$DFF|BbQU zh}IPKnXIQjed@>V05qJ~Q^0x-bk}Pk3fA<7s&WEvt~F_4duS(55jx{*^riy{p_4!q0!LMO&1#*O z3Dk?8J`L=giwIo99bzfpAu?u>P(!2*7-dO?xHR$Qu|hJB%{}`NI0eD4i|7<@Tde8X|{8qaNFQ?fJczl)_e8Ko%PcH z29e4$aw(aEdDFa_fw#RtGqbU=k)On!gG~l1BsYk3*zaKcHodL?zh8YBAp70@il>4n zAbV3*PF7vkAekrPo$NromW~Y$V{qaVm<~tie_&LIH+mbRBHSzap&#nlk~0mXJ@)WR zKL(&T;UMR81*)xBNw2Cs_y6CgtuUADJEyW4f(GS%g6N@Kuv@G{6$XPr6djlHT9Jg? z7Ig0P%m2wWr6>|o@n{mV6=WxeDy1D?QZq z$U1V?z{k6@{1(1MMZCX~ndK6x6mVfQ#}dUm_8h3CJVk3eFXJwKo92XaEft*+YNe`r7lLn`UbMe62 zHC5OSK|JyM^z3jGKHMG`Qag(v7(C2ILCCqPv*X-B>wr<^x8S}3+s3AvyLo8e#+#^m^r2{FvO(~J`X34iF###$^9w)KaU`+?TSfKBz|YqVK&M!m01$!UI|SlFG!C^?tAXxvBq3}uAuy) zOJc33{@JEW)4Il>3I-xX!{a;9l_}tU?AkduACCoj3hAMv2A(+unDJs}5MLK_x|-cD zfQ1+pLkW2vRzi_X=D}IL%q=v9Lq;62X>2UfRykX@CpE5%ikpEq zywXlLQ~CvvZHm3-b*%4cjwt^f`s=?-Q84he&_1tmjihA@2L19Zr<*}ja#bK8+~{Yy z8xJ*T0Omh~Vf?MiYX*JbnCZWGqrFKFug+oKIiNPE3@^^S*1zSAxw~zQg!#-=J-+`X zl4|`YFcrferz`zw__PvMU*FJ@=+yIoZd7Zr&0hiCjglA?-E`*eG*LdoHg0h3sI`4T zAREk*TRK2djHE0BO9mgeH`@^Q4QH7DIGi4kryl-L6U>^Q`w4t0Up+06uFmt26MbX- zPiF$x{r8z29t>c>A===xTis0H1|0|9s>@atK2s`mfw^mI$hjT!=Wz3Wr>KH8W@2df zK&15wBaNgR?vFRX4z+$ZdL8ptajd?l%xY_C0C#0I$lZAf*2cKW^XAMCVA5n<_Xd9e z+lrkI>87Z<*QWwKS0mr^v&1#j{Jg?<0X$bO7a<|Tr<5%#IFUGcRN^jHo3|7BOryVt zMR`zpj7>HhfW!s50q{F3T|eOZ1DP_Wdw0O{`lTCyidAabJiu+N^3*~^y*U7Ap1~>| z^)o+E!MgffOGRf05P|HZh%gP0`%s&U@Et&&9Z4$^kPj1+<4?+ges+{vf-0=gqbVaJ zlbg4Iq+?93^qW(OmY6$#GMVjF9rsGutHL#qo${x^`;5LM=hO@R<8`p6z54_TLo_i9 z_U|B$d1$WCD5X7q&0SIFQI1cU>R19EUz(FQ%_k$W8wv{8jALje-2iRx-Ubn=`2L4k zSoOD`^%9(NAjUte#?0tA+Cq6$ZGmk*=l zNqD#0N$)$?rkNo@wvmB`O`3Jl2pV%g^&r_6XfJR)Cfj1QeGS3gh+20-+}3WEa9O%j zpBaFbby;w!ktU+v=sYdMAN1;qbYMggQD{Yi+zb zC*po8neCG=pA=x`i|LN>4w~Y4wQa@rhwEV?lelqdWy#m)^ldf1JWRx}=yiWyx-)~$%O}I;8 z7e_Aqcr3Csv>*@q(6cQ3HDM~hHx?8^R$a0b0^14G&6b_`_f$bFW@#?>$%Pj{fTGUl zP+kYhPa3@;=tcF}P)4>GhiB}*y)Cmlmh?Jus7KN@EAz2R@sn}*G(ZPCjYVUPEN%~o zM)AFp9=BhH;AL*;R!XDjTg2+|Vp8$aiMue5NJfxxDT{LmT(tQqZY{DvOYG~3lXWl9 zD+cPf*m5_4ljB9~A}SO{V5zz1DKfk^Tn*p@)$4rneqP^-A5hkvHSSMl_?G9vM>8C* z@oXjG=hXo{2lg(kG4aM^`S$ou78*co`*w=HI_>X%_*yv8tww61&ZxU8`~$6P+1$b2%cyAENE0d zev#*5P`DXNFY~ENE+7c{#A_EtHil2p+}2;Bx@zEI>g#0ZF#sC3WXh1KN;c0!v;i zHMFE1?2^7LuMw6i0DT}y(&}pn4#zpoeMahBmwgfY42d+HH=s@oRF;!*P`HCV*$nUY zypd`+F`||61kI`P$b%Bg9+bj_s)asn8IeZkmdj9z3|V19t#j;$QlM+{ciQFcBSOMqmy zmYynENS5>y@GY`uySIcUw5D+F3GeyvxcAP z+o*Gjl-YC&X&)!El!&!5JgyLCV;RQ|@vfnk*yzWj78xYN9oT*{QBicQD_EQGW@F z6vBuLLIK&HSxO3DGPKz3r8(4`&ySw8ShUzatx(3@a{}q6OSbF?EO8|DUmf=diNC#7 z38W@wxyx+&5pew?(dn$Vn1-@;Gj@sMaYP1-;N>=D{x@zNV!=o?43;)F30o`>yZH9E zB{tN{>b8IiTJArq{LOsvDTGP)X-?}fyvCzPJNP3{c3qp+zi3Ixv2pDC6!wDBk)t!A zmjui9-n3a7J!j#yF0M^FgShe&ym-tfol^&90J>TvY+Be~e*P@0h6-XjOZNqUvW2qMHn~)6Da2M=~yZQN7vT-`UIkK@LPF1yERamqq zm`<4vT+QHpj>V))zes%n>V)fiYp3_39bLtUj+VB9l&HBnbZ03kDJXM}w8C=8dRW_a z1BA?ZYD)J>|lFeoH)brbND{1xODsu0Azkz zwj;BQIcHDbDM*bhrwJlIRPa=Mu1mVTpCc@zs{Z6jVrJ6E9aPeS@aTTU^6Kpp@`b-X?%iKv6ik-()Q&>v*`?^duEJ4ec3b>Fja+#%U4Tz z-$o`UCD3H|q%nNL7N)LaRwNXnPi{YFjnjqHIze!RzCKp2o+&+(KZ{%D!Tf7~-_pDm zE3!Mg#KG|aKh@Hj`bt3|nCRKF4g}S+5g)X6YwJ8oI$mx>-PItsp6onw#47R1YD2U( zWJwfgWQ04?@C@v#c(aqvyIZ=rFTjDM><7PQqB8qiFmRRfTC(%wpGl{r83t`Ztqeu2 zyzCr;NfvDJ*;+kGd@_#)XfV=x(dQZW<3JJx(G;>`Bo(h9FvNjJSCRocfkw>f+6xN3 zkKttekNJCTRyv`^kG;u~P~$Mwv(&TEvs;j_XvcJKG{+6;!IqJCC>f#vspf!SHAje*x{KVV6-cPzzvH zipK%#)cc{qa%Q0G0aIWdZr79K%@Li6oSU12daE;=>g6$!vK(lQLHyQ5PA>*=t%xpR=zMUDf^xiwO-^WojT-XXPj!0gab6R zV)i9rCEudE{qYcuAhqR&>L9Rc+- z3s=}eZao#t_SRO?*6!eatQDo5qMg^_*hxzDIY@L+ADgk}>-9SC)AA1=o{qgYcv9R8 zBJ53v@hdEyP3PnPkSKnuKbQ>o-uC=F5k%`&KRgx>kv|Ck?cs{KBK0Ldy9+27xMBw2 z>^RGIgAxTUM!2`cI{x>xGXO9|WfVzrf#@k*G0w{o*kSfzJ>Ame3FP_|WaIh22{QJT zmhThkb}QcdV6q(~t3fKJxfQB|242D@Xvy`6b%)|!$b*SIo%IIgdk-%*>t2>omPM9r zCFY7fR3;26oho~M5J93~#)Gg(uo?OCY0$-yFh`BB6i(EO1h;P&;y4A4M3g;BCo_jHskOj&(24*bxj|!!n+cyr zjA2}2xfAR3M_B+gn65_pKm}Z)w40AZ<{2MjQtE)JPSB>hz30?a#Ketj+a5{;R$aPN zIfLE-r>UNZp7^d2IvMe(&d^0LuGt`JWv?YW__kLKrQ}pGoYW57cMT7YU^nZbWBDt4 zczvXZ#FdJtWojzT?wgqN0w@xblY_?iTD$?YBxn5Cr@pdfpPui3X?X(S)NsNZ^8UzZ z5I!t8BTQigd(rPb9ViDRvt-quV`D}#!dEUVk?m9HdFj;FQ-5B=RL1O!&4=yu3bW&jKR(G* z#Z_p!QiRbNuVIcWZIV0oJxG{QlM= zW%|i`cW;mQ5qEKWR~!@GBsWf3WfcJKc_ntiKocUj8?Hq(;x4u-%wl3EkVH%#VAgz- zPR13IvC$X`bIVtnPox*mS4_zH%8ECzCxr85c!BeBinrXF^|f3+P%JjaN~kmN+kTmW zyfEM`DWTR#kx|emz@LBl9+9PhflCRI9JI|TEfeq|a;BCPd&@&;xGO#%m}fNqIm5{m z0(Ao8n1QW>+RCEbsvDfSIWV@?xke%V5bFUUhXeI7DF)Xf$ab#3x<2_GycmH-(oR3v zNIsyR!4&fhKV|`J8g;R!6f9RIx19a4W8oC1IAsG353BGZzy^hqY5da*N%eQ&R)z`$ zatw1lG*F`8TwMV;vD%aHcx^B{dmt3#T#b;k4SX@#jyZ!uYO=5O*GV<;lp=3Adp`o` z4Jpxwm9{r#8Ax998rK7UoQ$k1LdG4BwE;o-nF@~{zld8vRT{6^9LP$H^T*@yp8iP0 z=;;f2)K8!O1TQz}I?I*T!8)?1bSTRrr=LBjojqVG9MHq}pm93QQJ}-)Xv+Ya%UT-_ zDZ5$w{a(}=Rx4SGVy~XJ;8sMxxA;oSi5`x=!K(M6y7Vh}wQ&R>{ls2&fpE&N`Sg1! z?cwa0S#2<*q|ZfdBB#25Zu%Spn*7oFFdM{G0y+|GA?s!AjrIq+z3^Ru1D>@c{Or%I8h!x5bR1-8y6C=O45dm5<@kD~LnskB(M z1k&l*!=XgcsHIN>FNvxjgz9tUE>~=UDmMZ})1o6BI84tg7MylqxQXLw?_6(*WbL;% z493}OZa@P8yhWZ_`Q&?PM*Z6?+dH&{l6?z|4&xt@O#S!tce&9M<6nAQOxL---^dXp zpydC&GH-C2s8`wS1`UQRfCIVJ%gZYwP!0A0CqxGdFJMA$FKecWJb^j|5IWLcx6*b9 zUIT(*Q?^AkKscOR{KzPkZozf{FB?ua@%if-ag&8wDvQgF!fS=-D-xUeGc+kgSa<>b zt?eKc61^5wI~z=ZWh9VN0l_qRCPTtYPbq7kl>5B5SQkQ>=Ky^nU*6W*MZ88lq*AOw zZp=&UzoDHGunukLS|-1FD{3Br#el|`T(a5Z^wMu2_2XrhDTX$OQykVyG2$hcx zBx}SPtw^L8RJn@X&u}TSxd4xrq@j=&*12I?@dEeYBe6DXgiP?Ci_(Y29?wNGt(% zDa2ZAUpv^?+_n#}V+m5q4ZV7^?*v0YY@+J%cVK*=mH<9dYsm(JV_B&eosD!a(~&a@IJ|Q(r#zBC9(d9 zjwi?Ob=n~S=_%_@I?xqMt@HCq5!oIb^|~p?KOqRCi>~(i34RJBAR8cbu-zG+?T8wI zW;5=>*9WDu!EE=iWWits0~dt{qsBZxQ`k;N&U}y_d!0*0w!of!t+0MEiRm--2;_ig9SzU z<=B&7{wHeQ?}u-F4V9ahM<=b^H{HI*gll%N0P_K5=WW6^D8`^-jC3P!P1VGFxfJ~Q zbT~gs{h7Gu!5WCF6W)r(w-u!?vibUtyaQ4hb(i*5>mo z>g-~pHQ?+O|Io~gfs`IWpJ9E`7QG;>e(Rb%0qql1H>*ggqTl0Hl#M#RpvLH_4~ zpuRkBZ|^?xB~kEDsJjCsh7n{Ca0VsXLYbP1osyng&(tli@*ahLAldhnJ4er!@ zT$Jp#Z1i^j1pT7@H*As(Q1W0Rxb%ymDjV`|wIuU^CR!K;=4U7w7kR~6g>v)_Ud{yO zd-%ldo7Y7g*u^@SRnS1?c*S7|m>d+y3fS^&cdE=Hv6PxO>cQRl9xy*6yo}pJ7)Xn zBTsNaw0rmE%!Gh|fQ;*_mV^g6cGqaSN=Od?O0?b$|N73WXrEgYZR7zs`O2(G0PvGi z1fR>#0+fIdi-QDBVjIARWnUcD0syD^9p=g)2tk07teAl15wbX1#Cd~Of1WLdTrAN` zV+ziD?`;w8;VLx2(cxw-Hrb2y(QXNd!ALDVJSQP9t(h|0w7Fp#Z?WG&+=3&v{ewuv z!wIhvDL3r2gfU#!*jy93#j@PNWl@rA*9kq@~VoMS1LB- z2?mSE3vciQh-U&?l-~jkuTUc!0?6FQ;4wN#<@&;og<`dio?`x;Uyp>_$If=_7esM4 zUX#T^B>3689SCcD{u~+1PspusmZKB_R;fYfHs|Qc*%|g;UtSjt&dKR170)Pi3OEws zk;IwH0s+8%B&4@xkr3?iMnP_pG(vrukYN|W+2_#MAwkpUAyUfH4z%bJD#Q_ymRuHYqy;-F&a8st~4qf{TWaoXe|;*-z*_jxa9Z%{4U) zO!NqxfQmk)!OL-OXT(Zjcs9CZB9`Z^kq2e7dRE<<1%=6GckX^DtU8hP&bO*c^zR#5 z=83+6!cSViK`K9*@QQ#Na8{w+E2PMcQ6b~cgQ=*A?NKg%J9O0iGoMi_phb){kyPeO z_*{6TgvlBYBnv2bOH3gp`&&4bE_`OtiQmOdP3;mhZ}j zFc_v=T1dIBsI>?VX&sCJPX7MhVEEGuFN_(b)*vkEoAyEBiq1ak7Qir;0u#3k9_a$Q*;Pb?{71H+ZeZ+Kp2C}!!Phb#zpm9qX%bTZ&`1?l2_Dyy zm8dpilO?xJ?s%*TUP>06n4{xT0h_B#+w23Kk_NhhX4m>w5~b&RX!*_)kK%G(~MbdpEhh`WJrO7b|xXKs{yC~ z1v7&|6EpMAcHACps|Z(o^qj0+Wzzb-iQnK#(5&4RK7xoRvj9K81#WU zY|Z$Mtj)z({(1)ea%6YY2x;UiEmD-re|{hTa3fv0RH8AEhH+AQ28-)HdThHHl%gu` z$2dK|0(qg(4@@NNiKS-F24VQ*_Xi(C@-{&oWAHHqwN2v8^vIQezJGD~hgLy1^yQ}j zbQDB%!l0@Fjf~IqY)CYtFaB0&A}VufQXQXk3XAI4Ru{PyemN!;i_k!=y={`g09IV= zrMk(lZNNBzg+Oe|cEX32zlj?#0+!E@~1MO?q3uj<6%ojn)>-D|M0eNAjU2uy!Y5L{X;o2+(#Z;wTZm%H(*HRhekiA$% zyYx?0${1t)+IO+HLmr@R^Zq_v&2)GW+IOQu$BIHwJ*j3KwS(tDfM?fqotW!NWWT<& z1$eLsr$BbY>h~LHk0hS+{J8ez(7Dl>!&lkwqF^XOsOh2`$sW@bHNmQyAzPuLY$N0o zD66Tt&n}U-QzwinixYpRFL@8*i z?Bjw-1N_YKjV57>KCDr= zX_n0Fd)X@hWs&rKwK`QeGW~eO9o4W!rFzUrKx&4Yx2;IaaZ+q-ZOtT9-wo;PfMK~* z9=ZG#xN}wIJ?{oHaj_yL&iixFTVAuOb86=Vc_4voatn+j-Ho>ya;213Z!qEmdCApD zXH*)3i-(MAo#eD0|Mr684QYbOEfUn;lM3*vfMV&m)A&te%k_8rEF2;>jA<*t() z3voXP0Jj#V995$jg~RQLY}MU^14QF@S?{w0ti>n07WkEqpb-`#0ag7r8whN(1rIRW zD?ZAO^F-H14YU)&@&opVm4#9aOHmDbHhczkEhfo`z}Kz-wQRt=$|$CG4a@nVIKJ{=CW zgCQAWZ+DRLf+u$I`YFDT0(ZlW6ZTEQLj0p>JNfV()fFxvuX6rNdg%rDWWtR0$>2mP zcfNY{Fc*lNLu=mxK&ZHuCskqkG1QPuwp153Z)ApXV*d+p(4m4p!m=a zVyf|nLj{26L+Y=GP|?t~r|T-f+_q@Lovbygu!%D1<+zc^Vv6{~Ra456A!u zIwUAjS+))w=slPml&i?{6l?FxE@Dk^ZCFC@4pe7%xAE9ah|u0Od&?}e3ssk+-n0*{ zGIk#i0gJVk4)8w%EWZh+zXp5mOAcU4?M_uN_rtnSA7cPU%3mg^mdXTWV2y=!_XN}3SK4NfEqg#ytXW6g&lOu`(&nroS=eC;M^ zB7(Nh%dHvt2jL#QxYL}UTz=%5*)I73)?IpU2*-hN$2=pctX?>da7ffzr9$tyqgAW0 zWL0X?#94TlugZ!6_f;PW@bQaMaFZ`mlA7ZN3cR)2)cy0&6M~semmp0f-0et)_!MY1 z3DSoE`XR-mSMo3+7C!!$&ty&Mfn7f-cfYOn{>Um&nE=^x zRK=P^O`^-y1Ncq``9me-;KdXH%aD_toW7*#$hW8yNE`@^i93chT@PM7k=Hs1Xe~N` zOAs9qv4f7BlkY8)ks>34MiZSNh&dz5yBvs5{z2i$)d6R&qY@W_nj?!NhT}a!|$fPc4`>IcwRUBM}83@jV#d9ZJlpxFHwfx;Waz?dS(e z|M1r(MZX@AHE~T@a*Y>WakSJ}vMev9rp6uW;K59-9%|7orRp&?pRrTGf*GZui?oB) z(v=0+y`qK8Ezzc0!`b|J$ppoc{POoSEqn(MOL7aRQOK!T&wJ>uFqHOrchL8iM;?Ts@_s zmRf-B0v+cvD8E5w&^q*w#n4q@Q%k$9;5M{gs6HM4=x^LEtNJmyyW8Qe2l;U>>4?g* zn&Xd8QWou)W#)lHf0k_vlq2fmY4}S`Y8*2z&LIS+tYFK-XWc0T;^~TnLOuk-!T0_i z8Xxz5GrjY6$ZHbIZH!yp&zXvYOv;JCB!Y7E2=2s}5J-az%Qn*4eNDMYUlyRp2+jTr zqT*)fH0q?})o)+&Hb?BS-tM($RHIz|*%K;8@o=R9sc~_A(BH#p86KL@BFN9K#UZXqkmmZW?V3#=W?W$pDiO~frH^QY6HkL0ebbWxiVaFp#=4VJZ6ek)+CjT>NBvPd{C4ZMDy<^^sHpa$;p9?2s7B^ zu_y>v^wxU#P47K9-VwgDeA9MNcIEdHk&;EQsw%q~+{;haTIx%A{l_p{9_^V<-Ad~s zBu-HyQr<<|S=4qM{bBC9rQqDRu9vMam}Ql{7c|!p=%jHNWs@E%MC0OSEJvuk-*ze9$v#cwn)ΨuNpQ}N z-zrF;zl;lsucL(o7=ARnQu<3IUqc)NG&Ifi#s@=1kJPA3GJ>w{5?{HWAT&8PIZwb+ z-XE`xCy+2~DQ9LM9t=j_vY_MHEmbzWujS@ocU?Sp(wWfDlXxU#PdF6xdRb~uE7OpYHQa}VT;?6P0Rh4gxDCwBw^=?6z^=N-mVgsbW(2Nrhg)Es z%ktj-zOKDJF(u`lmos{(N{qMTuXSWM1aqSO(jgTI9*3<4O3h;@CB?(O(=mp^8ThN&$!704#DBr9 zb_l6d{u(CnexUzmp#0BlB5};7m-l1E!=(lvl{aS_f~pZA7fRjE!IbcF=l($d+E+W5 zrR{AV6GiJ52Gj_DLPU^qkecteW2FlUL9y#En+ z=QtF+h)L}=h^VbEe`!JT2!^Bgu1klMFkD5;<1sK5u*qd$1#FaDD0dt8>emR_M<2KjEui~$ z#oo|+{^w*75QZlRMmBp(-Ag#e=iNjuU!w2Zs&AH zvHA=oTXJsv|A(lrjEZvo-llU1=@yVKDWzj*DTk7fZcveKrMtUj0KoxKQV~=nL_$(P z0YzyEX_OH4-E)5bwO+m)kL#SpGxOZB_f?zB`Rg0sRox>)ki^ZldgLrC0IF#Rk{saT zb4r0a)@=LM?4oznWEGc>ds?vm?aiBs%RR!a@KRzoMKm2M22kDyRKeK_ghg?hRhPSI zS}FZ*E-N0-9UVn8-+;1c)m^{G|BX5k@}7dcL(ws@CCSg{a6Eq?GJ(_xQ&~!5b|$?b zsPi%!FtDmV5W{_;|L$qwtHvv2b62SEAJ-m0VhrRy!1KsV?PNuXXgBCV6D{}kjAaZS>t z3P4+&4;}}8*_V{3ed_=vJLpjWtb6&j=@%L1lgxsN%g3t*I`n9BS zKpYDQ7Xf?EUqYtX;67f19R|RNQ<*9p)n>cx-`f4O8)t|bcPOO@OK#+Drn}YX6{HtM zMuXM|FgUF;jP5C@ailwZGO27I&g;F=Z*}&-U<=;cb%{dAo2OP+s{%5T*bY?inGOQ{ z04Zg8EbIaWe;uK>i@*?Rv*v^eNM#FFsC@Ive94+b3MRP4>pGH` zJ&mU1?G>YSflyPNk8+vE`~ePjsVPbN$eZ9Yl!4y)mL5;hK+py1=c>mk4eI71|1L}s zuU)@}IJlu08_$j2a*SA$oZyf%QlMt-DG)T#>T7Y1OBpR?e^zxU5@?V=>$Sp79gQ^tz9btp0+i7sgBmc!=a;>mB z*W}mBMPih3%W@$H5B+Qt7)ic4=s^tEWQX!G0E@Cu5n1YKi zRqP~e_zf#XVsH+OH9)UHmfBVD+9O;&e zx?kx09Yi+o(~5kIhr13me__BTT@!SMcq;Z&n$5myO&*T#QU(2LOFJlY3&?7}a7Y$N_He90ueh>n)yO0vRLnAd8V4*SYVrkm zg0{?X&MpQj()zj0^UCCc(yrET8BOU+$Em^@mlEmdLaaE8>(JfIp_$)?VOn{qIiUUicl1= zEz!@pF9Gep9mov8(guZsGN{-dMQw5kAbu~! z77jRfrnpx3;Jn*L@}~}Gy}5?$Z|f^rBkgns7O;ImRAH!5{j zecdcM%14)0RLO&2N?-T zV_@tRfIF>^kB>p-B&T_SM&!4TqO;ea6s>!WKlm0tr3Q^0^aq2U81;d51 zFVbAEe{7nEJSAQW!?P5nmB+u*HHl@=JyS|gS)R|MxrbggH0(kFgGqMOx)!Ctz5rFp zztVZ|5$)-~uE^D;=Rj{0(XSbU-tQVjLI5`?G1mZUX4r?24g#e`7f7O^v!bSr0_yA! znD#M<_4@mk_K)677yt-0iCl6%HhUSkP5s{L_1hiuVOSQ^5w9kp^Z@wV=kMcv&`#@NSWhMtF5jj^H!10c!#(WJvJb$F0OwYu zB#4PnN^;purm|^J;OK2W2%phXlso?iq!RcC28pAuys*p?88m}O6QZ~gg=WdI6D@X5oh1JACoptm%H1K9-#8pCh0 zzXL%9?EN@H3lB|ATAf01F0+6zW#Jhgp;vKu?{()$ZXpZz0ND9JY8!NfH_6t-O6;bV zj>mH-VoubT+~aZ|zy1>&Nib< z&laH9to?A~@ePBG7U}0fC>24J4uE|?+4Jm(UW=;C5ix)I1$J0(DX(bUau&1hAjzKR zDXyS3F`aZWYg~Gz+jOL$i7AaKJ@VJP{7FadDofJEugD^$ajr{#D+&en{j*GPl|j{y z4U0>^A&j!^*`*vxbp<3i_|iL%O%7~zYhQHhP4K>&dApiG2RJsuKyydI=_eSl!`%=3 z^|K&=^mWUt?-6u+hD1eiWXH=dxn_f(9tt>!QTa6Zl1g4}G1xhN=L#O#oY#<0lNfrP zOR+BMt$$`+vVPFIVM@|4o8x=wNK*6h(P!r~>cbNTAQ2JIQVH0^`pa9VZ~|O4mOcW` zNYlWo9RA`1aZGe{_`Q1o#Hg3N0%!Du4|3Wy7>^RUW(@3r>Ar~6{I`yP$I1O3AzW~5 zepE3E#v8umcoPFIH#kjsO=84#p(ZZ78^9Saay(VmA9Mw)v_dIi9-w;$;6Q9G9Ejv5 z7?g=5RS}@*TG`#Tt2O3Dod2LWFskohdmT#_V~TQ{%ORs@pu8RzV{-M}iB9;&52)!n zNY)@~hyZ~5Iz3M>qBs^KH!*r@YSo(`HtTbN%GAHw22X>g_P2H$E%kZir!M^)0|wr9 zM^&5vVT2fYC!txKh`e+BJ);Y>mh(U25%w#@ci?+T((|9Nq5|NU)@L5Fh{R+hj@nWb;XnpxvVh1pPOdI`?WLMYWIOj zFIQ~SPNv%cTv?v%2HYS#SPv-sq(9-nn^-db*Jo-^Mdo)EmG8WGPxYHyithlHVu6^A z)m$`L?F{pG@ixX?g7Gv?w{gwKVQen_)}O3QKmZW&?~l37P%9f3zwL7^tm2iCf<;=V zucgo`9TKzvvcIihs}JTR@q8vwdqW|XSEC=L&|4WM!7qM$MjZL1-Sq3LkUp2#r0=aB zlhRg^v~&VI5Xa!K?w+I%(waSwn&5pJd|b}>-(~%eaHtP@J7v?8QZ+zVZSpekj+N;J zks3w_Co<+@+J0Tx4xq|wu7sQcHn|C3-ti>EejdY83!4{#0+Nc9)iq0&r1i#3>>*ES0@*9h$Q1DW*HR;G-ZgGsL%G@*#!t9ngGm zcl~}=c*_`_3A#6oVfPgz>$NQIxRl@<4G<$*8A<0rXv&JbIm77RQfLGFH?3Ar3)FJc zAsamSOwuyb#_ba8rCD-74;dd#0od86nRDgV4gGq6It~G^#&Y>TX0qD(Oxp6OH2EwL znTR`=pctYR8BIUZ-Ghz|?4+RJt1x&&e8B$zn-BB{kmgA}@wP=Ms|T2!8_4`>LCX(q zA87M>Y*oJkc(nKlb_Yg>t(Z_yzg*d7BSwt!w7@${$5vX_=gr{>SYdjDYMDyyx#hsd z3v{(cI@_#k9!L?YHYqN(;%)W|#FJ|y#CR`G+ZNT$-?p6?-fKnpHHej1Ht_J|I`sxa4}vD zN*oWsB2EEVa%QN$6K)z;{+5$ z;yVT)waS!Rf9mq}`s4lR)M*>veu(mA+$x7uxSilDh)w;*h%Re|LLU-_PZXQ^(O3&L zKpkK+8YzmwUb z9FamF8{D}FMb(x!aN1%=2`XOZhp3c2z^@P@FCI^0mWsC_B_mS{ip>g#8j$T+3gw3K z3}z!Utg%n#R8hGa5Q>4nk1jn;9LyD*go47Kx^5co(JRHqP~sDo zp8wer*8mj)@AoYm+(d%z;e54-fsy(h2RjRrS8ymi4lV_K)6r4hkdmslsD;|+f%YN_ zd$#&_>MoGElH=8T@hX+O{n_q`J5er+mtMK@>!n@NG=LvS8G??4zGNhh;bLFiR_P@FWut4>y^gW3B$s7QN*!0mt zab`pkluad~iFAoPFP1~XeWe~Z9G*j?kgXy;{dx$#Yrv(0{(bhsX{KXNF}yiCf(mSP z<+yCCn49vGqR`{RgIWW$n8YMl9@H@VCg>>v-<)&RG06%)X;8+QpK+c_a>F;Ep3n_S zEV9)Z0Ew~b%@GafeqzpI>z=|+Vm;sy$tuE_3q6=`c1clEzlS&91MAi7p?;KFX0(_g z(k2aKK>HrfN6of4KnUcDp{&R`VwZZ@`*+WQWeGVdIM^Ns7_I@AO?O zDYI3T%IbN!!serE=j3Lu;RV6TWU{isQb#eSHd1>k^n09P8_wT6Wu3>p)onmCYkyS?s$ap+0<~2X%&0r^AP&)i26x3RIAspX-p|IiGsZVhW~Vdx=jk*8^GvzJ zMa9812_2jDmxAm|RUmR*-+7wz3K{?p#sJe7-#r1Q z2Ue9)lSkL($!F07(n`qZa5~|a1!9yCPH;=r7ec8r0pZEHiJR3p#H!tk^r*m&hk^h8 z-s@h{8R_151s^s?Df^0t2uXg+RqwSyc4swc(&M(*SFC-6 zIDr1P3Qu;hC_!i0O6`^d`BV_;Wmcft0mSgqpaRhcKxBeu%_RA;+D$0d=t8<^ontc| zQY+%Pa7p=Cg~&qs8(FtC^TFlCrDd5!e(afK${)^Hmp}ZQoIxa!>ljc^wP)*~sbrt_ z4p=lAz#&RA>TB7d*k-Xm5NO#N=k=~&L$4jN;4liHaIQhiI=Fx5MIebPWl${bKv^V_4IS|wRE*YpB9T&DDy*Bs)$1hUBmvV|q4cMJ=!y3H z-~5hy)-!dpVU=AyDsv}@qkNm7B6_gh?*5Mlkj`Or6V+yL4RFv@p$7r?;L`E~`U8^g zFjCePvQz8te&*}ZqWpY2I#I~ys?4xGM)pG`N4zJi^<+RX6POk44r?RfDrfx!O~sRgar3IFnSFIScTkN2oBV^@r>wLKI z!Qtv3bM9v$9q!w>@)NM6R!R9Rx6B5eOPv2`bjOwp@#MHj)xYl#@?WhZ5Q>lS3xS=$ z=>JS6Y;Pe-b}3`CM^ozUvU_$Y>6-CF!?HQo2o51A?<}5q=Giw{M31fxKH?Hq1vB>&G?i5AW6(RlE&U3YN;MP)0wQf06P5r=hVR1W zF?$rbm@q>@=qkXJY#;u@=Xm%Ehh-GXJcyaleN-}d`x0Wq z0MYnUN$idQwb^}DvPrJj*Ua#y@$(4G`Z^xDd@qrXzlU^D_FqTA7Jd7i){4Pu0zo)S zBrU9qC#?@)EpM&7q)q_BCaNH;G` zCT3GWW4OdQbR(fTW=P$@<9%&N++uox1mGYsSD1Og^C7%z&Sf6TIlv;H*mTfL4u+c!q=Dq4h7!5h=?xJ1@G*5tX;6@?$& z*AU&&55^k^57)^nQhn?J1tS=E5TeT8BeNp+RQv>Og8!UdG5!s(T#L*5_~LT-j$sUk zJz2v5Lor_5+cef7U=Xr@T7jd0oKvVEgDU1@e1 z`iiS}=6EP422?#^ca?xt$(G^5QxBXf##UiEA*QjJ(ls<|f5Z9*3VIqB1J*zYf%Qe) zM;~~%bVNqNOouEHh|>AkeFxGh={5;}j>tWi!79AAK=1WXq73wukTYTRilqo-oILlz zj&CT|2%OzY8Ue|7-zt z>8+QyuN9F?IzyjG$C}cmINFWFRObd3G)fwt-PQFE^iVb-bbnXF|B(Gzo{B01)$4;N zpp2Y8t%CQy&<)Qb*ZBl${*SZtuxh|a0x2RkK`K-aYgUQZP2Yk70Ae++&+5T>)&Y=$ zuVH389+NI|4bG{@!5>}aXrNnWzT%m?DUJ(J2;c!9e-Aj!i(%m00&tbe&x?&y{4FKz z_x;t+gmD&ZEa+m==H5>0*P+ujw2A_<2$sXu_u71caOpQd1Q>8JrV)h9T?0iMFJvLB z>Cuwv1&FV8huaRkvOMN9A9?ih^$nec{nuWc0yN}HVE?s6VqpWsjg@^-5K%GSQgOD2 ziwcjcC*_ttg3<4wmBS{(KfN#S$zBh0R9qHMB$1CPBw5=DikD_x@KYcRy5TGTa`v93{VKT83egZ3Y*xaj7URh|meKPmq13J)YM^t%( zaIK+wD<7w+_iadc(RUOR-1!%zWA7nV?3RvC=o~?EQZ-sY!d{|zh)`#sgN1)p;U9#d z!NdWb+h0}Js%VB_cF&~TRe8TJ8R<4P_HfX+-R1f$T2w*fA!nG$_%^eQ*J#By7z~&? zZ@~4Oe%A>pA->Y3gVRDYY;gNVJ7kf9j_hXG4CBH4_fmS(R5Ecg;2vo2EYLvrby3du zA$ce_ub<$05dBzlCtk+#7Kr=Po{xj}EbIY|QNXIU@A=`F%KiY9VCt`>Zl5Zly%i<< z2Yn;8BBME}%;8v7FON*t-ZF4)eLQ*~zK8Gr)K@86L&rM{nG9ss54R2PV!=B$rh9kkd> zSZ8B@xs<+<)Dqi*mt#N_rUAu~%}|bFksbw`EUK@iwF6X`B3m{wpuhsm#{35nvQgyH zfOQmv(0ZcR?eFR^?YEf2S4;DDpq19|79xPOy}AHAUQLnx%i$`s81&Jj{5ua2z; zdf6j3AwV*$r?Sj0$3ifVS2PU|fs`ou4QmJ?kAm?=i*(y@%%bc63kUWp_O1I|3H@ zf5pigm0jbA9>4&L?q=(H$97T*lSU@CjyW&cxo5%ZWXV*UG%+%o|#JnFb6WfWopU&3Rp zoLrTR!-LZ(F#J0Ji{FQ#sqK=#9Rx{sD;YB$AN>HDC^}{(cD)JSP%Yewyrv~cu%%Nr zDdP`8aI{)noM>hx8rVdItkaHr zij!8xA*aNgUv}!o}5(o8?{Sncs@wBmJ_kC`&&?2NwxqO4QY zX-`j1(7Kouqo3fyL`Kv;$K$@&p);I1>$7AzuL}R!(^L;)^(?6N zbQA}jK1Pn^w%;^hQw*lIsjhtHF9ET&w98@!L0_hUbXpw&-|r% zOx{AmvFq4_J5onaoMh?@Bjs>2H-b_q?BC*Qqm?So1_|ak03I;**P_uyWwyPFm%wkI zAPIO!A!-e|Xc$s@y?rzdq5P27JU zdwrHS-6Qo1Q?r{;Z*M1aKJt_Nqu6ps@K!G=;)=v*z3uCc;4Rv+o1phN{xMr+Dg^K6fm}bxPzh2d zQigNOuI6zPKZ3m$G`eLPQzHZW1AK$qFI?F@Z7ZO+chyypk}R4s{9Ru6)GbR~L3G zU#NL`bJ*e4v32U*pJ7by;()UZn&9hv5!RcIxm5-gSxY|B7W5hKze6V?U=mK(;zA?B zS^%WRIMd~KvIB$d=P%S&-q|%qFwwUE0cXQ-16<-yR!^u*D>yH$=>S&eU9zJ^!qV=u z9BR>mM6x^S3 z8*B~!C7Zl-2V&7gk9T~E#1j^ySHlxPRot4L(je4`wvs&Fw-jJF!o-tlJu+wOf1&X; z`!FBQcxItg;{n^pu!^OJ2%>V7)=bL76*qQ&xTz3`R$p zsEU{_2xm7EngK2MZLMhPm=O2>fLR}@CH`G_*t?1Pvnn)!f&lx9(Uc%NX zjenX!W;*+sw@5KWvPCh=1L;P=Qfn{ww;rBZ^%c-60A!hJyFE0FjFx@h+V1FOdt07+ z@&ZO}vx(h566*<4f`e4b5D|bXy~VE~3$`zLLGnv#t$-?h8ym|gHKP$YgS9o6GQA4v zI&~xTMS8sYg{Z!#0!8>nPa=09FjN<^zrg%yf4J}jbmG9qtn9kv96td-7)%p=K2lPq zF^CugV*2ZiCr()*Dhg3EfDa4`uECA>AzlzG`k7|G!Xj8)hnCx8`~0FFRe@Kw7l1#| zZ2p%;_T8Z=x7HTn9DBTPYY@KWqX8fF6@93Z_$>l2`X2}0qR?U-4l#tI#ib+JcnCT; zaTdC;>>yQ8Rk9-jAO{HuW1+X4%Uyt2U;Cmnrw|N=`YzZWF#W=D*Zyu{4S+RF-vxY^ z7lszp_vD_2aM+P!f-(0ov6Az@(WIFkrS@_?ksF>6_=8Pg{dGgsf^zQGlu2tro!GdX zd>5E$s?@3PS`Vp=q6ztbJYU#aw|+G&D&$Ofhrc$kOq5nYqx?Ki6UjX48jH6tO0Yk0$jtz)u`NH`7RpVw&R96yJ%i8JK9|d@aYWnUmL=5N` zQNE?WY|A#ErSJr|(hFVN(OJT-x!|{F^fVCrz`oc=j?Qkptd}p+q--z72lCZ9{xw|+ zdy-deUS67VgWWVgiCchv*8oXU#ho^G2|$Zr~J0gD2PX9)L6eU`(xGzA>C(nZDGq>B=_#p)Cg)8 zwTjwD{n@ig?&(zhJZDXqd{N~u^eFz8yJ{x9Rd|{$Jb{XefV33;Wn!<`0MrD)7utS4 z1`+KQ#66G1K20gx*#AC3+-)5+_mha8bwZUUYJ^zyn>Q+Q3X(1^w}Ih#Xbs!JId;kR zW#ALG>T4Pq9QQyaxYQ3jPtaYwfLq=Av_+=~g{ID(gOxd+CsCjq-FG(}7B^I*Pt3#F z`0*DfVv6n?THEc(od~pyF5e=cC!HqknXJLTCHTK3Bh=Gbsuaf1Q48K$Wo1y*56eMR z%+yipb^aAb|+}pas<$#_gNAk>kH$YW{DN*HOcmKhdL3!>}i9*7xgoFgLN#t72Ho(*{ z^E5K}$c`J{AyLsKU68xkLh=9Ba9-lmW8>;%`&-xYE5|@>GUZ;I*&Ds8nmKXVnC#R! z$0F|Mk6Btq$P#wQH@ylZBq1Tyl~5PNm3GxAJm4eabbFlHreOmzg9!;J-v!|OwYkQk zV`89aR8R1OnzNppvY24az={y|%R`fyO=}mddPd#=hVkgvK!);D%_w6u^+P@mDKKnD z-tb}%&l+A(=7U`Ni^E>61uw~?GkPAi-ya6e3b9$@4VS)7aug|HN?V|)gB`Za^WQMW z=t)x#vchz;>!q?4+y>G&7lU4x1MdM28QIBlD)M36C-Z1z3@om3Uwf}J{@XVcTT%V?b?Oq13d9m#*qd=MA{l5`<3JxP-@ z&;J4UEsI?Tlu`iqsQtkPbh6_~|AZO`{ahS_P4I%hhhO7+cI1K3h1~S0uM5x`0!-Jo zf#Cy2`O6EVzQ-`1Fis{P6q+<5kzL*$AkwGS>I0ybst~4I4E_X?L4JJ)qWE^tew9L# zS`fh@J{)!34_Ts0is8WsQ4-mIOpqM-mY96_yzpq`e_;q$KPTEZ$r`i2;TXyHRGwRa zdcU+?T$rc>$0p6W+Y=_;M4QcEc~13$)xn&8Qe&ioI?h_Q6C|d_0Z#4w)Sdve%tGvP4uI^s?eERRwW^-3EcU}5C zGNnQSS7P;FxP+<)usCm90vzVnNk@BK{#h*P8k7rVr=FVQMP8SNt6^@z^Sj@$6a_=2 z=HDem-zRKj;cM0bc`F19iLEonkJM%WMxLFYusG0#qdy#;j1ptN?9gq~+X;M8iZ_Q4 zzYicb*7aA6paT#CKekVT*2kl~Aml4Pxk*XTUD~;tie(5|2?;#pm9C4RT4wm(cy2K` zhiuD`Q6rSyPV?n-J3tk16WbVHSLDoeXne7uGaoL`yW@EDkVFk;}rEgfm^v(S;>lncH3{v*v zE1+pU-Dm3+pksLJ-r!P){E0sKff2`C#VFQuR~XCfjir($eO~Fu?k*qbvjJWCezL&7 z!qt)q%*R0L5?B222G^^U+r|ri?nZGV=yIj7j}Vaq?F5>&HDu+R?D)1i0)yk$IVCYp zj>L!c0S&lI@Ps$A6A=yFOgm?6TD_8mkiTCVh%Oi0y9fj_OPqmVu1La z*kI7}!gMC5ZsH}WI}iG0*i8|pREY_7YQ15m9CNwa0lsW+NXN(+%2hfpe*OmP$o#@f z&Nwk^_2n8u-3bq&L2Heqr7VdhgX`9rqKst#w~m_Zf@fABnjqyeiF^Phy97+*WS}j* z!7(6dS^JpcHCi+kQ10S`z$HlUg2JZqk8-MtjoV%DzW7pmK(R0M;2sSBjkCz6RtUVE z_TZxcD$#&Ekkmikie@Yn7<*vf4h{}{pY;_{r$mq?Ddn{<>S>rT~xohV$#|>Ham>%e{_L#K(aWp9bDvA{N5%ihk-| zAzDNgOWOtz_CJKqE6o|%S91!tt%Q5qjpFD&gz9p5^7Al2yy-T}n0|eht`0su;N8B3 z9%>&wkUcHnjDoRQTx<#1Ur;eb7|smi!e(!AD~5ML!m zu{4G2(jET#REgba$DbGY4cSr+Ars9Cq`goNS3G`e?o@aIgd9TJe%H4kPYZYw@EGIz z5Tq2G0QPFnBp!0$T*oDFOVk*oh7YSGOvOIzA0Dc^==~>AV|nDQ=xp@LW0G%*TK;3Q z(G7qHB}gkNbJBy_>vuy_ON&fok8}i%Ak^?f#DoLPch3C#&W%irHWQB?2R=QnnVM5o zmDJy}_yM+owg@hW+VtG~Wck79kkyW=u0dB%_62~@h%H8Yc>Awa4)J%t&6!hD- zfbam4ppO^|(N?Idz$^i4zpleZ^R>Mp#&l*OD~KFBVJ0w(Etu?0`FQM&>Xd9z9pcQ2 zsu}>>;av>1Ed7#1nD=a3XkG~|C<6@tIZLJZmzqOpkDxHYyXPDabgPzu* zMtbt$wJLc<+?KSU7EXl@RWJGq$|C~?GV<5*xr~PoaI1-?i3r_FFT9899<6{z7Pe`% zN+M8DrC*jZY;!7{bSiS&?xiohLgG16J-~&q!USK6$J2sYnC9W%;bg`*ukL=&o?Hf; z7zE_FP{OLZBtjrZPE~^>$Wmvl{h;gwBvIpX!dZslUFgrC$m-X@zk}*?AaILLcLcv0 z6Zr&k3Sc0(ha3T8%Crk-RlXq(0Nj6pil62=3Gz(FFZmPl&?UTsb5HUP#bXfIj<;SR zTf0C0G^%5q{-dfA@*2{tX+&Gvp_t4=1gVMMvUnXD0L4zLLy8powd2|XC-NbM3sUbNdk29#&SdLBDXpVKK_&X>=ErgOPZrdgJ!=21ne+62 zbH_<_c%V<)4VeoIe}T!wWa?64y^ddBD<~_%q&M&=NUV!~9A|-161_a1fbq<~ddF%l zr~@#alZK8Ql2HP7k|AjTuv!N)7HR8DAgsKebpwK@%EDodCHH7vs6wY5c18;&CwpH0 z@g5p`2rRt2yDtCKgqpVJ^XHqIUv8GHuilyyjpC*j`RkUeoM=TsNO0wCGGddIm&9!K ze6h_5s*3oIsY*@qwMq)K-p1#)hT-x1?vmjBYuXu<<6@w4iYDqcm+w+Dc+kw)Le=dn za4noQ#f$G-161o9gpYB^I$9$B{RQD)SZJvHNW1)LLE{5|KnuV1_QurGOKy8Vi`>0> ztw5|yc1ki?7TBkcZCO+jkIMSBqbeV=l382<>2(v0Of0q zD7C3FJCh->A_Dms`)L|u)Jv*dJ`tCFdB~eY`3otWW{Cp2bOOoKr1v#Z5LZoj)4>j4 z$KFsO_dWQv;suvM#6d?K^zMuHaS|8HGy6!~)G$@b5Ht$}M>)n>ML~S9Lm$C(%nqd| z$;O(-vs8!yt zy2u%pT#d*&LVgCgoAKVTdc$`oZ2F25neZrye|jX z&=J?D9pd!-R4U{aP+S9WBlur`1H#g!nVm)I@XiaM&9k7B!0r1Ue*6i8aYj18wuG$! znp7if`gmJCNx*xTI?(3f({0d@;RO&4MY~+dB{5CPNwBSniNeOL2+DKB$epi47lQgHEr zyxj@-z5=k%UP||h3;4A&FFYVs(EPPC)=nWMjf=rd&K)t=wXsp0dT7Z)$u}5;^uA-38wh4N3Gn;em5m3{h|9s`U zO6H3&FniWuE*Y8iHheMGg3?F*iYn3`bNSbuzC~FyqMCPS)|W>P-G}7DP7@Eg-=#4%b?<*+%reCg1LK!8N_fxJI1WXWd}zEKUBUT^*&J3h?C zRs0G&)YpM&E%gk#+hh(1M}7%N^3Ci#iy*X$V!-AU=pkWZXSdojGF`>|%-v(aFc$6( zX61vvOo(Qh1RGxmLgk9bpk}~SQd}YH?>#PL8X&8Ne5S>fMFvf@M0&ee=KEVj%EXLD z0fdJ=oij0N7ntd|qk2jCGYzUb7PO&a8H6aGEipLf+**!*!(b~gU<1GvCDE?`EtD%? zl}iV_LDMHCan3F;K;SP&7*Gh+c>cxKvU5G}5-p-x-}mr#>ubDw2g1$0O-G}Di=%9O z*v%Lt6jXlbVNg1q-d^uV7TqgA8tkrt^4#P|FnqW^hSdtJ-l8T>jM;Ydb$I)k(XthZ6_Wf;lc0>9?odma!1CMAI~{T1sGAt<<`NSK)aN z_ zw{LdKDgKL4>(Je;1XeBGO?AaC`uFXuNCfFmMPo?qwZFrUx>n;ja7`#r>O<_ev z5vD}As`pvIY;UWJe9t9gE>$(D3rUBoS1);gp+C4#%yW%qyM!H352tjQiJVk6Ib*$I zsC+c#fw~}VVj{6T);r3FAq_7Q%RP@y;kQ<^%Md>e@-XlPPG>ZC zMxUUVhhX?z)jm6xDq-ts{>HW}pt@5xz&`g!}@TN}O2FRu2fb;C6u$cnXpeW?xmnaRQ6l z|ANh~yzKKlHCJxEtfsXGU-Kf9zoV^;&n?M9@DXX(5^iWkc@fSw%}=cO_`OK$g9CyK zS_5}w`9N)^A*>PVHQTc#NNcv~47c>)rW1Gw4eQZ2K+~;`_58{BV1umVPI+)cd+QDV49Jef&I{Qe{pR`6uLHC%45 zU%e{5I4h(d35m&|(}a9Q3d;n9X_M`uv-?ZxX_~wo!hf38)pkWLvO>>Gr=Xv`E{MJ| zsM4zGi1JxaIadTpI&p#BU_A_mHw03tjiuf%Hpn&3luV-mvF>KSZL)qTbwaZX zA1bXrL>L)i58+t~%y9IN#>=Mvm?1`n`m&`g(XvH%v#Id+Tw0b+^i>|_1X^Wm#)(xL zu&)?{dT1V4@?1e5`D^#vWs^qu&X%&^%lrH?D!mVADTD4$#X}$`%o=OWePli?(iUq< zBuO?~J?He~5NYPmrb(B_{EgRdKx0cZo52)_2e@Gr?q}Y9ynbI2nvNZF3j+IGYOCth)0DmOrLK(pcaNivJez7Wh`IoT z1rS)q@B33m*m$T4we-8#@pfJ?2d}>Ku1qerj0F4u3RA4k=3PD;-hY|efDtk_|aoc5tMcd*cHgFQJm6Ex-st}2tW1=upKqosns zR!6OF0S^iTB&#)ro+B^yr&xhnR^r~|fxKIE628KDdIa=C>0|ZQ?FaCOVTKX?y;HjP z^vpey#LRI&ByUQ$qiHII;zL>Mq@SRN{6o5jC%{3fYmQZ{!wZHbPx>nfs@3pI+<0Y? zrCCA=y%pX-W@LU|fe#2sP2P_;Bn*cDrPT~d=rzWdK3N4kV|2uMb*rnYOfO5qN$V(f zNf>fKejXjcjLf9)6hRsMi|J6I>8O3?tm+v8y|oHGfJBYZ&~x0_~Mdn1O;@CA0l6PN(US2?+kmf`!8bQ=|!c(9JZQgG6? zq(yPqiMgXAg>}Kf!3faVsWNxn32-g_k zLm%Y7f}QX7S6VtcI;Bv5hT$gQ)j;VzTyYB$HB+DO%(QyYN|u&RtAzbR^zi8BCVs&f z>u86^y>{C-YNe!VV*jF*Ipn<$+QQ%g3RAVy40P!7OVsr0mmj;k*D3FUJowQKElaep zY653OcTq3t-Ap+HP{Nk&Jq0LW0PzqwG0qumf3Z#vnhc0wY-3q0jVmv|7^)(-|4hOK z8}#3CS$}4m{cV?j13=SU3=NN3tXuKY4(;(nZckR*h&D5DIiagCY9?sHtEr<%S#aS8J^nl}+7s@pmjCsnt~eCD|x zyA}}{vKa=)RI-4LWgNzR$Kb`GZ<(Dffa0PQeYq9qjxi*^ogM>1EDcZ0^bfMd`sRZE z09gwzgM_X1B`|Ju0Br?S>Czc|%b)?Ne)J_!^-qOB5qxquSS_LN`2BN>(Q!Z3a}rHn zxdg(R69EQp4axy&bLET-7;u!Z`RE8a*GHXj&xdfFOI1jY*i*K2?;T9q8SvmBYFZEG zo!~Nf2%TkgpF;8n;tdPnsFqVRbrn|Z@N^9(Ot3OBv&RfSokRo>`yd?Ce=BC!iKv!? z81`Zu*krUpSnHkn>>Vj6!oY|Hr_sdZByBUm6+#fT2!w71lSJjSLxC@Emg&0aetG>q{r1E< zWev~D%b!qT3vu+@VN3otp#BQR)Eh8svd)6vKaCl z|GuXjU?r0#q&tRHI*>}hLYo{0qzRDN`CmwzxD=I*~%_UW``*P^ zIdMx1SO##@^m#?VENB&Qc~xbkCT+~N@PGXbg98FGAX`H3c4OV2`dC}wDbvO?w=Vx=f=&} z!;^zs=~{kvrU8oSo()F!r)aqP)CFW={FuP_tVPt`*~Qg8G3C_8DLsFehF&%<~=YJ|~Yx zT-Th5`bW7##m@8Ms{LTW>a|#q9KUk!aUZBRs*0*As%kp44`fTXwU3VEXaIzXZajYg z9NlnRfVtD|(pSv;Kq|SF3g*ns7MhN#28Bxz5fQ$eKn>8o{(mfecQ}`Q`+rupva-pZ z$w~;>dsAqcA(iZ`hP}6BuVf`6Dpa>wNJgYIt?Wce()zuw=llETKAz*a@25VW>vO%| z=Xt)?SvIslr4!+}dzV(fvcDj+E<><_z}-1Q(rw?Cd@c0}{T~ZWYu!lQyQfXrpK}yP zR^0ZXxY{+PGzrQM#1_i!H6^1FVtE;QVKi>b9xpWJqS2VW$moUFtjGAe(U1{4$-ZJB z;!8OqbLwcUH5&nwL!VHPB7T;FKz}@JUbwWiAWrLgf z+_hCO;@$j@weXq@)z|$#&>X$DR>ztK=$SCDsGfNtg}!?|8y5lB9mwPYT!tYCj6FlB|~E!niR$N zJ%=bCa*}G$Q3;O9X3?Z2_nJg9UEl5bymYOk>Kvy-6iuq<{wn%k5pywmu@$j9dpQO1 zEJQi07jK9&#JW63Gx2L zGAv?@CLKxle0p9%E4mNkAAT~$4PC_!<8@D}cDaeY#3z{9Xe57nfRdH&+$=qA=Od zpoDKO2$(=+cFU$(>&hW@Nhbw@Gg~egzIO7z%WA;da|Ey&@VMJU#m|$vK|H4tY_)gX zaELvpgONA+GUL>Pxsr&*)0D;}S7%>;Dibf&EVVE7X^0^n2iwu zOHHD)M)Q!WzRS4Ktss6tCma8sLF1(s#pv=o;Tkpj+ixWgC~zzADF`SCkJl2Qa~;%(7ZuQbfW|64vpII$d|%evEU zm)H<|u>9Lr-U60ciw=Ji=4*VWJLpS+l??o+@|7c*!t{xb@fn8L83A%Q0uY4{Fnpjm z4D6xwsfSfFl0;;gE53BSOJ2g(_IJsUPB7wm!Wwa>9|5Wx%ehCat(}>rN)==jiY7N* z*B;c!7I68*p3gxp!AfX^QqGipl^@FXVDaGe*z2F2&^6`VU3;uKVM4j2El0_x?9^EY zA|5hF#tF{A07Fv>RN78`;1wD&FoH19HRM)jwSJG=^!9 z+^DY_Mc3TCE=ppv1zPA1i4dmEW@&M}%Rgq&R-z(n>&v1&N1m%?r6mH4-fWDSfo(=t zQN6%kodWk4mBYNiVsVAn+dQ5h)$;frKM*CE$(h z5!ot`-x)immo$X+kBI6THnY%&kBQ~Qh`)Wx&G7UZ64S}64Fc;_bzG?u9*3aPbEf)D zuVXbHL5AF_?eE~GcW5~KN_zgkHzYZd0juwFQ~u(mdA9!iK{&(IG~?a5l}(K&S~9GD z?w?CkO0CY+=T?32SErS*I+vX^r_s+suXFbf{-#Sx0F!`73}3Jtk`#YI$?pPnl6*W0}HPEfxt#SJ3`pY1s%4t@9V&-%(uNTwZ|{=j2KkRplo7zPvmw6eE$G zU^>^Rc;iWlWyzUITffisO57>S#HywQ^Uv*PB{?Fdi%_tw*mVLH9@K~w;}7gkWFyM( zU|6*Pwr(6llGv;X-WB0f*VY_PbeliuxOQeHJGv$4PMD9y>+S_%7G>(W2N&Wz7=Z)s+v_2$o@BIdfx!|YOO~*WWY{)h7 zB!X8_d`ESEhyR-vxa_U2#?2+AkPWe@u}0Bl z*IpB`1d8hi$Q!BUIP8<@U`?@z&I<9;0TX#MB$1}pIh-vynx*bmt^y98C=`d<&u-U5 z+M{76<2l5HAiwl7gF>eL?*J^wNyoT=={?Es7|T7(dJ#5O9%Cm;b8lIbjTbClJ2|{8 zwyT5&C}I-~NUF-Js(Q_Bj@g_HkelQ>6K?Bp@d4h(@0$N<(%$AI)5FM@M5l?srC|Vu zxs)biOQX=hxew%kMU5xoWfR%V6WJMXk?P{v&>Nl5&*6$fV{_-5+!oot9^IRg32x!F zdNEvCN)psHG!k?*^gWX49Jvexj+o+J)>`($lab6cCOi0uqys}N^PI+in%~f8ih7#w zQ&I{7!sFi#U*o@re)B0azu-brf(UL8S(bCIuzAsmHlcAesXOEMAHO#c*B#)BfH;PC ztFli+9z6fqC{BvU_)2y%k==&rsFO!kOhVMs?3TEVfsL_BQG7zpvrS1(hUdo*)Hver z718+5vciPp&Gj+aQ~ZTFyQRWyzz&|i)CDc)@87>YrqWf^G>PnwjSL;Q8868k2>P*F z$QZvIVRG<`^rznUB)y)lN{#R1x-AX617eQw+ei?#Xj$KaRlGKS%Re=6*xRF+#k8+y zh|))i`!isZyg;FVRQ@e!nsCco*p6dzGQ3JSJ`!9^40^BcFMiy)8-UMko9YZk@nuq4 z$r!K0W3qH!?dR)uD-Fn^d(pYal`dCU(nL)Zfh{)z;n`+=X?5|gs{-GfeY%k^4xUEU zv2yG+{ky@EyDmoT#9>*(UfgoYF7wT8wWPNJ*Jq*QHVDS<^w!E+9uq4taW@5$4$#^p zKRxMJ5lN?iPw-oSd2Zl~^8)rAdN5`&OHIAP)Lz>rM9#_h^W&(G$TJ*#8oHJ<;>{on zV;;wGL^%6G94WMJQiIbtUU&+*&M4*;ZR`M|zpkypzTUhlel{xj8SGZ23BkK@AqR2C z$El^YQT2Me9+GqTk!5N4dai=qMj~(*JZ;<)pL^G{>lqbC!G^%s{ugdL*{Hi!s+J;-y409y>d#Cjbqe8u+E6|rCPEblX4Qt7%A3e+d~8}$VY zXsDNj^1O(|`c~0Iqlg*-4xdt$hV3NJn0^tvd+L^d3MQZM)$2ueawS)_<4BzFNM=zx zU$t4M(g+y^YS`o>R6|$Uhr=xptgjBwn85%QxgBv(A*Lj}s#A6=VwBdOfoZDbU? z8jpuY7(}U@N6XSITE*5IXb>$he9+#8so{eTtCp^_ww#TOjr@z)15QF|}FQWn`EoPh|2xG`+C z=9$;Tw-c}zs%tBWady0w?Gyj)ou&f|r=9SY za1Y-a_HscgnhE11dJ+7OvVD~pQY=2oVUgK-#9Pc}-!Gj((*%W0*@e8CTnNe`P?O<$ z1GzloqM*G{itU4xXFjg#2^t?2h*Plhh*-Crh|bNj=l(YG$@;g}wor8l+GzLgk_Al# z={J@E&)Ms_8T1)vTlZnU&WPlfTmSxD4RcnYZ13)@@dT(iQY4{?a=BDeTwJ_qD+7c& zRss8Z%U$x8Z~%DL#;anE#A@JYI?({A|r-nO^IV~5$sLD8o$RX zD^K`synJx;iG-1^l|jglgVkq}$7Nn@rn1o?5-2f6OKb&`E!A1<>Sm#a}- z;JSy@@9@5Qps=Q)+exUB{LjG!E#_3vVEHrQ?VA07jw8Td)@j#6(*2#wYgP~6EWA?Q znVTx0p}CMFB0+t7xa>{I*R;ZX$N2baFB6aFa8aKTXTN~fH?GWmq&w|r&~R?sEj$T_ zBJ6*5Q(gkvwFe}H?#axQ8w== zdanrIzy9JCh!7kR#)?ky_uoH<^uCXUFFZcmh09+zAf`_3Fv5 zO(U!l?$D0xQK9+v6Q3{>&V-Rrv5?S^_LSO2R0-8~E_h^1k+kTic!yh!iUcI5poODa zXkOS6_q+59AUXs(t=Zs4B23>W_0iJcFjuz)S#-mWc2oBa04Yz|4bUN9FquuPPGJU0 ztB_B98#e)6I*=}OmxiGaL`X^Y?u-gIsGz!vr(L47@SoUTXg7=l@Cm9Un&J}rZ(NeP z2nSYvJo?*ciT^4qE3IB8&FMXLGU0B)P0U*L*0bfxKXu)d-7X8&O&94U2<%(G_M`XS?UE4wV6LFf2!+aw;l_>YnkVoYDwlhs!GkMCNsUEfJou6KhJCoL@Jj02FTEOlc1M*N1%O>lWeH{B<) zI_Weup&UIz?g3Hf0kuJfAJAI(Ea5mO%<1ykr9i^AZW*FWer`KD-rPeoW z*@#14W!J0q#S%Q?dYC-$bIb$9jJ^pDM(OHnt!RqGPws*LB;PebHR$nG z=R>0YfAC$Clolrqd1TOTrZUcL0oU*73(`JkL^z&94uxez6BlP3wo6TQAl>mUi>Ez9O zBy^#5HG@2bMUYWRX=`8>(I59nrpW_bk(p+Ff+QHlsHZUX zCIwM6^5pK1KdDu6N9z(c%$7ZU-kKv!NkQ>_VT1@=9zTp=`y+R1SsgVD=Jlx_{=pmM zKZJiQmL<#-@R#k?dH0Vub|xb2vreAEnXzcnb0cLG-*@4jxU#)by(OBoDN9x90H#9; zj`7It<4!ZGVj#OF1I#j46W^Ujjng->hyt2&4i z*XW(1fU-N>s?iXoj;@;!Yr>M9-?d##y{8Wl>1-jV?oiZac=Uw*j&wXZi6Om9*Cv27 zg{D8%FUBt7W=7&p1@q*Oom1W$x-JXBZW$7<8{f5WIDzc(r@3k)DpG3X5H7s{o&X9$ zBCHmzGn_#(0RbhuL1CtxAq{v4-F8NmuPkn;hN4#ORxtZ*SCF-iQej<*dmKB!||s zTe_?jt^ajux@wp`)eyq8T~E9N|GpWd>UmaOxPoSdd4r5q!lq=;?M}W$%&A0v@FguA zO&E$We=E8?p-XD&S;}}wL&U;bcIn%yx(%>bWC{2B^FO20q)7CsMdJTT(B8jS3tEdy z2o;-~B#YMA%@lV}%3|#f$@OqWwH+QN+&%o#JjvjY4Yxa zU_uSN_C{XWxR7&uLA|{Az}ajdX3($A(sIwWSMo2fu1f2idGe&)-ODee7*>G03#9@aOH7XLjWe(aD3I@-HVD^ZFX{07!;Z@-93eHM zgNZ7l0Z46g^&^pcf<%*oVCV#w7{bAeXPF(4!);P?vJl;GxYT9B6eOF-F($|_Id=Zb zWi*cH^v7R~sJ#d)hc0Ai?p!OwmWFR|xcR+mwlv+Pl@bdv8)Ie>6S2oBS~`|AdnkK2 zpJ$*MXaVK$-@m_y0DiLHCRCIFL8d!+-NKNDRQ87I`|}gQ8p@3lo`q5yM0}y4fviLd z4&Dh0t9?hDc-wL8%3z}Rh=*F*lC9|?puKa;u>|Z1M)jNoqjE`chfanrp9`mby+MER z;VWL_wH(5SDpS85CIv`Au0yOjFGb~~dSrF~SA z)pfaqofJ_lDE~@|jam>*H^*H<>4vV2`lvzwDk?2I{R{K7D0{K=j`J8@SFXwFrAjI8 zCTu{g^ARHkBR1T6sA7FYIMZ+bP{pQZSsw-?ABOKxxcM(kLPmy^Y>KYf3lmgAa z3nCZU!)u~u@xfz#sV8nq+he(nc(-#^WQ4Yrm=4QLy)y^Tz21Gm)8^kxKkdgkYu!5Io_Wh$}EgK*1qN?qlA ztWy7Kfm~sylHNag#F8Xvir8_V9zqX}WWx;y6USyDFJ?EYrKu@d2=$;=zJ(+jz@8gT z=NdxrvMh}Db~pldR~U@!l-}}I8A`0xh)MgV*U=bR06NGuFG0alLrjEa&w1#As$*}}4R=oWEj#S4{fYG+K93N*;or0O!u$d+aIsUCi1&}T_R5Vb ztj@R}g>U2BStf8U_E)%x#?ignLcDZoXC$n&AxIS~w)B4Uhi~=m{nT=;!uua8@pdwg z9!1B=Y`!j2xe*<~}3g*}L+g^dox z8mLzgemNJ=k;{`)Ks75zrl9>FwBOmchZ8!^^?KxX(X4F6{O+j?+A7nr^BI|Dvcq5(6D!0+{KQy)4YXcu`Y+?gY6aXr64uB>zCEXjM0Bmp(-sMNbP_A&lQ^bfn z?y$(4ow#qpatB-BWxl(tiq$Mq^3%XlO^Q?}=DKqQccKPp1*R91D6*br)^L@hb&4O* zXI%Id=r-{dr184>Ib#8jXV$Bg zx$irn16<+e_^Y^a(w~#TAgnoF84b~)%O9|iQ?MIy4t?uQv;Bz|sqL?R>)Wk%Y|UB}1UrCzS3n>)_zviBTgEvMy6f zm;o+)-lwXh#QtK5sexEyTK*I@VtIc4zH1-T`3=CY}hpHzG9 zk|>B>R?UR!t2^e3M8sN5Kl*3uaszl>seWVpWb~s$b`!e6XvLzhTm3HXE1H{d1u%9O>$Z9{xp6v*49TQ{4fi;-y3G)TEPN_u{wx| zGWEJjXkQ+`@#XZ{w2D%>% zh#7*VJf{i~R$NtwLpI_*C(!&mMEwG18c*0-G+r_%0lA9!^;o?7k&o8t@weZbUM?-g zUBLJVWzk(XpdPghuiwgY1K4hRTJgih=EBK6KZQ$jOB#l6jfD9-{6arcHw1rWZ$lq6 z3r!+vM9wL^gg?89m8PaJNQ9>lPWq`H&e6Ar;`iJ#n}jP ze!p@=vjkmYYbFx(h}{=sU@lp?ZqfdCsF6#?aYx&SYHQKu_hsmU)7H;J*A&2rZGizF zK75GiIXr+JW&Vcp1y@(JD)^Vvu<2Rw)cVGv^;``hUsk-h3&9}WOD0gM`a2}CMs|-V zhd)b|-y zSi+B%hQH#eNJ8vDsnf1T+T4miL30F4`KdqJus}`pK0N%TOsVKDnt#&!#wzN_FgLq{tPtOVJZ( z^Eb?Fu`>Zv|GesY)#ZT%Iv0sPIjZ0xNr%U(U;E=&$sY2UUj2}w$2eH{8^8^v#TYeb zmy60(!|=z8hc9j0_(m7j`manUwTNDOZC+>BpcVG_Bo6`c9lgzYTw8JZs_6DS?8DQk z`0AiHYe99){yBhogRl_m3b|6yt|v)p=`CI(DBV60(>t##-aMpynfh}aYYx;B53*s~ z&G%BEvRn0=G>(5x*<8+BDpOvY$>nAcwISTus6rcD3(ZY@1^#s3dOx?TQ~GhYilPck z*Zsnof53!;>|y>n!z5qv`RJ(i?&uOL$~loGksfRl?#+=!j36KX6Vy{%?Ei+ebD#$+ zY^%I>kjXZgWTjEh8t(eK*UzTXWtYvqdzvlYQ(E~yFx3{mCzCB{BSN_=Op=w!T<-h_nA#{!9=uNAXk$oUIC0gH zTC4O~xkjxx{A)KCCZOay53U5K&%zJS>B#yfq{(`5yPeR?0-B&{2y=ws6SNH2FgMm} zk~k8ly-eiROGg=t>z|2r%GRdnrt-djBODsndY@iyULecZXX%krhT50%^Jzp!d~ zYf*etqFKpDXaDBxD33|)>-FHXKWO16gEH?%9i56UcWC<0^91FG-{X76JT4muLMpOw zzNFnxGu_P~7?_SdjdBrMwm&ujwrWl^@asS)z5WqxV2yF|6ILOn?#MJ>5sNL?Fr`mB z8ntF>zT=O8T-6@NKa-otdme_zcAY`oNEH^?4R8&<6Ys1l*%w@!^h(SKv0|dlcu7d+ z4gN>j`<0+h{)A#y-U66V0j-)KLw~@R4~5%Zcuet^?!5c&O7Z!#G<&RtH%C#NCISSH zX2@y^sx7oL&7sf6pu0Df-ajF>^w65Kr zvLQF|?uEdj^lsHF#Li?jpHJP~$o-d#7UJT{YagKP4+K_yk2ibv9CgOgFnrA7p=Rpf z#6F$L2KU&&3G0Wvl6E~l<5dU0>y{m)7P;s8XAcCzW6L%S8K?I+uv0rigFr(!z?T~n z@y7X;uoFpZ?K@g?f$)Iu)`R`17?0F;LF7xR_2Z=olCJEplH zFMHnU+dFI-q|qgTEyQK?u9u^uV>AtG6W@bK31VH&p+!jV1N%a1)nLdoez2oS^USXG z?S1OW!Qt(qXAh5#Kr$3!3>^0NpFhSsk<^9@x+%>xy?C4y*c?laa;dMiy80028$V-p|X)k=AZ$ge@^#ZlF)H%Qw{QjwYA z=pMBHPr^i%T5&7O1dTjZ)sD|rvO~VO=23jhel41YvG7ojJX@ZGgfI7(cpn`DXYP5v zNFrJyK+M9oWvC=MKQV6OJcW=s33%}W3ALyqAKM-3}Veqkc zIE+=_)^?XKUsfzeNt0Z@fa{<>Q5EL_0^_P+e)cEvv{XGpGPZ$3wyUPS*usypb*8^QnnswMsen$iSioAT$E z@U4{m0N>EC}PC^j^@v*@IZHedbw5M0nk z8O%?O^=j?Fl-UkM8NN_GMx`$DJ{J$cs6)HU55KIO^ zMpb3yJYeAF`j5`7I(36cYYYM9ux?)SXJs*^xmYdE=KZkJLIq5QRKhy zgx$!nPCn8-^usr*yiy1xWShPWlS>HI2%CmmTAq2RzqP%cQSd-o_V5gThR+W}f2556 zfkjK;=OW%Li1I4FwOU9lqRE$@kxVQCyVf(y385V zmJTnz(LT#TgX`2rZ}*|GD%aVAN)T|O0yG78LF`P#QQH+1C;m|i2LNTMj!iT#iblQ@ z(_s-dvKYT->mxbB$ePhl6)i1(1H&9BH;dEWk5HQ2f$X#q=bg}i4PF~BJo zGHO>fWcmfb$!MR;o#EB2JZ!-3P!QGzBq0{Qrg+uJoRokkc3 zxp2y&Hb4frAYpC_J+>;ia$BvjMZ&Jd_vT|_Wgi{0ehiRkZt-J5xurCQNKMe78_5uyx{zutodP3RwP+`plv@_GzP`iE!zhG$Ok z%!_gy)Dx}#)RBBIW~zizBI|0%dQ9gv($#CqX7Vjb&W#I?(eU2N1Gk$APsKs-qzhL{ z?qF4P{e|g;e^9`x;EF(-?1hd3x5n73i6otvYRW^VpteGMysOY@H}VV}{=3!HP?*HM zcZaw~*dbpH7f((`w(v*n=Qpd4-vObRtmboBe0&}kenxoUOZyx_Pw!pp zlz%p7qVL@a>wcv8RVCslE1D&^zdH=W9T_}sdHxTO#(LrYqU0&{oGH1}C-E~v;Bv;$ zR6L01t#b_f(!HFwO=q;ldsSCkQ6aO3#_#o`puESfaflV_>-Yba=?qx{f!O3<;+&Wp zY|*3-Rv^jFd=9OkzJ|tC>BQs(QCe0BA-g1HWJHzz;`j!DBF%G;l&nhi@ynp!FxKaO zvojHzU?j^YbqukBLa7z!r2oxLnwL4FR2y<C&S&37idK>VKy+Z-U9xU*RWSE$55N zAhq1~m_inTO$RrhTa4xG!4lTp>^^|LAblzk)ld%-VDJFgRJ!QC`Mh5H@U zdCVgc3tz^mF)Vgs1S{EZ;Dg-JLWUTFio@u8Zx$-~-&MR}f=N5GsPWX-Bl=+1(JklR z<$N@lY^2dxzP>K-(5&s5h>+Mg8-63=x2Q5t-=$aPJ=LlA^r{|f<9wr`ILoI|Svw|+l5ro5Fg_%)S&t)G2bYN zpVTQfZ{6V#yD0SjYC{KXUEM=3#CN`{t~VeMpx8s$wo~`ajDtzjDocdv)j=V89(~5K6a>9~_FPEB zZDx`#DVvVUlkzw|^Vgw`pK!&vvLQXrRLu#u>AFLeao~vL?^3g(W54H2( z?-=MmM?krm8gbaIH?6}>OyTFG4~<_ud3tT&gb*^Gn31 z0mj+&wKW1&UsZIhl9=_Ny7u&x#W_|q?H?;%bla}67vclTx@H#R1re<^(mc|9ZX!cP z?BT(^do@082*4&VG^Vr6#KrFY>rO|y4T||Xp&yce^Cc6R1<2R$rS-UZSc z%0n^{o?Y3D8(K^=hrsr_j$Q+0bmO3>GPl|5)4-V`WZ&j7IDUJK#|kZb_XD;D`55Pe z2e6HZ9o;j>N8o4IveMUnkpsFAvHb;wG)IuO4BeV5XL2c3n@4vk7ZHBfG2YsGN+vccqGvC`DdP|e(N3Ya=UmrA zY1}zbe3-9m1%w^c^5;HK{yE(}&D%k0OV2K&@s+u$JV@?HgR|~>{W*CBY_nA{ z3U?ar&Adp*rZnp891rO8Pw(u*JF~I2*8VntZv^7uWwe!}2Tk#@*cHwTnmKW?L2tdl zTRK=3DrHq3r`b>-mVFe8XQ2>cza-cme%;*%y-uui&Y)}0NqLPl!pC1#FKsu0-Htdt zdIv8f!#LSGvscL@Th+2>ZfC2Y70FT$gBoRe88^jgiE9KZ;`Rvu!uXFQi5e0KGWseD zH9AfU#x%Zw_BSJxJ@=lZ_0471sSu%QPCL~-u?HsPW*;&9l1*ZyL+Sf)PIF@xFO|ZV zZ=0Knoi`OjdcZN!>^Yu?DYgh=)4QU4e0*+uXBQX6Q+7n8Qy-!vOcU=vQ8&=p5LoF5 z0cyJY9pBBi&U_~9-AYpfeUtp9Lm#~UEQ2BP_}wKwou8_}@zo>(hq=F6FX zv+)l+U_L@PmelEWN^dNP&s%c%A7r=g$9%tNQ=igt1ht7pP>-%LP8z0#%tCfQrKvPn z1V$}?0OQTym&i{*Cvh`7$=%ZNj_e)MC3jneE+xA*)J3ts;5!zkkE;~o>U3%5_5T@Nffl`qA@VSjSBsVXDzfiC(+|_2e%Y?P zpPtyZL%rv)E%uSN3K^t#z(b%TNzKl};ggozH6>HU>T;)Mgqknhqn=*hbr>^O|!(cK||go=zj9$$Mff7Gf)(PvBSN1O%R-=gxC&XQcH0{q<Z3 zorc=M{~FrE-wv1m{*Esd&wGuFsryxAWF+|IZx|-~{dv{F2^h z2GB4EjIL*TH;LHMxwVfAeBLjZ%F(O?ih?V%yvPU@2_ zeKPOlZ|r_UuWQ%Th&xpF%H8c_2W|-7q~G7j;{2zEhLnuVkS{nWs49?62AsmSiQv&^ zmRV9J5(%$MzUixIZ3f|H&*a$s8{!WS4~smg-NQRsxezpzxOfF1O3t?gJnqc1AAvoI zeT_ja=e`;)RzZg`-T+Gc*C{}{N1OKChX=@lIr!J+?M?NGzDbvn4o_-xsZ2DPX?g8b zvv7j@uLBE$iKcS7cOHjRBiZWC3PLaJF9hMvc3gSgAfebvU@9+@iZ+ud2(v_4>jh$y zL7x-@%?%cteaV)0KJznpq;wwG2&y<$@(!g>Ow4Bz+nEBgWi~UXik#B_m_qQm! z1SB&pkM*N4$su?!A<$^_B}g8Ap7`f4L3Deh?ZIUO+>rAtJ-3R(PP3!-y_VIn(qZ|D!HH0-@CnNBHE-9(I?k4wi6oTksnt@6T9qCb|xn$q1=k2X?L2U zENKGI8{FN_5&TOA&ONb5A|Ei(hHYnJl6et5Q+(xbDa8#T_bxwAWpm?afTrxDD5kEg zm-;f+6rs{vyRWot2nh-0ukm#>&U4kEex|m2(Hfgq39~(UUsoPT&w1&ySBEHBvMv z?Xzzzx3>2}vD7|(rT^GI(lCQx-v+(z>*?uPU4bG^>V(F~TQoP0H*d@@jM}f|c{~nh zs~lkclI%Eb)S^E(SeU=qlQU}Mdn#nxK{ZT8GI+IReob^Bp@AyE*3%X8K0>lzy&`1e!aV2AoCGgo) z>~v!aIv}9RTyJtyz9v>X;K!O{^uHW3v71E(H0063>5>*DJNDe(qO5o-^5eQw<8Hf_ z*`Z=SYirtk!+R{nZ51jpPl=5vsK-Vsq^h!cX_a+MwZiA!=%b&D{#RRB6k=5H-0~&e z_VC1Ptj%$9>%Ekgq0T8$iG`kFsGS0f;Rn!hjL-SZvIL3SgwWMf?|-)PwuLD{w+2XW z#b7(jpvzP=7c+C@eeF8hFOPrK#q*rbseMZ1cPgK+wlIIw))iZjPmBGa;e%ftBYJK7 ztLwjDt+JSyL6S&Lf|B<*YxO*)8?$1mB8tk_r&MzDpy(u_#>w|z?Gv`Il#gn5M_;RuNpElC;|8m~KP{OeKuw44bd-eG)&92r3lLHi@-nENQ-i>Y_m#je5go?ECMmy@880XB`4k$+f`oV2GvNf3N$92JeRAn1_;}BYvH@h@*i-utpv_J2`9v_< zCDP-elT)K|H1#gfi`u=mGMNVE5O8lLeAw_b5g??mi{^2$mgAmHzP z5GR8nuN=wKZS>#Mc*`b_I&BL zw>)X*J7#*cMJfeV169M8&&tWkLFXvg$KSx|H8o`+Qio~yP>?vm?;hai=dW8~?~;)y zm1{#1)5gs#K@`#>B9ED0OGamBWN1-Hd6;_2*XgKjsYKI_-9Aoi!Wyg1)7dtXdE9hv z!s-QEK;r%vzFelthxqIshqZhiiQi%VMqxbr5~I1EYeGBO#oa~mvUw*;F|k!l=@rqP zB0ut?p@q`Sac&rYT3tZrmLgE#m601yG2*>{&p2P=VmefRySfN800Df=IOI?B+^k+?ClWzaI2GbZUDC3lTT+0gAT=ZTrox z-rvQn-${LAK9q7e>6r(XQkTbB6<$T@$hEZS^Iq8T>|n|PW@ct$?carNAsgQP&RBos z#VtJ4@uuJ2oEKpL=02mKG?lr$W0%GEbhTFNKM!bQ#RJK4;&cCQ~ECAM>#sbY9@Qi5YI!1(inKwcvZ6ctE(?3Fx7@l+WDb% zZem^B@o;Zt?I`-ezLPY@`$CUsam%<57NFWY z>4W@PisEDA^_TjOhpK~6D&-_Wzf1ywr&>lR z1J=SV`!ba;u5v36xhCu!8h}pC`k1AmboJtj(Py;6oTSHPh7D?NcomY;TRlEOKe~f{ z(r2o4WVFl0U(+n;0-?%=@DW20vCi$?d$zXrxOl0!{_}zCYKDRAcNbZn%P1Ne8kTNF zBcWdG@Rf}P#&Msf5nJ$y;Ii6o#Xf!xW?%Pnl8GhrQ_sxTukAR!jIyPwr^1HCqnH;# z#y|Jqdv4_GpA_@ly|O*B?6#Y#imJvR`stHDmS0`KS=-M4ssPSfyidB{?Aje44jBg- z=ZuHX8Sc6@JZBgc?OWG*Y}pdyL&DNx0ijKPwHu*q&6km}W@x-3A98iimCXrv1?IpV z(!+j!Wc-bN6<*0H=HN}3h7HKcn7iLtv47`j#lP60#nmsSCO_JQC zjY~|FFV`F**&nfFeev^~m+vn%kjEs7_{yA?@fc@o-{{z316+%Bx#52p~cVjR%TU`E3B<&X7H!wBjfsChlyz#WLJn6F7E^`ZuwCdw|9tDHv zUk0%qqUB9|t@w0CPVr!mLgrC^s-aj%RoAj^#+DL=zx zQYIPN8^i+=O6VWo0WN)6Sy}0~3xX^3M4*MVb;ST|ZzqQ-+58Y~qH^?}VMR~A4G#E! zX=GNg4=3&8ODZk?y4cblyz_p^@6ac$byMLMfr6?6@(JS*y1>Y!=kXt)t(b$WfkZ4@ zU$nkjsX?7@{>kLGy9P>xe$o0wF}mzp*q^%qa{Jc1Mr*H)OW$AGR_qKaTSvE#ul`}$ zkMZ^yM+&i2XTlya%Cm!vd8o72awl)nAJw(lllka1Q{u*H=FjLi5h)>`55GY2X|hb8JDpb^twB9d@Pt8Rtk>eO&(6CcHWMPB5yT@Zm>sh0(hyoe584{dq|mq+6aiMM76i*$T&jx+r^+b zef@>>sJs}?>qhUK{S*fNtb`Yvb4;#ltl16xrJn7|1teOS`kt&M*tha}WZ$7X({;*E|;*!QO7 z-B+TNWc!mW*<&fXkZs$cu&q0Z7j9q4FC64_G!ye4(Ilk=CE1om) zVkqhRZ!gM=&AtZkhMdl8k4V3=i^Ivd70$uIQG9t@{4+OHLY?Km;FZnq*CtbSrS~E4 ztnA!Z&Cq9b2>YTbFH7}Z6Ji?+JRKymsvAnnNs|()PNbQbV-HYS!>J<-7H*nRXClI1 zykikoh)HL8X~PjyHu?S6nxuTo;>QJROsA~*lwp&V#h2xlqyjOl zw0$E6F5PDRvo$u=)1mrW)9*Gj&D9%%!>zl*-Eg{6o+f%Zl0Tic{S?oCbF`zsGg)@# z!2y-Mebnh=CsK=J_zaj?f4lznz8jiDVQ65mH+Ft&E6Dl+`CaXRRmV8T6uL9abLn!D z+vQ*O%&>@j5^IBZzN)bF{EeXq^s=Ed6|;#P?5gwc6!-1>Jd=93V*VYPAI&T(2KV7rkuvzPV&0iyQsNLRNIW;=vfZEc#%~uXrgs=CaE%~?k_QIw#kteDD zyszgJjf&eB&fna>#ZJWV#T761ub$RKGvoQHZr_>yTLt1Waxw>+p0A!$4!AaaDxsm7 zn*B?};8lfJj#gcusJih|(G+1TV6XqMkmq>q;^(g`lXjzzPM}Kx!;rD^;{Y6I%ewZ+ z+b=pSO+`;1V7%+R)-PVgLYsBwHSOLD9wM$P)%-F(|^>#P$>KQZ^_$mKoT%4S#D+iTEh zhIVTYbspkz`1=lAQR|=IU0AB0uqu97e;#@VBYBnIVnelkkMZ`yHy-5naYJL3W=Qqh z0J6b1?(fVb?b4E0$>F?vf5J(IzV^{z5F_BLGH+uwSue9v-y1_BS&kDVxPidZw%!-r zSj+Yvi;9XOBm*wR2QTnmV&~)g(hzWCSlFNLJ@cyAg5u}jGqIEN5AKIDlr-u9YVf_BCsJ6WSiVj{tR!n9%}r{~R>j zZRdyW9d{3XA$`0xP21O%a^SNM+9yI>^X=(j429N2eoiRRs@2uJ^TV=+gLk6pBtpGv zKgLbfLiv|5O7Y-*U%xjKGqdt+hUTXp0}T~D!RgMb)mRUUIHW7 z_1SLqxli49DQC|E(?;cn?EgUS>;JZwBtr#7=5p0%^x9mWGN|rhCow-X?tj&;*|NLt zZ*yd@tE+2CXxXj)YmKqm(R&f#G#z^CG1`U5cI}k|+^pjFC*C(+qn|N66X$4lGVJV= z?+BsE)T%P+kEz`GN$(>hNvMHfU!p{_SI@H-GI`>BBcSb~=}x<313d^Zf>s zfjrQA)KyI`I<`pxxJa42MovkI6>cLvJc_$auE9wZV7Phq>#U1us3Q*x7gs3sCKoRX z`3)QTzg*tqCG*T*y$x%0F8=6ow6d}~b?N&Ns(-P3m#gMNK9P{n#r7r{@JO`D(k62RjWmeNNLN*L81H{H8@l-u)1Jb? zl*B~8u$#Wcp3t+_Ef!%dws?Lq$5d64D7rvyL$lk!(a&7`@##M(`Q?O!q8N&5S%=Gq1{N+djht0=4A4-{u*2?!C?~aEdLiK4#x#%0os*hOg=LjkG_)z35h?uG0&xHf{K|2JThdnyzweejbtQ`V&^q>EineX(C4}CBfQBBL1VR%5>Ai%afD{Q3dXXv!(xeHfNRf^p2&h;nR*LkF z6cH&RB8W5vR1iV%uiSgzd-uKf$M~P&7(zypbIv~d?7h}pbIwJnKu!Ig!9?E+tc z3+GUjtqE6e7ZpjARUfr@EG{gp6Eh)I(=I3|h-s|{fmh4RjkcZwq$}g^ez1!F0kW9} zT^cL0%cVF~oPaIl+;wY6|Q5^y8=V>5R4%E6n`(q4A4fV zEEL6&*6}Xxb1;pPYCpo>AM(kZGNYdQ&4aevBx}&T(gF{%9K487p2I`dkIl}hx?ffx z6j3_=5_pr%P;25>k3#)*f?a*{g5y))e2Zt{f*X-dzdl5c2Z6s%RQEv%T&?ybK#Fc| z71xU^HHV0UmtTKB%i0ke z4u#e!Tfh*0NBOnBbDWThu3Tj$^e!co@N?rm$&(7Gi+VnLA z(5Odrh^=XuRY=_D97(by>CD*KhrZ=SXcXU7W#{1Y_SciBhph|Y`uPa=rSDWptUH_W zC)3%2j2Y?!fDrdcX5%N zEgdsTd6#lC10s#PUe=_C+btyqGz83*bUp%uSpbDv7a4;LZb5bP54b^z&gQnZe@&BV zDb*PPWhn_5GHEUr82PRWTuVUbEPiv=oCGs3`YZ!=nwBFy{kE5LL>Uty<+Kb|6N%{f zxeYWH_g_Pp(x-T*5Z+W|=tK+~Xil#@`*3j$3Y|<3?I7Bl6bv5H;n15L7eTtxd3kwR zBS)KtK=0;$rPJn2U=bzt6pz*(CjU zpnEVp9{mrj?=2We70w!Vm+v0#Zy0ugu@$qzJFDVyrMaj#i_tuk99-UMOxlSG)-_Mv zp%&I)8@~Vb8UMKx&aGs17Wn&6Z&`a4S~+rqXRwa8@-2~0LJ@3u-7M9cp{9PL)%fYE zoCXstqbrX<;Dd_`vjg8NEY4iEqdmq-38Mic#ZvdKK)|m9U zmiN?-LK(2*qr z;-@Q#i!hq}4*3NIMtdTCpKTmIDw0{5RGr1XcArZd?WR2zh3;c*xpCu0(n*4ZE;Q6Q z%T-S1{|si-jk~SH`Z*|ZjZ|`-@qjcdxQ)L!{+hzAOFMQ7Jq3Y*flwrC-9~w5Wo2#U z0Ni{JiewX%{w5|Swzhc;@uR38%2B)6;&c1^`}U76p~*mNv2**hTcw7YI5!K7rjPGJ zK+_gYJ}4HyGe^!f-Tm!Gj^B$ARa8!&9KinDQ(pYSUC zB!dP3FLxn)X5)aqc5h6qu=`1TNiJ8W zs#!p{zxMaw=Nt1Jo60+PpnI*AXY-Y2kHIfc{8(gRI8jTtv^Sr8%u|c5<#5mE!uAMD zX(ryJS}dBu`fYmfBmg>e?A9$&5j|gYK0T%qOlFR_)$}9B{?j z?Gw8-Lhb|T6-gUXuX#{?YN83Ge#8$0Ig+``_e~8A+ax$EmmmuN)DLSh;g0z*&tFiX zrbZliI8cgeW&fsi9;MO+Vj|~*52 zvo~)~*neXG!&%SKkB8jr%hF_I#+Kmb%e#m1A7?MjnVOk(-|{p&{m|h={iUyiWZnjM zl?7_?<_C-}ND{`{{0ds;TB>UFP`Bi?h2-5DDL?a&MdSfzo3k$=sPB0jU2yz`4T{Q0 zFj>hiM#Jv>W3mFtbJOjX_tpl?FX!o`&thEqW>507vwyZT$l!$l)>94NL|0A$75Ck% zu8Z&p0oq_SaO~308}C8kZ@{0iwB3~Fz)ydoV)xDd z#;br&%+3x>*%UIlW8BYt-kB}8!%pI$-O2=&#Daj6i=MQ=BRBHP>BI}sL{16YD+d07^=KKmP468BOr?oxy} z>P>U#6oZM8aw2&`+OojfLR(BhCaPVi61Ki`he|UaUmgC&G@^2zE#JoRF?>E#B1>|darkX| zFeYEg>tZ~n&gV+b1#-Hfu@`D7cd{&vK-WbQ+UUn62%HE7^?~`f6x;Hl5;gmn%MyVS zXW3l^&#X<{vWj9nIu3PwND?Ibm>jM|`49zM6qTcZ^mjYa1OJx^hX66D57CtL; z4F<^8&+v>U56TK)KPHRt2h~_RW{k8)_mVi90BfDf8BgOHIC0aw_IBK=iWE&w>?a``54BMKW{RBW`qN zx<1oFDk?{=LM)(;Mw6X=6jA`DUk$ zXH4N2e5w%o)Zc8P#v-pCJN2RBrSvCTEA!#9D~nEPVF(V4^L)HAkZi6ZD&q}Hnp<%bv$~1Qs4gMO#Bf_|j<3K>l$cs5LZW>bvV7bLa;hB=-;@S$b zZI4g1!Mzg_VT-Klf0fF4yF$nqnJ#96nWfgtd9(am6?V*Q=_ZipUUbPW0+^6f%MZ3A z|BX6mL_VUB@qK5kFFsgkGu28@L z_EZMK<>5(WXTp9w_jfP1pulB9!&xW$HZ@41lc_`0)DO2MzLrqFsz_87~JDmoo)21|?5{jZVvB*YgYZ>XaWhm{0u~$*{8iBWS2TAs@waKS5As zyXvn?6z_5 zbLa31--vYTB#=jM{5*gN?%f%7c0IOA%ghTG2&yMkaRawQXzKGud8keQQZe;MlT_rQ zLA#H}p6L00*jXO!$T)7AFPF$S4UccY@DmLYh^gMh)Z~lP)6*|YM^edNi<b|9D}yv*~NH3GlDc((#9NS(7isrRLpx_B{P!0s3?qQbU$| zbNbV6zMHH`oHw#B%lS{8BsVcL;~E&FVLXyDESs0=dJXFRPAySW8D1a2#$<&<9BQwh z);sJvYnPy?|MNm0ImkFhz1H$-S^?qLZRhKO?n62=(xp-yMl{=TY&(`a~KkI5k=Xg2&Ikw9ah0cf|6HvhK;tedq-rdPeiGG7}0rkjQ}U z*&>sj-#*!rWTQxhb`8R)lp-B(94??~pL9i8#!P2Hx|fD1fyw!_{x@H`+C&JM`|HK| zM|G*PSvh^Zy><{i*EnwXc5*BUGfDM1 zR3f6-=bFM5Kwv*vPMz;v$$Sy$r zYm~BKQ!viPXuji+ur|XT@Z3ty6ywbtJf*03ruwon z6>HAMWB2v(yKew!(AL%#&y^}OsjEUdLf3(+NsSK;URfwLg@9TKQi<+C7!(g=!8JpH zyyW4D2{+VG#hp8vuXLJ{6kwY<{f23r+(@%Z8qbbNdwuNyQaC}!5@C<&ib3IcV7A%E z80U-A&5qy~=q2^H#nZDz?l`jzNyc>VBKOjI#MAD9srXqF^wxDqW@fD1hz?b9A$Pz5 zpUY|l3Uyh6u1vnYfgTqx?t$dAw|D%$&2S(WK9}D|F5T>LU5DU6F z#Z41T%HfX`=uDJxld#MOqKFfpZcl;WC!5Sn}*Ycc)MP=fGxXnX8M`vfp zc96y_{Qhz)cads($J_k*x@{H#NsbVFO)GtVog2X!D`*fTeN_AP1QzmKVUg9h1^Q0NjKx9IkcgyOV8x*$+phA{(Qp@3i z;}MXSM1sT5%a3r%?I#}sC+DXC&AC63Aa{UmYT~>V1MJOuU3SpN0@l8+FQ06)vV3Hn zXx;C%#}#=_)Z}jyS;D6W;}9CG$n{o8rfbIK;B!Jc6>4i~B8rD59 znor7xnhsRIr{7P9rh@8;eoZqJDSK?m)wFvCZ~=uoRX5#!siyHcu!PFGCLorZY`nei z=^7nhW8}NzL+-BzDk=c3(qASAa&d#`!xC8uwTF=@5g+Ff9kP?iVk=z_RJW|{DHj?{ zpJAD)G!LmaTqeOnTwOpwGvcVxBCHCIY;)64&4*=1=kA4=n3zJ5vSJFAYXY|GXKuvs zAM=s>z~mk)s0V!|3`|TaRv%`rw><3eBe~+8`m;&-_9JOEA{7%Kq2j7fSG=DA>k_3) zS}(drjuc0>faJWO(TzDz4kdr~gTz<*4pbL_UwvP`-mNN0O-~;`_R)*IHmD&*7OYG< zf&C+^to6CPyxdRE57J~vMZYzu>xyl^Baae{)W=WW6>da-2c(!+%Bkr&v~00`uXe+= zu~&%cw*Rn@nVMkegP@x}j)t1!-PD)%ezFQ}!}_?aZ9zja7J&>&KCA`tgIY)rW{;2i z`hgsB3%E^SraIaRtlx5o26>{>fQyqg;asq~>-nL?wUtEw5aoC?3t`*p#u#`JXdh?X zoqvoIJ-z9M;-);{2TFua!BayB)z_3Mj2Yq9a~8G&aK%14MXF8VixwB%0>@HoXIy;f zd^Gm5cofdi{W)*6$Z$1Db79k@o4V%QD|IXupE+v;TyVee{q_eyijLkn^Mqylol_*^ zfO+BXmeMOOn+g@i_y~)(HyO(TNr5K?7ig&>fjGY>me4-h9P{@u1pgeORtxuwu+E3% zPl|L04NqI#N~L#EJ$s^=S6#|t_8pjUtP~sz*=F?jH?gk zMsH{)1>S^QHD;@eyMfsXb}kq?p2=MRes%fo2!GMTPediRT3OJ10;~bN-(Tu7Eb|_m z{u^;sw+DbTY3~=n!Ajy7cSqS!lyQ1Bq6c4}k$_$7R@!4ZQP8fc9#IJgz`BqOLa*4~8Kf1J_zLEY!L3q)@a>!*1_MDs;>Z8|Xd6KRz+82dx%>mSONJ z`^r$_uph{C`)+C0Ax28%z1S`tZofOnJ0lsZ*yniczT-P~k$okrT@un75$y zOsI(cq)(+~FFnRiSgts*WPqH^)mNcI?0Zn2Tui%dn;XxJa)&4S#EBOGlL&*C=CfC! zYd34Zy2?8Mxc!|kfk^}Wv%&yXCnf>)0D@2ORz3z&sP~hHEUIbS?I)cvfWPe{3LL|jo?(LM`65j6{MxFzCTlzer@gi{6$>RSwc!R z71o3unLYm%mmUo#qRq1j>}gqmv$7~u$=}jHfTi$z2dsOe;SzlogFl%EgZ!R8_I@id z7(jAU{+qV|pkU?CcaUAwPnNl$%*kA!?89QcrfkG$>qah^eL4dS>(gKO0PN@`0g1YA zpq;n(DujF6zuIK6>R3%{1$weNT?!Wvonuqc{7$-eK*$3T6!k|9K}f6 zYVElM|49?Sgq%ucTOK*Ll*2=3Ly(AGs-6Cvpp~9XW|5$gnM|fL4r)RpQjO=SpM8*c z&v*l@AHea$KV;82eZlKn0W?r#=xKrigVZU;yG1_CdHfR9R19RnoqN6E)UY_0N)1sn zaB*nb)6|81Jv%l8Shg*O`mLmZ`r)qY+J=iDbd=YA**Z5jSAE4(Pp=!;5uVZZP^ksk z(oBXsj~XH%nvyLDR4wXGlVD^7W6 z-1jND^aux7OF?8uw3@^wzHR|jOHnBmo=cgB zc1_{6-_7^f?E+?B=EyOq{TRf}#r$o4J%NH#IA!z>8JA$Y>dV;iaHOEMwKex#w4Kfk zgP__|wc8hgXQ5)5?Pf!Jhr10zbI|MPh#hgSFi*b0nxjXEs*(IFmu|zt&u{uo1$;S4 z()KuM*Y8r95A9t8K*@Bj-+&$}E%*MgbH4pLemCoNYi&hE1r<r9mvzb{LtS7T2q} zX+R;6%3@H==md=2F%FHiE|w@LnmvAuEenKQmPKj$MR1k!a_0!}I7qd3Sb;L{ADt)! ztZJ0BK{}178SVrmPsui2N(vN#Ivl9J8-(}Ap`t!8*)7Wi2$6MmEHth91vJt|Xr)oe zE$Pt?0J8P#a9M>rgK=nidFz-S7Z;aaqmR$h`pb~6ibkQASyp}hAd}52we&w;ogPZ= zLtLzsYgbWMcgoM#!9#ntG>n;cEP)W}8ih28t$mI=PvJ{$y$|d^h@yi(wvoKMYLURb z%9Y#UiSeF&sc=C5!>yd{n7CN$xl7wQ0)BGolxTN7zm1B@%IH5^J(=su`rD>lQnt=N zjOHyez!HXNHULE4lp?SpB-L(QnNZhP}p`pOLb61!hP&kX1>>7(d8`;4wxwz=P@NZ?dzoGa6jq#BN1Bo<$ zh&I?L*I>tHG+~!^zCa-=SsJp*3+9xD)Gwe8^ZCmc+C;#*P@>Hczxn}LxU+W>0z2a1 z5-dx)cgq1P>q$R+eEFEGgy@S$`ntN}Hfc<$G!TN0D)d_mS5mwor)>YWX2K<)rsl}8 zICc#0o(1u){jnMrXgJg_NY~fbm+fGa$&Xqm(sjBWl{};7$VN`wod*@h$5^>;7PJA2 z*qA7;{f;g@C8=j;WUgl5asdT30yRTki0QaPFtIJnlZv0GH_3*OG&w1W)YwE%+oFcN z#YsW)uA0%b$n+f@zoA5c9iGWX*HI_I$UCqnJb zATf#AUOiph+`c?WkK;MOywRK~{LVvhgqyaQKp-eSdI1I+jsUe#|F}qTRg_ue${S6b zT_LC+^DIg=Hvy{7x=l?>E9o(C_wHSpSAXi1w;GgeNbPgPJxYahA1hTD=XHPr%n2p9 zL*`aQK_NsTHiS9lcJ;EgKteT#yAv0h_*($QnDwn4`ysv#T{>?kDSqGxMmJL5FOf2+ zij};E8OeRHNDB>mma*9WzPnO2_3G8n@v-Ukn1R_NYx`fx1|?QPoH9GKq@!j4n$v%w zvw05po|9~lBDaxwmp%NBcr9J7z z3?n$E*l-Pl-e0^f<>$~K@Olg}2M}3k$wlMAVj#o(xv-dV%trGsP(n0 z6i!p!dTUad!R) zMVX-%{sl)3VGO-+0@dx?^$HCd57#NAj-HNw20`B^dl1wCyWI#f8NKUA{lc}FG3w*D zKKVGajMt>_h)PoC@SF$|zH0)z-CuBV#eJ&-&adTPpopCH{0xTyt=!5Zrg)VrKm&N| zbSPT|MhKP=`FOta0m68HL6XT$Y8NsBdRRUs`SKv81c+O&RQqg>8Osa-S;p>>uoV>F zFrmWY*9?z7fM|2`NM&nN9}ZRxkR{w+ya~b(uFwER@_vJF5t-}WyxiQmB_)Tz)c{p< ziU}PYnLcp&2heRFDhe{$47V6wx}?L+L7)l5RhE06hZ!)v zrlg(vW)JRq_yNwncEgy&1~c_}jH{}We*m&g zxJJ7FF>`d7=bI|ApLoCV^7DjZU_BZ2qK6%4II;~UvbGz5^1q5r@x{YmR>oT`C&-cNZgY~D4+&Ipes6?xW%%Wx^-LR#XUNw z=Gv=iSg!Kb2*0U1T@!xDEXp3R66;Jc&*wd4ksW!tV<%t(ZKWMbW0iIiixg6h zIaK}Z)q_=nil?>_9brsTa2m4r4dq+lVOgK>0NM}M9X6hH2ct`KwQW)hYbl8r*cMtR zStofXC8wA3SM~MuGDm2rsUf{K_+16bm4x2X`lyGV9t~p;N!w&)uYtG6$P8JRy%r^Y zaYgBo`H||QUe|jw@;p7&^0T3O2Hg!i+j3x&F0ZJ|Ec(#1J{V5oi7);jac#Ht(vxGk zufpAgLH8ZFa^;F(bSIEc!ABXg(OJ+`>*!F4oF)V7mB0x`dTl3Quv?vDePLSKj(3A( z0+m}E@x%SQNjRuvqIc(MhrWUu*|g>uzkTfZILWARG>2>Zk!gI?2`w!xWkxM7a+!jn zmv6spT0n1>V4X2aAD|jOcxB>Lsd2jO@pJy{3((@(eeN0o#Q>eTe*;%BYvLCaxh`AH zL1?9`P9n&hXbFeu7D9yaa>!t0K4X@Ni-Fdd{p*pkC6q93Do$!tt()Dt{px`l=6|c9 zgWc5jIw%?}U-FMDii`J+&&VPdVgaQZp|OTopy+{Y11v0Z{CNkNf-`ATAliKLSP`Oh zh0-}DlI19M83_94NZ(H5^inwawgz$#$mvi-4T0bZAja&)^ka(G#gIQEF1u){tzf7S zKGyZf4o{l1U?3Y|c&(k3&{@qT24d`=O8N23&uMCELU`NQr2yQ*iy&w79I1iKV5+ea zLKJWWXlsTjpES*`Q$IQi3rQ?C??NsBMDxcX)2=^ccO&uq;n2YnaSu#OGaK$xiiED8 zYQ?5Y0_C2SyyW%8U#w7VlYu6EejQA_iYCZwwsDI7?`@T>pQHUq#hk!LHck<`F|X~r zjoa=glW8E)$feoDrq`u16ETp$v9H9JglOQk=R;_><)3~(*?~>k1k}jt_BIqgx_Wv} zZabQ+chQRiiqH*&uuYKgKHmkOkHn>rKd(Bwy4q|%!(#{22UrSQZfG(VN;*oN_6mFF zJK}xBDe25M=#iOC)dIm<0dF#eWjMEWW(SU^JB#Gs2h|hd6Rp9ptGuQOKZHfe#du_F?bM^xjg??+DsElP@{N;|lep828vX*9aV%Ct7>#mokjW&eblkzRWtS?r3tX#j zsYk8c$!!o>iXYS5#;CIQFDny8Iw>~Dj3LARN`h#G^NXRlp|S2BvCqE0vx6fW8k&I+o#t^~VG zN>%ux)$t1;G2%FS^dT~=5S-`@4><68xlr{lYWMqMn(umMiHwK;EH$%jfZ`EZ+MM8lW&EKpWp9;+z55DU3#v| z&JB{t7moaOV`JmXmvX)DZR#8x}y}spyMzJu{(d%^0Uiy8k)Ci9;I!eKL`Sy!OePjnp z&&bFKT;@I3A#dFVrcLqQOH878pQhjIhxYtf=xfwBxQI;;KwBC_n2DUhuv%Zqrs(e? zoqHC9-QR(Rl~@371LG<(8Lq%71mM>->KCbQW^n*EMZzLN+kCFQ;ZpKl@vR!Z?`Lzx z@W(K$dz6XsXJ0g)gyp;!s%nsm8Vq#9c%LkkXI^TrK4K2f+7jn0=O{J{!Je!3dw3oU z(>SeKoWzQGCtUlNAO8$|En=&B85S@0PJwM4TN1auTNGysf~x!KaW_0yb-J*}dfVS4B`2yRFg;!fC;3p4msWJ(5ugeg0o5ku#Nu%<~} zDA<=nF64K1cSE4ZO;ZL+b(#sjh8`$Z127pkqu@1`@azSOQNtIl$|69Q$zUm`C0=dK zGEUX+vhx*{w1qeXUKgy*7O`I-5i@K$bN4Mf@Z2EP9)fAYPeh|08 zW3N&Q^f=F_Q2JL5^+1xx>v+{5rI;Avk|(X;gveK&tp|`DyV!me7g!Kag2eDp5zM#@ ze*Xm8{=-)aNdjoI>=%2!VSbJF}MuF5Xa8tsGZP)@8CTKe*(>J5gls4L{@4G@i9 z=yd`e9jD>l*YrmdiYhoF>RccdZTBbCUUK2Hj^M{ngXVZ~X^=PpNcYHv@;8iuCRVC(IBhwNJ7ys zZB&vh!a`pP$R9B1tCXsw^2G0-AWkB9Gv`Y&QKf(1&|I{RrglLRDqArrO1GMDNLMMC ztk(KS`G5}&rm6LyDx{{N`LqWj74DxI5XTRqeOXQ@jP|fNr^xoJ{p-U0k0@g63C*R(O1$LV)Ha7(LpS#J@$euj&#`158@3PYm(v0O-VjP zQ<{LvDFW#-l6`x5+4J7&0PFemf!N0u#ITfGLk#GLEN2nJK!Oq%i*!SED>%y?V`bGO zF9GsB*w4T!2gyhF+h9ol{8t3Bh;h9ZmBckcY8GpW9H!AkvPQI+Y6mtw6Vx~of<@5l z3K;ci!yB`WHutQ>qttbGc!`~Jj`dNcviedW|3pdzzsE_Es_S^^m?W@}dA zNd(ld%$qkAJx5A`W)2Nu`(`f@^8V85uu{<1Lgg!opn4O;jTbJ&5e^v`ggdZExIo_D zryR`a>kveLx8RT<3+`Py{M{+kkRw<4Iu`hW%PUr zAw(UbYk(UOA!9=H_XzPs<8TOdb;Q5EFuX`|QBD?Ti6zrwXV=CS7Y*DwMkxK5In3Eh zO?GygdhdT9T>jsVV;ymxh?c<>}uP6tQkE|m?#*!Eu5E|r4 z3`UdA%+}n+o9G(y&)>0V9K6+%bUyG;MmxYigywLN{l|O$b@imb zNmoz$y8k+XV1$gZms>E}o^*bea9r(xQ24Mc>6`!cLD~QHL2W_^!8gEzbSMuv!T)(A zrGNW?Hr#-afFLvmCv8CV^6(4^b^xUd+RzU^i4F-s<8}1VZ~{Yp#d*KdC8*H2?qr literal 0 HcmV?d00001 diff --git a/images/hw-seq-cst.pdf b/images/hw-seq-cst.pdf new file mode 100644 index 0000000000000000000000000000000000000000..301b788a2a49baa95d99fe1b6e57d73cfbec13ad GIT binary patch literal 13771 zcmd6OcUY6l_HL9dY7p5L#7a?71R->!OOY-pRUz~afnW$hieLjoL_h=t1w@*F1f&{T zR6v@5^xl*zP3a}TUBSK2-t2SEy}#!^_m7)D_{f*}X6Bn&v)22*Yli)byaG2Lj|h_e z>$mzQqyQ@~E7r^oDItMGX}dXDvZAhOnAusH0k9c2eoYfB_b&(;EO!zwB) zh(sw_+FIM-S@}eHktkVPyz>=HoE+A{3F~O-h-bZkM9E<>Se%xVsX5dqZ%MEFM?UO2yOx?beD=-3szgEVMfR(LZTlnkM5vW>U;TVO41J@N zaV~@_`~k;n4vy97wQtR~Q6AIX&BNA8D5AA%*Kdj@JxGSYYggW6I&u0H$ zR&@X47uAvB;WNX9uG2;zSPbv`F|cF_RDb@gT^Q~?I?4ANiSuw}SSy>J&%nD%oevj@ zIm90$D(R%&Oj8PSeo|$+Qjxu&^@tr%!&%-nI(TDEs+qZ-al|rb7 z5r(d@vGMTjSfl`#0zkmP!Z##ERcVwSs zXD^@9VbjyMo}HF??8RVI8S(U~MMi2cS9-Rvo?eDgv5CH!*(<};EG%kre0DL95S) z3$@v!`>bQfgQVA&=DpL5$x<21xot+F>4rHrSDA;!P}74|p}oDmjmwu%+&*Z&@R5f{ zWA?MFa7f&4r>KOm4XTWvuWu>yKfow^iJZ-2Sn%uRJi?7uW`=4KRl>e9(HG;Haq}W+ zxUk5`>rktYV*1Ap)nf%Wf1b=(9&1Wgs2KGmdasNnpS<+2a+s+&hksDT%|c0O*RhT_ z*RxS2OJ=JJlgC6HkMo(yzcnjw$GP7m5hkMyQ)P)cbu;K_ao5MbVLXQJgOwrUt?A-! zGlO-};vVzg%TZBeGP!uO*szh9xOk!4>~N#;gVDr5S>ortNoOrFKhiQv#JUf!4B14a zCd>wq@|f&54%O4HE-hhtiz3$^8R;LvB}&YExVO_~yfx8LF^}>kPL85n@L=TIj@_gz zrZnaZ8#Np*3&XaiV&>uG>YCr?Hy#3WONxjQb~xGW|Tfk6v(M?NWX&?11U@ zKZpxUUPT)g5(14yQoHk_D_Qm23O={|{8rHsThFQc=7L=_N8Zl4Mg=xKD-q)?i`~bH zT*h_jf^3dK2cM97vn*Bb(b6yJwxsG96y1C~pqs9rn`&6NV1O;YB(12R(3+|f5J+|! z*v{fS-CGJ550)FUHLCLP@L*0m$j*P+s7b0mqZ+~E z(3xZV^J{s>8OxgRwf=hyQ{5!<+37QLjfZ53Z^%~O1F@rVTqd*X3Bg>0-zm$p6lD8& zI9+AfUgxmzaNT6}6L~H9eO}^(iE9f2?zZv4T-gyebE6HI%m*Iv%E}}8yr1V^T?*LK zC!uC@*TR5QSlBd!WaKO>FDH>mKSMl;K_|p@bM16W4fjQ{cEp~ul~z#9`rzw&+3iRF zojJq1nj2Nt%V^cOh`ir%ma~cRit2fxEA!)BMF-9eB1vD#nRcyjY`d8Eu<40?W{hU- zDyyhCD@VvwdKDw-(Wqo?ZS9lP!;>(Zwt{x%*3TJjN@iH=J6+85p|{v0 z(IAXV@A08V=kT_TlAsrUeu_N>E**W_>tZBpV(W4ox`YJ<@fD9x95}0f-nc{}R%Wbs zWpP@AuDG~ZPF7YJ+gpSis@_IJ`$LZ5n6R2|HkmAKtXiLU7e4py*|u89z=|DxR~c3t zG3C9n%F?BL@#5`T@eo5lQPoLIHtv;H*Q=La(NMhA1JVhnbzBUzO`=o56t?OQdFfO#{8NUr_?oc5= zGFhDJp?m>Ld*ao4hLiIlt$|RR=4c}Kee`wL;`N2mhEra5`)(~pJBWwK5SKWk2fu#` zJjQZsZr^0;t77-7;l%%AJcF#Cl|B^AbV~0H7{nS z{je1TeKB%sy$iTGW@)eU2FI9~Di&GSv}*!TC6$L--(1&P7;D&fN+DB+jg8IMFCZ{* zNKZ3vW^mBL{fSP#qoMH4+9)B6XzYnB`!=3Z`dA6KkG=L5Rp^?RR8vlL+NJeccHK|Z zT|Uc{0hYa{du2;Uwso3zimXP3g*R@pHU0SzOT7pk=?QKEeQUAD6?1z2Y7U$6<4s5C zwCjwNRE#7?Vp38JINiOc*GAbH&wb5qgdPVT724C5l$iKaQfWG`OnTD(LL7zR_uA(o z8?kr5)@N;$HzYzLHrDRlxpQX@6Oezr8$xTxv(ZtTJXn^O@R}qBcq`jszgDNU|q*to=iT1a5Xm-vp%z%GZ@`$s(gH{%GB97)WugVprrHwDo zjwGgip$_YLvMyR(eJ@#hPb8nYFTFV5>1gAYkuj^Qzz`%}OEI&UTUKC%Yojk-K)8sK%@@ zu)qUy!zxD-iI)NnVa{ql1B(u+%TO3`|Mn>`>nBA6A$THP&Az8V$U}Usr_gm-;Dozy zbA~ZFGm}@W6?_H6i__1?p{rT!$ozwHDDD+l-9v4hr%uHKAjHUth=`0;b?(5i$A_Y; zuAC|(H0IjtJ$F6ngRZ(@K~#^C7_$fj%+uOTJb!=l)@S7I-KOGh>&qh!z5Y+}UMH-G z%g>#J9Xc(PLnw4kTzbUgCr)r1wiJ7~cA%RE+V^*O%qMct=G6+h+tRV=g&z!#*wDKv zEiIj=1K#}9$&=^1zu@34nQ@jJf`U&c6Yyh=jX{*IJ)|c$D$z&Qj;GzV_UE|wt8M*4 z0(X}(AOr|if3%(E6zjcCV!t#a{(D`dfMVXmMYc^}{i%MmIYrCY!((oAAK8J<-Bt#G z-1&2?l9I*d6^}6on3y6ayYdaP!g8r|P#<=cOZSb5_|LgHc@+0Obfnnm+UnvdwQnMe zFP%+cCO$zVftjd2@1@G+?d=UC#2#(z7iqt4eRm|rqi*6dDW$J}QB~A)DHE@Q!|`vF zFiW)wmS8%vFs2ac=w07A4aj;`xAt-a67~t^8j2qoA}bci`R&C>2sHwbito6Lp}r-7 zsAk)h$KB;Wp^z&qN3_5{-lV*O7*n||_J+YlB)>N~(zn1OVI{LWnaiiQ4x0n-cbg&UV$o{`R|hMym(NDPq1 zv}X?0L}0t}0@uZFd@XA;_BLFpTku+2c^fh{H6<7{H(}dGG^8*b`3zohX$ipaSpN2g zB8ZRo7ARAN(^<(TMg8RgOa?BbFRBK+NSg01q@<)!RYm(;eU+(F~=$!{%iw$Q0t{yzy zS=yMWN<%}lY<)KR^kS|T0bU`2bSB%no}h^zsXHM&^Epz05`Y2&E^IX;Zm#`RCJWtLL&;SyWa*6%E}wu?YmUb8 zM}_PxGML~zA$0CG#{dqrh7ujP8-aQ<;byPHPX@5MKjf0Im-)^T^-Ui z+qYYYC-)tt2w(9eNKt;2p4Eu?BEXtg*4cHtqM{<3z9x*zy2UsAcRsS+2`1{eHU?oi z407$lK6-7gc{^fOcJ?`5SS=%D&qx5=&8a%}?q&FkuWMI@=}=Lj3(>GpcT)Dvful!L z3Avwd{pf`AlMe3G9)0i)N60ebalf!eQqoNFSHbfDJ&IAIR z?#=1q#n;0?A5si=J-h$c&{l?d0o1-n?8>MA}=QeU8*M3{*HDaD) zPbz^eT$U*KFJYmP0UT|CF}L+VFv!si~V%d7fVA+?5B@dP+enQJ3w*QBo*jm^Px0{7 zjmn1t1WGYHQ3(U|r?EpH>5mB~)VNG_i$b|?p&C+rLT$NrEt-X5!CPPZdrO*PL_ka! zbnVHbM~{FmL`K=;=0>mP+TZt<`AY_Z5i;`pc_~?TBm5Z*E~lCxKvc~_g(arH#HEYG zxp>eU@abS^Ndz{PqT=GPkpfvCBoI}*h}|21szuaVRiulGibnN&irlm&Wz}9C=hP59 zaO6k|A@K*p)(SNfRq%1J#KDddU~mlh+kj2W+{9|QrURJKg$?hn)qO7b8(}yMy z2t(Cj+>!PoBKhEsQVda)9b2p&fchT8*H51wgwf#<7S6M8BYJsxNl8gff*CX=T@Ec(3llAvcfxphcsLA`?iaIK_xN(r#{Y8hkpbW|R$ysi z0dvH7tyUveN~iF5-rZYX$caEm8V?T*jfeV7rbnvk>Y#sH%S2b!)+Pq%CMfO8rF(n# zkbUbh?z)iwa^cy-FCZ{hKzjEM+H?^kOtdGeGUcWrLbq6A(A*rJFmf@MZkylTEsH-P zDX9_dar5SD!(A5+Zkf(g?Cd_n1!|G}c1+v%Zk-b)6_r;c;+43&;B(}*S{_Wl4UtPH z6?{(rmA`j^^9A&?eyFCp`boOV<;#gfH*VbUHRvh1^;{Q-a?Pj|FkofpNzl7Ca4q36 zG0ew~dHm@A0LWQUQBf;3*CnW8`#tpa9i%K^@r;Aj0CseOxd6B7HsFai4|{rgZ0+{4 zNS!wj@>swSRNsTebZ~;3(x0DiGd|Wcl55{);{d$ozV>-q%aW_{3NZb8hvl->^uQyG ze!mS>=I9XVy_ zGFZ89DCJQ=K>W7(?=1&(-XfS#MhQ`%l%?_d*1ACKPoz6=;6QOvk&T;@(u4k^LbRl6 zIpS{@iGXLe1*b_2svrhAHAF~aUX%-A`b0FTyBl5N1im!K>1&z)T%T2KlyU{wZS*0| zB6K}*w`ADw*K&%ZrM+Y99KXE0^YL)J^JS_a;RZZ^M{BaoT~O2%eduwPu77sk554;~ zdT8v79w-GMCTKfgFz1bz%9)J6JOSXYm!?}=Ue3J6DIZbdx?hPAv^3CaA8ob$s+nX|JKHmlhJP%3s44mk5IOtLiz7! zZ)|D;weV8f!c|Fk4eSAlG=E(6bs=X$un_ zavKxPDWM;GA2Um;n1e{m^UlsAE5Rz>x!AEstUwnWo2ru1@96l2zg6vn_P>oDJF7R5 zF+$wqWrnuH6Cntj~c28XX=)F9|baZ-hlDo)e zRar$PRX4p8q~C*|D%WXmfcWb}$5c>I(73S+^!9VX{JA?xvP8%}{Hrk)Y0|5#F?p%A zxu&u*`IR_hvX^H|j%|}o6+}Sq)k%>R)6p++)rFuj$J#v0$jIn_LKoGrIGb6hX!q5Z zJM|**vn&yF8y)F`?m&?E=}1}IaF*evgAb#XV4dV+I%K8q`}q9Sxq9_#&fvEo=@?Px zq|gs-bB8>5>(tQ^X>1AYrwQ5Z`x9xJ2kiB+FD#ZE! z)ZUk*#>^Jn}z=61vmYb=lnsOkr( zP;7d6GF$(OY7$G9hmR$DLd<`XZf4vhH~cx$oFF~kmXRC+vKymTlAT(ui-ko(=-^`! z)_dr4azvoKTmCvHpv%k4-|k+6QMX7VO!wC68oqP-FyYniDzz}(XRH>P3cv-7ld2e} zgXn!VF;jLgNz)hILHp0YN04-M@dsE0ZGt;}uCWOVx7O5*`>}Xk`DYwl17y3Sb{6;s39e~7|7dxqV2LIMr!?KYax>(7A+lY_LU=U8Gys&w0Ero4kcsahZR5#3$Yc=`6iMHFkjF@h2B2yOIfP|KJ4QK$fXK(DT+@G1p$u z9K4Q@UGqEF=@{sw^p;MB0iWgioSQe*x7}weUD$X0IL7W3#G2TUkT}Afm;WHSo}NW1 zr1iNbjTYkG9OU1TwxQc>tw>K7|84DBi6?159&)exlLZ&Mwsa*3pd%9# zQwJLO^S}QZ2B{#Gvjw1qj*X4kFwb{gU^$-J(zCGJw-Le(8RYeX z&fIHpz}B>#H8r0=eK)q&x4yR8f%fzDO*IT)1W8g(C^;bk0RCaWEzo~(a1d;pF<7aAy{~w%YpP1{^#BZBB9uCDHikfeP(V~8PDcNYGU))x{jrt|$w_-u+^|r$o zRT}C)?X>@QHx61sZqR>us;4lSz`gJjvN!~V$jC^$HfXaR33a|6g zL`lc)cQ9m9GZ4R=GL8P)b3ph3i7m;E;qmb_i3%) z0PYj5_Hs&pWqWR&#~1*HpIllAN+BRS%bEUw{78Zx|H+ddy>w_0w{MIlZhOfJm#DXioj_0X#Q60c}mGV!S9KiR+X@5M&h((o%C`V$?L!LfTOT;*lJR z9hpA-(H77gOc4=}ci zGE_R^@p^gbTM+jV)OaG`#KxC0H0#2?b}gygMn&yTX=P<)woOUJzf#~7ZuXp=-<48G zVf4N4ZkSJc=FB!XH^TxYxP}-NyDR(o`1ye&59c-rXNfNOT3M;26^1e_034eH4$1nS zZ7GA)Qa|)dcfJvF$tL$;`F!?zeLXvAAhRnUn;kXwfU@H|aK^q-DQ<~13*?Xi0nY?;uRs!`O=XLF`QlHsmV7( zL&LFH&`0>X<=yNGT&L?=8-0Y_&lh~eTm+qF%>VXS%^rk__~x8h)xD@o)H3Jy+fCgQ=9krrz`o&(RuhE-6ZFZRBXwz6*vgb)6;>rd7j;uS4ROIE&f<=NG}5H-kmw3Oah zByWV#XMdMJbpG0V-G=#}KY#Ld-#@DDZkFY-=oqC^noC2whgTvR%vLEDS#?D<_Qea# za;${RQ&ooHDSDFU#z-eLPx|fEnwe<)jTb24YOdc#Y z9v4!&wK5ks^_ZNg3{;V;C)ImnJ?BeTm-y+^7C`bKTQ-Q5I8*9NAG&v##cwd3$z=k> z{GsWjm+FtWU0q#SL>#+;5$e6U_Mz{V%stns?sGkHkhGURBvdLRBlF?I2T6~Gr;__J z6C$iMkfX8<_4xF5UtiQ1dF6W=rUh)?dwtn@!5IjVW$7ESefs6$*=-9cw03o4=!9C{ z=oCLcKdp6^T{bO+(9AA2O@;~NVMx~xfn4Q&W)L)!aEvWzj0{P zf;FUY=6O~cxz)_VEi&{jdrj?G2xA zOw&#Onzol&qEcL>BYF>d00r?L;5%Y9p968y5H7v&wk1@Q4wZwX~al`dJKpnkaac@57A@5|5Kv1z?e=n*E2 z3s=mS1Q53`z-mH4w!euCv^jvhBO-L65o|I%JzCIqzroPdl;gt7BS(%4M!frAHHL<2sDQgoMHZ-)JTx z(_+a)u3K^QO&ZdcbR9j(_0i%L^+VUyEx^SWX&2Nr{sgq~b($twm2;IgvcKOXFBQ0* z=K#2X<=)XT-+?N^WM>$*JoYw+#$_X~;HBGr-W!Gm5Bol$btMqDZz-=@kJTd(vXbs| zHoZk|6kY5d7kn1BWVjd)8w~bfS@yy9g8Z;zvvZ*@UZ@$K+$gy;w)jlxxk5+JrKvu0 zeK@%Eqr$iZm?jLu{tRh@7{k1Ifn3eQf3hF^IA@a^Q?wf6elxmq$T%wwil@KoIUgAk=;u8L8~x0Bg;y zMn3(_`0gXU4K1&)mO9OXqbP}+yG8f8D)cO5|I&2QJ{ijofqrjubJzDl%Uf1>yr6;3 zD|!EoBc-u)YSCgkV!gmpn*&cR(Y0B5*ovJJ&H{&v*-cj58GXjGz+z^$3wd;r+LhEU=@Z|4)O1d1f5#!Sq8{am|9vFkO{{)@1`Br62;ZA{g- zilAk2VtuT%hN=QcC0zyz3bYxVLP9Nh2SSX(4{_@sZv7U?G`v^WM06SBHEJA~SpDf-%Me2`Su z4~uOGj4u_a?Oq=ffbAITR_4dtZP#apUx+$e+*@XHFlbk0k@k9#{wf}_osp70VEm$M zwWEgXp!1Zis$~}olG#2{-IVNi#tuo5(IY!I%zi$2uxrd05XlRhP^gXBej?giB!4dO2z7UkTg5v}2mes<&q5wm zEJ=-a@A1*oS4%wI#th#mgDljZdP1DgPB`hdFqJswPlH;59eD!XWo@85-5T&=+GBrZ zDzWPR?gQ;gSSD%xqffqj^XB{*x46{mgn)1f_?ZdrTC}$I!Hp}-yXonL zT*97F+0M*!Y)J@D(4$9B7aAd~X3_U~&R)(_S*a4Y*C;C~7L=^vfPF0n*OJwv0k^AE z%(_}$SX(Xi4_|DA0Nr07_Y5%gIqY_X2@`eb-b;8WW=oxHoC3~&4?}zyQ9Rmhe1RJl`e+pW4zq@gW`6MJn`ocQTZ7krMB^^6+{PUuu zz1IN+$9PPMuAF6w4GzANqRB2*0>Zt3)n{Os%MiM2q9l!ed@T)^r2dk-O>!d(f&Q(j2<-Fcu*GVOn;wc)r(dNztlsDs}C3^GlDG zx>Znn)@;!z>Pl1H#)?U0SC_$p4;8Xfv?2$K7kdT7nGx@K+Djh~KxiUFJb!+SnYkDC zDS1`Ue(LBTK{lb;=7<-|PBQ96isQpROrZC&P~0K)m80j~hQjn<6H^r#r@!KG%ZdTE zlO^(MGjBYUtONH042!z+215avWT|%iu%2EUgEZv_xHC$0sc#?dWK)rwv#{pEr|BX} zet>p87@$Ncz2BZAAB6>rY<-8$enbV}P~0A;=u7+R*v1oQXJW^eV4qpv_}8c2t2SaU z2E5Kk9-RV1^z>7ZUfPXd-M&fi00>0z7wkUP%4G1CXw;rmik&L<;urz8VjG z^299SR>{Wt>O?+Ovo<8`LYVA^^@Din0x^-`Q2DNnK5V;)V%{GLjEbu_YQ6bo|oT`(i9wn%}vL*$M@7^q|O(5hAM8we` z4xXm=4?cM^)ba>~$+7=>gKr{nlfl2oy@`PRzuBEW)CUkY$}pVG9)`!MUoOtBvy8tw zserU}wD{ww1^h=n0zy53LA~Hw%?tjmrC%peu52DVxol}+YbuMq$!fq0B}DiI zSos9`d4vp+C{0UetP9TE(wUWddgYIEE5H8dWu+c$**s4IM@ry4iX$G5rZ}@wUq=&( zx?+l>o>bxgv&Aw!cP`luaM5)?ZII|j1d#DNR%3)pLVLs{$|M4K-zda~t ziZ{hzt*K2x4gc1X$lo52gYzzUERK~!fcw|E8fP>=KR@f{sT)>2mK6@{u)+%vEOFGs zGr~N4!aTe@{H$mWaF9Gs7FOJNEEeO;V~%w|pF4*{UB+6-!|@tc4tX(tUVcGdVg3vJ zyn?*^LR`H3XL)(gLXpiDZLyC3r*cJlhM4+cb^O;o-U~1xTkgRZKCt2~_xSil zg}@g6aqj{@Si(Q=3Bs&wy(a)Coc_9p$C=tSLiN%5`Pz?i#Qg*b$ zvQlT3`oBD@fy5;Rd3k;j1yKb-836@h!3%ts1TR1jg@yP<;DuyGrC22{$tYYB;Nz9& zmk|*Zl9LzVyC5igK}JAOM3`4WSXkzgl;N*+Ws1XZjuW4NpwI;*JNqRK1?2w%n*Rn* literal 0 HcmV?d00001 diff --git a/images/hw-tso.pdf b/images/hw-tso.pdf new file mode 100644 index 0000000000000000000000000000000000000000..12f4870fd44df2b9e75646cc4c8640449e1982e6 GIT binary patch literal 19746 zcmd6P1z1&S*EWuUVxS^oAqWCWcZalq0t!d!00II6!hu7I#EhU4N=Zly(%o=KQ4k~* z>6Y&9{MW{rZ$RI7zWT5K`n_f@_TFd56YE)VuX{aI@?sJUER0+PRDJ#R-w4>qnaMHQ zh6Mcl1WbyLO?Ancl;yMyb#*KVm=r9vEq1O*8Efh55-=$lJg|63&cn%0z;sjBK>wiy zIU6T40h5S8mF>6+-ndpV#XcL@Xq3Cu09x?08rHX)N;kL?tjHn(R_9zNhQ z(e#vp!0jlbqVB2W$fs3h+2zl2*0Lk-?YpDO(4KE3UV3~ZU+Yx1>Oo=^hIYeK`-Bg8 zCkvjrb3?^B4gavr9G_=M`0x|H*EL0fA#BSbAuaQSWUmVxrdA6{>#nj{S5@J`zX#X6 zZw|bbAY!0a`r?5uJ%Bw(R7reG9_LnY@`315xM*Lo_JjSnr$+_|sJ-akoSd*+VtYQ} zl2|g3phv01{Kt_gR_h+T%) zNSz-@$jh^-3*pgTFPO@g;h(Pw;z*2&62qVdsw`2pP2ELLO4h~_U5RK;kn&nodR>_= zTJHYz>SDH%cnUgTw#3P8#oE*iN9M31tn}w2(DI@@tWir!(_O!A+yZVmELee9N!=24 zzG&;K(DrIQksSY>sn)l``zKMj^-CftQM7}GZ5g^GXj5Sm6O)GCOSU5sIu#yG%EUOV z`U2WDK=0!VLQGe_3Z<09A++j5^z)Ie_30KAax2Q*vhvD{sPoZk zm?D%6s&wmKNefrEO~31QvgnHw2}9wV6Z%p{k}uEQkw~qs65L$)c3HsozB*99&0 z)tri&A6_jpf52xJ<964Zu0_1QDb%_6D2qQp{J6qVYy;31$*p%Scs5#Uy>Ycct1|z9x z(gt%Ov^gqAM1AWVn_kUrt}ew`SyCLDzldJ57%hX08w6UT|nz_yME(6)bUny3HMGF2Svpe*Al4 z8~t(73HKdGvl&sFYK5J7`t@O$;?)?t8Z@r}*3Y53Hkga-@qo8>&g(3@PcP4piRZhv z^tXwnSj0EX`?bcz#a%OqSfP=+9P#$;jg}YVpZ&&J!(@7_d+f22ix0}t`62_f7X5Il zWU}!^l<<5qZL4OY?dC^9p_*W>=?+XuS1v}g%sg2+U1Z|!cge&Y;|@;8ExYv6Fo7ox zWMYLBTSLJZ!S#tuQa&p&{?xpbgGbLE=%G_?8uqGYD%pU+)K^&z9vJkfiT*~Zbc)bt ztcotx7k_oN-Z5-e_-Q37a2cmsY=^tRb?31jzLZExRbfpNO}HJ!wq4Hl);i$@_M4ag zz*#)2M2$?z32kO|+H~fbovMEmc;As>bP;65vWBH1uBbiBV1D4WT+EbZ)%Dm*R;^mG z;STvW{JK@XR+H_YCrOwzl5*P8v_2l^>NK55uSf{UeRYB3w2avJYmXeON!3}^6&Fg6 z%IfOZYHsRc0)5+qRaIxh?3dc=Lit*f)s&_hl2kH{Qj4rWj?Zs*l%aVku&70r_3cI) z+p@zC?7Yaa;wfhtRHGzrv@noV`n|x>GBTR<6c=@lr#fzq_m(;h>I^jyQz%7h|ipH85COmEa%Utu3F+?pB+867{X(ILU5(G zQS=Dh;TUtKBHmO6XEvs;z=`R;WEXJ%%O8W0%e*c)3$X#({s^M_kU4T>sjrX=54fS@ z9n;!#jDy=w!Ga((r(%?!YRJ^DZ)j*h*4S3%kI8poEMC!0*M-F!Bvo*>bn8>M(I5ojz?EE=IfiP1E;zQgyw75 zUQ^%BpReOn%X%2Wdyc;y<1l|QJx$W{GOS?x`C2Z?R~IbHiIw6MmZy7!;)mc)xn$zh zoI}UXF+Zq0`87N0Eo%U$g$CAd_RHo{ZiyfMXh$yQ6aEnjCBb3C{!gzQH~Pt%PKmXl z1VnTz{V=#7R$aGFjax+zHg}{826tn&qWTrAk0FQ6wJx&?($u1*_5@U70_T@g2iA?G zQZ?;n#k0rWc?ueK=B1+@npN}4m1{K}D zS&C0~U>u!xU-+(;r{G##=iQn|PMQ+TmSc*RV~HvGv@0sX2H#>_UnMq6 z)#3>YC5Cb48Hq;a1i4hDpX#7gN-+#u&*qeMpS*t9HzGF-AT$W%VBJTmq5;JT4$YAS9hC@R~!%Q66s zl9xY;zFfGSV-rY(rqa;*JZRjWB_$BQ_RpsoxH6>sBca%!P z9D+)7nAs1%@7v!f@f#6`c6bR})V?zEUa*6Uu9@|AGk9Fwkm(9UL&y^>7g z-qeD0q)$=_1s1+EW|xhX=R$@7&wkblO~7 zBudR`^c6iXXqVTiw=~g)mD14AXqa*{JZo+sI!vYXwL)68z$*D1KJH1ZY$z?C_@PRa zmlE!@D7$`L2wiI7U3;$*P~@dJc}uUvw--X_W>dp9MC}|Lwj#ydpC-PMiIq%=^z_TX z^axryp8Ng>{^iPE^7yBluZmjyx@6GyDjl6T^Cpp|aV3q%R0dBt^bb>MBvh(5C#$u9 zWnxzooGl~5R+DJj-C;CnNm18Tsuh^M6&`>VCriwjqq&uhNxYX_ygpSxI~jHvC*3EP z;v1mppt9+q8k!$eiSoG+NXMedJLs!0pckNS)%Ie0a;};wAaQMJk}g1Tn~-dPR_av^ z%9g?s6mjSnTE1#{o@b*rc(O=?_tisz)_N>Hwkr2qs%D8sQNyX!=W7e2 zY_nuZCCqd9j=_M|C4wbjkEPvOYbm*B73Z?k;zW5+GJg0xy}$2g6}%~*R>Bd}GIpCA zQ#dQ(OVLEqn`78y2s2fRBGItXx|>=)I^YwvJcjRj?m@HBj&xl+=YaF1aDcXnt)8Efup#cwyI#pHHi;CU#!575g{PT4f#{AankwEKN3fV% zvU&S*6!h&p+0|>UJr}+iEvn^#0Tqz;9y{Uu@%eEX)##xs2`%PBHFuQQG2MlY?~FTg zZg=H8!(~Ox`y^gFIMJHkKapAQUobE@c>4|Wl`0LCIDBdajT(X82jClY=CPQMUL8ot zcx?g(PkXSjR-i1qlB%g>_BWjLT}pFe>8^&c!uh&tQ2(V{&2Kakg^1V<8m=zHbZQqz zOa-vQw|f&JBPkZ`1rl1c*Y#?HK0gaUW2MISy&xn@VZAgf#%`z+5Eir>9vNhqSQsPjwHdpp!3P-ae z5V@ZgY^(hl#!d{xhG46z{OA-s&(jb6zW>Bc!#Int;w15XFOHp$^iP~#1r^=wL@0Q! zQy2PG%G7B$6sS*oIY62@z{3TN;%5{(&D1T&H_47OgC#QX`Smx9CMgKv@w%pwukRG5 zDT`n+AN(EBb|9h8Z1roD)N6kx&9JN)P;)~4FWCl8Ey3J0 z9%m(*z`PpGo>}-NmpJcMI^9#UUFl8PJSWlT7nOesMF0!gl7h5gk8$k9%$8-TKnxdaI5ncqGy_Rvvs)+?F$-JFj-V;?#jo z-mXPm*fDPgha~w=xjL?wF$&l&oD@DSX|vR(zrHvgE65i}l$UC`cyL|qwJihx#>__^ zgJiW_Srgp-(%%-#1B4NO7sFNb{rSbG_~Am14r!Fa;IIF&=JF8bDE<*~X8iO_1>v~` zV%k0&RjnC?&x?dDvq#)aIB7QS(&?pS`3etG%T1rym+0uYc$~BoGOo0>y>Zj}N%9U3 z4h>92iPu{-iHf$y5>rK<2v|+DE)?DCi7U35)y|$7dFLtHGoCTGK8d!QEsxhEdpuK$ z51w6IT-;4#+=I`j7e^IG^ZGrA3gq4}3vadNVtS&S+#NX@jo&I-r$A%_cEC;P2387% z*5eGZUB2afM&~yrrQp1#`sV=(T%t4G29POf2 zvkkM2TBcwT^?)}U)RpK4YZkg8YX5PO(v#l@agY+Pa&RcA<(d#@>RMiLdlRh*5~}IA zX&GeCc5(uPKF@ah*j7WdOzf?|x$Y;^u3;wKg}4j`P_BGtePy3t(>TtSlbj-C{Ef|i z&B8l3kWD{^C*!zbgSpG`N+QUe||HVTdz=*-%Z?b&1EjEw< zXGn_Aa_p*XzTN6v!jv-NCWYACk7Rx*9EZRPR?Y}O(PJ^*3^QL7$d+mKsob5Udii~) zdA$ItYxxydx7WHGKDD9K*_}HdN+OTV-5#zBEyt@1WTP?CFC6q&d(Z+dxSFb}YP9{) zqen??neub@G>1r*TliRS;p6!X^L&9POB)NZLMXEO5J7v}1^bpHmDj<+bk=7G%RGn1 z#4JzJ0#5OkGy=erDy|Ar>yUHr>xH)Y`C^0F4erXmZ&K1EweJC-;@~o|P*5UK)1Ho8 zvS0YBy>OOEBP8_OW*kE z4>1A@_W1E*p6y9LB@Ne%X>dTy@0#+7@txY;D2StpL~|dtWxxX~GvDLY#{u{7wO?PJ z4$o)G70n_-+D_2E^NiiMnA;awED&9Lwyr5%r=l^XDFI~!|BqVxatYn)3h21f?uty> z!O5K=E9RMbzrXy8{c@Lej9k|J(x;97QiOsl_t)&3Y6%t0_{5IxX$$@()8EhK!om*{ z{E9^ADlHz|eJ%^@3BhDBeO4}KDGBc|pXV|`2U#5j=)_)kow{p-nHYL{e0NV35VT-8PQiKWy0El;>Jup` zsZ71v$O$^mek+$H@?E2%B=&AlKA5k3Zm_z*VzdEgJ}f&ZOKaWdN)skOr9a5)&j%O< zD9Od%Vlt2}*XtKJ3>)*z`WpwebEegT!HY0f&&iPST)Rh@&p^!J!DZaeJ|!Y=zGqnoZOk~0tjIacz5eB) zB#k0fi$d_wR0OBNb7eK@%%cxK)3)cuNod?%i$aK#;GVCNWTC;qYKn@!rNyq;cA2M) zyBB&bjEZ;#5;f3=FTZs1B56EGQ{d&b~v&}-&f7>sEcH7A`)EQau%z;m@tKiu`}cx(E*E$lZ0(Bj7EqN0c8 zDl&hUmvWY7!cuwDy*lhC7Pmm5nM#Ux)QrDov_T$F0@UX9ZT137REaS6*DAxYuPno?MCoS+0^=*J?P= zrsr~8mS^w`;Fpp1>r0>rx(gqhA6mC)<+S(qG~>y|0TO!f71T+6y*@OUe9M*|S?g?AJ5x ziCo3Bv?97~?Ihx=4*TsJNO*}J{p+wM6Fu2gkZaceDN<6#pZ?C#ZBX>CRNGt2B^?k& z2Lvdg(Mk6#r@PgYY==XwY596fwicPvOI7qkb#qLVU+!8kmwl#f9H(%@jXnrEm8gUP z->m4#^4Y|0$8CEYn*LPv{QP{mQV)r37H-q$$}V|P$f2-x=;={LW_8X-dko7&M{X)WCOksjOAp@v zzOQc<>|a$ChNn9%q*Y?0HQPujeaxMy_@;SQZnv$>qj`7D4GO;UkFvYh-xqNb^{ed* zh%;3oNoH>W%cJpyTs`kN{p!{#pplJ$+Z9zN)VyKQDO(EAu#KOM-0lDv&&QCZ-nCa;`U}I_TyNJa};l zdoz^RG6&NW_Cr0)U5cPk1eXCDP5R@Y2a7mz4gCrezk}nj0)EO+ zl%0wkt@rWtHZZ6LIelk9?ns8a(zHYmtq=Kr)9@KSOdP@b2iltstRHf)>YoVE9iWWt zk6LH^)l5#cY;{@p#H0AEr;^lir#{n!qm`AfU3MrIE%#fxarI9*jqjH~k95D9M#xF5q|&>$9K4Q|Bw37HCp9slbux9u3f z^e?-UbGw5E=No1(>|Q^`=UE@PoGa=uDPX7`25o5x|5;CU29_3EbYgc)SncL=50k_+ zL}Zn7kM(PV{MH z-qOf^BxL=?^li<&5E>9GSmr*t_d9^1x_f|%?EmFE=b7*SKC<#!P7ut9Y`CC6zg+N# zz1>-C(PZM?s$r`K0|L&`4G7%8_8(fOt}^)9V6~vlUyZEH*9(OY&T~Heaw8-c97QL4 z+`GKN-9|ka;7{q7-4KLl+I6ojj=RrKwWd=#*^mBo8(m7C$jfd>2!#AP8>8Q1JxSlHl4^i(I%ZEYGYZhB@r>f^3k2fXK)D?i~IJOks z@4wqXV(Nsp?O1GyXk=^Pw&rBIy5P1@wUM8iDMoQc0#oIC9U1}==0*00X^@%u7w-~W zf5c)tUA%7MU%&qS1=$wNaLpr4?}iT_L?AAq+%?5b_W{8cTKFOgktM^{lNGqzvhhyE zCG%Ut!hek9+1LR_hS+Yv$PrZbT)j7?psqefBE~Db+&)Z< zTzFV0BFD20n@-0P%~s#nR7qI!ktf}=-ulYj>Bd(eM;RP?A>kVbviScF z@gB!PS}}g|Z0f^%Dd@n^-$ra|cl*q_irdBvp8Rt+4J#72?*)!L`)by4l2%0bHyni$ z#2d)L9D`C*$pCanqd1lNA>@(Tt|w(>vBz$d2Yt z0nY<#eS?HsLmEmc(_nU)|ys z8H`g_Ao4)tt~FOWQ!0A6ad3PG6WOeRE&Bji))me~&5~k7Mv_QTB7^Kk`2J{Ib^9GE zMOo;^XTK}W8my$&0om`Q<3jW%-}}&6tMDZ_R~a;)pvSS6waa)YE1Q|6wrJ7u!31VL#>nkO%B8F%d-uR?>{uBtn^z$U~lowz<)nQi;)xgZ2AizjxZVZ*ya# z)sr@lk+jbOgzHiZIarO*>UwB4^=>(J-z~xh`pCy$dZ<|~Yk81jg)Cf9+hZfnU!F}kWYL-R>?nzw^ab{ZGXTLC z&Q;M-N_t#ke<%;$Uik+dPXQ}{Ud>1zl0LBwC=2^=7kbWBf9&9y3x}t7oo&wQRke8`m zXL67iK8`COFMTIu4}-jPG8{h@-QQo~S-hfW`|sB= z4L;`-E$zwlwA;a)uHG=W_Q*n!DS0(v10s{kWZkA4Knfm=wiHY~f-Kb3sb&6Z5mT(u zFLA9&Fxf+O6nu;WLqiE2S2#^NZN5f|2Zm;S`eCJZo2wCnCr*Ss0#o_Vd~+OYyA1dFVf`Zq2D|k85s#O3k`Am zjg`;xxWq5!1lK(a&4pL;j*!DEC+ZkLOAu9qjUKF#Rd@PVeY6{_^3%?Qq-!vrj4mk| zzfGEQH{>q<_3b=XM~jYXza$L@&VsVTNW=?0tFa68pWcfhDpE%;5}8L9<~t{8CClFg zUIXL9V#Vh6#RJotc7=;87jm0mt`<5Jn`hMvtN>-ZnG^(x96kNi_`X}W4j?-BIrVSY z!ANc*qJ0rq#gGWs-$5%6`skc0N}KJks0U0VGxO?c*AE{)AV%-kA+6@qhyaB^uTjW7 z_1m56yBx38=N_UvDCu8V`=>dN3iX4mTDw&D9+muGQ`4$ydsX+zs`hRbwR4eaIrhzG zhj@+fo7+F^x%OPXd8rPrJ&0OCfhzG?J?b+sK!xc?K>XZuBO*rf-1};8T?12QqeJ8dEVF3yM_E`Sw5 z=F(iK-rvS}myJG_zT`8Sw@bhNcie)Q{;7=rkt^_zmPbD}O^o7>vhu?<`r=>RLjGy) zTWLAg&1auqOEM1s$wjNNOKY{4S5*{i}k_9vRvrUIru>QPHp9DFp}0!>XPAM12N4 zrNY1?;-CgFk3<0NNh%tcIHNZ?$XEMs4f8j%T^{Bhk7DOx|DCwtc6d40PiT)_wcjx5 zizB<&(VjW@zceq&KRNq*JUVlAkFHxi2TxI#{d;Gz&&1#`?^NW!w{oGETJsX)Zdeh> z__Eob?fEs(3$yNQueJ{Qx32I1Y>vSV|HrlWPxJDCcWRfnziZ{|x?~63s_5F~?eA7F zpVQT>7<)j;5rG=h9iD?(6$PnL{P!1=AS~>gG`IjRmrC9SeaJ6TP>Hgvlr2|3Xn5wI zwEWLn|G#_w3Fkpm1z%~{11*G%=b0aTQi;3Fqm&jNV)Xi_la5cgeHJPA33*y5hY6Nm zn;T<)I_co%`n`^L;>xh?0J_uxn{xZ7lSdba4}HNs6&OH!hS0Uj)n$MF>BP9d6OUIZ z?M2AAxB0>K&p1wK$et79kc&6q+g|1Z@NFTU7V4i)a$cG5A3>L1#->QZw`qpkp&@%t za?DKdLg`vX>lQ0CeQ1@#w4^#4d( z|CIs#-=3SL^t)osl>V^T6L1gnPW{w}|8|Go{xp$$rda=NRMdc+^?EoYtO|nF)AzwSfU`! zK1dGkBDFyi5Q56*04{)>bY=!6A0i-+7(}AEmC|Y}{rb?Q%@m4m<_9}oqOaExhXn30 zFj;|3lod4yjDiHnuU>KnY>_&dl>MQXayK9e?2=YHQ>f}JZI*IB*qg2#_cU2N?#wVj z&UxJ35ISzQ)RL|Iyqb-T4Idw$-Z{XyT?Z>JKS^4d2708=67N)Af7#skk1t|*GIoSz zcMJA3El>q$f`tv>^&SiWQmiJu9b{(89X$cz?M*;Z5BHK)wO4_h7dTW|cN_*;&0QXP z@rVtJbT9ib(mhT}CFq|11kh~GDgliDrS}7+2e$}4y2#cNXo)5!Q;_0mq+NZQ2(IHO z;dmz=^^PA13KYVIos8dUT!YJ>X~5OjbgLqxkhGDPfp1g!!~2B!1xKS^m-Pe7B{3Vx z2Pji4NjoYJ^PYIMTa1E%t}mJu^LTzJIyxHr89?E3pJ0=GDgMjcrf+TdZD#Ig+e0{6 z?j!Y@I$DUHbou;l1U=JX({`0H6zGdpR3)pm7)3eFCzBkrD?ml|PXt2m#aSJo$GEw> zebRSw9f;)sy`kZQrozd)U}Pp}?@OBLT<48;ef!Jvb#W#~AXz z727|VU5SqkJMHPDX?op<+}~wTSIB|D5(+dTDx&(s_TbMD{Ja4w$Av7QXFyqoJ3eGi zQAUHBWDe^cJt;tuP+69$gHJARA0wYu+q-WD^ERT0ev0` ztKr)_D^N%T9+V|l0%`sG5PdtC3v)Kra{!f!#<3bqBD_i^$a)I&?F&WJ?!Reqv1}-> ztBl}S+`GF<3@RC7Cn`k=1^r-Y6o{6{=cy#f32h&yt@VDl{x8) z%{^kqd*TO$`VELc#pd9F?sQDwU&@r#kdpoR(rQ>-JY>>InlM@<E2O!XcFi4sV+pzwrMQnYmu%NnJGR_^arM^CtEYL8Vm}H6u40dZ zlW_E2pcH3eS3-gh$LJ5}3-G7%n7IM`A!n4BD&c@D91bK9u>1;KHk*qrg9_j7NRs+( z&fVHoa(5K(ZT=gX{guVQj^c-^F-Xs(!t=84wO)`y-9s)ymoZ-5DY&bRM)-iK4tiyPmJXl&jN0x`D29!h~PD>~Qk4{dlzR(HCxT0-IlVEWACsK$>nu{45CxlXBX97$V{nb>MM9T?10FG$@ax zYhD1;HCy#=G|mF}GMzR+{hBKU7Su37?nF~!KxZ$|J^ctBw%2=Ng>3v7qb4d!H-Ksb z&{|mjy<_bk02yY|xYT~epgv3hxHPN4Ii@g4t@DZD!1J<4TC1=;)itP43q*@^y6aK6 zg}=(ga#^4dW(bH9x4MjgsR%jyo>P*SyaNJayYEtXkn2ThV}rA1fiQA{j^;!$WD1Jy z*Q*NL7pA)S^4eO{b?QMHfHNPT>8>*CdtHGxaRXRYlfZ-osBrL;cEz6+VyGaQaJ#wB z*nSX~D*PRi|07^wWaybmEFOi%7UzG^ktjULL5~zFf%kjp#HCgccAPzAv5`xDbV^kW zLZE7aEeC8!nUpSot+ycw?CbA;&t}QT=QK-)(06Adpq|s@*4NjQ2o-P4RmT@ZVQQh? z=vs^0AIURlZRf#5!0SB8bbyvj53lkPEXB43pq*63BHlyca`%&n4*VYyOO*5WqDkHr zgVgYi0h;(=Deau=dhMmJpser|4)W7s`C|!*jsAv=kPtRunNOX0sBO61Aj3ozY7bd* z?H+<$p|lXYOS+5<8Ye1Wxx2eJr7j>0g{a!g_6v7#hR`?Y*lSP6S$EB=#`mI+J_Z8e z04<9ktjJqk;kG=*1quafhl%hU2y1PvJQ=Pcd01>G&-(o0Vv^AQ7O#A9Pn^K>w zcTpOyXh38mM33VIde^hXd+vMh3=~*&mjW*r*K$m-2|@Ap6~7=EI_;+x;M%yhg|3yy z%s`PT{_;p6(`=pn_oeY^1 zI_ZKc*;-6>3U@@vzcUkb_mWNy`z2oBe6*6NxhY-ag)p)f2RSkhmRk42R6{+5I10Op z6qQ<}YbRfrxt7`vx_0g{^&$)2IaaF)<;7~Js^abeS5wk( z$lrpd2o{~t(X;e7d41Ogjhzl12RAj&Uue10yi~!(bqzrEx6KYvQ-{U9X|4+w(qsT) z++<5?INGw^AU1vw>XT6~5b1cTc}5T{qM2bfCyc{Zl@dC}hMw9PTLBCjp%ssVX3^Nk zPzY7#Io3r^6JjbdBabRN$it z^15kw90r)?q&8q|o<>`aC+8--+Z<$abZrglWdUUp#BMQW-L5^Q9-aGO{|&#&*r3J= zy!&;|M~H%eqc`7UyF8WL{WS5wa075!Za1_eh0-as*RCBFFp!dRXO*E&g`Z-l(d|DT;Fi3a*?I8;xsTyW!&%J)Ix!)xl#ngvbVA z=;b#BU)8ga>aj~6YJdc~RFQod@DrPgrApFo-Bnb)s^>bke%7f+=X3}=b(i`B$e3Xt z!wOWO!G53$KvQsel`t!H90eMu?AQ`m55@WK&>di4(&Z{HGvk2mJ$QPN)32f7F3)qI zYpemouI%)zChj&cD_M)ZGTv8mJ!+M|)&Dw22*SdFc2JVk$*0X#anim~4w?cG=i%fF zo8xA*fzsoc7y&VM5c*9FM+1aCP3!g3dHpA{(Z`?0X|2u;5{I3_%eoJCQ34G7*>CNT z*SmK+uuM^*?g$mfJ3ipeC|ENwGT!4m)RRkYzcv~RNhqUlF|XFB5?Jk4W*QY-0___3 z&5;T`6hwy(YNr-e5$kc>Bpeu(ZLcUBnNmcD8~WS^{J~E8%QOn`mWh9+f{yseH~?*@ znrgfyH9!XVkD;^A4!nr|z~pi#a}EEp4Y@&+2Pt18cVZ7Q4b-Cz01Gr}!nR5CIMftA zi@I=E?VZd1D&rG811BwMyk3wwC^PayQ4uX4Dc-|Uu(K0oS@RG{DG{ahKH(85NfhrA z(*~tx_#N0b`4*!-3OJfD8;Zp<;DRVOlp_2NcKjod>y%gN6*vNxDRDykT@TST6ki5( zW&jrg`xz=KoA^>l7*wzNcY>XjlBBzS{SFG87mm!MM^03OO$$*CUOU$h$;rDdP)Mqo zq7LPiXe?CPR8tv-g^W29$$E8k0}S)ng9OKq|VrFn}V23))L~US?=!RLhwNF|YHkrVEjY4HL0BFej&VS7-{FqhoekM4d^xCxe8~>Tiak-#Jyiggh@*G%GfBA4hgcf3(X?DomU~#+_q7W+Mq~eEs zedsly;dv*PsQ_Fd%A^GwH1G%|%rH8_`c;^(`GU*Jzw!yFi3w-jaFK<>&uz*hik0p9 z%3MoHJF<;v0unE_p%z7|Eb611jCo~+HWvuwNG|1b7&TvQ@^WB=TDQxy`BEmU&1#tV z;5+U*61cl~aVK_$#$@qJv>#4g=M*$CE^8;reTJ;vXi7~emD>Fjn zl9@O?bfTDLr-C(zMGzGJsAtSn{-wgf4AVhBrJ(~^K)tacF+#R-z&1hg9BY9WYnQpf z><3}u4Ir__OkokfH5=IkLBZ&zP{3J$yiVYBJueG9z@shDI*d0`j`*9duAQ)^a{!o$ z8bmO&H9@h(XHL53H#Jo4m2R4TphrWQl_4)l$i5h%a`3JwTinjKBZfJY!WZ0w1DLki z3Zbn#CYp)&7*_rDkn+GW(Z?SEHc)80CIzmipPJxeqeAJRLd>lrb?o1KF9?;mEIPjW3}fNUhhDSD`snK4O4{nKI|j?oe0+m<{{)Dt3gu81 zkAdswu(iApUsyGzPY-G*_}k7rKYkI}OlGXd4}2XmoPuy{?x z|0m_p!(?Tz|vXA?p^)ymjVu+neU4GcyRw;H&amKBGtLx2ue zSUb{h&HmC@v8i8eOk-_xV}RySZ32=F(j?PPvkJrpjM2q9^)!>%x@F8UJv%iRpW3Q0 zH#b)YJa@pqXpBqjRa|`RL=o7`h;FL8>T}(tuI@-j;MMQl-6|Kj7OVs2ak!$bCok9lcu4 zEz-0Pgbu&`egp|NG^M0IL+Rlx1anVd4Fe6mJ=-Y2H4_SV?p<;O6W@o<_rO8efD|O~ ztRl3T6tqfPz^s(GxcIkNIWjiAmv4?iJ+O+>aaF}pk*p3N`q@m*f4YcqnQhB6d*`nM zjzrU(W;(Eom8$pcBPW2hj@JSVjoU@%)w+(H#LM^{$By^jV1BqB)1DQ-L6Za&cC&!} z@0pOm+oK(f4gl|A;o(f%n}*$mt2>lWg5Nbk+VRj?*3%l6OlA?lO#`#&R&WikTZ{2H zo@t{LO=#5A0agU(sovL1iF{MC>&bKxI7~C@)?LIK4rF+h)H|1L-9~}NZzeRTU zjI$|$uE~QxcQJw^WOpTGb0g$03pXbV5Ari|!ntefrGMHPiH&W~wn%gXtX!=3nDIm? z&G$2hhEzwBX}#_BsVA;Hh^N|daP8NRv+w%Ok1d|$clL9-t^2@0O9W#>uEq>^aIvzH zvvM)36ENM?HOE+Db#%?ikxilg+z#r;F*7-`U)0VvO|VlFZ1ZGd0XsgKlOtWZOTZ+r zg+(@iV*Tr$KRb$?BOU&Gk13=9<^)VK1`o{1)sXhxh3|@DEa71mq_clM$nwjBqFNSO zk1+bkr{E30e2Ht<1ER2vlm!M$evOUc$97fbXjWEM@}14B$SpABun!hFbihg%i|k3o z$;iUV$jrz}j=pAXZOv%q#XPXofsg*znx^nj_tB%>4SZ-}Vam(I^e@}_ z_u$!Jb@d3CVK*-3|M*AF$-%+KL9TcF$2Arn78aN}#yHn;oNnf1y;-8kuG*eJQNIUb&(Ck?qVqg~$Uy zS|}GMXB28ZdsiW-C4&;7yQJzlZj^)XkTm`780I)a=%GLvb&s@$53gpmu*yeWR z=rIN_TF4#21T}g;c_N?Lz-d<0swgkoCfE_X*EO_-o_5o|2X)B|qKiA(77U zEi8gKE#^uyym8lJ_7|UPcFOed`;H)*VH?y(T8j1!aVh8JD`wMv^taGB?%E$GZt2s= zA8b!Os?-Uqz|n3-Z4s7E&wR@MJQ}gMu?C%rI(0@Wx_LlnME;3MVVB6({fxsIc@~LE z_7Tg0$L39%;}#lU*k@9kXRL{-2=B4rjN62E??>Nu-P0?Hmn9bZ3FeTg^Es6<7E0@} z`^;zj+sbtM3OqrHg9vQEda^h*tb^7>xt6cR+`IUUHpth^nj5dVaOPz* z)7_j+%lgrS2cs#um$u-O{uzC^uFqw|qlg33GE$WG9;Yvjg=?99#lgpqMLnw)sfLlW z73e^`g~SKFV3Jd>FjzZds=Q6s z_WqCgN17kQns*fa>0r5iO6l0UfMAKThbGle32vzkqP*pEZ|`n7nRKV^F6--#fYOhC zRnFVmy_B)^1(}{9-p@<8JZ_)PqFW*EO|ym!D8x-LFmuo7njM-;6t5=ke${s$0c|JU zZ-;p2fIdYhp;q2NySyAa`vYE0%IP==4Ma)%zaRI$Ze8Ba^nqPWyF5P0GMf~ox2It) z{oN0V_hi|C&&t5Zy2>}kAJ<^7q&gxqt07f#7b1@ne7lbm{SHTRJx8-8*S9j+PY0=O zzEE;$*&CQ<&vrhC5D_sGk{M|!-qb7U^Hb{De;U3e+Qh_2RX;w_bDzC62`5@c?jOd^~pc2*J$5Z|24eo%wh33BNPd2K$)gL%ER zSZ9)6^so$dbTwj(M4hg}YNTtzbM47u!f0!-Hfg)CZF#$lHkj`uHfYAjtV|5Mk?^6v z#c1-D+1kxL{5Q8r6Vm;3Ohf7^mk=0gBNx+Q`Hgu`gd*le%dmfX%b`bxn|-1FnDuaz zl1}6by$OCpIY4}MM#yJ6BRLciK}zZ;WS@F*sPJ)j-d^8w($9E<)O>Z)*6lKB^ioi6 zJCvxoyHYqn=UM0>eo)_T<1_*y8Kbow`w%k(n03l>IdasR} zwYJ_6>m;#UAI4k6S-3yiJJBWNqZk{xy~R%U6R+L6!-<&--WkPq{(E|#xZP%&NVg~s zX2z{r)sb$^Aj!OK@&7OBU>0jooHY)QVmp#v&xZcv%9n6K-$qz5N-)EesL5;cW7b|yFre52y-fY_10Y6~1d6sJIQD0XF z`o!}d*p$g9x;A(-&FInj+jE~3-GzjzHLqFQ_|K{6u?ZGlaFCCp*9nv4tr}n|&>dJ6 z176H8Ht_dJ338;C3yuZD<>uZj1@JPbYEr-RZak7E#U66hM02z-xpJ2=3ciMpl^4ge zeqrM%61g$p3L~MQz5WW@q%gwZi+W7FDlo^YKixWyvr$X0gK?uZ{QQ*xF`FhyV}FwY z(=XK~1I5c0pGSEcUYCWjxO&BX3T0|EJY(JH+N1#EHGOuE&j>x%%w(D$J(#BjqLL06 z-ql+)3=>+uZETz7baOW5IY9wgrU=s>bM)rAN6hyeFqeRvWbF{92Xkk=oaUunhQ=qJ z#3H1r#Jf4{o|_kH#YF@k6BKZ^ZjQ4JH*RlXH$AID^R+JGT`N~25aPfFR{gPMo2@Sk zJ5t5PL%3`_b@9obj~^V!JJ#PiqSWH3!;$m=c)mYAx|Hw^3F3pROHD(raaPfC!BZWJ zUS4_gamz&fdj$8@*(8fFwgII~e^HXKO$45)7d!a$5i$Lk_L9{0Bdn%kO)qW!s&>Gz zgbtqFK!#p9%y(X+)D+}7l*3HSymZcWI8Lv-)t5)kf+lkya$L2B=F8qumiXLqtn;Y= zP_y@vsMz=nJ0Ljtp>pfjs|IASB@-u4a~J?Yhfnju^(a zqt97~T%R!yT2H=Qr#DFWdi(MTO^m>cJwXg36LLDmdHdS(3g3baj5TTw>MNfau z){kBAzV}(H#Ka74ADW%!4vWvRT)%I(v<~OXb0@n-s;wk|qBjrHSV)l5yY})M?e1UV zhkN-eA0ZsoLf%LG7k}KdVi%bVDh%FQGiQo=%#G~jXFr-^v68~rXoAdz)U~b^+O2gG zPi(s^XCj_8k!cn6y2FMqM%;LX6&1`EdSb1Jzz;4M(_t(OLxS5etk2Pxx=(ZxkE6f5 zc^N-U_ZI#GlHSRAWh2b^&!g9hH--4`si+rxf-O(I;XwhNNRl$;oTbbibnr^IJ2 zM$(~EKEczj6~gL(9xiMvEbcbqX)k{%zWU9Gw?01f({j-_n%KtUJncr^{9|P`q$A#w z(jZ1I+5q#RQ4norIQFz$$oIENpb&=Wh~i}*f?%P0LGYy?u1;9#-f^ZVuUHbP-<95= z;Pd2Fi83camy8Xk3s07qRO=Z5v!@FW?={lmbqiSDmUo}i+0oW}D+0@q2y z2c85^2qk*y<|7nn@64wsdFoe=Go|2;*I%>rk9v#es_m6Y_tMEnEW8Ef6gxZ!R|^)X z=NPS7e6Y+=k$lU!io2naJo$}mWA1k{Ld~E&Y%%P1yyYJsbS;8{GM=Cjx@)>3PlfA_ zjRqwSXA9vY_UyET4UsZ~#dI}eVq5Tq~ep~2driMMm3f3rMtf8g_!a!Ur9)*`l0W8*WI38 z4k;hl@qImP(gw6~RDZ@r-=U4UmZo!Z;y~c)(7|msQcpB+*A$+S$d3{scoCkhh+`RF zjee7$QgMDNczA;t=VBc&J_UZjr+%4MA+;`iarxVklov(!DgpUU7mMLcC%;AuUxPG} zUWI-uM*Yw!?~5W|4vhQ?d}%&66uy(vMIUminz??A2_pn4YGu?nsdIS-z4eQfKEz$; zAK%y#<)bz+CMjmJYz(|qDYU3O*Cp=9QcDO5tDgTnz|M7g@<8P3%eV`vhq~2#8c~Y) zqi$!%Z@jx(0qYm9V>ogtiPWWXB|CAsMxnX}n`lqZ+d!PNni?v@ z3AfYxHk6gU*pGyAbT@zDeiw@l>95%^%S5#9GV{KQaDAiA7+Q?O@qAAsF1dEa?_QA! z#BPHu7v7@}^K~}YF=a(OVhHgDP;^T7Xy~+}62Ixx?Z%PSJd&hT@Q$KW@Ltd1WOhCQ z4s~Ue#9#s_$8rVF#tB{ei6`~_oBYqJ)7;m5yuP5QMQgi1J|UI%Nl~R#^$S|nV7f<6 zx(?H23FL!H>hJP|94f9BYA*ZUFRiFVT#95sl|RgIOP8W|ihb{VSegf-#kZahlAF)2 zZFY%4A3713)4#r{@n0_^@F^cNUHL*>h#6br6kX@S5|Jd3y?lrweLYHrXwz zW7H%RhvBnfUgFDDdh;RU_T_T!Ta*ai+-z#dHj;f0@+CUt>6otcYacgpamvvdIZPXR zXWZm7>*h0(VQyB(QEP#rR$2(3jsITqiyWYc5|#!$!bGkI?#W=*TM??wptXB`xo?>M za-J@v)mK@projl-2B-b^E*AJ0z4<3?wBbAt5Do@lNumv!#{K z-v>J_YL=xYILCNd!R6cBM1)UuE&D>b6}HWfMqRqsOh`rfJquS~I7QsAYommGmf#{P z@!+C6=vT4qd=iXriPLsct4Ky~zuBqw>+<)!zS~3XVLu=bKEFA$e^QT&66;wgu|D)K zvEELL9OZ2fCq}<7zJEU99Ch&_8-sPttGSyt-{XA(gTQIe!YQ$S6h-|upg{z*l1@dp zti2RWH8?cfLxX;bOK5VxVQkI;6z!A?^SZ3ya!EmA|E{@c?ITXc(DO$1JUe=VTReohA2lZIo8R$pNRjSuCTw&BkzENZnz`=v)c_IPhYIA5%$4@M&@-u}$i?9+ zTj})7K6*BpLLie#qRkUofNANh2Ejd@>{y^9Dp{dB(w%n$<|a>h7=1s}%P%%?*Yi-= zKAo9vCAssDI|A6KU}tDPaqNc>|H*>BEHPK%2KubqTP07P>pIaYqxzteD?=i|Ebdwf zFWm_A6X)VUR`d@OwH3?FCFwkqS1k$R##LlzBhKr9$d}`U^;wy6M);kDb)RGk6iWU; z5cbOWXlBY9b4{bp1au+tx9fpkz+bKhkQ>iWv5w!#kiYiaSX|p(k8l$DwCYnQ|;o|pqohL zuA3<+%DKQZ2v5B_mvAKG#8)Xl`oLDEr>mWwITq9#q+1aeuMELuW1F}q6}`ELPPauz zEl4F{5?=K1B|na|{MnBLoDMdse+-Hnn?-v#E)y0=@d}AvCO1StU2~ zyJrg*-tujyy_O<4Dq9)PK4R8?+$Q3&>4q%XQ);=g>e*mZLJG|Lre>3;zwwl+VDToe z*c=PPcE__u?1*X8N7TctY|qJnT5hpL!TvhcMG>gSZ#M%5xjOsR=P@A*9CK3%){)Y0 zwmj+`D?}5sgkLLnE3tXqMri5RkFGNNmC9lPZM3tuOc~uh9@p#<&*Ph^07*@~+O1k- zUt+DkLN#T}_BuhUK)o(WB=EKk6XjDM!jz4hn`){!+>^|4Rwcs~3^~PCnF7&lc+jq$Fmq z{+=9F_*wf)a`YvHnu?05HD^=bgPA{vT>Ss%|IiHJPZ_vSQUBd!DTY8XQ(2h8Zx##t zlg0k41iOsPU$W~Gb5MENt6(am5EBzPEAw4GzirM`QV(YbJ(c+|J?ZbF<^Ck+7pTDC zCoZ6ea&WOlqVYfrFquOJ0tG^0FiQaFDhiAC#@M5maB&LCO3vq z2K#G6$ln^O+2U;7(M}Xm3PXW5X}KfQ~G`(&S}eY8A3RZUI> zs03A$gF$7~Ay7>iTuxR&{Q?p!BddVCpsr5lk^?KKSpKs6Y%#c>Gb*nDmIH{0Xy|JK F{taauvA6&L literal 0 HcmV?d00001 diff --git a/images/race.pdf b/images/race.pdf new file mode 100644 index 0000000000000000000000000000000000000000..281a7846f9abdcd21782c727bc4fd79e16d4038f GIT binary patch literal 4553 zcmd^?c|4Te`^OC_MrBJ9GLbDY`!HfGGbDSaEFs1il3^HQt3fJDWGRWF)l+0imU_rq zmeGQuOc5rs4nmO--+Ov`o~P&Qw|xKl{qsAo`*rSfpZjypb)9ov_x(C=Wm|%&CR|G! ztUNH--U&uQU=W(eF|eK<7a!g@$o*&fFNK9Fx1$G5oAlD<7s{YG=GXe1EK?l;%QVGoftqO1M?9mAwFcvJ~}BJ z3^nzkGAMKi)RanMPzV$<%@df{lH%_TOpF0Mu><39;2;K_Lh=KLWlvr`!PxRfp7lw> z%xq&y?7q#)>(pPH-?D`W8XZpFp;xWmWG-sE?#nvc@bV5@_1l_xx69w)(E(t`qOG84 zMIoW}`8Qgs%C88Wi6JC>G2C%~mzadv>|{--S4difVcEOz$z@y=EOhGq<3!Q=pJt?iYkk*4*QPWII%R;ZHdAZN6tP1J8TF7C7Eq#^`yr@6?z5nCgb~*;9 zI3o{2e9w33?d;qh#StPqu1YR?Xbd(oKG&s|w&94i6bsMtc44O4+V=~xGEb;EUPkqm0uY)?mD_axV zzlCzf69|>c;UDg1Enn21DSe2{imU*uxxT@fF+)1`rL2e`z8z2!>)$gp!mr_Jg-v+m zVA#z5n!Sh&)!9!~?}(h+tor;?5hkDO7D4fiV2stdtE93Q7IZdrjl{!Q4Y%&BJH({A zgp>+!AJ@q#v~H`c$lSN<;qs=cvKzc*)!`<#mQcI&bHmicg0>vhZ zwNI;IF9jyV(W^sJO=K6#wypNf(-d9N>76BRHkHrImZMgDnOK4)q|qrzbhu<(JfOgH^>FOle^+FmkLI65(Vijv~(n3>K zp}(lg^X}eaKUPL=bQ!&|bYqL%_S>MCzM8ZS8~(IyzO6l?#QZB6Jx&S{i|tNc_xmiP}D+7v%;nsg-xuGuf9T6+EIMo=iq13RKrJ;-10250F1I8=lXfo7-cb zz{c6ql;?LlX#2PFM^1g+dEkak=J(YjHG$v0#Io2$*36V|0~*AsyHOt!Q|8_k>X{jQ zEv<;o3bDIrz(pRenq*UI@+wM7!&UCrf5O{EUx0-n%hWMNzMBI&9_MR>=hY9j#E`LROlFh;JY_vd;AgzLhWMNswL;U&e|U8|u>-HZ5-nYP*NOJNzSARIPI^#aK74&x z$9+Ee~MRe#v&sD|X77wJQH4Qm~z z8jFfIyc&wWo)nCHVJdrnWL-Jz^P7;&p^N{6=CgYeN3 z=lS<}Hpo1aR@y?F3itndwyiW!;rAX*sxCA({c)mDT;fSfy|ArPf&NW<(tYh;Wj}S% zc+y=vX%g(toL;AQfteJ9!ihWb!D?YukEQ=WM|7Ud(Al zIY7pYh@tXdY?Qyc5P#xunI5MiyEx&SZKf0WY;32K%cI@tBYKF|m)PJ22Kw<8E}oN` zxT#PuQb{}8R9N2~mdxLu);X-0vt<6DHgR#{gA->sf>|k7p?pC)gp;%tibfs2rK*d64SG z7w-5WNxcl&CSk9}{R`)9PZ95(?EX++Y$X&czzpiLa zCWKPQMA3EjuX00HuJ&}xIWOXGA04qtcy~TC?)LYa^!ymTH&`zgNyUCXZhLXI!C-50 zgJt1_sFa(^M|F|qB}G*dB`Pm{nctyiwrx@9u*R4+k2@`6J!TBFH-707 zEb$)?!H1VzhGo{&);;XIlz&jL%-^Gq|IRj9nVpQLcL zVWn5iG~rw+?|MK+-Rr*ce8{?CZ*AmuH3t$ zcL3+z5m-2!_mcz7hL5>kff< z5C6}~^v1W7e4w>qzOIof!soSa{h_tS(Z5*w121iVu%s2m(}!eC3xhbr00k0`fWXmkEwn2bYDWp8 z1=GotAP5ghf5PY=Z9oW!e=s6|i2!8!GXUNUg7B6DB!?}D&cjc{pPHX3%zNgo|8K(O zxex?~TKISdL7aIW+5vX)v|wN`oVVbg1L121;zgWK$;T4Gg z-+c%mBLCJ0hXW!0XCDj(U#r7lf&aumbx0U?%~&KF1BB||bZDKmIxG^%fj@N&I?0Dh zq5sGuqR(*(Z*5RJ8VyJqUJ8Ms`~AIW5MB=O+60KR9>y30gA)iQFqje2NE?MQHZd|m zqP30Ca8nZ<49W-x(Zj$25y1pSK${>5C~br(+C&>`WP;Mc8W~|>CJ3DCA73De&iJvT PC^!}iR#rB#F$Mn%EW0>; literal 0 HcmV?d00001 From c99ea30f02ccc01165ee5a9876f693ecf7def6a4 Mon Sep 17 00:00:00 2001 From: Yu-Ting Shi Date: Sat, 29 Jun 2024 04:38:37 +0800 Subject: [PATCH 2/6] Add weaker models (x86-TSO and ARM) to the "Memory consistency" section --- concurrency-primer.tex | 91 ++++++++++++++++++++++++++++++++++++++---- 1 file changed, 83 insertions(+), 8 deletions(-) diff --git a/concurrency-primer.tex b/concurrency-primer.tex index ae136ca..3e29cbe 100644 --- a/concurrency-primer.tex +++ b/concurrency-primer.tex @@ -1094,15 +1094,13 @@ \subsection{Memory consistency models} When a program is compiled and executed, it doesn't always follow the written order. The system may change the sequence and optimize it to simulate line-by-line execution, as long as the final result matches the expected outcome. -This requires an agreement between the programmer and the system (hardware, compiler, etc.), ensuring that if the rules are followed, the execution will be correct. Correctness here means defining permissible outcomes among all possible results, known as Memory Consistency Models. These models allow the system to optimize while ensuring correct execution. +This requires an agreement between the programmer and the system (hardware, compiler, etc.), ensuring that if the rules are followed, the execution will be correct. Correctness here means defining permissible outcomes among all possible results, known as memory consistency models. These models allow the system to optimize while ensuring correct execution. -Memory Consistency Models operate at various levels. For example, when machine code runs on hardware, processors can reorder and optimize instructions, and the results must match expectations. Similarly, when converting high-level languages to assembly, compilers can rearrange instructions while ensuring consistent outcomes. Thus, from source code to hardware execution, agreements must ensure the expected results. - -One can envision hardware that achieves sequential consistency as follows: each thread has direct access to shared memory, and memory processes only one read or write operation at a time. This naturally ensures sequential consistency. +Memory consistency models operate at various levels. For example, when machine code runs on hardware, processors can reorder and optimize instructions, and the results must match expectations. Similarly, when converting high-level languages to assembly, compilers can rearrange instructions while ensuring consistent outcomes. Thus, from source code to hardware execution, agreements must ensure the expected results. \subsubsection{Sequential consistency (SC)} -In the 1970s, Leslie Lamport proposed the most common memory consistency model, Sequential Consistency (SC), defined as follows: +In the 1970s, Leslie Lamport proposed the most common memory consistency model, sequential consistency (SC), defined as follows: \begin{quote} A multiprocessor system is sequentially consistent if the result of any execution is the same as if the operations of all the processors were executed in some sequential order, and the operations of each individual processor appear in this sequence in the order specified by its program. @@ -1117,6 +1115,7 @@ \subsubsection{Sequential consistency (SC)} To enhance the understanding of sequential consistency, consider the following simple example. Two threads write to and read from two shared variables \monobox{x} and \monobox{y}, both initially set to \monobox{0}. \begin{ccode} +// Litmus Test: Message Passing int x = 0; int y = 0; @@ -1141,12 +1140,88 @@ \subsubsection{Sequential consistency (SC)} Observing these orders, we see that none result in \monobox{r1 = 1} and \monobox{r2 = 0}. Thus, sequential consistency only allows the outcomes \monobox{(r1, r2)} to be \monobox{(1, 1)}, \monobox{(0, 1)}, and \monobox{(0, 0)}. With this convention, software can expect that \monobox{(1, 0)} will not occur, and hardware can optimize as long as it ensures the result \monobox{(1, 0)} does not appear. -We can imagine sequentially consistent hardware as the figure \ref{hw-seq-cst} shows: each thread can directly access shared memory, and memory processes one read or write operation at a time, naturally ensuring sequential consistency. In fact, there are multiple ways to implement sequentially consistent hardware. It can even include caches and be banked, as long as it ensures that the results behave the same as the aforementioned model. - -\centering +\begin{center} \includegraphics[keepaspectratio,width=0.7\linewidth]{images/hw-seq-cst} \captionof{figure}{The memory model of sequentially consistent hardware.} \label{hw-seq-cst} +\end{center} + +We can imagine sequentially consistent hardware as the figure \ref{hw-seq-cst} shows: each thread can directly access shared memory, and memory processes one read or write operation at a time, naturally ensuring sequential consistency. In fact, there are multiple ways to implement sequentially consistent hardware. It can even include caches and be banked, as long as it ensures that the results behave the same as the aforementioned model. + +\subsubsection{Total store order (TSO)} + +Although sequential consistency is considered the "golden standard" for multi-threaded programs, its many constraints limit performance optimization. As a result, it is rarely implemented in modern processors. Instead, more relaxed memory models are used, such as the total store order (TSO) memory model adopted by the x86 architecture. One can envision the hardware roughly as follows: + +\begin{center} +\includegraphics[keepaspectratio,width=0.7\linewidth]{images/hw-tso} +\captionof{figure}{The memory model of x86-TSO hardware.} +\label{hw-tso} +\end{center} + +All processors can read from a single shared memory, but each processor writes only to its own write queue. + +Consider the following Write Queue (Store Buffer) Litmus Test: + +\begin{ccode} +// Litmus Test: Write Queue (Store Buffer) +int x = 0; +int y = 0; + +// Thread 1 // Thread 2 +x = 1; y = 1; +r1 = y; r2 = x; +\end{ccode} + +Sequential consistency does not allow \monobox{r1 = r2 = 0}, but TSO does. In a sequentially consistent memory model, \monobox{x = 1} or \monobox{y = 1} must be written first, followed by the read operations, so \monobox{r1 = r2 = 0} cannot occur. However, under the TSO memory model, the write operations from both threads might still be in their respective queues when the read operations occur, allowing \monobox{r1 = r2 = 0}. + +Non-sequentially consistent hardware typically supports additional memory barrier (fence) instructions to control the order of read and write operations. These barriers ensure that writes before the barrier are completed (queues emptied) before any subsequent reads are performed. + +\begin{ccode} +// Thread 1 // Thread 2 +x = 1; y = 1; +barrier; barrier; +r1 = y; r2 = x; +\end{ccode} + +The reason total store order (TSO) is named as such is because once a write operation reaches shared memory, it indicates that all processors are aware that the value has been written. There will be no situation where different processors see different values. That is, the following litmus test will not have \monobox{r1 = 1}, \monobox{r2 = 0}, \monobox{r3 = 1}, but \monobox{r4 = 0}. + +Consider the following Independent Reads of Independent Writes (IRIW) Litmus Test: + +\begin{ccode} +// Litmus Test: Independent Reads of Independent Writes (IRIW) +int x = 0; +int y = 0; + +// Thread 1 // Thread 2 // Thread 3 // Thread 4 +x = 1; y = 1; r1 = x; r3 = y; + r2 = y; r4 = x; +\end{ccode} + +Once Thread 3 reads \monobox{r1 = 1}, \monobox{r2 = 0}, it indicates that the write \monobox{x = 1} reached shared memory before \monobox{y = 1}. If at this point Thread 4 reads \monobox{r3 = 1}, it means both writes \monobox{y = 1} and \monobox{x = 1} are visible to Thread 4, so \monobox{r4} can only be \monobox{1}. We can say "Thread 1's write to \monobox{x}" happens before "Thread 2's write to \monobox{y}". + +\subsubsection{Relaxed memory order (RMO)} + +\begin{center} +\includegraphics[keepaspectratio,width=0.4\linewidth]{images/hw-relaxed} +\captionof{figure}{The memory model of \textsc{Arm} relaxed hardware.} +\label{hw-relaxed} +\end{center} + +As shown in figure \ref{hw-relaxed}, the \textsc{Arm} instruction set adopts a more relaxed memory model. Each thread maintains its own copy of the memory, and every read and write operation targets this private copy. When writing to its own memory, it also propagates the changes to the memory of other threads. Thus, this model does not have a total store order. Furthermore, read operations can be delayed until they are actually needed. + +The write order seen by one thread can differ from the order seen by other threads because write operations can be reordered during propagation. However, reads and writes to the same memory address must still follow a total order. Therefore, the following litmus test cannot result in \monobox{r1 = 1}, \monobox{r2 = 2}, but \monobox{r3 = 2}, \monobox{r4 = 1}. Which write overwrites which must be visible to all threads. This guarantee is known as coherence. Without coherence, programming for such a system would be very difficult. + +All the litmus tests mentioned above are allowed under the relaxed memory model of \textsc{Arm}, except for the following example. Neither \textsc{Arm}, x86-TSO, nor sequential consistency model would result in \monobox{r1 = 1}, \monobox{r2 = 2}, \monobox{r3 = 2}, and \monobox{r4 = 1}. + +\begin{ccode} +// Litmus Test: Coherence +int x = 0; +int y = 0; + +// Thread 1 // Thread 2 // Thread 3 // Thread 4 +x = 1; x = 2; r1 = x; r3 = x; + r2 = x; r4 = x; +\end{ccode} \subsection{C11/C++11 atomics} From 6c1b062e87f73a9f4ce06e6ab06376a07f60df17 Mon Sep 17 00:00:00 2001 From: Yu-Ting Shi Date: Sat, 29 Jun 2024 11:24:04 +0800 Subject: [PATCH 3/6] Fix inconsistency of code style 1. split setences into separate lines 2. change the quotation marks "..." as ``...'' --- concurrency-primer.tex | 77 +++++++++++++++++++++++++++++++----------- 1 file changed, 57 insertions(+), 20 deletions(-) diff --git a/concurrency-primer.tex b/concurrency-primer.tex index 3e29cbe..c81ace4 100644 --- a/concurrency-primer.tex +++ b/concurrency-primer.tex @@ -1092,11 +1092,17 @@ \section{Memory orderings} \subsection{Memory consistency models} -When a program is compiled and executed, it doesn't always follow the written order. The system may change the sequence and optimize it to simulate line-by-line execution, as long as the final result matches the expected outcome. +When a program is compiled and executed, it doesn't always follow the written order. +The system may change the sequence and optimize it to simulate line-by-line execution, as long as the final result matches the expected outcome. -This requires an agreement between the programmer and the system (hardware, compiler, etc.), ensuring that if the rules are followed, the execution will be correct. Correctness here means defining permissible outcomes among all possible results, known as memory consistency models. These models allow the system to optimize while ensuring correct execution. +This requires an agreement between the programmer and the system (hardware, compiler, etc.), ensuring that if the rules are followed, the execution will be correct. +Correctness here means defining permissible outcomes among all possible results, known as memory consistency models. +These models allow the system to optimize while ensuring correct execution. -Memory consistency models operate at various levels. For example, when machine code runs on hardware, processors can reorder and optimize instructions, and the results must match expectations. Similarly, when converting high-level languages to assembly, compilers can rearrange instructions while ensuring consistent outcomes. Thus, from source code to hardware execution, agreements must ensure the expected results. +Memory consistency models operate at various levels. +For example, when machine code runs on hardware, processors can reorder and optimize instructions, and the results must match expectations. +Similarly, when converting high-level languages to assembly, compilers can rearrange instructions while ensuring consistent outcomes. +Thus, from source code to hardware execution, agreements must ensure the expected results. \subsubsection{Sequential consistency (SC)} @@ -1106,13 +1112,19 @@ \subsubsection{Sequential consistency (SC)} A multiprocessor system is sequentially consistent if the result of any execution is the same as if the operations of all the processors were executed in some sequential order, and the operations of each individual processor appear in this sequence in the order specified by its program. \end{quote} -On modern processors, ensuring sequential consistency involves many optimization constraints, which slow down program execution. If some conventions are relaxed, such as not guaranteeing program order within each processing unit, performance can be further improved. +On modern processors, ensuring sequential consistency involves many optimization constraints, which slow down program execution. +If some conventions are relaxed, such as not guaranteeing program order within each processing unit, performance can be further improved. -A memory consistency model is a conceptual convention. This means the program's execution results must conform to this model. However, when a program is compiled and run on computer hardware, there is significant flexibility in adjusting the execution order. As long as the execution results match the predefined convention, the actual order can vary depending on the circumstances. +A memory consistency model is a conceptual convention. +This means the program's execution results must conform to this model. +However, when a program is compiled and run on computer hardware, there is significant flexibility in adjusting the execution order. +As long as the execution results match the predefined convention, the actual order can vary depending on the circumstances. -It is important to note that sequential consistency does not imply a single order or a single result for the program. On the contrary, sequential consistency only requires that the program appears to execute in some interleaved order on a single thread, meaning a sequentially consistent program can still have multiple possible results. +It is important to note that sequential consistency does not imply a single order or a single result for the program. +On the contrary, sequential consistency only requires that the program appears to execute in some interleaved order on a single thread, meaning a sequentially consistent program can still have multiple possible results. -To enhance the understanding of sequential consistency, consider the following simple example. Two threads write to and read from two shared variables \monobox{x} and \monobox{y}, both initially set to \monobox{0}. +To enhance the understanding of sequential consistency, consider the following simple example. +Two threads write to and read from two shared variables \monobox{x} and \monobox{y}, both initially set to \monobox{0}. \begin{ccode} // Litmus Test: Message Passing @@ -1124,7 +1136,8 @@ \subsubsection{Sequential consistency (SC)} y = 1; r2 = x; \end{ccode} -If this program satisfies sequential consistency, then for Thread 1, \monobox{x = 1} must occur before \monobox{y = 1}, and for Thread 2, \monobox{r1 = y} must occur before \monobox{r2 = x}. For the entire program, the following six execution orders are possible: +If this program satisfies sequential consistency, then for Thread 1, \monobox{x = 1} must occur before \monobox{y = 1}, and for Thread 2, \monobox{r1 = y} must occur before \monobox{r2 = x}. +For the entire program, the following six execution orders are possible: \begin{verbatim} | x = 1 | x = 1 | x = 1 | @@ -1138,7 +1151,9 @@ \subsubsection{Sequential consistency (SC)} | r2 = x(1) | y = 1 | y = 1 | \end{verbatim} -Observing these orders, we see that none result in \monobox{r1 = 1} and \monobox{r2 = 0}. Thus, sequential consistency only allows the outcomes \monobox{(r1, r2)} to be \monobox{(1, 1)}, \monobox{(0, 1)}, and \monobox{(0, 0)}. With this convention, software can expect that \monobox{(1, 0)} will not occur, and hardware can optimize as long as it ensures the result \monobox{(1, 0)} does not appear. +Observing these orders, we see that none result in \monobox{r1 = 1} and \monobox{r2 = 0}. +Thus, sequential consistency only allows the outcomes \monobox{(r1, r2)} to be \monobox{(1, 1)}, \monobox{(0, 1)}, and \monobox{(0, 0)}. +With this convention, software can expect that \monobox{(1, 0)} will not occur, and hardware can optimize as long as it ensures the result \monobox{(1, 0)} does not appear. \begin{center} \includegraphics[keepaspectratio,width=0.7\linewidth]{images/hw-seq-cst} @@ -1146,11 +1161,16 @@ \subsubsection{Sequential consistency (SC)} \label{hw-seq-cst} \end{center} -We can imagine sequentially consistent hardware as the figure \ref{hw-seq-cst} shows: each thread can directly access shared memory, and memory processes one read or write operation at a time, naturally ensuring sequential consistency. In fact, there are multiple ways to implement sequentially consistent hardware. It can even include caches and be banked, as long as it ensures that the results behave the same as the aforementioned model. +We can imagine sequentially consistent hardware as the figure \ref{hw-seq-cst} shows: each thread can directly access shared memory, and memory processes one read or write operation at a time, naturally ensuring sequential consistency. +In fact, there are multiple ways to implement sequentially consistent hardware. +It can even include caches and be banked, as long as it ensures that the results behave the same as the aforementioned model. \subsubsection{Total store order (TSO)} -Although sequential consistency is considered the "golden standard" for multi-threaded programs, its many constraints limit performance optimization. As a result, it is rarely implemented in modern processors. Instead, more relaxed memory models are used, such as the total store order (TSO) memory model adopted by the x86 architecture. One can envision the hardware roughly as follows: +Although sequential consistency is considered the ``golden standard'' for multi-threaded programs, its many constraints limit performance optimization. +As a result, it is rarely implemented in modern processors. +Instead, more relaxed memory models are used, such as the total store order (TSO) memory model adopted by the x86 architecture. +One can envision the hardware roughly as follows: \begin{center} \includegraphics[keepaspectratio,width=0.7\linewidth]{images/hw-tso} @@ -1172,9 +1192,12 @@ \subsubsection{Total store order (TSO)} r1 = y; r2 = x; \end{ccode} -Sequential consistency does not allow \monobox{r1 = r2 = 0}, but TSO does. In a sequentially consistent memory model, \monobox{x = 1} or \monobox{y = 1} must be written first, followed by the read operations, so \monobox{r1 = r2 = 0} cannot occur. However, under the TSO memory model, the write operations from both threads might still be in their respective queues when the read operations occur, allowing \monobox{r1 = r2 = 0}. +Sequential consistency does not allow \monobox{r1 = r2 = 0}, but TSO does. +In a sequentially consistent memory model, \monobox{x = 1} or \monobox{y = 1} must be written first, followed by the read operations, so \monobox{r1 = r2 = 0} cannot occur. +However, under the TSO memory model, the write operations from both threads might still be in their respective queues when the read operations occur, allowing \monobox{r1 = r2 = 0}. -Non-sequentially consistent hardware typically supports additional memory barrier (fence) instructions to control the order of read and write operations. These barriers ensure that writes before the barrier are completed (queues emptied) before any subsequent reads are performed. +Non-sequentially consistent hardware typically supports additional memory barrier (fence) instructions to control the order of read and write operations. +These barriers ensure that writes before the barrier are completed (queues emptied) before any subsequent reads are performed. \begin{ccode} // Thread 1 // Thread 2 @@ -1183,7 +1206,9 @@ \subsubsection{Total store order (TSO)} r1 = y; r2 = x; \end{ccode} -The reason total store order (TSO) is named as such is because once a write operation reaches shared memory, it indicates that all processors are aware that the value has been written. There will be no situation where different processors see different values. That is, the following litmus test will not have \monobox{r1 = 1}, \monobox{r2 = 0}, \monobox{r3 = 1}, but \monobox{r4 = 0}. +The reason total store order (TSO) is named as such is because once a write operation reaches shared memory, it indicates that all processors are aware that the value has been written. +There will be no situation where different processors see different values. +That is, the following litmus test will not have \monobox{r1 = 1}, \monobox{r2 = 0}, \monobox{r3 = 1}, but \monobox{r4 = 0}. Consider the following Independent Reads of Independent Writes (IRIW) Litmus Test: @@ -1197,7 +1222,9 @@ \subsubsection{Total store order (TSO)} r2 = y; r4 = x; \end{ccode} -Once Thread 3 reads \monobox{r1 = 1}, \monobox{r2 = 0}, it indicates that the write \monobox{x = 1} reached shared memory before \monobox{y = 1}. If at this point Thread 4 reads \monobox{r3 = 1}, it means both writes \monobox{y = 1} and \monobox{x = 1} are visible to Thread 4, so \monobox{r4} can only be \monobox{1}. We can say "Thread 1's write to \monobox{x}" happens before "Thread 2's write to \monobox{y}". +Once Thread 3 reads \monobox{r1 = 1}, \monobox{r2 = 0}, it indicates that the write \monobox{x = 1} reached shared memory before \monobox{y = 1}. +If at this point Thread 4 reads \monobox{r3 = 1}, it means both writes \monobox{y = 1} and \monobox{x = 1} are visible to Thread 4, so \monobox{r4} can only be \monobox{1}. +We can say "Thread 1's write to \monobox{x}" happens before "Thread 2's write to \monobox{y}". \subsubsection{Relaxed memory order (RMO)} @@ -1207,11 +1234,21 @@ \subsubsection{Relaxed memory order (RMO)} \label{hw-relaxed} \end{center} -As shown in figure \ref{hw-relaxed}, the \textsc{Arm} instruction set adopts a more relaxed memory model. Each thread maintains its own copy of the memory, and every read and write operation targets this private copy. When writing to its own memory, it also propagates the changes to the memory of other threads. Thus, this model does not have a total store order. Furthermore, read operations can be delayed until they are actually needed. - -The write order seen by one thread can differ from the order seen by other threads because write operations can be reordered during propagation. However, reads and writes to the same memory address must still follow a total order. Therefore, the following litmus test cannot result in \monobox{r1 = 1}, \monobox{r2 = 2}, but \monobox{r3 = 2}, \monobox{r4 = 1}. Which write overwrites which must be visible to all threads. This guarantee is known as coherence. Without coherence, programming for such a system would be very difficult. - -All the litmus tests mentioned above are allowed under the relaxed memory model of \textsc{Arm}, except for the following example. Neither \textsc{Arm}, x86-TSO, nor sequential consistency model would result in \monobox{r1 = 1}, \monobox{r2 = 2}, \monobox{r3 = 2}, and \monobox{r4 = 1}. +As shown in figure \ref{hw-relaxed}, the \textsc{Arm} instruction set adopts a more relaxed memory model. +Each thread maintains its own copy of the memory, and every read and write operation targets this private copy. +When writing to its own memory, it also propagates the changes to the memory of other threads. +Thus, this model does not have a total store order. +Furthermore, read operations can be delayed until they are actually needed. + +The write order seen by one thread can differ from the order seen by other threads because write operations can be reordered during propagation. +However, reads and writes to the same memory address must still follow a total order. +Therefore, the following litmus test cannot result in \monobox{r1 = 1}, \monobox{r2 = 2}, but \monobox{r3 = 2}, \monobox{r4 = 1}. +Which write overwrites which must be visible to all threads. +This guarantee is known as coherence. +Without coherence, programming for such a system would be very difficult. + +All the litmus tests mentioned above are allowed under the relaxed memory model of \textsc{Arm}, except for the following example. +Neither \textsc{Arm}, x86-TSO, nor sequential consistency model would result in \monobox{r1 = 1}, \monobox{r2 = 2}, \monobox{r3 = 2}, and \monobox{r4 = 1}. \begin{ccode} // Litmus Test: Coherence From a48f6339ddd387025537bd1afa73632141d24467 Mon Sep 17 00:00:00 2001 From: Yu-Ting Shi Date: Sat, 6 Jul 2024 11:51:14 +0800 Subject: [PATCH 4/6] Replace the execution results of code with LaTeX table syntax --- concurrency-primer.tex | 57 ++++++++++++++++++++++++++++++++---------- 1 file changed, 44 insertions(+), 13 deletions(-) diff --git a/concurrency-primer.tex b/concurrency-primer.tex index c81ace4..2e45dab 100644 --- a/concurrency-primer.tex +++ b/concurrency-primer.tex @@ -1137,19 +1137,50 @@ \subsubsection{Sequential consistency (SC)} \end{ccode} If this program satisfies sequential consistency, then for Thread 1, \monobox{x = 1} must occur before \monobox{y = 1}, and for Thread 2, \monobox{r1 = y} must occur before \monobox{r2 = x}. -For the entire program, the following six execution orders are possible: - -\begin{verbatim} -| x = 1 | x = 1 | x = 1 | -| y = 1 | r1 = y(0) | r1 = y(0) | -| r1 = y(1) | y = 1 | r2 = x(1) | -| r2 = x(1) | r2 = y(1) | y = 1 | -+-------------------+-------------------+-------------------+ -| r1 = y(0) | r1 = y(0) | r1 = y(0) | -| x = 1 | x = 1 | r2 = x(0) | -| y = 1 | r2 = x(1) | x = 1 | -| r2 = x(1) | y = 1 | y = 1 | -\end{verbatim} +For the entire program, the following six execution orders are possible: + +\begin{center} +\noindent +\begin{tabular}{|c|c|c|} \hline +\begin{lstlisting} +x = 1 +y = 1 + r1 = y(1) + r2 = x(1) +\end{lstlisting}& +\begin{lstlisting} +x = 1 + r1 = y(0) +y = 1 + r2 = y(1) +\end{lstlisting}& +\begin{lstlisting} +x = 1 + r1 = y(0) + r2 = x(1) +y = 1 +\end{lstlisting}\\ \hline +\begin{lstlisting} + r1 = y(0) +x = 1 +y = 1 + r2 = x(1) +\end{lstlisting}& +\begin{lstlisting} + r1 = y(0) +x = 1 + r2 = x(1) +y = 1 +\end{lstlisting}& +\begin{lstlisting} + r1 = y(0) + r2 = x(0) +x = 1 +y = 1 +\end{lstlisting}\\ \hline +\end{tabular} +\captionof{table}{6 possible execution orders of the message passing litmus test.} +\end{center} Observing these orders, we see that none result in \monobox{r1 = 1} and \monobox{r2 = 0}. Thus, sequential consistency only allows the outcomes \monobox{(r1, r2)} to be \monobox{(1, 1)}, \monobox{(0, 1)}, and \monobox{(0, 0)}. From 81b7ce49020fe26fba24687135d971374ad09bc6 Mon Sep 17 00:00:00 2001 From: Yu-Ting Shi Date: Sat, 6 Jul 2024 13:26:16 +0800 Subject: [PATCH 5/6] Fix the inconsistency of quotation marks --- concurrency-primer.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/concurrency-primer.tex b/concurrency-primer.tex index 2e45dab..fd40a89 100644 --- a/concurrency-primer.tex +++ b/concurrency-primer.tex @@ -1255,7 +1255,7 @@ \subsubsection{Total store order (TSO)} Once Thread 3 reads \monobox{r1 = 1}, \monobox{r2 = 0}, it indicates that the write \monobox{x = 1} reached shared memory before \monobox{y = 1}. If at this point Thread 4 reads \monobox{r3 = 1}, it means both writes \monobox{y = 1} and \monobox{x = 1} are visible to Thread 4, so \monobox{r4} can only be \monobox{1}. -We can say "Thread 1's write to \monobox{x}" happens before "Thread 2's write to \monobox{y}". +We can say ``Thread 1's write to \monobox{x}'' happens before ``Thread 2's write to \monobox{y}''. \subsubsection{Relaxed memory order (RMO)} From 99a06b1db3c241c76210e6dce71958d02890bdcd Mon Sep 17 00:00:00 2001 From: Yu-Ting Shi Date: Tue, 23 Jul 2024 03:56:51 +0800 Subject: [PATCH 6/6] Address text consistency and merge related statements - Changed "doesn't" to "does not" for formal English writing - Fixed the inconsistency of quotation marks - Merged related statements into one paragraph --- concurrency-primer.tex | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/concurrency-primer.tex b/concurrency-primer.tex index fd40a89..6a58285 100644 --- a/concurrency-primer.tex +++ b/concurrency-primer.tex @@ -1092,9 +1092,8 @@ \section{Memory orderings} \subsection{Memory consistency models} -When a program is compiled and executed, it doesn't always follow the written order. +When a program is compiled and executed, it does not always follow the written order. The system may change the sequence and optimize it to simulate line-by-line execution, as long as the final result matches the expected outcome. - This requires an agreement between the programmer and the system (hardware, compiler, etc.), ensuring that if the rules are followed, the execution will be correct. Correctness here means defining permissible outcomes among all possible results, known as memory consistency models. These models allow the system to optimize while ensuring correct execution.