@article{10391, abstract = {We use numerical simulations to show how a fully flexible filament binding to a deformable cylindrical surface may acquire a macroscopic persistence length and a helical conformation. This is a result of the nontrivial elastic response to deformations of elastic sheets. We find that the filament’s helical pitch is completely determined by the mechanical properties of the surface, and can be easily tuned by varying the surface stretching rigidity. We propose simple scaling arguments to understand the physical mechanism behind this phenomenon and present a phase diagram indicating under what conditions one should expect a fully flexible chain to behave as a helical semiflexible filament. Finally, we discuss the implications of our results.}, author = {Šarić, Anđela and Pàmies, Josep C. and Cacciuto, Angelo}, issn = {1079-7114}, journal = {Physical Review Letters}, keywords = {general physics and astronomy}, number = {22}, publisher = {American Physical Society}, title = {{Effective elasticity of a flexible filament bound to a deformable cylindrical surface}}, doi = {10.1103/physrevlett.104.226101}, volume = {104}, year = {2010}, } @inproceedings{1042, abstract = {Recent years have seen tremendous progress in the field of cold and ultracold molecules. A central goal in the field is currently the realization of stable rovibronic ground-state molecular samples in the regime of quantum degeneracy, e.g. in the form of molecular Bose-Einstein condensates, molecular degenerate Fermi gases, or, when an optical lattice is present, molecular Mott-insulator phases. However, molecular samples are not readily cooled to the extremely low temperatures at which quantum degeneracy occurs. In particular, laser cooling, the \'workhorse\' for the field of atomic quantum gases, is generally not applicable to molecular samples. Here we take an important step beyond previous work1 and provide details on the realization of an ultracold quantum gas of ground-state dimer molecules trapped in an optical lattice as recently reported in Ref. 2. We demonstrate full control over all internal and external quantum degrees of freedom for the ground-state molecules by deterministically preparing the molecules in a single quantum state, i.e. in a specific hyperfine sublevel of the rovibronic ground state, while the molecules are trapped in the motional ground state of the individual lattice wells. We circumvent the problem of cooling by associating weakly-bound molecules out of a zero-temperature atomic Mott-insulator state and by transferring these to the absolute ground state in a four-photon STIRAP process. Our preparation procedure directly leads to a long-lived, lattice-trapped molecular many-body state, which we expect to form the platform for many of the envisioned future experiments with molecular quantum gases, e.g. on precision molecular spectroscopy, quantum information science, and dipolar quantum systems.}, author = {Danzl, Johann G and Mark, Manfred and Haller, Elmar and Gustavsson, Mattias and Hart, Russell and Nägerl, Hanns}, pages = {256 -- 269}, publisher = {World Scientific Publishing}, title = {{Production of a quantum gas of rovibronic ground-state molecules in an optical lattice}}, doi = {10.1142/9789814282345_0024}, year = {2010}, } @article{1044, abstract = {Control over all internal and external degrees of freedom of molecules at the level of single quantum states will enable a series of fundamental studies in physics and chemistry1,2. In particular, samples of ground-state molecules at ultralow temperatures and high number densities will facilitate new quantum-gas studies3 and future applications in quantum information science4. However, high phase-space densities for molecular samples are not readily attainable because efficient cooling techniques such as laser cooling are lacking. Here we produce an ultracold and dense sample of molecules in a single hyperfine level of the rovibronic ground state with each molecule individually trapped in the motional ground state of an optical lattice well. Starting from a zero-temperature atomic Mott-insulator state with optimized double-site occupancy6, weakly bound dimer molecules are efficiently associated on a Feshbach resonance7 and subsequently transferred to the rovibronic ground state by a stimulated four-photon process with >50% efficiency. The molecules are trapped in the lattice and have a lifetime of 8 s. Our results present a crucial step towards Bose-Einstein condensation of ground-state molecules and, when suitably generalized to polar heteronuclear molecules, the realization of dipolar quantum-gas phases in optical lattices8-10.}, author = {Danzl, Johann G and Mark, Manfred and Haller, Elmar and Gustavsson, Mattias and Hart, Russell and Aldegunde, Jesus and Hutson, Jeremy and Nägerl, Hanns}, journal = {Nature Physics}, number = {4}, pages = {265 -- 270}, publisher = {Nature Publishing Group}, title = {{An ultracold high-density sample of rovibronic ground-state molecules in an optical lattice}}, doi = {10.1038/nphys1533}, volume = {6}, year = {2010}, } @article{1045, abstract = {We report on the observation of confinement-induced resonances in strongly interacting quantum-gas systems with tunable interactions for one- and two-dimensional geometry. Atom-atom scattering is substantially modified when the s-wave scattering length approaches the length scale associated with the tight transversal confinement, leading to characteristic loss and heating signatures. Upon introducing an anisotropy for the transversal confinement we observe a splitting of the confinement-induced resonance. With increasing anisotropy additional resonances appear. In the limit of a two-dimensional system we find that one resonance persists.}, author = {Haller, Elmar and Mark, Manfred and Hart, Russell and Danzl, Johann G and Reichsöllner, Lukas and Melezhik, Vladimir and Schmelcher, Peter and Nägerl, Hanns}, journal = {Physical Review Letters}, number = {15}, publisher = {American Physical Society}, title = {{Confinement-induced resonances in low-dimensional quantum systems}}, doi = {10.1103/PhysRevLett.104.153203}, volume = {104}, year = {2010}, } @article{1046, abstract = {The phenomenon of matter-wave interference lies at the heart of quantum physics. It has been observed in various contexts in the limit of non-interacting particles as a single-particle effect. Here we observe and control matter-wave interference whose evolution is driven by interparticle interactions. In a multi-path matter-wave interferometer, the macroscopic manybody wave function of an interacting atomic Bose-Einstein condensate develops a regular interference pattern, allowing us to detect and directly visualize the effect of interaction-induced phase shifts. We demonstrate control over the phase evolution by inhibiting interaction-induced dephasing and by refocusing a dephased macroscopic matter wave in a spin-echo-type experiment. Our results show that interactions in a many-body system lead to a surprisingly coherent evolution, possibly enabling narrow-band and high-brightness matterwave interferometers based on atom lasers.}, author = {Gustavsson, Mattias and Haller, Elmar and Mark, Manfred and Danzl, Johann G and Hart, Russell and Daley, Andrew and Nägerl, Hanns}, journal = {New Journal of Physics}, publisher = {IOP Publishing Ltd.}, title = {{Interference of interacting matter waves}}, doi = {10.1088/1367-2630/12/6/065029}, volume = {12}, year = {2010}, } @article{1047, abstract = {Particles in a perfect lattice potential perform Bloch oscillations when subject to a constant force, leading to localization and preventing conductivity. For a weakly interacting Bose-Einstein condensate of Cs atoms, we observe giant center-of-mass oscillations in position space with a displacement across hundreds of lattice sites when we add a periodic modulation to the force near the Bloch frequency. We study the dependence of these "super" Bloch oscillations on lattice depth, modulation amplitude, and modulation frequency and show that they provide a means to induce linear transport in a dissipation-free lattice.}, author = {Haller, Elmar and Hart, Russell and Mark, Manfred and Danzl, Johann G and Reichsöllner, Lukas and Nägerl, Hanns}, journal = {Physical Review Letters}, number = {20}, publisher = {American Physical Society}, title = {{Inducing transport in a dissipation-free lattice with super bloch oscillations}}, doi = {10.1103/PhysRevLett.104.200403}, volume = {104}, year = {2010}, } @article{1049, abstract = {Quantum many-body systems can have phase transitions even at zero temperature; fluctuations arising from Heisenbergĝ€™s uncertainty principle, as opposed to thermal effects, drive the system from one phase to another. Typically, during the transition the relative strength of two competing terms in the systemĝ€™s Hamiltonian changes across a finite critical value. A well-known example is the Mottĝ€" Hubbard quantum phase transition from a superfluid to an insulating phase, which has been observed for weakly interacting bosonic atomic gases. However, for strongly interacting quantum systems confined to lower-dimensional geometry, a novel type of quantum phase transition may be induced and driven by an arbitrarily weak perturbation to the Hamiltonian. Here we observe such an effectĝ€"the sineĝ€"Gordon quantum phase transition from a superfluid Luttinger liquid to a Mott insulatorĝ€ "in a one-dimensional quantum gas of bosonic caesium atoms with tunable interactions. For sufficiently strong interactions, the transition is induced by adding an arbitrarily weak optical lattice commensurate with the atomic granularity, which leads to immediate pinning of the atoms. We map out the phase diagram and find that our measurements in the strongly interacting regime agree well with a quantum field description based on the exactly solvable sineĝ€"Gordon model. We trace the phase boundary all the way to the weakly interacting regime, where we find good agreement with the predictions of the one-dimensional Boseĝ€"Hubbard model. Our results open up the experimental study of quantum phase transitions, criticality and transport phenomena beyond Hubbard-type models in the context of ultracold gases.}, author = {Haller, Elmar and Hart, Russell and Mark, Manfred and Danzl, Johann G and Reichsöllner, Lukas and Gustavsson, Mattias and Dalmonte, Marcello and Pupillo, Guido and Nägerl, Hanns}, journal = {Nature}, number = {7306}, pages = {597 -- 600}, publisher = {Nature Publishing Group}, title = {{Pinning quantum phase transition for a Luttinger liquid of strongly interacting bosons}}, doi = {10.1038/nature09259}, volume = {466}, year = {2010}, } @inproceedings{11797, abstract = {Inspired by online ad allocation, we study online stochastic packing integer programs from theoretical and practical standpoints. We first present a near-optimal online algorithm for a general class of packing integer programs which model various online resource allocation problems including online variants of routing, ad allocations, generalized assignment, and combinatorial auctions. As our main theoretical result, we prove that a simple dual training-based algorithm achieves a (1 − o(1))-approximation guarantee in the random order stochastic model. This is a significant improvement over logarithmic or constant-factor approximations for the adversarial variants of the same problems (e.g. factor 1−1𝑒 for online ad allocation, and log(m) for online routing). We then focus on the online display ad allocation problem and study the efficiency and fairness of various training-based and online allocation algorithms on data sets collected from real-life display ad allocation system. Our experimental evaluation confirms the effectiveness of training-based algorithms on real data sets, and also indicates an intrinsic trade-off between fairness and efficiency.}, author = {Feldman, Jon and Henzinger, Monika H and Korula, Nitish and Mirrokni, Vahab S. and Stein, Cliff}, booktitle = {18th Annual European Symposium on Algorithms}, isbn = {3642157742}, issn = {1611-3349}, location = {Liverpool, United Kingdom}, pages = {182–194}, publisher = {Springer Nature}, title = {{Online stochastic packing applied to display ad allocation}}, doi = {10.1007/978-3-642-15775-2_16}, volume = {6346}, year = {2010}, } @inproceedings{11798, abstract = {Starting with two models fifty years ago, the discrete marriage game [1] and the continuous assignment game [2], the study of stable matchings has evolved into a rich theory with applications in many areas. Most notably, it has lead to a number of truthful mechanisms that have seen a recent rejuvenation in the context of sponsored search. In this paper we survey the history of these problems and provide several links to ongoing research in the field.}, author = {Dütting, Paul and Henzinger, Monika H}, booktitle = {7th International Conference on Algorithms and Complexity}, isbn = {9783642130724}, issn = {1611-3349}, location = {Rome, Italy}, pages = {6–12}, publisher = {Springer Nature}, title = {{Mechanisms for the marriage and the assignment game}}, doi = {10.1007/978-3-642-13073-1_2}, volume = {6078}, year = {2010}, } @inproceedings{11838, abstract = {Two-sided matching markets play a prominent role in economic theory. A prime example of such a market is the sponsored search market where $n$ advertisers compete for the assignment of one of $k$ sponsored search results, also known as ``slots'', for certain keywords they are interested in. Here, as in other markets of that kind, market equilibria correspond to stable matchings. In this paper, we show how to modify Kuhn's Hungarian Method (Kuhn, 1955) so that it finds an optimal stable matching between advertisers and advertising slots in settings with generalized linear utilities, per-bidder-item reserve prices, and per-bidder-item maximum prices. The only algorithm for this problem presented so far (Aggarwal et al., 2009) requires the market to be in ''general position''. We do not make this assumption.}, author = {Dütting, Paul and Henzinger, Monika H and Weber, Ingmar}, booktitle = {27th International Symposium on Theoretical Aspects of Computer Science}, isbn = {978-3-939897-16-3}, issn = {1868-8969}, location = {Nancy, France}, pages = {287--298}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik}, title = {{Sponsored search, market equilibria, and the Hungarian Method}}, doi = {10.4230/LIPICS.STACS.2010.2463}, volume = {5}, year = {2010}, } @inproceedings{11863, abstract = {Suppose you buy a new laptop and, simply because you like it so much, you recommend it to friends, encouraging them to purchase it as well. What would be an adequate price for the vendor of the laptop to pay for your recommendation? Personal recommendations like this are of considerable commercial interest, but unlike in sponsored search auctions there can be no truthful prices. Despite this "lack of truthfulness" the vendor of the product might still decide to pay you for recommendation e.g. because she wants to (i) provide you with an additional incentive to actually recommend her or to (ii) increase your satisfaction and/or brand loyalty. This leads us to investigate a pricing scheme based on the Shapley value [5] that satisfies certain "axioms of fairness". We find that it is vulnerable to manipulations and show how to overcome these difficulties using the anonymity-proof Shapley value of [4].}, author = {Dütting, Paul and Henzinger, Monika H and Weber, Ingmar}, booktitle = {Proceedings of the 19th international conference on World wide web }, isbn = {9781605587998}, location = {Raleigh, NC, United States}, pages = {1085--1086}, publisher = {Association for Computing Machinery}, title = {{How much is your personal recommendation worth?}}, doi = {10.1145/1772690.1772816}, year = {2010}, } @article{11885, abstract = {Over the last years the h-index has gained popularity as a measure for comparing the impact of scientists. We investigate if ranking according to the h-index is stable with respect to (i) different choices of citation databases, (ii) normalizing citation counts by the number of authors or by removing self-citations, (iii) small amounts of noise created by randomly removing citations or publications and (iv) small changes in the definition of the index. In experiments for 5,283 computer scientists and 1,354 physicists we show that although the ranking of the h-index is stable under most of these changes, it is unstable when different databases are used. Therefore, comparisons based on the h-index should only be trusted when the rankings of multiple citation databases agree.}, author = {Henzinger, Monika H and Suñol, Jacob and Weber, Ingmar}, issn = {1588-2861}, journal = {Scientometrics}, number = {2}, pages = {465--479}, publisher = {Springer Nature}, title = {{The stability of the h-index}}, doi = {10.1007/s11192-009-0098-7}, volume = {84}, year = {2010}, } @article{11975, abstract = {A new method was developed for the quantitative analysis of steryl glycosides in biodiesel (fatty acid methyl esters). This method is much more sensitive than existing methods and has minimum limits of quantification of 50 μg/kg, compared to previously published minimum limits of quantification of about 15 mg/kg. The analysis is based on gas chromatography–mass spectroscopy determination of simple pre-treated and silylated samples via single ion monitoring at 147, 204, 217 m/z, which are specific ions for the silylated sugar moiety. Quantification was carried out using cholesteryl β-d-glucopyranoside as internal standard. The modified synthesis and purification of the internal standard is also presented as well as the characterization by NMR and mass spectroscopy. The advantage of the method compared with other approaches is the simplified sample preparation avoiding extra pre-treatment steps coupled with complete derivatization of the sugar hydroxyl groups by using N,O-bis(trimethylsilyl)acetamide with 5% trimethylchlorosilane as derivatization reagent. On the given conditions high recovery rates ≥89% can be obtained. Evaluation of lab specific variance and intermediate precision underline the robustness of the method which will be further assessed by Round robin tests.}, author = {Pieber, Bartholomäus and Schober, Sigurd and Goebl, Christoph and Mittelbach, Martin}, issn = {0021-9673}, journal = {Journal of Chromatography A}, number = {42}, pages = {6555--6561}, publisher = {Elsevier}, title = {{Novel sensitive determination of steryl glycosides in biodiesel by gas chromatography-mass spectroscopy}}, doi = {10.1016/j.chroma.2010.08.006}, volume = {1217}, year = {2010}, } @article{12199, abstract = {The four microsporangia of the flowering plant anther develop from archesporial cells in the L2 of the primordium. Within each microsporangium, developing microsporocytes are surrounded by concentric monolayers of tapetal, middle layer and endothecial cells. How this intricate array of tissues, each containing relatively few cells, is established in an organ possessing no formal meristems is poorly understood. We describe here the pivotal role of the LRR receptor kinase EXCESS MICROSPOROCYTES 1 (EMS1) in forming the monolayer of tapetal nurse cells in Arabidopsis. Unusually for plants, tapetal cells are specified very early in development, and are subsequently stimulated to proliferate by a receptor-like kinase (RLK) complex that includes EMS1. Mutations in members of this EMS1 signalling complex and its putative ligand result in male-sterile plants in which tapetal initials fail to proliferate. Surprisingly, these cells continue to develop, isolated at the locular periphery. Mutant and wild-type microsporangia expand at similar rates and the ‘tapetal’ space at the periphery of mutant locules becomes occupied by microsporocytes. However, induction of late expression of EMS1 in the few tapetal initials in ems1 plants results in their proliferation to generate a functional tapetum, and this proliferation suppresses microsporocyte number. Our experiments also show that integrity of the tapetal monolayer is crucial for the maintenance of the polarity of divisions within it. This unexpected autonomy of the tapetal ‘lineage’ is discussed in the context of tissue development in complex plant organs, where constancy in size, shape and cell number is crucial.}, author = {Feng, Xiaoqi and Dickinson, Hugh G.}, issn = {1477-9129}, journal = {Development}, keywords = {Developmental Biology, Molecular Biology, Anther Tapetum, Arabidopsis, Cell Fate Establishment, EMS1, Reproductive Cell Lineage}, number = {14}, pages = {2409--2416}, publisher = {The Company of Biologists}, title = {{Tapetal cell fate, lineage and proliferation in the Arabidopsis anther}}, doi = {10.1242/dev.049320}, volume = {137}, year = {2010}, } @article{12200, abstract = {Key steps in the evolution of the angiosperm anther include the patterning of the concentrically organized microsporangium and the incorporation of four such microsporangia into a leaf-like structure. Mutant studies in the model plant Arabidopsis thaliana are leading to an increasingly accurate picture of (i) the cell lineages culminating in the different cell types present in the microsporangium (the microsporocytes, the tapetum, and the middle and endothecial layers), and (ii) some of the genes responsible for specifying their fates. However, the processes that confer polarity on the developing anther and position the microsporangia within it remain unclear. Certainly, data from a range of experimental strategies suggest that hormones play a central role in establishing polarity and the patterning of the anther initial, and may be responsible for locating the microsporangia. But the fact that microsporangia were originally positioned externally suggests that their development is likely to be autonomous, perhaps with the reproductive cells generating signals controlling the growth and division of the investing anther epidermis. These possibilities are discussed in the context of the expression of genes which initiate and maintain male and female reproductive development, and in the perspective of our current views of anther evolution.}, author = {Feng, Xiaoqi and Dickinson, Hugh G.}, issn = {0300-5127}, journal = {Biochemical Society Transactions}, keywords = {Biochemistry, Anther Development, Arabidopsis, Cell Fate, Microsporangium, Polarity, Receptor Kinase}, number = {2}, pages = {571--576}, publisher = {Portland Press Ltd.}, title = {{Cell–cell interactions during patterning of the Arabidopsis anther}}, doi = {10.1042/bst0380571}, volume = {38}, year = {2010}, } @article{12653, abstract = {Daily streamflow from stations close to five Swiss glaciers is analyzed for trends with the Mann-Kendall test. We consider a common period of record (1974–2004) and longer periods based on data availability. The trend statistical significance is tested on annual and seasonal bases. We also examine changes in precipitation, temperature, and snow cover characteristics. Highly glacierized basins show statistically significant positive trends in annual streamflow caused by increasing streamflow in spring and summer. Trends are more numerous and stronger at lower and mid than at the upper quantiles. The basin characterized by lower glacier coverage, conversely, does not exhibit consistently statistically significant trends. Changes in precipitation are not sufficient to explain the observed streamflow trends. Air temperature sees an increase in mean, minimum, and maximum values at all sites. Variations in the seasonal snow accumulation and ablation process are evident. Solid precipitation is decreasing at all sites and trends may be due to a shift from snowfall into rainfall. Mean snow depth is also decreasing, and its duration is getting shorter because of a decrease in solid precipitation and enhanced melting. Trend magnitude attenuates with longer time series. Contrasting trends are detected for different subperiods in the last 70 years: statistically significant negative trends are observed in the periods 1944–1974 and 1954–1984 for Aletschgletscher, in contrast with the results for the common period. These trends are explained by different rates of ice volume changes, and the sign of trends is clearly related to phases of positive or negative glacier mass balance.}, author = {Pellicciotti, Francesca and Bauder, A. and Parola, M.}, issn = {1944-7973}, journal = {Water Resources Research}, keywords = {Water Science and Technology}, number = {10}, publisher = {American Geophysical Union}, title = {{Effect of glaciers on streamflow trends in the Swiss Alps}}, doi = {10.1029/2009wr009039}, volume = {46}, year = {2010}, } @article{1300, abstract = {Motion vision is a major function of all visual systems, yet the underlying neural mechanisms and circuits are still elusive. In the lamina, the first optic neuropile of Drosophila melanogaster, photoreceptor signals split into five parallel pathways, L1-L5. Here we examine how these pathways contribute to visual motion detection by combining genetic block and reconstitution of neural activity in different lamina cell types with whole-cell recordings from downstream motion-sensitive neurons. We find reduced responses to moving gratings if L1 or L2 is blocked; however, reconstitution of photoreceptor input to only L1 or L2 results in wild-type responses. Thus, the first experiment indicates the necessity of both pathways, whereas the second indicates sufficiency of each single pathway. This contradiction can be explained by electrical coupling between L1 and L2, allowing for activation of both pathways even when only one of them receives photoreceptor input. A fundamental difference between the L1 pathway and the L2 pathway is uncovered when blocking L1 or L2 output while presenting moving edges of positive (ON) or negative (OFF) contrast polarity: blocking L1 eliminates the response to moving ON edges, whereas blocking L2 eliminates the response to moving OFF edges. Thus, similar to the segregation of photoreceptor signals in ON and OFF bipolar cell pathways in the vertebrate retina, photoreceptor signals segregate into ON-L1 and OFF-L2 channels in the lamina of Drosophila.}, author = {Maximilian Jösch and Schnell, Bettina and Raghu, Shamprasad V and Reiff, Dierk F and Borst, Alexander}, journal = {Nature}, number = {7321}, pages = {300 -- 304}, publisher = {Nature Publishing Group}, title = {{ON and off pathways in Drosophila motion vision}}, doi = {10.1038/nature09545}, volume = {468}, year = {2010}, } @article{1301, abstract = {Motion vision is essential for navigating through the environment. Due to its genetic amenability, the fruit fly Drosophila has been serving for a lengthy period as a model organism for studying optomotor behavior as elicited by large-field horizontal motion. However, the neurons underlying the control of this behavior have not been studied in Drosophila so far. Here we report the first whole cell recordings from three cells of the horizontal system (HSN, HSE, and HSS) in the lobula plate of Drosophila. All three HS cells are tuned to large-field horizontal motion in a direction-selective way; they become excited by front-to-back motion and inhibited by back-to-front motion in the ipsilateral field of view. The response properties of HS cells such as contrast and velocity dependence are in accordance with the correlation-type model of motion detection. Neurobiotin injection suggests extensive coupling among ipsilateral HS cells and additional coupling to tangential cells that have their dendrites in the contralateral hemisphere of the brain. This connectivity scheme accounts for the complex layout of their receptive fields and explains their sensitivity both to ipsilateral and to contralateral motion. Thus the main response properties of Drosophila HS cells are strikingly similar to the responses of their counterparts in the blowfly Calliphora, although we found substantial differences with respect to their dendritic structure and connectivity. This long-awaited functional characterization of HS cells in Drosophila provides the basis for the future dissection of optomotor behavior and the underlying neural circuitry by combining genetics, physiology, and behavior.}, author = {Schnell, Bettina and Jösch, Maximilian A and Förstner, Friedrich and Raghu, Shamprasad and Otsuna, Hideo and Ito, Kei and Borst, Alexander and Reiff, Dierk}, issn = {1522-1598}, journal = {Journal of Neurophysiology}, number = {3}, pages = {1646 -- 1657}, publisher = {American Physiological Society}, title = {{Processing of horizontal optic flow in three visual interneurons of the Drosophila brain}}, doi = {10.1152/jn.00950.2009}, volume = {103}, year = {2010}, } @misc{9764, author = {Rosas, Ulises and Barton, Nicholas H and Copsey, Lucy and Barbier De Reuille, Pierre and Coen, Enrico}, publisher = {Public Library of Science}, title = {{Heterosis and the drift load}}, doi = {10.1371/journal.pbio.1000429.s003}, year = {2010}, } @article{3402, abstract = {Model checking transactional memories (TMs) is difficult because of the unbounded number, length, and delay of concurrent transactions, as well as the unbounded size of the memory. We show that, under certain conditions satisfied by most TMs we know of, the model checking problem can be reduced to a finite-state problem, and we illustrate the use of the method by proving the correctness of several TMs, including two-phase locking, DSTM, and TL2. The safety properties we consider include strict serializability and opacity; the liveness properties include obstruction freedom, livelock freedom, and wait freedom. Our main contribution lies in the structure of the proofs, which are largely automated and not restricted to the TMs mentioned above. In a first step we show that every TM that enjoys certain structural properties either violates a requirement on some program with two threads and two shared variables, or satisfies the requirement on all programs. In the second step, we use a model checker to prove the requirement for the TM applied to a most general program with two threads and two variables. In the safety case, the model checker checks language inclusion between two finite-state transition systems, a nondeterministic transition system representing the given TM applied to a most general program, and a deterministic transition system representing a most liberal safe TM applied to the same program. The given TM transition system is nondeterministic because a TM can be used with different contention managers, which resolve conflicts differently. In the liveness case, the model checker analyzes fairness conditions on the given TM transition system.}, author = {Guerraoui, Rachid and Thomas Henzinger and Vasu Singh}, journal = {Distributed Computing}, number = {3}, pages = {129 -- 145}, publisher = {Springer}, title = {{Model checking transactional memories}}, doi = {10.1007/s00446-009-0092-6}, volume = {22}, year = {2010}, }