Popular in Course
Popular in Nursing and Health Sciences
This 127 page Class Notes was uploaded by Dr. Kurtis Nolan on Sunday September 6, 2015. The Class Notes belongs to N 1 at University of Texas at Austin taught by Staff in Fall. Since its upload, it has received 15 views. For similar materials see /class/181627/n-1-university-of-texas-at-austin in Nursing and Health Sciences at University of Texas at Austin.
Reviews for FIRST
Report this Material
What is Karma?
Karma is the currency of StudySoup.
You can buy or earn more Karma at anytime and redeem it for class notes, study guides, flashcards, and more!
Date Created: 09/06/15
4 DISTORTION AND Gownns DICHOTOMY THEOREM We have seen that distortable spaces exist and more over every X either contains a distortable subspace or an isornorph of some 19 1 g p lt 00 or co Two main problems rernain 1 To classify which X if any have the property that every uniformly continuous f S X gt R is oscillation stable for all 5 gt 0 Y Q X there exists Z Q Y with oscf 32 lt e 2 Is 2 distortable ls 19 distortable for 1 lt p lt oo Recall that 1 and co are not distortable We have also seen that 2 is distortable this also holds for 19 1 lt p lt oo iff there exist sets A B Q 52 with dA B gt 0 and for all X Q 2 A H SX y 0 and B H SX y 0 How could we nd such sets A and B If we walked over 52 how could we decide which vectors to put in A and which in B If we stood at 1 6 52 it would look no different than standing at any other 3 E SEQ Could the answer be different for different Ep s No by virtue of the Mazur map Mp Mp 51 gt Sgp is given by Mpa f1 Sign ailaz39llplfii MI is a uniform homeomorphism between the two unit spheres Rib and thus fm E MCIM1 Sgp gt qu is a uniform homeomorphism 171 onto and the map and its inverse are uniformly continuous Moreover fm and fgql preserve block subspaces subspaces spanned by block bases It follows that if some 19 1 g p lt oo admits sets AB Q Sgp with dA B gt 0 and A H X y 0 B H X y 0 for all X Q 19 then this holds for all p E 1oo For example if such sets exist in 351 then for small enough 5 MPAE MPBE form such a pair in Sgp Here for C Q Sgp CE E x E Sgp dxC lt 5 In particular we see that if 2 is distortable then not every uniformly continuous f 51 gt R is oscillation stable let f dUla Now we do have distortion in some spaces such as T or S We can indeed identify different types of vectors in these spaces Ff averages and averages of RIS s So to solve the distortion problem the rough idea is to generalize the Mazur map to more spaces and use the existence of A and B in some space to transfer it back to 2 The generalized Mazur map was prepared for use in Gil Lo although they did not focus on the properties of the map as such First we define the entropy rnap EX 2 1 Coo X X gt O000 where X is a space with a normalized 1 unconditional basis ei EX is given by EXUML Z 10g 0 logO E 0 FX Sgl coo gt S X is given by FXUL the unique 1 E SX so that if 1 E inei then i Eh7 L 2 Ehy for all y E SX ii supp h supp 1 iii sign h1 sign 511 for all Z Of course such an 1 must be shown to exist Now if X is uniformly convex and uniformly smooth one can show that FX extends to a uniform homeomorphism of 51 onto SX le 19 then FX Mp With some additional tricks we obtain Theorem 41 082 Let X have an unconditional ba sis Then SX and 551 are uniformly homeomorphic i co is not nitely representable in X The only if direction is due to Enflo More general results exist see BL Theorem 42 082 For 1 lt p lt 00 19 is biorthog onally distortable More precisely there exists 5139 i 0 and sets Ak Q Sgp and A Q ng Jr 1 for h E N so that i for all a E Ak there exists xquot E A with gt 1 5k 11 for all a E Ak and xquot E A with 5 9 lt Emmet 111 for all e gt 0 and h AtE H Y 0 for all Y Q 19 pr 2 then Ak AZ Moreover the sets Ak and A are spreading and J unconditional ie a E At i m 6 At The biorthogonal distortion of 19 comes from the norms 115an 115611sz EnHJIH We outline the steps in the proof First we recall from 81 that there exist integers pg T 00 so that setting Ck 51 E S 1 is an RIS average of length pk 1 Pk CL ES 51 51pkisa k Hm 1 block basis of By then 61029 satisfy iiii above With respect to S Of course these must be precisely quanti ed We then de ne sets in 51 xquot on Bkk CIZECZ L kECk lJIZlGMl lelltlxklHxZowkH121 Here 51 0 wk Each Bk is 1 unconditional and spreading Moreover this takes work B95 H Y y 0 for all Y Q 1 This is done using the maps E3 and 173 Let s see how to proceed in 2 for simplicity Set AkxESEQlxl2EBkAZ Thus Ak M2Bk so Ak satis es iii and also i To see ii let L kEAkgE4 Withk37 and lifle 22 0 MVWZOMW and W2 2 0 lidWWW be as in the de nition of Bk and By 1 50 1 Then ltlkla WD 3 A WOWWWOWOW2 J 12 12 3 Z leOWAjM 2 women 1 j E Mail lwelgtmltl2t lxklgt12 S Agmin f Remarks Our original argument was Maureyed Mau rey also extended the proof to show that the sets Bk could be taken to be symmetric E Bk ltgt L Mm E Bk for all permutations 7r of N Maurey M2 also proved that if X has an uncondi tional basis and 1 is not nitely representable in X then X contains an arbitrarily distortable subspace Theorem 43 G2 Every uniformly continuous f 00 gt R is oscillation stable The proof also appears in BL and involves an inge nious use of idernpotent ultra lters and the special prop erty of co that if 1 and y are close on all coordinates say 3 5 then yH g e The proof was motivated by an ultrafilter proof of Hindrnan s theorern due to Glazer Thus not every LipschitZ f 51 gt R is oscillation stable but for co the picture is different We combine the theorems above With llilrnan7s The orern 33 to get the following Theorem 44 a X does not contain a distortable subspace i for all Y Q X either Co or 1 embeds into Y b Every f SX gt R is oscillation stable i X is cosatm ated ie for all Y Q X c0 lt gt Y In our discussion of the unconditional basic sequence problem we saw that Ramsey theory was quite useful in ob taining results via stabilization of some property in terms of subspaces given by subsequences of a basis Since XGM exists there can not be a Ramsey theo rem that could succeed in always nding an unconditional basic sequence Since 2 is distortable we know that even in a nice space we cannot say if we nitely color 55 then some subspace is up to an e monochromatic This only works for co saturated spaces Of course for seeking un conditional bases or more generally a nice subspace one needs only check among all block bases of a given basis It turns out that there is indeed a sort of block Ramsey theorem due to Gowers G3 and G4 but it is phrased roughly in terms of either you get a monochro matic block subspace or you have a winning strategy for the alternative An application is Gowers dichotomy the orem First we need some notation Assume X has a ba sis ei and let 2 2X consist of all nite block bases of ei in BX Let a Q E and we consider a 2 player game Player S for subspace chooses a block sub space X1 of X X1 when is a block basis of e1 Then player V for vector chooses x1 6 Bltx gt and plays alternate in this fashion V wins if at some point 1513 L n E 0 If Y is a block subspace of X then a is called strate gically large for Y if V has a winning strategy for the game played solely in Y Let 5 6i7 6139 gt 0 We set 08 E Z 3 E 0 with g 6139 for z g n This is the familiar fattening one needs when analysis meets Ramsey theory Finally we say a is large for X if for all block subspaces W of X some further block basis of W E 0 Theorem 45 G3 G4 Let 0 Q 2X be large for X and 5 6239 6139 gt 0 Then there exists a block subspace Y of X so that 05 is strategically large for Y So given any X and 0 Q 2X we can nd Y so that either 0 2Y 0 or 05 is strategically large for Y This beautiful theorem has an important application which we now present Theorem 46 Gowers Dichotorny Theorem Every X contains Y which either has an unconditional basis or is H Sketch of proof The proof is based upon the fact that we may assume X has a basis ei and if X contains no unconditional basic sequence then for all N and all block bases of ei one can nd a further block basis 31 E Z 101 with n n H Zena gt NH 22 1 1 We let 0N be all such blocks So 0N2 is large for X for all N Thus given N we can nd a block subspace Y of X so that UN2L is strategi cally large for Y Using ON2L Q UN for an appropriate 5 and a diagonal argument we obtain Z so that UN is strategically large for Z for all N Then just as in the proof that XGM is Hi we obtain Z is Hl D Theorem 45 seems to be not that easy to use It is obvious that given a one can nd Y with either 2Y g 00 or for all block subspaces Z of X 2Z 0 y 0 There is also an in nite version of Theorem 45 due to Gowers One puts a suitable complete metric on 200X roughly the topology of pointwise convergence Theorem 47 G3 G4 If a Q 200X is analytic and large for X then for all 5 X has a block subspace Y with 05 strategically large for Y 102 Gowers used this theorem to prove Theorem 48 Let X have an unconditional basis Then there exists a block subspace Y which is either quasi minirnal or no two subspaces generated by disjointly supported block bases are isomorphic Y is quasiminimal if for all W Z Q Y there exists U Q W and V Q Z with U isomorphic to V As an example T is quasi minimal see eg 08 An important application of Gowers dichotomy the orem was the nal solution to the famous homogeneous Banach space problem It had been shown K T J 1 that if X is homogeneous and not isomorphic to 2 then X contains a subspace with out an unconditional basis Theorem 49 G3 K T Jl T Jll Assume X is homogeneous ie X N Y for all Y Q X Then X N 2 103 Indeed let X be homogeneous and choose Y Q X With either a an unconditional basis or b Y is Hl If X 76 2 then both a and b are impossible the rst by the K T J 1 result and the second since an Hl space is not isomorphic to any proper subspace The following problem remains open Problem If every subspace of X has an unconditional basis is X N 2 A partial result is known If every subspace of X X 52 2X has an unconditional basis then X N 2 K T J2 We should remark that there does exist a space a convexi ed Tsirelson space all of Whose subspaces have a basis Which is not isomorphic to 2 J01 We end this section With Maurey s proof of the di chotomy theorem This uses the ideas of Gowers in prov ing his block Ramsey theorem and indicates that the avor of the argument is inherited from the Nash Williams proof that open sets are Ramsey Maurey s Proof M3 We may assume X has a bimonotone basis ei We will say X is H a 5 gt 0 if for all block subspaces Y and Z of X there exist 3 E Y z E Z so that My 2H lt ElliZH It is easy to check that X is Hl iff it is Hl for all 5 gt 0 Claim If X contains no Canconditional basic se quence then for 5 gt 20 X contains a block subspace which is Hl5 Once we have established the claim a diagonal argu ment yields the theorem For the rest of the argument we will work with the rational linear span of ei and of block bases Thus our subspaces will be countable sets For x y E X X X and a block subspace Z of X we say x y accepts Z if for all block subspaces U V of Z there exists it E U v E V With xuyv E A E 6 XXX lt eHwzH x y rejects Z if for all V Q Z rational block subspace x 3 does not accept V Write X X X xn yn n E N Inductively choose X1 2 X2 2 X7111 block subspace of X so that for each 71 either Jim 3 accepts Xn 0r rejects Xn Let Z be a diagonal space of the Xn s ie Z has block basis With a block basis of Xn for all n Thus for all 71 mm 3 either accepts 0r rejects Z If 0 0 accepts Z then Z is Hle Assuming 0 0 rejects Z we shall construct a block basis 2k 1 g g 2 so that for all dz3 and i m 1 m Hm sglzm 1 1 provided that ak jkNZk for some integer jjkj g N 2k for k g m Where N gt 165 is a xed integer By a standard perturbation argument we get that is 2 unconditional which is a contradiction to our hypothesis In other words we shall construct so that for a1 as above and I J partitioning 1 2 m Hts 21H 2 allxyH if Zakzk7 y I J ie x y E A for such a and 3 Thus we wish to construct so that for all m and all such say which we call a reasonable pair formed from 2071 reject Z Indeed if x7 3 rejects Z then for all Z Q Z x 3 does not accept Z Hence there exists U V Q Z so that for all av E U gtlt V xayv E A Leta v 0 to get H511 31H 2 8H1 31H Now if say rejects Z then for all W Q Z there exists W Q W so that for all 11 E W aw y rejects Z Otherwise there exists W Q Z so that for all U Q W there exists no E U so that a a0 3 accepts Z Thus for all V Q W there exists aha E U gtlt V so that x a0 21431 v E A Hence x y accepts W which contradicts x y rejects Z Assume are chosen so that all reasonable pairs formed from them reject Z Since there are only nitely many such pairs there exists by our above argument W Q Z so that for all w E W and all reasonable pairs x y x wy rejects Z Choose 1 lt HanH lt 2 an E W Let Lquot y be a reasonable pair from 20711 Then 51 y CI aan y or 513 azn Where 133 is a reasonable pair from Both pairs reject the second from the symmetry of A and reasonable pairs D Q W J i 111 wfg39j Moritz Nagel 12062006 il Outline I Basic Ideas Cabibbo Angle I Generalization Mathematical Structures I Today s Results I Some Consequences Basic Ideas Cabibbo Angle Basic Ideas Cabibbo Angle I Experiments show the existence of a charged electroweak coupling between an up and down quark and between an up and strange quark i1 Basic Ideas Cabibbo Angle I How can that be explained by the Standard Model Recall that the SM describes the charged electroweak interaction only between the members of a lefthanded fermion doublet Exp V 1 For 6 we get J51 2167 75 e e L 2 i1 Basic Ideas Cabibbo Angle I So which doublet should we create with the up down and strange quark l Hint The strangenesschanging coupling is weaker than the strangenesspreserving coupHng i1 Basic Ideas Cabibbo Angle I To solve this problem in 1963 N Cabibbo suggested a superposition state d of a down quark and a strange quark I We can now formulate the doublet u u d39 doosSssin3 i1 Basic Ideas Cabibbo Angle I That idea solves the situation very well It explains the difference in the strangeness changing and strangenesspreserving decays and it also preserves a universal electroweak coupling constant g K4 Rd ig 4175 ig 175 cos19 s1n3 J5 2 J5 2 i1 Basic Ideas Cabibbo Angle I Soon after it became clear that this was not the whole story Some decays could not be explained by Cabibbo s ideas I In 1974 Cabibbo s ideas could be restored with the discovery of the charm quark and the formulation of the following doublets land ll d S with d39dcos9ssin19 ands39z dsin19scosl9 i I Basic Ideas Cabibbo Angle I The basic idea can be written as a rotation between the electroweak eigenstates of the quark and the flavor eigenstates aquot 0053C sinSC d V d S39 sin3C 0053C s 3 3C Cabibbo Angle i1 Basic Ideas Cabibbo Angle I After it became clear that there should be a third family this basic idea led to the general model of defining a unitary rotation VCW between the electroweak eigenstates of the quarks and the flavor eigenstates aquot d S39 VCKM S b39 b CKM Cabibbo KobayashiMaskawa i1 Basic Ideas Cabibbo Angle I Only rotation of down type quarks convention today I Rotation of up type quarks and down type quarks can be expressed by only one rotation due to the form of the electroweak interaction Lagrangian of d s ltgt 5 1 7 PLVCKM s b b a a zwmw down izl a Generalization Mathematical Structures Generalization Mathematical Structures I Foeramilies 2N flavors one needs a NxN unitary matrix I N2 complex numbers I 2N2 real numbers I What are the free parameters Generalization Mathematical Structures I Unitary condition leads to N2 constraints I 2N1 phase factors can be absorbed by quark fields I That gives 2N2N22N1N12 independent parameters I Of those independent numbers are NN12 rotation angles called quark mixing angles and are N 1N22 complex phases Generalization Mathematical Structures I N2 I One free parameter a quark mixing angle the Cabibbo Angle cos 8C sin 8C V sin 8C cos 8C Generalization Mathematical Structures I N3 I Four free parameters three quark mixing angles and one complex phase 1395 012013 013512 5136 1395 1395 VCKMS 623312 6125135236 612623 3123133236 613323 1395 1395 312323 6126235136 612323 6233123136 613623 CU cos 91 and Si sm 911 Generalization Mathematical Structures I This is the standard parameterization of VCW by the Particle Data Group 1395 1 0 0 613 0 S136 012 512 VCKMS 0 623 52339 0 1 0 512 612 0 i5 0 s23 623 sl3e 0 613 0 0 1 f J Rotation of d and squark Rotation of s and bquark remember case N22 Rotation of d and bquark plus phasefactor 5 Today s Results Today s Results I The transition probability from one quark to another quark is proportional to the magnitude squared of the elements of the matrix VCKM Vud Vus Vub VCKAI Vcd cs 101 Kd Ks Kb Therefore those values are measurable i I Today s Results I The Particle Data Group 2005 gives 0973909751 o2210227 000480014 ap o2210227 0973009744 00370043 0002900045 00390044 0999009992 i I a Today s Results l The Cabibbo Angle has also been measured and is approximately 13 Consequences Consequences I The neutral current remains the same since the rotation matrix VCKM is unitary Jneulral Jneutral 9 C9 dL 67L EL Eng707 QSinz 6wVCKM SL bL dR c7R ER 5RVW707 Qsin26wVCW SR bR il Consequences I The quark mixing that results from the VCW matrix leads to new terms in the charged current d 1 27 5 f7 PLVCW s b il Consequences I New decays are possible uptype quarks can decay into all down type quarks and vise versa I No neutral flavorchanging decays il Consequences I CP Violation build into the SM VCW contains complex phase 6 Hamiltonian His complex Time reversal operation TUK THTI H Time reversal violated CPT theorem yields CP violation as well has been seen in nature Solution Technique of Adjoint Problem D Fuentes Institute for Computational Engineering and Sciences The University of Texas at Austin Austin Texas April 27 2005 Advantages of Adjoint Solve 23 the computational work of finite difference computation of gradient similiar for calibration optimal control and mesh refinement software reuse Outline o Inverse Problem Calibration 0 Solution Technique 0 Current Results Pennes Model Combining all terms the problem statement is as follows Find the spatially and temporally varying temperature field Tx t such that pCpg Ii V39hTVTWTCbloodTTa Qlaserltx9 75 in 9 given the boundary condition kTVT n hT TOO on 89 and the initial condition Tx 0 T0 in n in the classical sense Pennes Model where kT the scalar coefficient of thermal conductivity Ta K Temperature of arterial blood T K Temperature of tissue homogeneous medium cblood specific heat of blood wT k9 perfusion coefficient Has units of mass sm3 flow of blood to tissue per unit volume of tissue Pennes Model For Physical and mathematical reasons assume that the thermal conductivity and blood perfusivity are smooth mon inc easing bounded and analytic functions of temperature Pennes Model Variational Formulation Standard arguements to obtain the weak form of the equations integrate in time and apply the initial conditions weakly 739 8 BT 6 v 20 Q papa ft kT 6VT V39v wT 6cbloodT Ta 390 dazdt thdAdtTx0 vx 0 da 0 39 Q Fn39v 2 QlaseTnXv dazdt hTOO39vdAdt l T0 39vx0 da 0 9 0 69 9 Inverse Problem Calibration Given a set of laser parameters no and an experimentally determined temperature field at all time Tempx t Find the best combination of model coefficients 3 E Rm that produces the temperature field T E V such that QltTltno6gtgt T ltTltxtgt Texpltxtgtgt2 dwelt satisfies QTno gngQltTltno gtgt M a e Rm EIT st BTBv Fnov W E V Solution Technique Calibration We wish to compute the gradient of the objective function with respect to the model coefficients 8Q 816239 Solving for the lagrange multiplier 10 E 12 such that QiaseAT q BTa 16 19p aneshTCI Vq E V QcalibT3 I i 1m Leads to a solution method for each of the posed problem 8Q 8BT9 16 p Cal39brat39on 39 39 a i 8e 8 Solution Technique Calibration 8 8T Q a T gt 86239 816239 Using a Galerkin representation of the temperature field as a guide BT9 16 v 86239 a BT 3 v F070 12 e B39 T 3 3 21 v o 86239 239 where B T q v E BT 061 v BT 11 Solution Technique Calibration Notice that solving for the Lagrange multiplier p E v such that B T 6110 Q T q Vq E V implies B T 8T 8T m B me 1 Q T and the gradient of the quantity of interest may be calculated by evaluating the partial of the semilinear form with respect to the model coefficient at the primal and dual solutions 8Q BT9 16 p 86239 816239 Adjoint Solve Discretization consistent with numerical computations of forward solve Reasonable Discretization of Continuous Adjoint Dual Problem Numerically Consistent Adjoint Solve Start with CrankNicholson on Pennes Equation Tk Tk l Pcp At vie kTk 9 16VTk V39vk wTk 9 16CbloodTk E Ta vie d5 th vk dA Qla53Txvk da hTCgt0 vk dA V39vk k 12n an 2 2 n 2 an 2 2 with T0 T0x and Tk Let k Tk E 0 1 11kg E vi 1 i1 i1 Numerically Consistent Adjoint Solve Then the discretized Pennes equation is equivalent to C719 a c l At 2 Where M is the mass matrix M 2 9 pcquiqudw 1 le 1 78 fk k 17 quot397 n the source term is jg 1 39 oo 239 A f Molaseumkjmdacfth 15 d Numerically Consistent Adjoint Solve and the vector valued function g is defined as 943725 39quot yj bjakmkl V yj bj 39VQbi div j j w yj jaw09w1 Cblood yj j Ta div A hgyjqu dA Numerically Consistent Adjoint Solve The gradient of the objective function with respect to the control parameters may be computed exactly through th ag 07k ak l s sk 1 At A W an 2 lt8 u lt 2 k1 where 539 k 1 n m kl pk E ZAZ39 2 i1 is the solution of the adjoint formulation Numerically Consistent Adjoint Solve 1 p 1 r 1 1 62k 61quot 1 p r 1 M V Ak Ak a At lt gt 2 ayj 2 T a a 1 a 1 k1 k a a 1 710 5 89 a 2 a g A k 1n 1 yy 1 a 1 1 a 1 quot n1 a T a 1 Mgtn g a a 7 An k n 2 A z 11 Adjoint Solve of Continuous problem The Derivative of the semilinear form is A T a A B T Tp pcp pT dacdt 0 n at T A A We kT kzo k1VT Vp T VT Vp dacdt 0 9 8T T A A 8w f wT we w1Tp T T mp dwdt 0 9 8T TXTpx139dav l th dAdt n 0 an Adjoint Solve of Continuous problem For the quantity of interest particular to this problem cm 1 T Tx t 0T x t Tm dwelt T Tx t Tm dwelt lim 1 U Q 20Tx t Tew fx t 0 dxdt 9 0 0 2 0 T Q Tx t Tm Tx t dxdt Adjoint Solve of Continuous problem Notice that the strong form of the adjoint formulation is as follows Given the spatially and temporally varying temperature field Tx t find the Lagrange multiplier px t such that P0p v o ltkltTgtvpgt 1 mVT w wltmgt p 2 ltT6gt p T Ta M Temp in r given the Cauchy boundary condition kTVpnhp0 ona and the terminal condition px 739 0 in Q in the classical sense Adjoint Solve of Continuous problem T 8k T BVT Vp dacdt 0 Q ako T 8k 0 Q 1 T 8k 0 2 T 8k 0 Q 3 T 8w 5a 5T Tap d cdt 0 Q 0 T 8w Lag 5T Tap d cdt 0 1 T 8w 5a 5T Tap d cdt 0 Q 2 0TQaa wTBT Tap davdt W3 WQ 20 Adjoint Solve of Continuous problem 1 16 1 ml 891 k T k MA 2 A 2 oz gt A k1n 1 r 2 o 1 691 o To MAquot amp 5 X k 71 At 8y Code Structure GMP Matlab LBIE for Mesh generation hp3D for fully parallel data structures and mesh refinement Petsc for parallel robust nonlinear equation solvers Matlab for optimization Dual Solution um um Dual Solution Dual Solution Dual Solution Dual Solution Dual Solution Dual Solution Dual Solution m Dm mm 7 LAnr Dnum Dual Solution Dual Solution Dual Solution Dual Solution LAnr Dnum Dual Solution Unr llnulvrr m Dm mm Dual Solution Dual Solution m Dm mm Dual Solution Dual Solution m Ununrr m Dm mm Dual Solution m Ununrr m Dm mm Dual Solution m Ununrr m Dm mm 1 r nunqu Lw mum Dual Solution m Ununrr Lw mum Verification Problem Allmanan Linux Amman mm 5 mman Verification a Problem Allmanan Linux Amman mm H nunnnwn Verification Problem n a asnnnw Allmanan Linux Amman mm Verification Problem x snunnwn Allmanan Linux Amman mm Quicksort again David Kitchin Adrian Quark Jayadev Misra Department of Computer Science University of Texas at Austin http0rccsresutexasedu Describe Quicksort using 0 Recursion nicely done in Functional programming 0 Mutable Data Structure nicely done in Imperative programming 0 Concurrency Orc an Orchestration Theory 0 Site Basic service component 0 Concurrency combinators for integrating sites 0 Theory includes nothing other than the combinators N0 notion of data type thread process channel synchronization Sites 0 A site is called like a procedure with parameters 0 Site returns at most one value 0 The value is published Site calls are strict Examples of Sites 7ampampH lt println random Prompt Email Ref Semaphore Channel Database Timer External Services Google Search MySpace CNN Any Java Class instance Sites that create sites MakeSemaphore MakeCharmel Overview of Dre 0 Orc program has o a set of de nitions 0 a goal expression over sites and combinators o The goal expression is executed Its execution o calls sites o publishes values Structure of Orc Expression 0 Simple just a site call CNAd Publishes the value returned by the site 0 Composition of two Orc expressions Structure of Orc Expression 0 Simple just a site call CNAd Publishes the value returned by the site 0 Composition of two Orc expressions do f and g in parallel f l g Symmetric composition Structure of Orc Expression 0 Simple just a site call CNAd Publishes the value returned by the site 0 Composition of two Orc expressions do f and g in parallel f l g Symmetric composition for all x from f do g f gtxgt g Sequential composition Structure of Orc Expression 0 Simple just a site call CNAd Publishes the value returned by the site 0 Composition of two Orc expressions do f and g in parallel f l g Symmetric composition for all x from f do g f gtxgt g Sequential composition for some x from g do f f ltxlt g Pruning Examples 0 CNNd lBBCd Calls CNN and BBC simultaneously Publishes up to two values 0 CNNd l BBCd gtxgt Emailaddressx Publishes up to two values from Email 0 Emailaddressx ltxlt CNNd l BBCd Publishes at most one value from Email Some Fundamental Sites 0 z39fb boolean 17 returns a signal if b is true remains silent if b is false 0 Rtimert integer t t 2 0 returns a signal ttime units later 0 stop never responds Same as if false 0 signal returns a signal immediately Same as if true Publish a signal at every time unit def metronome signal l Rtimerl gtgt metronome Laws Based on Kleene Algebra Zero and i Commutativity of i Associativity of i Idempotence of NO Associativity of gtgt Left zero of gtgt Right zero of gtgt NO Left unit of gtgt Right unit of gtgt Left DistributiVity of gtgt over NO Right DistributiVity of gtgt over i fistopf figgf fighfgih fiff fgtgtggtgthfgtgt ggtgt h stop gtgt f stop f gtgt stop stop Signalgtgtff fgtxgt letx f fgtgtghfgtgtgfgtgth figgtgthfgtgthggtgth Additional Laws Distiibutivity over gtgt if gis xfree f gtgtg ltxlt hf ltxlt h gtgt g Distiibutivity over i if gis xfree f ig ltxlthf ltxlth g Distiibutivity over ltlt if gis yfree f ltxlt g ltylt h f ltylt h ltxlt g Elimination of where if f is xfree for site M ltxlt M f i M gtgt stop Operational semantics of Orc Traces of an expression Special treatment for unbound variables Ordering of expressions based on subset ordering over traces Congruence Combinators are monotonic and continuous Holds in the timed model too Encoding To compute 1 2 3 add1x ltxlt add23 Functional Core Language Data Types Number Boolean String with usual operators Conditional Expression if E then F else G Data structures Tuple and List Pattern Matching Function De nition Closure Variable Binding Silent expression val x 1 2 val y x x val z xO expression is silent val u if 0 lt 5 then 0 else 2 Example Fibonacci numbers def H0 11 def Hn val x7y Hn 71 wHy def Fibn val x7 7 Hn 7 Goal expression Fib 5 Translating Functional Core to Pure Orc Operators to Site calls 1 2 3 t0 addlx ltxlt add23 if Ethen F else G ifb gtgt F ln0tb gt c gt ifc gtgt G ltbltE val x Gfollowed by F F ltxlt G Data Structures Patterns Site calls and variable bindings Function De nitions Orc de nitions Corningling with Orc expressions Components of Orc expression could be functional Components of functional expression could be Orc 12lz1 is letx lletCy ltxlt addl2 ltylt add23 Convention whenever expression F appears in a context where a single value is expected convert it to x ltxlt F 1 22l37 is addxy ltxlt l ltylt 2 l3 Example Fibonacci numbers 1 gtX7ygt WWW def Fibn Hn gtx77gt x 7 Goal expression Fib 5 Dice Throw def thr0w random6 1 0 def WW def WM 7 if thr0w thr0w 7 then 1 else 0 aw 71gt 0 uslbnba gtqgt 1 14an gtmgt gtzfgt 0mm gt4gt Mmm gtbgt 1 72an gtdgt L slbnba gtqqgt 0 ltlt WU ltqqult qq o I ltlt qq gtxgt va ltun ltqult WW 0131ltlt CW udxa fap 9m0pum gt x gt 36pr 011401111 fap p91121sum1 AAOILLL equ Forkjoin parallelism Call sites M and N concurrently Return their values as a tuple after both respond u7 v ltult ltvlt N or simply MONO Mutable Structures val r Ref rwrite3 or r 3 rread or r def swapRefsxy x7 gtzgt x y397 gtgt y z Random Permutation val N 20 size of permutation array val ar llArrayArrayNlambdai i Randomize array a of size n n 2 1 def randomize1 signal def randomizen randomn gtkgt swapRefsarn 7 17 ark gtgt randomizen 7 1 randomize N Binary Search Tree Pointer Manipulation def searchkey return true or false searchstartkey gt77 77qgt q 7 null def insertkey true if value was inserted false if it was there searchstartkey gtp7 d qgt if q null then Ref gtrgt r key7 null7 null gtgt updatep7 d r gtgt true else false def delete key Semaphore val s Semaphore 2 s is a semaphore with initial value 2 sacquire srelease Rendezvous val s Semaphore0 val t Semaphore0 def send trelease gtgt sacquire def receive tacquire gtgt srelease nparty Rendezvous using 2n 7 1 semaphores ReadersWriters val req Buffero val cb Counter def reqget gtbsgt gtgt cbinc gtgt srelease gtgt if b gtgt cb0nZer0 gtgt cbinc gtgt srelease gtgt cb0nZer0 gtgt def startb val s Semaphore0 reqputbs gtgt sacquire def quit cbdec Scan swap over array a def lri ifi ltt A az 17 then lrz39 1 elsei def rli if ai gt17 then rli 7 1 elsei def swapij ai7 gtzgt ai a0 gtgt a39 z Partition def partpst def lri if i ltt A az 17 then lrz39 1 elsei def rli if ai gt17 then rli 7 1 else i lrsrlt gts t gt ifs1ltt gtgt s39waps7 t gtgt partps1t71 ifs 1 t gtgt swaps 7 t gtgt s z fs 1gtt gtgtt Returns m where S am p am1atgtp Sorting def sortst if s 2 tthen signal else partas7s1t gtmgt swammvs gtgt sortsm 7 1s0rtm 1t gtgt signal sort07 alength 7 1 Putting the Pieces together def quicksorta def swapxy ax7 gtzgt ax ay7 gtgt ay 2 def partpst def lri i i ltt A az 17 then lrz39 1 elsei def rli ifai gt17 then rli 7 1 elsei lrsrlt gts7tgt i s1ltt gtgt swapst gtgt partps1t71 ifs1t gtgt swapSt gtgt s ifs 1gtt gtgtt def sortst if s 2 tthen signal else partas7s 17t gtmgt swapms gtgt sorts7 m 7 1s0rtm 17 t gtgt signal sort0alength 7 1 Remarks and Proof outline Concurrency Without locks sortm7 n sorts the segment does not touch items outside the segment Then sorts7 m 7 1 and sortm 17 t are noninterfering partltp7 s7 t does not modify any value outside this segment May read values
Are you sure you want to buy this material for
You're already Subscribed!
Looks like you've already subscribed to StudySoup, you won't need to purchase another subscription to get this material. To access this material simply click 'View Full Document'