[{"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","citation":{"ista":"Petrov T, Igler C, Sezgin A, Henzinger TA, Guet CC. 2021. Long lived transients in gene regulation. Theoretical Computer Science. 893, 1–16.","chicago":"Petrov, Tatjana, Claudia Igler, Ali Sezgin, Thomas A Henzinger, and Calin C Guet. “Long Lived Transients in Gene Regulation.” Theoretical Computer Science. Elsevier, 2021. https://doi.org/10.1016/j.tcs.2021.05.023.","apa":"Petrov, T., Igler, C., Sezgin, A., Henzinger, T. A., & Guet, C. C. (2021). Long lived transients in gene regulation. Theoretical Computer Science. Elsevier. https://doi.org/10.1016/j.tcs.2021.05.023","ama":"Petrov T, Igler C, Sezgin A, Henzinger TA, Guet CC. Long lived transients in gene regulation. Theoretical Computer Science. 2021;893:1-16. doi:10.1016/j.tcs.2021.05.023","ieee":"T. Petrov, C. Igler, A. Sezgin, T. A. Henzinger, and C. C. Guet, “Long lived transients in gene regulation,” Theoretical Computer Science, vol. 893. Elsevier, pp. 1–16, 2021.","short":"T. Petrov, C. Igler, A. Sezgin, T.A. Henzinger, C.C. Guet, Theoretical Computer Science 893 (2021) 1–16.","mla":"Petrov, Tatjana, et al. “Long Lived Transients in Gene Regulation.” Theoretical Computer Science, vol. 893, Elsevier, 2021, pp. 1–16, doi:10.1016/j.tcs.2021.05.023."},"title":"Long lived transients in gene regulation","external_id":{"isi":["000710180500002"]},"article_processing_charge":"No","author":[{"last_name":"Petrov","full_name":"Petrov, Tatjana","first_name":"Tatjana"},{"last_name":"Igler","full_name":"Igler, Claudia","first_name":"Claudia","id":"46613666-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Sezgin","full_name":"Sezgin, Ali","id":"4C7638DA-F248-11E8-B48F-1D18A9856A87","first_name":"Ali"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","last_name":"Henzinger","orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A"},{"id":"47F8433E-F248-11E8-B48F-1D18A9856A87","first_name":"Calin C","full_name":"Guet, Calin C","orcid":"0000-0001-6220-2052","last_name":"Guet"}],"project":[{"name":"The Wittgenstein Prize","grant_number":"Z211","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"}],"publication":"Theoretical Computer Science","day":"04","year":"2021","isi":1,"has_accepted_license":"1","date_created":"2021-07-11T22:01:18Z","date_published":"2021-06-04T00:00:00Z","doi":"10.1016/j.tcs.2021.05.023","page":"1-16","acknowledgement":"Tatjana Petrov’s research was supported in part by SNSF Advanced Postdoctoral Mobility Fellowship grant number P300P2 161067, the Ministry of Science, Research and the Arts of the state of Baden-Wurttemberg, and the DFG Centre of Excellence 2117 ‘Centre for the Advanced Study of Collective Behaviour’ (ID: 422037984). Claudia Igler is the recipient of a DOC Fellowship of the Austrian Academy of Sciences. Thomas A. Henzinger’s research was supported in part by the Austrian Science Fund (FWF) under grant Z211-N23 (Wittgenstein Award).","oa":1,"publisher":"Elsevier","quality_controlled":"1","ddc":["004"],"date_updated":"2023-08-10T14:11:19Z","file_date_updated":"2022-05-12T12:13:27Z","department":[{"_id":"ToHe"},{"_id":"CaGu"}],"_id":"9647","status":"public","tmp":{"short":"CC BY-NC-ND (4.0)","name":"Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International (CC BY-NC-ND 4.0)","legal_code_url":"https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode","image":"/images/cc_by_nc_nd.png"},"article_type":"original","type":"journal_article","language":[{"iso":"eng"}],"file":[{"file_name":"2021_TheoreticalComputerScience_Petrov.pdf","date_created":"2022-05-12T12:13:27Z","creator":"dernst","file_size":2566504,"date_updated":"2022-05-12T12:13:27Z","success":1,"checksum":"d3aef34cfb13e53bba4cf44d01680793","file_id":"11364","relation":"main_file","access_level":"open_access","content_type":"application/pdf"}],"publication_status":"published","publication_identifier":{"issn":["0304-3975"]},"volume":893,"oa_version":"Published Version","abstract":[{"lang":"eng","text":"Gene expression is regulated by the set of transcription factors (TFs) that bind to the promoter. The ensuing regulating function is often represented as a combinational logic circuit, where output (gene expression) is determined by current input values (promoter bound TFs) only. However, the simultaneous arrival of TFs is a strong assumption, since transcription and translation of genes introduce intrinsic time delays and there is no global synchronisation among the arrival times of different molecular species at their targets. We present an experimentally implementable genetic circuit with two inputs and one output, which in the presence of small delays in input arrival, exhibits qualitatively distinct population-level phenotypes, over timescales that are longer than typical cell doubling times. From a dynamical systems point of view, these phenotypes represent long-lived transients: although they converge to the same value eventually, they do so after a very long time span. The key feature of this toy model genetic circuit is that, despite having only two inputs and one output, it is regulated by twenty-three distinct DNA-TF configurations, two of which are more stable than others (DNA looped states), one promoting and another blocking the expression of the output gene. Small delays in input arrival time result in a majority of cells in the population quickly reaching the stable state associated with the first input, while exiting of this stable state occurs at a slow timescale. In order to mechanistically model the behaviour of this genetic circuit, we used a rule-based modelling language, and implemented a grid-search to find parameter combinations giving rise to long-lived transients. Our analysis shows that in the absence of feedback, there exist path-dependent gene regulatory mechanisms based on the long timescale of transients. The behaviour of this toy model circuit suggests that gene regulatory networks can exploit event timing to create phenotypes, and it opens the possibility that they could use event timing to memorise events, without regulatory feedback. The model reveals the importance of (i) mechanistically modelling the transitions between the different DNA-TF states, and (ii) employing transient analysis thereof."}],"intvolume":" 893","month":"06","scopus_import":"1"},{"publisher":"Springer Nature","quality_controlled":"1","date_published":"2019-09-17T00:00:00Z","doi":"10.1007/978-3-030-31304-3_9","date_created":"2019-12-04T16:07:50Z","page":"155-187","day":"17","publication":"17th International Conference on Computational Methods in Systems Biology","isi":1,"year":"2019","project":[{"grant_number":"Z211","name":"The Wittgenstein Prize","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"},{"_id":"251EE76E-B435-11E9-9278-68D0E5697425","name":"Design principles underlying genetic switch architecture","grant_number":"24573"}],"title":"Transient memory in gene regulation","author":[{"full_name":"Guet, Calin C","orcid":"0000-0001-6220-2052","last_name":"Guet","first_name":"Calin C","id":"47F8433E-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger"},{"id":"46613666-F248-11E8-B48F-1D18A9856A87","first_name":"Claudia","full_name":"Igler, Claudia","last_name":"Igler"},{"full_name":"Petrov, Tatjana","orcid":"0000-0002-9041-0905","last_name":"Petrov","id":"3D5811FC-F248-11E8-B48F-1D18A9856A87","first_name":"Tatjana"},{"id":"4C7638DA-F248-11E8-B48F-1D18A9856A87","first_name":"Ali","last_name":"Sezgin","full_name":"Sezgin, Ali"}],"external_id":{"isi":["000557875100009"]},"article_processing_charge":"No","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","citation":{"ista":"Guet CC, Henzinger TA, Igler C, Petrov T, Sezgin A. 2019. Transient memory in gene regulation. 17th International Conference on Computational Methods in Systems Biology. CMSB: Computational Methods in Systems Biology, LNCS, vol. 11773, 155–187.","chicago":"Guet, Calin C, Thomas A Henzinger, Claudia Igler, Tatjana Petrov, and Ali Sezgin. “Transient Memory in Gene Regulation.” In 17th International Conference on Computational Methods in Systems Biology, 11773:155–87. Springer Nature, 2019. https://doi.org/10.1007/978-3-030-31304-3_9.","ieee":"C. C. Guet, T. A. Henzinger, C. Igler, T. Petrov, and A. Sezgin, “Transient memory in gene regulation,” in 17th International Conference on Computational Methods in Systems Biology, Trieste, Italy, 2019, vol. 11773, pp. 155–187.","short":"C.C. Guet, T.A. Henzinger, C. Igler, T. Petrov, A. Sezgin, in:, 17th International Conference on Computational Methods in Systems Biology, Springer Nature, 2019, pp. 155–187.","ama":"Guet CC, Henzinger TA, Igler C, Petrov T, Sezgin A. Transient memory in gene regulation. In: 17th International Conference on Computational Methods in Systems Biology. Vol 11773. Springer Nature; 2019:155-187. doi:10.1007/978-3-030-31304-3_9","apa":"Guet, C. C., Henzinger, T. A., Igler, C., Petrov, T., & Sezgin, A. (2019). Transient memory in gene regulation. In 17th International Conference on Computational Methods in Systems Biology (Vol. 11773, pp. 155–187). Trieste, Italy: Springer Nature. https://doi.org/10.1007/978-3-030-31304-3_9","mla":"Guet, Calin C., et al. “Transient Memory in Gene Regulation.” 17th International Conference on Computational Methods in Systems Biology, vol. 11773, Springer Nature, 2019, pp. 155–87, doi:10.1007/978-3-030-31304-3_9."},"month":"09","intvolume":" 11773","alternative_title":["LNCS"],"scopus_import":"1","oa_version":"None","abstract":[{"lang":"eng","text":"The expression of a gene is characterised by its transcription factors and the function processing them. If the transcription factors are not affected by gene products, the regulating function is often represented as a combinational logic circuit, where the outputs (product) are determined by current input values (transcription factors) only, and are hence independent on their relative arrival times. However, the simultaneous arrival of transcription factors (TFs) in genetic circuits is a strong assumption, given that the processes of transcription and translation of a gene into a protein introduce intrinsic time delays and that there is no global synchronisation among the arrival times of different molecular species at molecular targets.\r\n\r\nIn this paper, we construct an experimentally implementable genetic circuit with two inputs and a single output, such that, in presence of small delays in input arrival, the circuit exhibits qualitatively distinct observable phenotypes. In particular, these phenotypes are long lived transients: they all converge to a single value, but so slowly, that they seem stable for an extended time period, longer than typical experiment duration. We used rule-based language to prototype our circuit, and we implemented a search for finding the parameter combinations raising the phenotypes of interest.\r\n\r\nThe behaviour of our prototype circuit has wide implications. First, it suggests that GRNs can exploit event timing to create phenotypes. Second, it opens the possibility that GRNs are using event timing to react to stimuli and memorise events, without explicit feedback in regulation. From the modelling perspective, our prototype circuit demonstrates the critical importance of analysing the transient dynamics at the promoter binding sites of the DNA, before applying rapid equilibrium assumptions."}],"volume":11773,"language":[{"iso":"eng"}],"publication_identifier":{"isbn":["9783030313036","9783030313043"],"eissn":["1611-3349"],"issn":["0302-9743"]},"publication_status":"published","status":"public","type":"conference","conference":{"start_date":"2019-09-18","location":"Trieste, Italy","end_date":"2019-09-20","name":"CMSB: Computational Methods in Systems Biology"},"_id":"7147","department":[{"_id":"CaGu"},{"_id":"ToHe"}],"date_updated":"2023-09-06T11:18:08Z"},{"acknowledgement":"This work has been supported by the National Research Network RiSE on Rigorous Systems Engineering\r\n(Austrian Science Fund (FWF): S11402-N23, S11403-N23, S11404-N23, S11411-N23), a Google\r\nPhD Fellowship, an Erwin Schrödinger Fellowship (Austrian Science Fund (FWF): J3696-N26), EPSRC\r\ngrants EP/H005633/1 and EP/K008528/1, the Vienna Science and Technology Fund (WWTF) trough\r\ngrant PROSEED, the European Research Council (ERC) under grant 267989 (QUAREM) and by the\r\nAustrian Science Fund (FWF) under grant Z211-N23 (Wittgenstein Award).","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","quality_controlled":"1","oa":1,"day":"01","publication":"Leibniz International Proceedings in Informatics","has_accepted_license":"1","year":"2016","doi":"10.4230/LIPIcs.CONCUR.2016.6","date_published":"2016-08-01T00:00:00Z","date_created":"2018-12-11T11:50:07Z","article_number":"6","project":[{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"grant_number":"267989","name":"Quantitative Reactive Modeling","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"Z211","name":"The Wittgenstein Prize"}],"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","citation":{"apa":"Haas, A., Henzinger, T. A., Holzer, A., Kirsch, C., Lippautz, M., Payer, H., … Veith, H. (2016). Local linearizability for concurrent container-type data structures. In Leibniz International Proceedings in Informatics (Vol. 59). Quebec City; Canada: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2016.6","ama":"Haas A, Henzinger TA, Holzer A, et al. Local linearizability for concurrent container-type data structures. In: Leibniz International Proceedings in Informatics. Vol 59. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2016. doi:10.4230/LIPIcs.CONCUR.2016.6","ieee":"A. Haas et al., “Local linearizability for concurrent container-type data structures,” in Leibniz International Proceedings in Informatics, Quebec City; Canada, 2016, vol. 59.","short":"A. Haas, T.A. Henzinger, A. Holzer, C. Kirsch, M. Lippautz, H. Payer, A. Sezgin, A. Sokolova, H. Veith, in:, Leibniz International Proceedings in Informatics, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016.","mla":"Haas, Andreas, et al. “Local Linearizability for Concurrent Container-Type Data Structures.” Leibniz International Proceedings in Informatics, vol. 59, 6, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016, doi:10.4230/LIPIcs.CONCUR.2016.6.","ista":"Haas A, Henzinger TA, Holzer A, Kirsch C, Lippautz M, Payer H, Sezgin A, Sokolova A, Veith H. 2016. Local linearizability for concurrent container-type data structures. Leibniz International Proceedings in Informatics. CONCUR: Concurrency Theory, LIPIcs, vol. 59, 6.","chicago":"Haas, Andreas, Thomas A Henzinger, Andreas Holzer, Christoph Kirsch, Michael Lippautz, Hannes Payer, Ali Sezgin, Ana Sokolova, and Helmut Veith. “Local Linearizability for Concurrent Container-Type Data Structures.” In Leibniz International Proceedings in Informatics, Vol. 59. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. https://doi.org/10.4230/LIPIcs.CONCUR.2016.6."},"title":"Local linearizability for concurrent container-type data structures","author":[{"full_name":"Haas, Andreas","last_name":"Haas","first_name":"Andreas"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger"},{"first_name":"Andreas","last_name":"Holzer","full_name":"Holzer, Andreas"},{"first_name":"Christoph","full_name":"Kirsch, Christoph","last_name":"Kirsch"},{"full_name":"Lippautz, Michael","last_name":"Lippautz","first_name":"Michael"},{"last_name":"Payer","full_name":"Payer, Hannes","first_name":"Hannes"},{"last_name":"Sezgin","full_name":"Sezgin, Ali","id":"4C7638DA-F248-11E8-B48F-1D18A9856A87","first_name":"Ali"},{"first_name":"Ana","full_name":"Sokolova, Ana","last_name":"Sokolova"},{"first_name":"Helmut","last_name":"Veith","full_name":"Veith, Helmut"}],"publist_id":"6280","oa_version":"Published Version","abstract":[{"text":" The semantics of concurrent data structures is usually given by a sequential specification and a consistency condition. Linearizability is the most popular consistency condition due to its simplicity and general applicability. Nevertheless, for applications that do not require all guarantees offered by linearizability, recent research has focused on improving performance and scalability of concurrent data structures by relaxing their semantics. In this paper, we present local linearizability, a relaxed consistency condition that is applicable to container-type concurrent data structures like pools, queues, and stacks. While linearizability requires that the effect of each operation is observed by all threads at the same time, local linearizability only requires that for each thread T, the effects of its local insertion operations and the effects of those removal operations that remove values inserted by T are observed by all threads at the same time. We investigate theoretical and practical properties of local linearizability and its relationship to many existing consistency conditions. We present a generic implementation method for locally linearizable data structures that uses existing linearizable data structures as building blocks. Our implementations show performance and scalability improvements over the original building blocks and outperform the fastest existing container-type implementations. ","lang":"eng"}],"month":"08","intvolume":" 59","alternative_title":["LIPIcs"],"scopus_import":1,"file":[{"relation":"main_file","access_level":"open_access","content_type":"application/pdf","file_id":"4795","creator":"system","file_size":589747,"date_updated":"2018-12-12T10:10:10Z","file_name":"IST-2017-793-v1+1_LIPIcs-CONCUR-2016-6.pdf","date_created":"2018-12-12T10:10:10Z"}],"language":[{"iso":"eng"}],"publication_status":"published","volume":59,"ec_funded":1,"_id":"1095","status":"public","pubrep_id":"793","type":"conference","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"conference":{"name":"CONCUR: Concurrency Theory","start_date":"2016-08-23","location":"Quebec City; Canada","end_date":"2016-08-26"},"ddc":["004"],"date_updated":"2021-01-12T06:48:14Z","department":[{"_id":"ToHe"}],"file_date_updated":"2018-12-12T10:10:10Z"},{"_id":"10898","article_number":"17","conference":{"end_date":"2013-05-16","location":"Ischia, Italy","start_date":"2013-05-14","name":"CF: Conference on Computing Frontiers"},"type":"conference","status":"public","date_updated":"2022-06-21T08:01:19Z","citation":{"ista":"Haas A, Lippautz M, Henzinger TA, Payer H, Sokolova A, Kirsch CM, Sezgin A. 2013. Distributed queues in shared memory: Multicore performance and scalability through quantitative relaxation. Proceedings of the ACM International Conference on Computing Frontiers - CF ’13. CF: Conference on Computing Frontiers, 17.","chicago":"Haas, Andreas, Michael Lippautz, Thomas A Henzinger, Hannes Payer, Ana Sokolova, Christoph M. Kirsch, and Ali Sezgin. “Distributed Queues in Shared Memory: Multicore Performance and Scalability through Quantitative Relaxation.” In Proceedings of the ACM International Conference on Computing Frontiers - CF ’13. ACM Press, 2013. https://doi.org/10.1145/2482767.2482789.","short":"A. Haas, M. Lippautz, T.A. Henzinger, H. Payer, A. Sokolova, C.M. Kirsch, A. Sezgin, in:, Proceedings of the ACM International Conference on Computing Frontiers - CF ’13, ACM Press, 2013.","ieee":"A. Haas et al., “Distributed queues in shared memory: Multicore performance and scalability through quantitative relaxation,” in Proceedings of the ACM International Conference on Computing Frontiers - CF ’13, Ischia, Italy, 2013, no. 5.","ama":"Haas A, Lippautz M, Henzinger TA, et al. Distributed queues in shared memory: Multicore performance and scalability through quantitative relaxation. In: Proceedings of the ACM International Conference on Computing Frontiers - CF ’13. ACM Press; 2013. doi:10.1145/2482767.2482789","apa":"Haas, A., Lippautz, M., Henzinger, T. A., Payer, H., Sokolova, A., Kirsch, C. M., & Sezgin, A. (2013). Distributed queues in shared memory: Multicore performance and scalability through quantitative relaxation. In Proceedings of the ACM International Conference on Computing Frontiers - CF ’13. Ischia, Italy: ACM Press. https://doi.org/10.1145/2482767.2482789","mla":"Haas, Andreas, et al. “Distributed Queues in Shared Memory: Multicore Performance and Scalability through Quantitative Relaxation.” Proceedings of the ACM International Conference on Computing Frontiers - CF ’13, no. 5, 17, ACM Press, 2013, doi:10.1145/2482767.2482789."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","article_processing_charge":"No","author":[{"first_name":"Andreas","full_name":"Haas, Andreas","last_name":"Haas"},{"first_name":"Michael","last_name":"Lippautz","full_name":"Lippautz, Michael"},{"last_name":"Henzinger","full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"},{"first_name":"Hannes","full_name":"Payer, Hannes","last_name":"Payer"},{"full_name":"Sokolova, Ana","last_name":"Sokolova","first_name":"Ana"},{"first_name":"Christoph M.","full_name":"Kirsch, Christoph M.","last_name":"Kirsch"},{"id":"4C7638DA-F248-11E8-B48F-1D18A9856A87","first_name":"Ali","last_name":"Sezgin","full_name":"Sezgin, Ali"}],"department":[{"_id":"ToHe"}],"title":"Distributed queues in shared memory: Multicore performance and scalability through quantitative relaxation","abstract":[{"lang":"eng","text":"A prominent remedy to multicore scalability issues in concurrent data structure implementations is to relax the sequential specification of the data structure. We present distributed queues (DQ), a new family of relaxed concurrent queue implementations. DQs implement relaxed queues with linearizable emptiness check and either configurable or bounded out-of-order behavior or pool behavior. Our experiments show that DQs outperform and outscale in micro- and macrobenchmarks all strict and relaxed queue as well as pool implementations that we considered."}],"oa_version":"None","scopus_import":"1","quality_controlled":"1","publisher":"ACM Press","month":"05","publication_status":"published","year":"2013","publication_identifier":{"isbn":["978-145032053-5"]},"publication":"Proceedings of the ACM International Conference on Computing Frontiers - CF '13","language":[{"iso":"eng"}],"day":"01","date_created":"2022-03-21T07:33:22Z","doi":"10.1145/2482767.2482789","issue":"5","date_published":"2013-05-01T00:00:00Z"},{"file_date_updated":"2020-07-14T12:45:31Z","department":[{"_id":"ToHe"}],"date_updated":"2023-02-21T16:06:49Z","ddc":["000","004"],"conference":{"start_date":"2013-01-23","end_date":"2013-01-25","location":"Rome, Italy","name":"POPL: Principles of Programming Languages"},"type":"conference","pubrep_id":"198","status":"public","_id":"2181","ec_funded":1,"related_material":{"record":[{"relation":"later_version","status":"deleted","id":"10901"}]},"publication_status":"published","publication_identifier":{"isbn":["978-1-4503-1832-7"]},"language":[{"iso":"eng"}],"file":[{"date_created":"2018-12-12T10:14:33Z","file_name":"IST-2014-198-v1+1_popl128-henzinger-clean.pdf","creator":"system","date_updated":"2020-07-14T12:45:31Z","file_size":294689,"checksum":"adf465e70948f4e80e48057524516456","file_id":"5086","access_level":"open_access","relation":"main_file","content_type":"application/pdf"}],"scopus_import":1,"month":"01","abstract":[{"text":"There is a trade-off between performance and correctness in implementing concurrent data structures. Better performance may be achieved at the expense of relaxing correctness, by redefining the semantics of data structures. We address such a redefinition of data structure semantics and present a systematic and formal framework for obtaining new data structures by quantitatively relaxing existing ones. We view a data structure as a sequential specification S containing all "legal" sequences over an alphabet of method calls. Relaxing the data structure corresponds to defining a distance from any sequence over the alphabet to the sequential specification: the k-relaxed sequential specification contains all sequences over the alphabet within distance k from the original specification. In contrast to other existing work, our relaxations are semantic (distance in terms of data structure states). As an instantiation of our framework, we present two simple yet generic relaxation schemes, called out-of-order and stuttering relaxation, along with several ways of computing distances. We show that the out-of-order relaxation, when further instantiated to stacks, queues, and priority queues, amounts to tolerating bounded out-of-order behavior, which cannot be captured by a purely syntactic relaxation (distance in terms of sequence manipulation, e.g. edit distance). We give concurrent implementations of relaxed data structures and demonstrate that bounded relaxations provide the means for trading correctness for performance in a controlled way. The relaxations are monotonic which further highlights the trade-off: increasing k increases the number of permitted sequences, which as we demonstrate can lead to better performance. Finally, since a relaxed stack or queue also implements a pool, we actually have new concurrent pool implementations that outperform the state-of-the-art ones.","lang":"eng"}],"oa_version":"Submitted Version","publist_id":"4801","author":[{"first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724"},{"first_name":"Christoph","last_name":"Kirsch","full_name":"Kirsch, Christoph"},{"last_name":"Payer","full_name":"Payer, Hannes","first_name":"Hannes"},{"first_name":"Ali","id":"4C7638DA-F248-11E8-B48F-1D18A9856A87","full_name":"Sezgin, Ali","last_name":"Sezgin"},{"first_name":"Ana","last_name":"Sokolova","full_name":"Sokolova, Ana"}],"title":"Quantitative relaxation of concurrent data structures","citation":{"mla":"Henzinger, Thomas A., et al. “Quantitative Relaxation of Concurrent Data Structures.” Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Language, ACM, 2013, pp. 317–28, doi:10.1145/2429069.2429109.","apa":"Henzinger, T. A., Kirsch, C., Payer, H., Sezgin, A., & Sokolova, A. (2013). Quantitative relaxation of concurrent data structures. In Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming language (pp. 317–328). Rome, Italy: ACM. https://doi.org/10.1145/2429069.2429109","ama":"Henzinger TA, Kirsch C, Payer H, Sezgin A, Sokolova A. Quantitative relaxation of concurrent data structures. In: Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Language. ACM; 2013:317-328. doi:10.1145/2429069.2429109","ieee":"T. A. Henzinger, C. Kirsch, H. Payer, A. Sezgin, and A. Sokolova, “Quantitative relaxation of concurrent data structures,” in Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming language, Rome, Italy, 2013, pp. 317–328.","short":"T.A. Henzinger, C. Kirsch, H. Payer, A. Sezgin, A. Sokolova, in:, Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Language, ACM, 2013, pp. 317–328.","chicago":"Henzinger, Thomas A, Christoph Kirsch, Hannes Payer, Ali Sezgin, and Ana Sokolova. “Quantitative Relaxation of Concurrent Data Structures.” In Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Language, 317–28. ACM, 2013. https://doi.org/10.1145/2429069.2429109.","ista":"Henzinger TA, Kirsch C, Payer H, Sezgin A, Sokolova A. 2013. Quantitative relaxation of concurrent data structures. Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming language. POPL: Principles of Programming Languages, 317–328."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","project":[{"grant_number":"267989","name":"Quantitative Reactive Modeling","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"_id":"25F5A88A-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S11402-N23","name":"Moderne Concurrency Paradigms"}],"page":"317 - 328","date_created":"2018-12-11T11:56:11Z","date_published":"2013-01-01T00:00:00Z","doi":"10.1145/2429069.2429109","year":"2013","has_accepted_license":"1","publication":"Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming language","day":"01","oa":1,"publisher":"ACM","quality_controlled":"1","acknowledgement":" and an Elise Richter Fellowship (Austrian Science Fund V00125). "},{"volume":8052,"related_material":{"record":[{"id":"1832","status":"public","relation":"later_version"}]},"ec_funded":1,"file":[{"file_name":"IST-2014-197-v1+1_main-queue-verification.pdf","date_created":"2018-12-12T10:08:58Z","file_size":337059,"date_updated":"2020-07-14T12:45:39Z","creator":"system","checksum":"bdbb520de91751fe0136309ad4ef67e4","file_id":"4721","content_type":"application/pdf","relation":"main_file","access_level":"open_access"}],"language":[{"iso":"eng"}],"publication_status":"published","month":"08","intvolume":" 8052","alternative_title":["LNCS"],"scopus_import":1,"oa_version":"Submitted Version","abstract":[{"lang":"eng","text":"Linearizability of concurrent data structures is usually proved by monolithic simulation arguments relying on identifying the so-called linearization points. Regrettably, such proofs, whether manual or automatic, are often complicated and scale poorly to advanced non-blocking concurrency patterns, such as helping and optimistic updates.\r\nIn response, we propose a more modular way of checking linearizability of concurrent queue algorithms that does not involve identifying linearization points. We reduce the task of proving linearizability with respect to the queue specification to establishing four basic properties, each of which can be proved independently by simpler arguments. As a demonstration of our approach, we verify the Herlihy and Wing queue, an algorithm that is challenging to verify by a simulation proof."}],"file_date_updated":"2020-07-14T12:45:39Z","department":[{"_id":"ToHe"}],"ddc":["000","004"],"date_updated":"2023-02-23T10:16:27Z","status":"public","pubrep_id":"197","type":"conference","conference":{"name":"CONCUR: Concurrency Theory","start_date":"2013-08-27","end_date":"2013-08-30","location":"Buenos Aires, Argentina"},"_id":"2328","series_title":"Lecture Notes in Computer Science","doi":"10.1007/978-3-642-40184-8_18","date_published":"2013-08-01T00:00:00Z","date_created":"2018-12-11T11:57:01Z","page":"242 - 256","day":"01","has_accepted_license":"1","year":"2013","quality_controlled":"1","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","oa":1,"title":"Aspect-oriented linearizability proofs","author":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger"},{"last_name":"Sezgin","full_name":"Sezgin, Ali","id":"4C7638DA-F248-11E8-B48F-1D18A9856A87","first_name":"Ali"},{"last_name":"Vafeiadis","full_name":"Vafeiadis, Viktor","first_name":"Viktor"}],"publist_id":"4598","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"mla":"Henzinger, Thomas A., et al. Aspect-Oriented Linearizability Proofs. Vol. 8052, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2013, pp. 242–56, doi:10.1007/978-3-642-40184-8_18.","short":"T.A. Henzinger, A. Sezgin, V. Vafeiadis, 8052 (2013) 242–256.","ieee":"T. A. Henzinger, A. Sezgin, and V. Vafeiadis, “Aspect-oriented linearizability proofs,” vol. 8052. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, pp. 242–256, 2013.","apa":"Henzinger, T. A., Sezgin, A., & Vafeiadis, V. (2013). Aspect-oriented linearizability proofs. Presented at the CONCUR: Concurrency Theory, Buenos Aires, Argentina: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.1007/978-3-642-40184-8_18","ama":"Henzinger TA, Sezgin A, Vafeiadis V. Aspect-oriented linearizability proofs. 2013;8052:242-256. doi:10.1007/978-3-642-40184-8_18","chicago":"Henzinger, Thomas A, Ali Sezgin, and Viktor Vafeiadis. “Aspect-Oriented Linearizability Proofs.” Lecture Notes in Computer Science. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2013. https://doi.org/10.1007/978-3-642-40184-8_18.","ista":"Henzinger TA, Sezgin A, Vafeiadis V. 2013. Aspect-oriented linearizability proofs. 8052, 242–256."},"project":[{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Reactive Modeling","grant_number":"267989"}]},{"type":"technical_report","pubrep_id":"123","status":"public","_id":"5402","author":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A"},{"id":"4C7638DA-F248-11E8-B48F-1D18A9856A87","first_name":"Ali","last_name":"Sezgin","full_name":"Sezgin, Ali"}],"file_date_updated":"2020-07-14T12:46:45Z","department":[{"_id":"ToHe"}],"title":"How free is your linearizable concurrent data structure?","date_updated":"2020-07-14T23:04:47Z","citation":{"chicago":"Henzinger, Thomas A, and Ali Sezgin. How Free Is Your Linearizable Concurrent Data Structure? IST Austria, 2013. https://doi.org/10.15479/AT:IST-2013-123-v1-1.","ista":"Henzinger TA, Sezgin A. 2013. How free is your linearizable concurrent data structure?, IST Austria, 16p.","mla":"Henzinger, Thomas A., and Ali Sezgin. How Free Is Your Linearizable Concurrent Data Structure? IST Austria, 2013, doi:10.15479/AT:IST-2013-123-v1-1.","short":"T.A. Henzinger, A. Sezgin, How Free Is Your Linearizable Concurrent Data Structure?, IST Austria, 2013.","ieee":"T. A. Henzinger and A. Sezgin, How free is your linearizable concurrent data structure? IST Austria, 2013.","apa":"Henzinger, T. A., & Sezgin, A. (2013). How free is your linearizable concurrent data structure? IST Austria. https://doi.org/10.15479/AT:IST-2013-123-v1-1","ama":"Henzinger TA, Sezgin A. How Free Is Your Linearizable Concurrent Data Structure? IST Austria; 2013. doi:10.15479/AT:IST-2013-123-v1-1"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","ddc":["000","004"],"oa":1,"alternative_title":["IST Austria Technical Report"],"publisher":"IST Austria","month":"06","abstract":[{"lang":"eng","text":"Linearizability requires that the outcome of calls by competing threads to a concurrent data structure is the same as some sequential execution where each thread has exclusive access to the data structure. In an ordered data structure, such as a queue or a stack, linearizability is ensured by requiring threads commit in the order dictated by the sequential semantics of the data structure; e.g., in a concurrent queue implementation a dequeue can only remove the oldest element. \r\nIn this paper, we investigate the impact of this strict ordering, by comparing what linearizability allows to what existing implementations do. We first give an operational definition for linearizability which allows us to build the most general linearizable implementation as a transition system for any given sequential specification. We then use this operational definition to categorize linearizable implementations based on whether they are bound or free. In a bound implementation, whenever all threads observe the same logical state, the updates to the logical state and the temporal order of commits coincide. All existing queue implementations we know of are bound. We then proceed to present, to the best of our knowledge, the first ever free queue implementation. Our experiments show that free implementations have the potential for better performance by suffering less from contention."}],"oa_version":"Published Version","page":"16","date_created":"2018-12-12T11:39:07Z","doi":"10.15479/AT:IST-2013-123-v1-1","date_published":"2013-06-12T00:00:00Z","year":"2013","publication_status":"published","publication_identifier":{"issn":["2664-1690"]},"has_accepted_license":"1","language":[{"iso":"eng"}],"file":[{"file_size":249790,"date_updated":"2020-07-14T12:46:45Z","creator":"system","file_name":"IST-2013-123-v1+1_main-concur2013.pdf","date_created":"2018-12-12T11:53:19Z","content_type":"application/pdf","relation":"main_file","access_level":"open_access","checksum":"ce580605ae9756a8c99d7b403ebb8eed","file_id":"5480"}],"day":"12"},{"pubrep_id":"124","status":"public","type":"technical_report","_id":"6440","title":"Replacing competition with cooperation to achieve scalable lock-free FIFO queues ","file_date_updated":"2020-07-14T12:47:30Z","department":[{"_id":"ToHe"}],"author":[{"first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger"},{"first_name":"Hannes","last_name":"Payer","full_name":"Payer, Hannes"},{"id":"4C7638DA-F248-11E8-B48F-1D18A9856A87","first_name":"Ali","full_name":"Sezgin, Ali","last_name":"Sezgin"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","ddc":["000","005"],"citation":{"apa":"Henzinger, T. A., Payer, H., & Sezgin, A. (2013). Replacing competition with cooperation to achieve scalable lock-free FIFO queues . IST Austria. https://doi.org/10.15479/AT:IST-2013-124-v1-1","ama":"Henzinger TA, Payer H, Sezgin A. Replacing Competition with Cooperation to Achieve Scalable Lock-Free FIFO Queues . IST Austria; 2013. doi:10.15479/AT:IST-2013-124-v1-1","short":"T.A. Henzinger, H. Payer, A. Sezgin, Replacing Competition with Cooperation to Achieve Scalable Lock-Free FIFO Queues , IST Austria, 2013.","ieee":"T. A. Henzinger, H. Payer, and A. Sezgin, Replacing competition with cooperation to achieve scalable lock-free FIFO queues . IST Austria, 2013.","mla":"Henzinger, Thomas A., et al. Replacing Competition with Cooperation to Achieve Scalable Lock-Free FIFO Queues . IST Austria, 2013, doi:10.15479/AT:IST-2013-124-v1-1.","ista":"Henzinger TA, Payer H, Sezgin A. 2013. Replacing competition with cooperation to achieve scalable lock-free FIFO queues , IST Austria, 23p.","chicago":"Henzinger, Thomas A, Hannes Payer, and Ali Sezgin. Replacing Competition with Cooperation to Achieve Scalable Lock-Free FIFO Queues . IST Austria, 2013. https://doi.org/10.15479/AT:IST-2013-124-v1-1."},"date_updated":"2020-07-14T23:06:19Z","month":"06","oa":1,"alternative_title":["IST Austria Technical Report"],"publisher":"IST Austria","oa_version":"Published Version","abstract":[{"text":"In order to guarantee that each method of a data structure updates the logical state exactly once, al-most all non-blocking implementations employ Compare-And-Swap (CAS) based synchronization. For FIFO queue implementations this translates into concurrent enqueue or dequeue methods competing among themselves to update the same variable, the tail or the head, respectively, leading to high contention and poor scalability. Recent non-blocking queue implementations try to alleviate high contentionby increasing the number of contention points, all the while using CAS-based synchronization. Furthermore, obtaining a wait-free implementation with competition is achieved by additional synchronization which leads to further degradation of performance.In this paper we formalize the notion of competitiveness of a synchronizing statement which can beused as a measure for the scalability of concurrent implementations. We present a new queue implementation, the Speculative Pairing (SP) queue, which, as we show, decreases competitiveness by using Fetch-And-Increment (FAI) instead of CAS. We prove that the SP queue is linearizable and lock-free.We also show that replacing CAS with FAI leads to wait-freedom for dequeue methods without an adverse effect on performance. In fact, our experiments suggest that the SP queue can perform and scale better than the state-of-the-art queue implementations.","lang":"eng"}],"date_created":"2019-05-13T14:13:27Z","date_published":"2013-06-13T00:00:00Z","doi":"10.15479/AT:IST-2013-124-v1-1","page":"23","language":[{"iso":"eng"}],"day":"13","file":[{"file_name":"2013_TechRep_Henzinger.pdf","date_created":"2019-05-13T14:11:39Z","file_size":549684,"date_updated":"2020-07-14T12:47:30Z","creator":"dernst","file_id":"6441","checksum":"a219ba4eada6cd62befed52262ee15d4","content_type":"application/pdf","relation":"main_file","access_level":"open_access"}],"publication_status":"published","year":"2013","has_accepted_license":"1","publication_identifier":{"issn":["2664-1690"]}},{"month":"07","alternative_title":["LNCS"],"publisher":"Springer","scopus_import":1,"quality_controlled":"1","acknowledgement":"This work was supported by the ERC Advanced Investigator grant on Quantitative Reactive Modeling (QUAREM) and by the Swiss National Science Foundation.","oa_version":"None","abstract":[{"lang":"eng","text":"Continuous-time Markov chains (CTMC) with their rich theory and efficient simulation algorithms have been successfully used in modeling stochastic processes in diverse areas such as computer science, physics, and biology. However, systems that comprise non-instantaneous events cannot be accurately and efficiently modeled with CTMCs. In this paper we define delayed CTMCs, an extension of CTMCs that allows for the specification of a lower bound on the time interval between an event's initiation and its completion, and we propose an algorithm for the computation of their behavior. Our algorithm effectively decomposes the computation into two stages: a pure CTMC governs event initiations while a deterministic process guarantees lower bounds on event completion times. Furthermore, from the nature of delayed CTMCs, we obtain a parallelized version of our algorithm. We use our formalism to model genetic regulatory circuits (biological systems where delayed events are common) and report on the results of our numerical algorithm as run on a cluster. We compare performance and accuracy of our results with results obtained by using pure CTMCs. © 2012 Springer-Verlag."}],"ec_funded":1,"date_created":"2018-12-11T12:01:36Z","volume":"7358 ","doi":"10.1007/978-3-642-31424-7_24","date_published":"2012-07-01T00:00:00Z","page":"294 - 309","language":[{"iso":"eng"}],"day":"01","year":"2012","publication_status":"published","status":"public","project":[{"grant_number":"267989","name":"Quantitative Reactive Modeling","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425"}],"conference":{"name":"CAV: Computer Aided Verification","location":"Berkeley, CA, USA","end_date":"2012-07-13","start_date":"2012-07-07"},"type":"conference","_id":"3136","department":[{"_id":"CaGu"},{"_id":"ToHe"}],"title":"Delayed continuous time Markov chains for genetic regulatory circuits","publist_id":"3561","author":[{"id":"47F8433E-F248-11E8-B48F-1D18A9856A87","first_name":"Calin C","full_name":"Guet, Calin C","orcid":"0000-0001-6220-2052","last_name":"Guet"},{"last_name":"Gupta","full_name":"Gupta, Ashutosh","id":"335E5684-F248-11E8-B48F-1D18A9856A87","first_name":"Ashutosh"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger"},{"id":"3B43276C-F248-11E8-B48F-1D18A9856A87","first_name":"Maria","full_name":"Mateescu, Maria","last_name":"Mateescu"},{"id":"4C7638DA-F248-11E8-B48F-1D18A9856A87","first_name":"Ali","last_name":"Sezgin","full_name":"Sezgin, Ali"}],"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","citation":{"ista":"Guet CC, Gupta A, Henzinger TA, Mateescu M, Sezgin A. 2012. Delayed continuous time Markov chains for genetic regulatory circuits. CAV: Computer Aided Verification, LNCS, vol. 7358, 294–309.","chicago":"Guet, Calin C, Ashutosh Gupta, Thomas A Henzinger, Maria Mateescu, and Ali Sezgin. “Delayed Continuous Time Markov Chains for Genetic Regulatory Circuits,” 7358:294–309. Springer, 2012. https://doi.org/10.1007/978-3-642-31424-7_24.","apa":"Guet, C. C., Gupta, A., Henzinger, T. A., Mateescu, M., & Sezgin, A. (2012). Delayed continuous time Markov chains for genetic regulatory circuits (Vol. 7358, pp. 294–309). Presented at the CAV: Computer Aided Verification, Berkeley, CA, USA: Springer. https://doi.org/10.1007/978-3-642-31424-7_24","ama":"Guet CC, Gupta A, Henzinger TA, Mateescu M, Sezgin A. Delayed continuous time Markov chains for genetic regulatory circuits. In: Vol 7358. Springer; 2012:294-309. doi:10.1007/978-3-642-31424-7_24","ieee":"C. C. Guet, A. Gupta, T. A. Henzinger, M. Mateescu, and A. Sezgin, “Delayed continuous time Markov chains for genetic regulatory circuits,” presented at the CAV: Computer Aided Verification, Berkeley, CA, USA, 2012, vol. 7358, pp. 294–309.","short":"C.C. Guet, A. Gupta, T.A. Henzinger, M. Mateescu, A. Sezgin, in:, Springer, 2012, pp. 294–309.","mla":"Guet, Calin C., et al. Delayed Continuous Time Markov Chains for Genetic Regulatory Circuits. Vol. 7358, Springer, 2012, pp. 294–309, doi:10.1007/978-3-642-31424-7_24."},"date_updated":"2021-01-12T07:41:18Z"}]