conference paper published yes Pavol Cerny author 4DCBEFFE-F248-11E8-B48F-1D18A9856A87 Edmund Clarke author Thomas A Henzinger author 40876CD8-F248-11E8-B48F-1D18A9856A870000−0002−2985−7724 Arjun Radhakrishna author 3B51CAC4-F248-11E8-B48F-1D18A9856A87 Leonid Ryzhyk author Roopsha Samanta author 3D2AAC08-F248-11E8-B48F-1D18A9856A87 Thorsten Tarrach author 3D6E8F2C-F248-11E8-B48F-1D18A9856A870000-0003-4409-8487 ToHe department CAV: Computer Aided Verification Quantitative Reactive Modeling project Formal methods for the design and analysis of complex systems project Rigorous Systems Engineering project 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. https://research-explorer.ista.ac.at/download/1729/4715/IST-2015-336-v1+1_long_version.pdf application/pdfno Springer2015San Francisco, CA, United States eng 00049147040001110.1007/978-3-319-21668-3_11 9207180 - 197 https://research-explorer.ista.ac.at/record/1130 https://research-explorer.ista.ac.at/record/1338 P. Cerny, E. Clarke, T.A. Henzinger, A. Radhakrishna, L. Ryzhyk, R. Samanta, T. Tarrach, 9207 (2015) 180–197. 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> 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>. P. Cerny <i>et al.</i>, “From non-preemptive to preemptive scheduling using synchronization synthesis,” vol. 9207. Springer, pp. 180–197, 2015. 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>. 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> 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. 17292018-12-11T11:53:42Z2025-09-23T08:54:01Z