@inproceedings{10190, abstract = {The verification of concurrent programs remains an open challenge, as thread interaction has to be accounted for, which leads to state-space explosion. Stateless model checking battles this problem by exploring traces rather than states of the program. As there are exponentially many traces, dynamic partial-order reduction (DPOR) techniques are used to partition the trace space into equivalence classes, and explore a few representatives from each class. The standard equivalence that underlies most DPOR techniques is the happens-before equivalence, however recent works have spawned a vivid interest towards coarser equivalences. The efficiency of such approaches is a product of two parameters: (i) the size of the partitioning induced by the equivalence, and (ii) the time spent by the exploration algorithm in each class of the partitioning. In this work, we present a new equivalence, called value-happens-before and show that it has two appealing features. First, value-happens-before is always at least as coarse as the happens-before equivalence, and can be even exponentially coarser. Second, the value-happens-before partitioning is efficiently explorable when the number of threads is bounded. We present an algorithm called value-centric DPOR (VCDPOR), which explores the underlying partitioning using polynomial time per class. Finally, we perform an experimental evaluation of VCDPOR on various benchmarks, and compare it against other state-of-the-art approaches. Our results show that value-happens-before typically induces a significant reduction in the size of the underlying partitioning, which leads to a considerable reduction in the running time for exploring the whole partitioning.}, author = {Chatterjee, Krishnendu and Pavlogiannis, Andreas and Toman, Viktor}, booktitle = {Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications}, issn = {2475-1421}, keywords = {safety, risk, reliability and quality, software}, location = {Athens, Greece}, publisher = {ACM}, title = {{Value-centric dynamic partial order reduction}}, doi = {10.1145/3360550}, volume = {3}, year = {2019}, } @inproceedings{6673, abstract = {Several classic problems in graph processing and computational geometry are solved via incremental algorithms, which split computation into a series of small tasks acting on shared state, which gets updated progressively. While the sequential variant of such algorithms usually specifies a fixed (but sometimes random) order in which the tasks should be performed, a standard approach to parallelizing such algorithms is to relax this constraint to allow for out-of-order parallel execution. This is the case for parallel implementations of Dijkstra's single-source shortest-paths (SSSP) algorithm, and for parallel Delaunay mesh triangulation. While many software frameworks parallelize incremental computation in this way, it is still not well understood whether this relaxed ordering approach can still provide any complexity guarantees. In this paper, we address this problem, and analyze the efficiency guarantees provided by a range of incremental algorithms when parallelized via relaxed schedulers. We show that, for algorithms such as Delaunay mesh triangulation and sorting by insertion, schedulers with a maximum relaxation factor of k in terms of the maximum priority inversion allowed will introduce a maximum amount of wasted work of O(łog n poly(k)), where n is the number of tasks to be executed. For SSSP, we show that the additional work is O(poly(k), dmax / wmin), where dmax is the maximum distance between two nodes, and wmin is the minimum such distance. In practical settings where n >> k, this suggests that the overheads of relaxation will be outweighed by the improved scalability of the relaxed scheduler. On the negative side, we provide lower bounds showing that certain algorithms will inherently incur a non-trivial amount of wasted work due to scheduler relaxation, even for relatively benign relaxed schedulers.}, author = {Alistarh, Dan-Adrian and Nadiradze, Giorgi and Koval, Nikita}, booktitle = {31st ACM Symposium on Parallelism in Algorithms and Architectures}, isbn = {9781450361842}, location = {Phoenix, AZ, United States}, pages = {145--154}, publisher = {ACM Press}, title = {{Efficiency guarantees for parallel incremental algorithms under relaxed schedulers}}, doi = {10.1145/3323165.3323201}, year = {2019}, } @article{7398, abstract = {Transporters of the solute carrier 6 (SLC6) family translocate their cognate substrate together with Na+ and Cl−. Detailed kinetic models exist for the transporters of GABA (GAT1/SLC6A1) and the monoamines dopamine (DAT/SLC6A3) and serotonin (SERT/SLC6A4). Here, we posited that the transport cycle of individual SLC6 transporters reflects the physiological requirements they operate under. We tested this hypothesis by analyzing the transport cycle of glycine transporter 1 (GlyT1/SLC6A9) and glycine transporter 2 (GlyT2/SLC6A5). GlyT2 is the only SLC6 family member known to translocate glycine, Na+, and Cl− in a 1:3:1 stoichiometry. We analyzed partial reactions in real time by electrophysiological recordings. Contrary to monoamine transporters, both GlyTs were found to have a high transport capacity driven by rapid return of the empty transporter after release of Cl− on the intracellular side. Rapid cycling of both GlyTs was further supported by highly cooperative binding of cosubstrate ions and substrate such that their forward transport mode was maintained even under conditions of elevated intracellular Na+ or Cl−. The most important differences in the transport cycle of GlyT1 and GlyT2 arose from the kinetics of charge movement and the resulting voltage-dependent rate-limiting reactions: the kinetics of GlyT1 were governed by transition of the substrate-bound transporter from outward- to inward-facing conformations, whereas the kinetics of GlyT2 were governed by Na+ binding (or a related conformational change). Kinetic modeling showed that the kinetics of GlyT1 are ideally suited for supplying the extracellular glycine levels required for NMDA receptor activation.}, author = {Erdem, Fatma Asli and Ilic, Marija and Koppensteiner, Peter and Gołacki, Jakub and Lubec, Gert and Freissmuth, Michael and Sandtner, Walter}, issn = {1540-7748}, journal = {The Journal of General Physiology}, number = {8}, pages = {1035--1050}, publisher = {Rockefeller University Press}, title = {{A comparison of the transport kinetics of glycine transporter 1 and glycine transporter 2}}, doi = {10.1085/jgp.201912318}, volume = {151}, year = {2019}, } @article{7395, abstract = {The mitochondrial electron transport chain complexes are organized into supercomplexes (SCs) of defined stoichiometry, which have been proposed to regulate electron flux via substrate channeling. We demonstrate that CoQ trapping in the isolated SC I+III2 limits complex (C)I turnover, arguing against channeling. The SC structure, resolved at up to 3.8 Å in four distinct states, suggests that CoQ oxidation may be rate limiting because of unequal access of CoQ to the active sites of CIII2. CI shows a transition between “closed” and “open” conformations, accompanied by the striking rotation of a key transmembrane helix. Furthermore, the state of CI affects the conformational flexibility within CIII2, demonstrating crosstalk between the enzymes. CoQ was identified at only three of the four binding sites in CIII2, suggesting that interaction with CI disrupts CIII2 symmetry in a functionally relevant manner. Together, these observations indicate a more nuanced functional role for the SCs.}, author = {Letts, James A and Fiedorczuk, Karol and Degliesposti, Gianluca and Skehel, Mark and Sazanov, Leonid A}, issn = {1097-2765}, journal = {Molecular Cell}, number = {6}, pages = {1131--1146.e6}, publisher = {Cell Press}, title = {{Structures of respiratory supercomplex I+III2 reveal functional and conformational crosstalk}}, doi = {10.1016/j.molcel.2019.07.022}, volume = {75}, year = {2019}, } @article{7405, abstract = {Biophysical modeling of neuronal networks helps to integrate and interpret rapidly growing and disparate experimental datasets at multiple scales. The NetPyNE tool (www.netpyne.org) provides both programmatic and graphical interfaces to develop data-driven multiscale network models in NEURON. NetPyNE clearly separates model parameters from implementation code. Users provide specifications at a high level via a standardized declarative language, for example connectivity rules, to create millions of cell-to-cell connections. NetPyNE then enables users to generate the NEURON network, run efficiently parallelized simulations, optimize and explore network parameters through automated batch runs, and use built-in functions for visualization and analysis – connectivity matrices, voltage traces, spike raster plots, local field potentials, and information theoretic measures. NetPyNE also facilitates model sharing by exporting and importing standardized formats (NeuroML and SONATA). NetPyNE is already being used to teach computational neuroscience students and by modelers to investigate brain regions and phenomena.}, author = {Dura-Bernal, Salvador and Suter, Benjamin and Gleeson, Padraig and Cantarelli, Matteo and Quintana, Adrian and Rodriguez, Facundo and Kedziora, David J and Chadderdon, George L and Kerr, Cliff C and Neymotin, Samuel A and McDougal, Robert A and Hines, Michael and Shepherd, Gordon MG and Lytton, William W}, issn = {2050-084X}, journal = {eLife}, publisher = {eLife Sciences Publications}, title = {{NetPyNE, a tool for data-driven multiscale modeling of brain circuits}}, doi = {10.7554/elife.44494}, volume = {8}, year = {2019}, }