利用同步合成从非抢占到抢占调度
From Non-preemptive to Preemptive Scheduling using Synchronization Synthesis
摘要：
我们提出了一个计算机辅助编程方法的并发性。该方法允许程序员假设一个友好的，非抢占式的调度程序，我们的合成过程插入同步，以确保最终的程序工作，即使与抢占式调度。正确性规范是隐式的，从非抢占行为中推断出来。让我们考虑程序对外部接口的调用序列。该规范要求在抢占式调度器下产生的任何这样的序列应当被包括在在非抢占式调度器下产生的这样的序列的集合中。该解决方案是基于有限抽象，有界语言包含模的独立关系的算法，和插入同步的规则。我们将该方法应用于设备驱动程序编程，其中驱动程序线程调用设备的软件接口和操作系统提供的API。我们的实验表明，我们的合成方法是精确和高效的，而且，因为它不需要明确的规格，是更实际的比传统的方法基于用户提供的断言。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
