干扰自由

在计算机科学中，干扰自由是一种用于证明具有共享变量的并发程序部分正确性的技术。Hoare逻辑早先被引入以证明顺序程序的正确性。在她的博士论文（以及由此产生的论文）中，在导师DavidGries的指导下，SusanOwicki将这项工作扩展到了并发程序上。自20世纪60年代中期以来，并发编程一直被用于将操作系统编码为并发进程的集合（特别是见Dijkstra.），但没有正式的机制来证明正确性。对各个进程的交错执行序列进行推理是很困难的，容易出错，而且不能扩大规模。干扰自由适用于证明而不是执行序列；人们表明一个进程的执行不能干扰另一个进程的正确性证明。一系列错综复杂的并发程序已经用干扰自由证明了正确性，干扰自由为随后开发具有共享变量的并发程序并证明其正确性的许多工作提供了基础。Owicki-Gries的论文AnaxiomaticprooftechniqueforparallelprogramsI获得了1977年ACM的编程语言和系统最佳论文奖。注意。Lamport提出了一个类似的想法。他写道：在写完这篇论文的最初版本后，我们了解到Owicki最近的工作。他的论文没有像Owicki-Gries那样受到关注，也许是因为它使用了流程图而不是像if语句和while循环这样的编程结构文本。Lamport是在概括Floyd的方法，而Owicki-Gries是在概括Hoare的方法。基本上所有后来在这个领域的工作都使用文本而不是流程图。下面在关于辅助变量的部分提到另一个区别。

不干涉原则1.对每个单独的部分给出一个完整的规格。2.当满足其规格的程序部分可用时，检查总问题是否得到解决。3.构建各个部分，以满足其规格，但彼此独立，并在其中使用。使用Hoare逻辑的进程S1和S2的规格{pre-S1}{pre-S2}{pre-S2}S1S2{post-S1}{pre-S2}{pre-S2}的含义。如果在前提条件pre-Si为真的状态下执行Si，那么在终止时，后条件post-Si为真。EdsgerW.Dijkstra在大约1965年写的EWD117《作为人类活动考虑的编程》中介绍了不干涉原则。该原则指出：整体的正确性可以通过只考虑部分的外部规格（通篇缩写为规格）而不是其内部构造来确定。Dijkstra概述了使用这一原则的一般步骤，如右图所示，他还举了几个在编程之外使用这一原则的例子。但它在编程中的使用是一个主要问题。例如，使用一个方法（子程序、函数等）的程序员应该只依靠它的规范来确定它的作用和如何调用它，而绝不是依靠它的实现。程序规格是用Hoare逻辑编写的，由TonyHoare爵士提出，如右图中进程S1和S2的规格就是例子。现在考虑使用共享变量的并发编程。两个（或更多）进程S1和S2的规格是以其前后条件给出的，我们假设S1和S2的实现是满足其规格的。

但是，当并行执行它们的实现时，由于它们共享变量，可能会出现竞赛条件；一个进程将共享变量改为另一个进程的证明中没有预期的值，所以另一个进程不能按预期工作。因此，Dijkstra的不干涉原则被违反了。在导师DavidGries的指导下，SusanOwicki在她1975年的康奈尔大学计算机科学博士论文中提出了干扰自由的概念。如果进程S1和S2满足干扰自由，那么它们的并行执行将按计划进行。Dijkstra称这项工作是将Hoare逻辑应用于并发进程的xxx个重要步骤。为了简化讨论，我们将注意力限制在只有两个并发进程，尽管Owicki-Gries允许更多。在证明大纲方面的干扰自由{P}的证明大纲S{Q}，其中S是。Owicki-Gries介绍了Hoare三元组{P}S{Q}的证明大纲。