[{"file_date_updated":"2020-07-14T12:44:44Z","publication_status":"published","has_accepted_license":"1","abstract":[{"text":"We present a computer-aided programming approach to concurrency. The approach allows programmers to program assuming a friendly, non-preemptive scheduler, and our synthesis procedure inserts synchronization to ensure that the final program works even with a preemptive scheduler. The correctness specification is implicit, inferred from the non-preemptive behavior. Let us consider sequences of calls that the program makes to an external interface. The specification requires that any such sequence produced under a preemptive scheduler should be included in the set of sequences produced under a non-preemptive scheduler. We guarantee that our synthesis does not introduce deadlocks and that the synchronization inserted is optimal w.r.t. a given objective function. The solution is based on a finitary abstraction, an algorithm for bounded language inclusion modulo an independence relation, and generation of a set of global constraints over synchronization placements. Each model of the global constraints set corresponds to a correctness-ensuring synchronization placement. The placement that is optimal w.r.t. the given objective function is chosen as the synchronization solution. We apply the approach to device-driver programming, where the driver threads call the software interface of the device and the API provided by the operating system. Our experiments demonstrate that our synthesis method is precise and efficient. The implicit specification helped us find one concurrency bug previously missed when model-checking using an explicit, user-provided specification. We implemented objective functions for coarse-grained and fine-grained locking and observed that different synchronization placements are produced for our experiments, favoring a minimal number of synchronization operations or maximum concurrency, respectively.","lang":"eng"}],"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","short":"CC BY (4.0)"},"intvolume":"        50","volume":50,"date_created":"2018-12-11T11:51:27Z","scopus_import":"1","day":"01","author":[{"full_name":"Cerny, Pavol","id":"4DCBEFFE-F248-11E8-B48F-1D18A9856A87","last_name":"Cerny","first_name":"Pavol"},{"first_name":"Edmund","full_name":"Clarke, Edmund","last_name":"Clarke"},{"orcid":"0000−0002−2985−7724","first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A"},{"first_name":"Arjun","full_name":"Radhakrishna, Arjun","id":"3B51CAC4-F248-11E8-B48F-1D18A9856A87","last_name":"Radhakrishna"},{"last_name":"Ryzhyk","full_name":"Ryzhyk, Leonid","first_name":"Leonid"},{"first_name":"Roopsha","full_name":"Samanta, Roopsha","id":"3D2AAC08-F248-11E8-B48F-1D18A9856A87","last_name":"Samanta"},{"first_name":"Thorsten","orcid":"0000-0003-4409-8487","last_name":"Tarrach","id":"3D6E8F2C-F248-11E8-B48F-1D18A9856A87","full_name":"Tarrach, Thorsten"}],"oa_version":"Published Version","title":"From non-preemptive to preemptive scheduling using synchronization synthesis","citation":{"ieee":"P. Cerny <i>et al.</i>, “From non-preemptive to preemptive scheduling using synchronization synthesis,” <i>Formal Methods in System Design</i>, vol. 50, no. 2–3. Springer, pp. 97–139, 2017.","short":"P. Cerny, E. Clarke, T.A. Henzinger, A. Radhakrishna, L. Ryzhyk, R. Samanta, T. Tarrach, Formal Methods in System Design 50 (2017) 97–139.","ama":"Cerny P, Clarke E, Henzinger TA, et al. From non-preemptive to preemptive scheduling using synchronization synthesis. <i>Formal Methods in System Design</i>. 2017;50(2-3):97-139. doi:<a href=\"https://doi.org/10.1007/s10703-016-0256-5\">10.1007/s10703-016-0256-5</a>","apa":"Cerny, P., Clarke, E., Henzinger, T. A., Radhakrishna, A., Ryzhyk, L., Samanta, R., &#38; Tarrach, T. (2017). From non-preemptive to preemptive scheduling using synchronization synthesis. <i>Formal Methods in System Design</i>. Springer. <a href=\"https://doi.org/10.1007/s10703-016-0256-5\">https://doi.org/10.1007/s10703-016-0256-5</a>","mla":"Cerny, Pavol, et al. “From Non-Preemptive to Preemptive Scheduling Using Synchronization Synthesis.” <i>Formal Methods in System Design</i>, vol. 50, no. 2–3, Springer, 2017, pp. 97–139, doi:<a href=\"https://doi.org/10.1007/s10703-016-0256-5\">10.1007/s10703-016-0256-5</a>.","chicago":"Cerny, Pavol, Edmund Clarke, Thomas A Henzinger, Arjun Radhakrishna, Leonid Ryzhyk, Roopsha Samanta, and Thorsten Tarrach. “From Non-Preemptive to Preemptive Scheduling Using Synchronization Synthesis.” <i>Formal Methods in System Design</i>. Springer, 2017. <a href=\"https://doi.org/10.1007/s10703-016-0256-5\">https://doi.org/10.1007/s10703-016-0256-5</a>.","ista":"Cerny P, Clarke E, Henzinger TA, Radhakrishna A, Ryzhyk L, Samanta R, Tarrach T. 2017. From non-preemptive to preemptive scheduling using synchronization synthesis. Formal Methods in System Design. 50(2–3), 97–139."},"issue":"2-3","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","oa":1,"language":[{"iso":"eng"}],"pubrep_id":"656","department":[{"_id":"ToHe"}],"file":[{"content_type":"application/pdf","access_level":"open_access","file_name":"IST-2016-656-v1+1_s10703-016-0256-5.pdf","checksum":"1163dfd997e8212c789525d4178b1653","relation":"main_file","date_updated":"2020-07-14T12:44:44Z","creator":"system","file_size":1416170,"date_created":"2018-12-12T10:13:05Z","file_id":"4985"}],"month":"06","quality_controlled":"1","page":"97 - 139","ddc":["000"],"_id":"1338","date_updated":"2023-09-20T11:13:51Z","type":"journal_article","article_processing_charge":"No","doi":"10.1007/s10703-016-0256-5","publisher":"Springer","ec_funded":1,"date_published":"2017-06-01T00:00:00Z","status":"public","publication":"Formal Methods in System Design","project":[{"call_identifier":"FP7","grant_number":"267989","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","name":"The Wittgenstein Prize","call_identifier":"FWF"},{"name":"IST Austria Open Access Fund","_id":"B67AFEDC-15C9-11EA-A837-991A96BB2854"}],"publist_id":"5929","isi":1,"year":"2017","related_material":{"record":[{"id":"1729","status":"public","relation":"earlier_version"}]},"external_id":{"isi":["000399888900001"]}},{"publication_identifier":{"issn":["2663-337X"]},"publication_status":"published","file_date_updated":"2021-11-17T13:46:55Z","abstract":[{"text":"In this thesis we present a computer-aided programming approach to concurrency. Our approach helps the programmer by automatically fixing concurrency-related bugs, i.e. bugs that occur when the program is executed using an aggressive preemptive scheduler, but not when using a non-preemptive (cooperative) scheduler. Bugs are program behaviours that are incorrect w.r.t. a specification. We consider both user-provided explicit specifications in the form of assertion\r\nstatements in the code as well as an implicit specification. The implicit specification is inferred from the non-preemptive behaviour. Let us consider sequences of calls that the program makes to an external interface. The implicit specification requires that any such sequence produced under a preemptive scheduler should be included in the set of sequences produced under a non-preemptive scheduler. We consider several semantics-preserving fixes that go beyond atomic sections typically explored in the synchronisation synthesis literature. Our synthesis is able to place locks, barriers and wait-signal statements and last, but not least reorder independent statements. The latter may be useful if a thread is released to early, e.g., before some initialisation is completed. We guarantee that our synthesis does not introduce deadlocks and that the synchronisation inserted is optimal w.r.t. a given objective function. We dub our solution trace-based synchronisation synthesis and it is loosely based on counterexample-guided inductive synthesis (CEGIS). The synthesis works by discovering a trace that is incorrect w.r.t. the specification and identifying ordering constraints crucial to trigger the specification violation. Synchronisation may be placed immediately (greedy approach) or delayed until all incorrect traces are found (non-greedy approach). For the non-greedy approach we construct a set of global constraints over synchronisation placements. Each model of the global constraints set corresponds to a correctness-ensuring synchronisation placement. The placement that is optimal w.r.t. the given objective function is chosen as the synchronisation solution. We evaluate our approach on a number of realistic (albeit simplified) Linux device-driver\r\nbenchmarks. The benchmarks are versions of the drivers with known concurrency-related bugs. For the experiments with an explicit specification we added assertions that would detect the bugs in the experiments. Device drivers lend themselves to implicit specification, where the device and the operating system are the external interfaces. Our experiments demonstrate that our synthesis method is precise and efficient. We implemented objective functions for coarse-grained and fine-grained locking and observed that different synchronisation placements are produced for our experiments, favouring e.g. a minimal number of synchronisation operations or maximum concurrency.","lang":"eng"}],"has_accepted_license":"1","date_created":"2018-12-11T11:50:19Z","oa_version":"Published Version","title":"Automatic synthesis of synchronisation primitives for concurrent programs","author":[{"first_name":"Thorsten","orcid":"0000-0003-4409-8487","last_name":"Tarrach","full_name":"Tarrach, Thorsten","id":"3D6E8F2C-F248-11E8-B48F-1D18A9856A87"}],"day":"07","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","citation":{"chicago":"Tarrach, Thorsten. “Automatic Synthesis of Synchronisation Primitives for Concurrent Programs.” Institute of Science and Technology Austria, 2016. <a href=\"https://doi.org/10.15479/at:ista:1130\">https://doi.org/10.15479/at:ista:1130</a>.","ista":"Tarrach T. 2016. Automatic synthesis of synchronisation primitives for concurrent programs. Institute of Science and Technology Austria.","apa":"Tarrach, T. (2016). <i>Automatic synthesis of synchronisation primitives for concurrent programs</i>. Institute of Science and Technology Austria. <a href=\"https://doi.org/10.15479/at:ista:1130\">https://doi.org/10.15479/at:ista:1130</a>","mla":"Tarrach, Thorsten. <i>Automatic Synthesis of Synchronisation Primitives for Concurrent Programs</i>. Institute of Science and Technology Austria, 2016, doi:<a href=\"https://doi.org/10.15479/at:ista:1130\">10.15479/at:ista:1130</a>.","ama":"Tarrach T. Automatic synthesis of synchronisation primitives for concurrent programs. 2016. doi:<a href=\"https://doi.org/10.15479/at:ista:1130\">10.15479/at:ista:1130</a>","ieee":"T. Tarrach, “Automatic synthesis of synchronisation primitives for concurrent programs,” Institute of Science and Technology Austria, 2016.","short":"T. Tarrach, Automatic Synthesis of Synchronisation Primitives for Concurrent Programs, Institute of Science and Technology Austria, 2016."},"language":[{"iso":"eng"}],"oa":1,"file":[{"file_id":"9179","creator":"dernst","date_updated":"2021-02-22T11:39:32Z","date_created":"2021-02-22T11:39:32Z","file_size":1523935,"checksum":"319a506831650327e85376db41fc1094","relation":"main_file","content_type":"application/pdf","access_level":"open_access","file_name":"2016_Tarrach_Thesis.pdf","success":1},{"file_id":"10296","file_size":1306068,"date_created":"2021-11-16T14:14:38Z","creator":"cchlebak","date_updated":"2021-11-17T13:46:55Z","relation":"main_file","checksum":"39efcd789f0ad859ff15652cb7afc412","file_name":"2016_Tarrach_Thesispdfa.pdf","access_level":"closed","content_type":"application/pdf"}],"department":[{"_id":"ToHe"},{"_id":"GradSch"}],"month":"07","supervisor":[{"first_name":"Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","last_name":"Henzinger"}],"main_file_link":[{"open_access":"1","url":"http://thorstent.github.io/theses/phd_thorsten_tarrach.pdf"}],"ddc":["000"],"page":"151","type":"dissertation","date_updated":"2023-09-07T11:57:01Z","_id":"1130","publisher":"Institute of Science and Technology Austria","doi":"10.15479/at:ista:1130","article_processing_charge":"No","alternative_title":["ISTA Thesis"],"date_published":"2016-07-07T00:00:00Z","ec_funded":1,"project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"267989","name":"Quantitative Reactive Modeling"},{"call_identifier":"FWF","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","name":"The Wittgenstein Prize","call_identifier":"FWF"}],"status":"public","degree_awarded":"PhD","publist_id":"6230","related_material":{"record":[{"relation":"part_of_dissertation","status":"public","id":"1729"},{"status":"public","relation":"part_of_dissertation","id":"2218"},{"id":"2445","status":"public","relation":"part_of_dissertation"}]},"year":"2016"},{"month":"07","department":[{"_id":"ToHe"}],"file":[{"file_id":"4715","creator":"system","date_updated":"2020-07-14T12:45:13Z","file_size":481922,"date_created":"2018-12-12T10:08:53Z","checksum":"6ff58ac220e2f20cb001ba35d4924495","relation":"main_file","content_type":"application/pdf","access_level":"local","file_name":"IST-2015-336-v1+1_long_version.pdf"}],"pubrep_id":"336","language":[{"iso":"eng"}],"citation":{"ama":"Cerny P, Clarke E, Henzinger TA, et al. From non-preemptive to preemptive scheduling using synchronization synthesis. 2015;9207:180-197. doi:<a href=\"https://doi.org/10.1007/978-3-319-21668-3_11\">10.1007/978-3-319-21668-3_11</a>","ieee":"P. Cerny <i>et al.</i>, “From non-preemptive to preemptive scheduling using synchronization synthesis,” vol. 9207. Springer, pp. 180–197, 2015.","short":"P. Cerny, E. Clarke, T.A. Henzinger, A. Radhakrishna, L. Ryzhyk, R. Samanta, T. Tarrach, 9207 (2015) 180–197.","ista":"Cerny P, Clarke E, Henzinger TA, Radhakrishna A, Ryzhyk L, Samanta R, Tarrach T. 2015. From non-preemptive to preemptive scheduling using synchronization synthesis. 9207, 180–197.","chicago":"Cerny, Pavol, Edmund Clarke, Thomas A Henzinger, Arjun Radhakrishna, Leonid Ryzhyk, Roopsha Samanta, and Thorsten Tarrach. “From Non-Preemptive to Preemptive Scheduling Using Synchronization Synthesis.” Lecture Notes in Computer Science. Springer, 2015. <a href=\"https://doi.org/10.1007/978-3-319-21668-3_11\">https://doi.org/10.1007/978-3-319-21668-3_11</a>.","apa":"Cerny, P., Clarke, E., Henzinger, T. A., Radhakrishna, A., Ryzhyk, L., Samanta, R., &#38; Tarrach, T. (2015). From non-preemptive to preemptive scheduling using synchronization synthesis. Presented at the CAV: Computer Aided Verification, San Francisco, CA, United States: Springer. <a href=\"https://doi.org/10.1007/978-3-319-21668-3_11\">https://doi.org/10.1007/978-3-319-21668-3_11</a>","mla":"Cerny, Pavol, et al. <i>From Non-Preemptive to Preemptive Scheduling Using Synchronization Synthesis</i>. Vol. 9207, Springer, 2015, pp. 180–97, doi:<a href=\"https://doi.org/10.1007/978-3-319-21668-3_11\">10.1007/978-3-319-21668-3_11</a>."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"full_name":"Cerny, Pavol","id":"4DCBEFFE-F248-11E8-B48F-1D18A9856A87","last_name":"Cerny","first_name":"Pavol"},{"first_name":"Edmund","last_name":"Clarke","full_name":"Clarke, Edmund"},{"first_name":"Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Arjun","id":"3B51CAC4-F248-11E8-B48F-1D18A9856A87","full_name":"Radhakrishna, Arjun","last_name":"Radhakrishna"},{"first_name":"Leonid","last_name":"Ryzhyk","full_name":"Ryzhyk, Leonid"},{"last_name":"Samanta","full_name":"Samanta, Roopsha","id":"3D2AAC08-F248-11E8-B48F-1D18A9856A87","first_name":"Roopsha"},{"orcid":"0000-0003-4409-8487","first_name":"Thorsten","last_name":"Tarrach","id":"3D6E8F2C-F248-11E8-B48F-1D18A9856A87","full_name":"Tarrach, Thorsten"}],"day":"01","scopus_import":1,"title":"From non-preemptive to preemptive scheduling using synchronization synthesis","oa_version":"Submitted Version","volume":9207,"date_created":"2018-12-11T11:53:42Z","has_accepted_license":"1","intvolume":"      9207","abstract":[{"lang":"eng","text":"We present a computer-aided programming approach to concurrency. The approach allows programmers to program assuming a friendly, non-preemptive scheduler, and our synthesis procedure inserts synchronization to ensure that the final program works even with a preemptive scheduler. The correctness specification is implicit, inferred from the non-preemptive behavior. Let us consider sequences of calls that the program makes to an external interface. The specification requires that any such sequence produced under a preemptive scheduler should be included in the set of such sequences produced under a non-preemptive scheduler. The solution is based on a finitary abstraction, an algorithm for bounded language inclusion modulo an independence relation, and rules for inserting synchronization. We apply the approach to device-driver programming, where the driver threads call the software interface of the device and the API provided by the operating system. Our experiments demonstrate that our synthesis method is precise and efficient, and, since it does not require explicit specifications, is more practical than the conventional approach based on user-provided assertions."}],"publication_status":"published","file_date_updated":"2020-07-14T12:45:13Z","year":"2015","related_material":{"record":[{"status":"public","relation":"dissertation_contains","id":"1130"},{"id":"1338","relation":"later_version","status":"public"}]},"publist_id":"5398","project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"267989","name":"Quantitative Reactive Modeling"},{"grant_number":"Z211","name":"The Wittgenstein Prize","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"}],"status":"public","ec_funded":1,"conference":{"location":"San Francisco, CA, United States","start_date":"2015-07-18","end_date":"2015-07-24","name":"CAV: Computer Aided Verification"},"date_published":"2015-07-01T00:00:00Z","doi":"10.1007/978-3-319-21668-3_11","alternative_title":["LNCS"],"publisher":"Springer","date_updated":"2023-09-20T11:13:50Z","_id":"1729","type":"conference","series_title":"Lecture Notes in Computer Science","page":"180 - 197","ddc":["000"],"quality_controlled":"1"},{"file_date_updated":"2020-07-14T12:45:22Z","publication_identifier":{"isbn":["978-1-4503-3300-9"]},"publication_status":"published","has_accepted_license":"1","abstract":[{"lang":"eng","text":"We present a method and a tool for generating succinct representations of sets of concurrent traces. We focus on trace sets that contain all correct or all incorrect permutations of events from a given trace. We represent trace sets as HB-Formulas that are Boolean combinations of happens-before constraints between events. To generate a representation of incorrect interleavings, our method iteratively explores interleavings that violate the specification and gathers generalizations of the discovered interleavings into an HB-Formula; its complement yields a representation of correct interleavings.\r\n\r\nWe claim that our trace set representations can drive diverse verification, fault localization, repair, and synthesis techniques for concurrent programs. We demonstrate this by using our tool in three case studies involving synchronization synthesis, bug summarization, and abstraction refinement based verification. In each case study, our initial experimental results have been promising.\r\n\r\nIn the first case study, we present an algorithm for inferring missing synchronization from an HB-Formula representing correct interleavings of a given trace. The algorithm applies rules to rewrite specific patterns in the HB-Formula into locks, barriers, and wait-notify constructs. In the second case study, we use an HB-Formula representing incorrect interleavings for bug summarization. While the HB-Formula itself is a concise counterexample summary, we present additional inference rules to help identify specific concurrency bugs such as data races, define-use order violations, and two-stage access bugs. In the final case study, we present a novel predicate learning procedure that uses HB-Formulas representing abstract counterexamples to accelerate counterexample-guided abstraction refinement (CEGAR). In each iteration of the CEGAR loop, the procedure refines the abstraction to eliminate multiple spurious abstract counterexamples drawn from the HB-Formula."}],"date_created":"2018-12-11T11:55:05Z","day":"15","scopus_import":1,"author":[{"first_name":"Ashutosh","last_name":"Gupta","full_name":"Gupta, Ashutosh","id":"335E5684-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000−0002−2985−7724","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","last_name":"Henzinger"},{"id":"3B51CAC4-F248-11E8-B48F-1D18A9856A87","full_name":"Radhakrishna, Arjun","last_name":"Radhakrishna","first_name":"Arjun"},{"last_name":"Samanta","id":"3D2AAC08-F248-11E8-B48F-1D18A9856A87","full_name":"Samanta, Roopsha","first_name":"Roopsha"},{"last_name":"Tarrach","id":"3D6E8F2C-F248-11E8-B48F-1D18A9856A87","full_name":"Tarrach, Thorsten","orcid":"0000-0003-4409-8487","first_name":"Thorsten"}],"title":"Succinct representation of concurrent trace sets","oa_version":"Submitted Version","citation":{"chicago":"Gupta, Ashutosh, Thomas A Henzinger, Arjun Radhakrishna, Roopsha Samanta, and Thorsten Tarrach. “Succinct Representation of Concurrent Trace Sets,” 433–44. ACM, 2015. <a href=\"https://doi.org/10.1145/2676726.2677008\">https://doi.org/10.1145/2676726.2677008</a>.","ista":"Gupta A, Henzinger TA, Radhakrishna A, Samanta R, Tarrach T. 2015. Succinct representation of concurrent trace sets. POPL: Principles of Programming Languages, 433–444.","mla":"Gupta, Ashutosh, et al. <i>Succinct Representation of Concurrent Trace Sets</i>. ACM, 2015, pp. 433–44, doi:<a href=\"https://doi.org/10.1145/2676726.2677008\">10.1145/2676726.2677008</a>.","apa":"Gupta, A., Henzinger, T. A., Radhakrishna, A., Samanta, R., &#38; Tarrach, T. (2015). Succinct representation of concurrent trace sets (pp. 433–444). Presented at the POPL: Principles of Programming Languages, Mumbai, India: ACM. <a href=\"https://doi.org/10.1145/2676726.2677008\">https://doi.org/10.1145/2676726.2677008</a>","ama":"Gupta A, Henzinger TA, Radhakrishna A, Samanta R, Tarrach T. Succinct representation of concurrent trace sets. In: ACM; 2015:433-444. doi:<a href=\"https://doi.org/10.1145/2676726.2677008\">10.1145/2676726.2677008</a>","short":"A. Gupta, T.A. Henzinger, A. Radhakrishna, R. Samanta, T. Tarrach, in:, ACM, 2015, pp. 433–444.","ieee":"A. Gupta, T. A. Henzinger, A. Radhakrishna, R. Samanta, and T. Tarrach, “Succinct representation of concurrent trace sets,” presented at the POPL: Principles of Programming Languages, Mumbai, India, 2015, pp. 433–444."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa":1,"pubrep_id":"317","language":[{"iso":"eng"}],"department":[{"_id":"ToHe"}],"file":[{"checksum":"f0d4395b600f410a191256ac0b73af32","relation":"main_file","content_type":"application/pdf","access_level":"open_access","file_name":"IST-2015-317-v1+1_author_version.pdf","file_id":"5314","creator":"system","date_updated":"2020-07-14T12:45:22Z","file_size":399462,"date_created":"2018-12-12T10:17:56Z"}],"month":"01","quality_controlled":"1","page":"433 - 444","ddc":["005"],"_id":"1992","date_updated":"2021-01-12T06:54:33Z","type":"conference","doi":"10.1145/2676726.2677008","publisher":"ACM","date_published":"2015-01-15T00:00:00Z","conference":{"location":"Mumbai, India","start_date":"2015-01-15","end_date":"2015-01-17","name":"POPL: Principles of Programming Languages"},"status":"public","publist_id":"5091","year":"2015"},{"year":"2014","related_material":{"record":[{"id":"1130","status":"public","relation":"dissertation_contains"}]},"publist_id":"4749","status":"public","project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","name":"Quantitative Reactive Modeling","call_identifier":"FP7"},{"grant_number":"S11402-N23","name":"Moderne Concurrency Paradigms","call_identifier":"FWF","_id":"25F5A88A-B435-11E9-9278-68D0E5697425"}],"ec_funded":1,"conference":{"location":"Vienna, Austria","name":"CAV: Computer Aided Verification","start_date":"2014-07-18","end_date":"2014-07-22"},"date_published":"2014-07-22T00:00:00Z","alternative_title":["LNCS"],"doi":"10.1007/978-3-319-08867-9_38","publisher":"Springer","_id":"2218","date_updated":"2023-09-07T11:57:01Z","type":"conference","page":"568 - 584","ddc":["000"],"main_file_link":[{"url":"https://link.springer.com/chapter/10.1007%2F978-3-319-08867-9_38","open_access":"1"}],"quality_controlled":"1","month":"07","department":[{"_id":"ToHe"}],"file":[{"file_id":"4995","date_created":"2018-12-12T10:13:14Z","file_size":416732,"creator":"system","date_updated":"2020-07-14T12:45:33Z","relation":"main_file","checksum":"a631d3105509f239724644e77a1212e2","file_name":"IST-2014-297-v1+1_cav14-final.pdf","content_type":"application/pdf","access_level":"open_access"},{"file_size":616293,"date_created":"2018-12-12T10:13:15Z","creator":"system","date_updated":"2020-07-14T12:45:33Z","file_id":"4996","file_name":"IST-2014-297-v2+1_cav14-final2.pdf","content_type":"application/pdf","access_level":"open_access","relation":"main_file","checksum":"f8b0f748cc9fa697ca992cc56c87bc4e"}],"oa":1,"pubrep_id":"297","language":[{"iso":"eng"}],"citation":{"short":"P. Cerny, T.A. Henzinger, A. Radhakrishna, L. Ryzhyk, T. Tarrach, in:, Springer, 2014, pp. 568–584.","ieee":"P. Cerny, T. A. Henzinger, A. Radhakrishna, L. Ryzhyk, and T. Tarrach, “Regression-free synthesis for concurrency,” presented at the CAV: Computer Aided Verification, Vienna, Austria, 2014, vol. 8559, pp. 568–584.","ama":"Cerny P, Henzinger TA, Radhakrishna A, Ryzhyk L, Tarrach T. Regression-free synthesis for concurrency. In: Vol 8559. Springer; 2014:568-584. doi:<a href=\"https://doi.org/10.1007/978-3-319-08867-9_38\">10.1007/978-3-319-08867-9_38</a>","mla":"Cerny, Pavol, et al. <i>Regression-Free Synthesis for Concurrency</i>. Vol. 8559, Springer, 2014, pp. 568–84, doi:<a href=\"https://doi.org/10.1007/978-3-319-08867-9_38\">10.1007/978-3-319-08867-9_38</a>.","apa":"Cerny, P., Henzinger, T. A., Radhakrishna, A., Ryzhyk, L., &#38; Tarrach, T. (2014). Regression-free synthesis for concurrency (Vol. 8559, pp. 568–584). Presented at the CAV: Computer Aided Verification, Vienna, Austria: Springer. <a href=\"https://doi.org/10.1007/978-3-319-08867-9_38\">https://doi.org/10.1007/978-3-319-08867-9_38</a>","ista":"Cerny P, Henzinger TA, Radhakrishna A, Ryzhyk L, Tarrach T. 2014. Regression-free synthesis for concurrency. CAV: Computer Aided Verification, LNCS, vol. 8559, 568–584.","chicago":"Cerny, Pavol, Thomas A Henzinger, Arjun Radhakrishna, Leonid Ryzhyk, and Thorsten Tarrach. “Regression-Free Synthesis for Concurrency,” 8559:568–84. Springer, 2014. <a href=\"https://doi.org/10.1007/978-3-319-08867-9_38\">https://doi.org/10.1007/978-3-319-08867-9_38</a>."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","day":"22","author":[{"last_name":"Cerny","full_name":"Cerny, Pavol","first_name":"Pavol"},{"full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A","orcid":"0000−0002−2985−7724"},{"last_name":"Radhakrishna","full_name":"Radhakrishna, Arjun","id":"3B51CAC4-F248-11E8-B48F-1D18A9856A87","first_name":"Arjun"},{"first_name":"Leonid","last_name":"Ryzhyk","full_name":"Ryzhyk, Leonid"},{"full_name":"Tarrach, Thorsten","id":"3D6E8F2C-F248-11E8-B48F-1D18A9856A87","last_name":"Tarrach","first_name":"Thorsten","orcid":"0000-0003-4409-8487"}],"oa_version":"Submitted Version","title":"Regression-free synthesis for concurrency","volume":8559,"date_created":"2018-12-11T11:56:23Z","has_accepted_license":"1","abstract":[{"lang":"eng","text":"While fixing concurrency bugs, program repair algorithms may introduce new concurrency bugs. We present an algorithm that avoids such regressions. The solution space is given by a set of program transformations we consider in the repair process. These include reordering of instructions within a thread and inserting atomic sections. The new algorithm learns a constraint on the space of candidate solutions, from both positive examples (error-free traces) and counterexamples (error traces). From each counterexample, the algorithm learns a constraint necessary to remove the errors. From each positive examples, it learns a constraint that is necessary in order to prevent the repair from turning the trace into an error trace. We implemented the algorithm and evaluated it on simplified Linux device drivers with known bugs."}],"intvolume":"      8559","file_date_updated":"2020-07-14T12:45:33Z","publication_status":"published","publication_identifier":{"isbn":["978-331908866-2"]}},{"quality_controlled":"1","ddc":["000","004"],"page":"951 - 967","type":"conference","date_updated":"2023-09-07T11:57:01Z","_id":"2445","publisher":"Springer","doi":"10.1007/978-3-642-39799-8_68","alternative_title":["LNCS"],"conference":{"location":"St. Petersburg, Russia","start_date":"2013-07-13","end_date":"2013-07-19","name":"CAV: Computer Aided Verification"},"date_published":"2013-07-01T00:00:00Z","ec_funded":1,"project":[{"name":"Quantitative Reactive Modeling","grant_number":"267989","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","call_identifier":"FWF"}],"status":"public","publist_id":"4458","related_material":{"record":[{"id":"1130","relation":"dissertation_contains","status":"public"}]},"year":"2013","publication_status":"published","file_date_updated":"2020-07-14T12:45:40Z","intvolume":"      8044","abstract":[{"lang":"eng","text":"We develop program synthesis techniques that can help programmers fix concurrency-related bugs. We make two new contributions to synthesis for concurrency, the first improving the efficiency of the synthesized code, and the second improving the efficiency of the synthesis procedure itself. The first contribution is to have the synthesis procedure explore a variety of (sequential) semantics-preserving program transformations. Classically, only one such transformation has been considered, namely, the insertion of synchronization primitives (such as locks). Based on common manual bug-fixing techniques used by Linux device-driver developers, we explore additional, more efficient transformations, such as the reordering of independent instructions. The second contribution is to speed up the counterexample-guided removal of concurrency bugs within the synthesis procedure by considering partial-order traces (instead of linear traces) as counterexamples. A partial-order error trace represents a set of linear (interleaved) traces of a concurrent program all of which lead to the same error. By eliminating a partial-order error trace, we eliminate in a single iteration of the synthesis procedure all linearizations of the partial-order trace. We evaluated our techniques on several simplified examples of real concurrency bugs that occurred in Linux device drivers."}],"has_accepted_license":"1","date_created":"2018-12-11T11:57:42Z","volume":8044,"title":"Efficient synthesis for concurrency by semantics-preserving transformations","oa_version":"Submitted Version","author":[{"last_name":"Cerny","full_name":"Cerny, Pavol","id":"4DCBEFFE-F248-11E8-B48F-1D18A9856A87","first_name":"Pavol"},{"first_name":"Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Arjun","last_name":"Radhakrishna","id":"3B51CAC4-F248-11E8-B48F-1D18A9856A87","full_name":"Radhakrishna, Arjun"},{"last_name":"Ryzhyk","full_name":"Ryzhyk, Leonid","first_name":"Leonid"},{"orcid":"0000-0003-4409-8487","first_name":"Thorsten","full_name":"Tarrach, Thorsten","id":"3D6E8F2C-F248-11E8-B48F-1D18A9856A87","last_name":"Tarrach"}],"day":"01","scopus_import":1,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"ama":"Cerny P, Henzinger TA, Radhakrishna A, Ryzhyk L, Tarrach T. Efficient synthesis for concurrency by semantics-preserving transformations. In: Vol 8044. Springer; 2013:951-967. doi:<a href=\"https://doi.org/10.1007/978-3-642-39799-8_68\">10.1007/978-3-642-39799-8_68</a>","ieee":"P. Cerny, T. A. Henzinger, A. Radhakrishna, L. Ryzhyk, and T. Tarrach, “Efficient synthesis for concurrency by semantics-preserving transformations,” presented at the CAV: Computer Aided Verification, St. Petersburg, Russia, 2013, vol. 8044, pp. 951–967.","short":"P. Cerny, T.A. Henzinger, A. Radhakrishna, L. Ryzhyk, T. Tarrach, in:, Springer, 2013, pp. 951–967.","ista":"Cerny P, Henzinger TA, Radhakrishna A, Ryzhyk L, Tarrach T. 2013. Efficient synthesis for concurrency by semantics-preserving transformations. CAV: Computer Aided Verification, LNCS, vol. 8044, 951–967.","chicago":"Cerny, Pavol, Thomas A Henzinger, Arjun Radhakrishna, Leonid Ryzhyk, and Thorsten Tarrach. “Efficient Synthesis for Concurrency by Semantics-Preserving Transformations,” 8044:951–67. Springer, 2013. <a href=\"https://doi.org/10.1007/978-3-642-39799-8_68\">https://doi.org/10.1007/978-3-642-39799-8_68</a>.","apa":"Cerny, P., Henzinger, T. A., Radhakrishna, A., Ryzhyk, L., &#38; Tarrach, T. (2013). Efficient synthesis for concurrency by semantics-preserving transformations (Vol. 8044, pp. 951–967). Presented at the CAV: Computer Aided Verification, St. Petersburg, Russia: Springer. <a href=\"https://doi.org/10.1007/978-3-642-39799-8_68\">https://doi.org/10.1007/978-3-642-39799-8_68</a>","mla":"Cerny, Pavol, et al. <i>Efficient Synthesis for Concurrency by Semantics-Preserving Transformations</i>. Vol. 8044, Springer, 2013, pp. 951–67, doi:<a href=\"https://doi.org/10.1007/978-3-642-39799-8_68\">10.1007/978-3-642-39799-8_68</a>."},"language":[{"iso":"eng"}],"pubrep_id":"199","oa":1,"file":[{"checksum":"70c70ca5487faba82262c63e1b678a27","relation":"main_file","access_level":"open_access","content_type":"application/pdf","file_name":"IST-2014-199-v1+1_cav2013-final.pdf","file_id":"5158","creator":"system","date_updated":"2020-07-14T12:45:40Z","file_size":365548,"date_created":"2018-12-12T10:15:37Z"}],"department":[{"_id":"ToHe"}],"month":"07"}]