[{"_id":"13179","status":"public","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)"},"article_type":"original","type":"journal_article","ddc":["000"],"date_updated":"2023-07-17T08:43:19Z","department":[{"_id":"DaAl"}],"file_date_updated":"2023-07-03T13:09:39Z","oa_version":"Published Version","abstract":[{"lang":"eng","text":"Writing concurrent code that is both correct and efficient is notoriously difficult. Thus, programmers often prefer to use synchronization abstractions, which render code simpler and easier to reason about. Despite a wealth of work on this topic, there is still a gap between the rich semantics provided by synchronization abstractions in modern programming languages—specifically, fair FIFO ordering of synchronization requests and support for abortable operations—and frameworks for implementing it correctly and efficiently. Supporting such semantics is critical given the rising popularity of constructs for asynchronous programming, such as coroutines, which abort frequently and are cheaper to suspend and resume compared to native threads.\r\n\r\nThis paper introduces a new framework called CancellableQueueSynchronizer (CQS), which enables simple yet efficient implementations of a wide range of fair and abortable synchronization primitives: mutexes, semaphores, barriers, count-down latches, and blocking pools. Our main contribution is algorithmic, as implementing both fairness and abortability efficiently at this level of generality is non-trivial. Importantly, all our algorithms, including the CQS framework and the primitives built on top of it, come with formal proofs in the Iris framework for Coq for many of their properties. These proofs are modular, so it is easy to show correctness for new primitives implemented on top of CQS. From a practical perspective, implementation of CQS for native threads on the JVM improves throughput by up to two orders of magnitude over Java’s AbstractQueuedSynchronizer, the only practical abstraction offering similar semantics. Further, we successfully integrated CQS as a core component of the popular Kotlin Coroutines library, validating the framework’s practical impact and expressiveness in a real-world environment. In sum, CancellableQueueSynchronizer is the first framework to combine expressiveness with formal guarantees and solid practical performance. Our approach should be extensible to other languages and families of synchronization primitives."}],"intvolume":" 7","month":"06","scopus_import":"1","language":[{"iso":"eng"}],"file":[{"content_type":"application/pdf","access_level":"open_access","relation":"main_file","file_id":"13187","checksum":"5dba6e73f0ed79adbdae14d165bc2f68","success":1,"date_updated":"2023-07-03T13:09:39Z","file_size":1266773,"creator":"alisjak","date_created":"2023-07-03T13:09:39Z","file_name":"2023_ACMProgram.Lang._Koval.pdf"}],"publication_status":"published","publication_identifier":{"eissn":["2475-1421"]},"volume":7,"article_number":"116","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"ista":"Koval N, Khalanskiy D, Alistarh D-A. 2023. CQS: A formally-verified framework for fair and abortable synchronization. Proceedings of the ACM on Programming Languages. 7, 116.","chicago":"Koval, Nikita, Dmitry Khalanskiy, and Dan-Adrian Alistarh. “CQS: A Formally-Verified Framework for Fair and Abortable Synchronization.” Proceedings of the ACM on Programming Languages. Association for Computing Machinery , 2023. https://doi.org/10.1145/3591230.","ieee":"N. Koval, D. Khalanskiy, and D.-A. Alistarh, “CQS: A formally-verified framework for fair and abortable synchronization,” Proceedings of the ACM on Programming Languages, vol. 7. Association for Computing Machinery , 2023.","short":"N. Koval, D. Khalanskiy, D.-A. Alistarh, Proceedings of the ACM on Programming Languages 7 (2023).","apa":"Koval, N., Khalanskiy, D., & Alistarh, D.-A. (2023). CQS: A formally-verified framework for fair and abortable synchronization. Proceedings of the ACM on Programming Languages. Association for Computing Machinery . https://doi.org/10.1145/3591230","ama":"Koval N, Khalanskiy D, Alistarh D-A. CQS: A formally-verified framework for fair and abortable synchronization. Proceedings of the ACM on Programming Languages. 2023;7. doi:10.1145/3591230","mla":"Koval, Nikita, et al. “CQS: A Formally-Verified Framework for Fair and Abortable Synchronization.” Proceedings of the ACM on Programming Languages, vol. 7, 116, Association for Computing Machinery , 2023, doi:10.1145/3591230."},"title":"CQS: A formally-verified framework for fair and abortable synchronization","article_processing_charge":"No","author":[{"last_name":"Koval","full_name":"Koval, Nikita","first_name":"Nikita","id":"2F4DB10C-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Khalanskiy","full_name":"Khalanskiy, Dmitry","first_name":"Dmitry"},{"orcid":"0000-0003-3650-940X","full_name":"Alistarh, Dan-Adrian","last_name":"Alistarh","first_name":"Dan-Adrian","id":"4A899BFC-F248-11E8-B48F-1D18A9856A87"}],"oa":1,"quality_controlled":"1","publisher":"Association for Computing Machinery ","publication":"Proceedings of the ACM on Programming Languages","day":"06","year":"2023","has_accepted_license":"1","date_created":"2023-07-02T22:00:43Z","date_published":"2023-06-06T00:00:00Z","doi":"10.1145/3591230"},{"_id":"13180","article_type":"original","type":"journal_article","status":"public","date_updated":"2023-07-17T08:39:19Z","department":[{"_id":"TiBr"}],"abstract":[{"lang":"eng","text":"We study the density of everywhere locally soluble diagonal quadric surfaces, parameterised by rational points that lie on a split quadric surface"}],"oa_version":"Preprint","scopus_import":"1","main_file_link":[{"url":"https://arxiv.org/abs/2203.06881","open_access":"1"}],"month":"05","intvolume":" 16","publication_identifier":{"issn":["1944-4176"],"eissn":["1944-4184"]},"publication_status":"published","language":[{"iso":"eng"}],"volume":16,"issue":"2","citation":{"ista":"Browning TD, Lyczak J, Sarapin R. 2023. Local solubility for a family of quadrics over a split quadric surface. Involve. 16(2), 331–342.","chicago":"Browning, Timothy D, Julian Lyczak, and Roman Sarapin. “Local Solubility for a Family of Quadrics over a Split Quadric Surface.” Involve. Mathematical Sciences Publishers, 2023. https://doi.org/10.2140/involve.2023.16.331.","ama":"Browning TD, Lyczak J, Sarapin R. Local solubility for a family of quadrics over a split quadric surface. Involve. 2023;16(2):331-342. doi:10.2140/involve.2023.16.331","apa":"Browning, T. D., Lyczak, J., & Sarapin, R. (2023). Local solubility for a family of quadrics over a split quadric surface. Involve. Mathematical Sciences Publishers. https://doi.org/10.2140/involve.2023.16.331","short":"T.D. Browning, J. Lyczak, R. Sarapin, Involve 16 (2023) 331–342.","ieee":"T. D. Browning, J. Lyczak, and R. Sarapin, “Local solubility for a family of quadrics over a split quadric surface,” Involve, vol. 16, no. 2. Mathematical Sciences Publishers, pp. 331–342, 2023.","mla":"Browning, Timothy D., et al. “Local Solubility for a Family of Quadrics over a Split Quadric Surface.” Involve, vol. 16, no. 2, Mathematical Sciences Publishers, 2023, pp. 331–42, doi:10.2140/involve.2023.16.331."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"first_name":"Timothy D","id":"35827D50-F248-11E8-B48F-1D18A9856A87","last_name":"Browning","full_name":"Browning, Timothy D","orcid":"0000-0002-8314-0177"},{"full_name":"Lyczak, Julian","last_name":"Lyczak","first_name":"Julian","id":"3572849A-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Sarapin","full_name":"Sarapin, Roman","first_name":"Roman"}],"external_id":{"arxiv":["2203.06881"]},"article_processing_charge":"No","title":"Local solubility for a family of quadrics over a split quadric surface","publisher":"Mathematical Sciences Publishers","quality_controlled":"1","oa":1,"year":"2023","day":"26","publication":"Involve","page":"331-342","date_published":"2023-05-26T00:00:00Z","doi":"10.2140/involve.2023.16.331","date_created":"2023-07-02T22:00:43Z"},{"title":"Cryo-EM software packages: A sys-admins point of view","file_date_updated":"2023-07-18T09:28:30Z","department":[{"_id":"ScienComp"}],"article_processing_charge":"No","author":[{"full_name":"Elefante, Stefano","last_name":"Elefante","first_name":"Stefano","id":"490F40CE-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Stadlbauer, Stephan","last_name":"Stadlbauer","id":"4D0BC184-F248-11E8-B48F-1D18A9856A87","first_name":"Stephan"},{"full_name":"Alexander, Michael F","last_name":"Alexander","id":"3A02A8FA-F248-11E8-B48F-1D18A9856A87","first_name":"Michael F"},{"id":"45BF87EE-F248-11E8-B48F-1D18A9856A87","first_name":"Alois","full_name":"Schlögl, Alois","orcid":"0000-0002-5621-8100","last_name":"Schlögl"}],"ddc":["000"],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"mla":"Elefante, Stefano, et al. “Cryo-EM Software Packages: A Sys-Admins Point of View.” ASHPC23 - Austrian-Slovenian HPC Meeting 2023, EuroCC, pp. 42–42.","apa":"Elefante, S., Stadlbauer, S., Alexander, M. F., & Schlögl, A. (n.d.). Cryo-EM software packages: A sys-admins point of view. In ASHPC23 - Austrian-Slovenian HPC Meeting 2023 (pp. 42–42). Maribor, Slovenia: EuroCC.","ama":"Elefante S, Stadlbauer S, Alexander MF, Schlögl A. Cryo-EM software packages: A sys-admins point of view. In: ASHPC23 - Austrian-Slovenian HPC Meeting 2023. EuroCC; :42-42.","short":"S. Elefante, S. Stadlbauer, M.F. Alexander, A. Schlögl, in:, ASHPC23 - Austrian-Slovenian HPC Meeting 2023, EuroCC, n.d., pp. 42–42.","ieee":"S. Elefante, S. Stadlbauer, M. F. Alexander, and A. Schlögl, “Cryo-EM software packages: A sys-admins point of view,” in ASHPC23 - Austrian-Slovenian HPC Meeting 2023, Maribor, Slovenia, pp. 42–42.","chicago":"Elefante, Stefano, Stephan Stadlbauer, Michael F Alexander, and Alois Schlögl. “Cryo-EM Software Packages: A Sys-Admins Point of View.” In ASHPC23 - Austrian-Slovenian HPC Meeting 2023, 42–42. EuroCC, n.d.","ista":"Elefante S, Stadlbauer S, Alexander MF, Schlögl A. Cryo-EM software packages: A sys-admins point of view. ASHPC23 - Austrian-Slovenian HPC Meeting 2023. ASHPC: Austrian-Slovenian HPC Meeting, 42–42."},"date_updated":"2023-07-18T09:32:16Z","status":"public","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":"ASHPC: Austrian-Slovenian HPC Meeting","start_date":"2023-06-12","location":"Maribor, Slovenia","end_date":"2023-06-15"},"type":"conference_abstract","_id":"13162","date_created":"2023-06-23T11:03:18Z","date_published":"2023-07-01T00:00:00Z","page":"42-42","publication":"ASHPC23 - Austrian-Slovenian HPC Meeting 2023","language":[{"iso":"eng"}],"file":[{"date_updated":"2023-07-18T09:28:30Z","file_size":380354,"creator":"dernst","date_created":"2023-07-18T09:28:30Z","file_name":"2023_ASHPC_Elefante.pdf","content_type":"application/pdf","access_level":"open_access","relation":"main_file","checksum":"0ab6173cd5c5634ed773cd37ff012681","file_id":"13250","success":1}],"day":"01","year":"2023","publication_status":"accepted","has_accepted_license":"1","month":"07","oa":1,"quality_controlled":"1","publisher":"EuroCC","oa_version":"Submitted Version"},{"file":[{"checksum":"ec8e4295d54171032cdd1b01423eb4a6","file_id":"13249","success":1,"access_level":"open_access","relation":"main_file","content_type":"application/pdf","date_created":"2023-07-18T09:18:55Z","file_name":"2023_ASHPC_Schloegl.pdf","creator":"dernst","date_updated":"2023-07-18T09:18:55Z","file_size":316959}],"language":[{"iso":"eng"}],"publication_status":"inpress","month":"07","oa_version":"Submitted Version","file_date_updated":"2023-07-18T09:18:55Z","department":[{"_id":"ScienComp"},{"_id":"EM-Fac"}],"ddc":["000"],"date_updated":"2023-07-18T09:30:54Z","status":"public","type":"conference_abstract","conference":{"name":"ASHPC: Austrian-Slovenian HPC Meeting","end_date":"2023-06-15","location":"Maribor, Slovenia","start_date":"2023-06-13"},"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)"},"_id":"13161","date_published":"2023-07-01T00:00:00Z","date_created":"2023-06-23T11:01:23Z","page":"59-59","day":"01","publication":"ASHPC23 - Austrian-Slovenian HPC Meeting 2023","has_accepted_license":"1","year":"2023","publisher":"EuroCC","quality_controlled":"1","oa":1,"acknowledgement":"Thanks to Jesse Hansen for his suggestions on improving the abstract.","title":"Running Windows-applications on a Linux HPC cluster using WINE","author":[{"id":"45BF87EE-F248-11E8-B48F-1D18A9856A87","first_name":"Alois","last_name":"Schlögl","full_name":"Schlögl, Alois","orcid":"0000-0002-5621-8100"},{"last_name":"Elefante","full_name":"Elefante, Stefano","first_name":"Stefano","id":"490F40CE-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Hodirnau, Victor-Valentin","last_name":"Hodirnau","first_name":"Victor-Valentin","id":"3661B498-F248-11E8-B48F-1D18A9856A87"}],"article_processing_charge":"No","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"ama":"Schlögl A, Elefante S, Hodirnau V-V. Running Windows-applications on a Linux HPC cluster using WINE. In: ASHPC23 - Austrian-Slovenian HPC Meeting 2023. EuroCC; :59-59.","apa":"Schlögl, A., Elefante, S., & Hodirnau, V.-V. (n.d.). Running Windows-applications on a Linux HPC cluster using WINE. In ASHPC23 - Austrian-Slovenian HPC Meeting 2023 (pp. 59–59). Maribor, Slovenia: EuroCC.","ieee":"A. Schlögl, S. Elefante, and V.-V. Hodirnau, “Running Windows-applications on a Linux HPC cluster using WINE,” in ASHPC23 - Austrian-Slovenian HPC Meeting 2023, Maribor, Slovenia, pp. 59–59.","short":"A. Schlögl, S. Elefante, V.-V. Hodirnau, in:, ASHPC23 - Austrian-Slovenian HPC Meeting 2023, EuroCC, n.d., pp. 59–59.","mla":"Schlögl, Alois, et al. “Running Windows-Applications on a Linux HPC Cluster Using WINE.” ASHPC23 - Austrian-Slovenian HPC Meeting 2023, EuroCC, pp. 59–59.","ista":"Schlögl A, Elefante S, Hodirnau V-V. Running Windows-applications on a Linux HPC cluster using WINE. ASHPC23 - Austrian-Slovenian HPC Meeting 2023. ASHPC: Austrian-Slovenian HPC Meeting, 59–59.","chicago":"Schlögl, Alois, Stefano Elefante, and Victor-Valentin Hodirnau. “Running Windows-Applications on a Linux HPC Cluster Using WINE.” In ASHPC23 - Austrian-Slovenian HPC Meeting 2023, 59–59. EuroCC, n.d."}},{"file_date_updated":"2023-07-19T06:55:39Z","department":[{"_id":"MiLe"},{"_id":"ZhAl"}],"date_updated":"2023-07-19T06:59:19Z","ddc":["530"],"article_type":"original","type":"journal_article","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)"},"status":"public","keyword":["General Materials Science","Physical and Theoretical Chemistry"],"_id":"13251","volume":14,"issue":"27","ec_funded":1,"publication_identifier":{"eissn":["1948-7185"]},"publication_status":"published","file":[{"success":1,"file_id":"13253","checksum":"c0c040063f06a51b9c463adc504f1a23","relation":"main_file","access_level":"open_access","content_type":"application/pdf","file_name":"2023_JourPhysChemistry_Wei.pdf","date_created":"2023-07-19T06:55:39Z","creator":"dernst","file_size":2121252,"date_updated":"2023-07-19T06:55:39Z"}],"language":[{"iso":"eng"}],"month":"07","intvolume":" 14","abstract":[{"text":"A rotating organic cation and a dynamically disordered soft inorganic cage are the hallmark features of organic-inorganic lead-halide perovskites. Understanding the interplay between these two subsystems is a challenging problem, but it is this coupling that is widely conjectured to be responsible for the unique behavior of photocarriers in these materials. In this work, we use the fact that the polarizability of the organic cation strongly depends on the ambient electrostatic environment to put the molecule forward as a sensitive probe of the local crystal fields inside the lattice cell. We measure the average polarizability of the C/N–H bond stretching mode by means of infrared spectroscopy, which allows us to deduce the character of the motion of the cation molecule, find the magnitude of the local crystal field, and place an estimate on the strength of the hydrogen bond between the hydrogen and halide atoms. Our results pave the way for understanding electric fields in lead-halide perovskites using infrared bond spectroscopy.","lang":"eng"}],"oa_version":"Published Version","author":[{"orcid":"0000-0001-8913-9719","full_name":"Wei, Yujing","last_name":"Wei","first_name":"Yujing","id":"0c5ff007-2600-11ee-b896-98bd8d663294"},{"last_name":"Volosniev","full_name":"Volosniev, Artem","orcid":"0000-0003-0393-5525","id":"37D278BC-F248-11E8-B48F-1D18A9856A87","first_name":"Artem"},{"full_name":"Lorenc, Dusan","last_name":"Lorenc","id":"40D8A3E6-F248-11E8-B48F-1D18A9856A87","first_name":"Dusan"},{"full_name":"Zhumekenov, Ayan A.","last_name":"Zhumekenov","first_name":"Ayan A."},{"first_name":"Osman M.","last_name":"Bakr","full_name":"Bakr, Osman M."},{"last_name":"Lemeshko","full_name":"Lemeshko, Mikhail","orcid":"0000-0002-6990-7802","first_name":"Mikhail","id":"37CB05FA-F248-11E8-B48F-1D18A9856A87"},{"id":"45E67A2A-F248-11E8-B48F-1D18A9856A87","first_name":"Zhanybek","last_name":"Alpichshev","orcid":"0000-0002-7183-5203","full_name":"Alpichshev, Zhanybek"}],"external_id":{"arxiv":["2304.14198"],"isi":["001022811500001"]},"article_processing_charge":"Yes (via OA deal)","title":"Bond polarizability as a probe of local crystal fields in hybrid lead-halide perovskites","citation":{"chicago":"Wei, Yujing, Artem Volosniev, Dusan Lorenc, Ayan A. Zhumekenov, Osman M. Bakr, Mikhail Lemeshko, and Zhanybek Alpichshev. “Bond Polarizability as a Probe of Local Crystal Fields in Hybrid Lead-Halide Perovskites.” The Journal of Physical Chemistry Letters. American Chemical Society, 2023. https://doi.org/10.1021/acs.jpclett.3c01158.","ista":"Wei Y, Volosniev A, Lorenc D, Zhumekenov AA, Bakr OM, Lemeshko M, Alpichshev Z. 2023. Bond polarizability as a probe of local crystal fields in hybrid lead-halide perovskites. The Journal of Physical Chemistry Letters. 14(27), 6309–6314.","mla":"Wei, Yujing, et al. “Bond Polarizability as a Probe of Local Crystal Fields in Hybrid Lead-Halide Perovskites.” The Journal of Physical Chemistry Letters, vol. 14, no. 27, American Chemical Society, 2023, pp. 6309–14, doi:10.1021/acs.jpclett.3c01158.","ieee":"Y. Wei et al., “Bond polarizability as a probe of local crystal fields in hybrid lead-halide perovskites,” The Journal of Physical Chemistry Letters, vol. 14, no. 27. American Chemical Society, pp. 6309–6314, 2023.","short":"Y. Wei, A. Volosniev, D. Lorenc, A.A. Zhumekenov, O.M. Bakr, M. Lemeshko, Z. Alpichshev, The Journal of Physical Chemistry Letters 14 (2023) 6309–6314.","apa":"Wei, Y., Volosniev, A., Lorenc, D., Zhumekenov, A. A., Bakr, O. M., Lemeshko, M., & Alpichshev, Z. (2023). Bond polarizability as a probe of local crystal fields in hybrid lead-halide perovskites. The Journal of Physical Chemistry Letters. American Chemical Society. https://doi.org/10.1021/acs.jpclett.3c01158","ama":"Wei Y, Volosniev A, Lorenc D, et al. Bond polarizability as a probe of local crystal fields in hybrid lead-halide perovskites. The Journal of Physical Chemistry Letters. 2023;14(27):6309-6314. doi:10.1021/acs.jpclett.3c01158"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","project":[{"call_identifier":"H2020","_id":"2688CF98-B435-11E9-9278-68D0E5697425","grant_number":"801770","name":"Angulon: physics and applications of a new quasiparticle"}],"page":"6309-6314","doi":"10.1021/acs.jpclett.3c01158","date_published":"2023-07-05T00:00:00Z","date_created":"2023-07-18T11:13:17Z","isi":1,"has_accepted_license":"1","year":"2023","day":"05","publication":"The Journal of Physical Chemistry Letters","quality_controlled":"1","publisher":"American Chemical Society","oa":1,"acknowledgement":"We thank Bingqing Cheng and Hong-Zhou Ye for valuable discussions; Y.W.’s work at IST Austria was supported through ISTernship summer internship program funded by OeADGmbH; D.L. and Z.A. acknowledge support by IST Austria (ISTA); M.L. acknowledges support by the European Research Council (ERC) Starting Grant No. 801770 (ANGULON).\r\nA.A.Z. and O.M.B. acknowledge support by KAUST."}]