等待免费算法正确性证明的一般方法

我已经使用通用构造来设计等待免费二分查找树的算法。每个方法都有线性化点。但我不确定我如何正式证明这种算法的正确性。等待免费算法正确性证明的一般方法

在搜索类似的论文时，我发现他们已经证明算法是无等待的，只能生成可线性执行。这种情况是必要的还是充足的？

是否有任何其他正式的方法来证明等待自由算法的正确性？

来源

2014-04-18 grillSandwich

我想你最好问这个问题[cs.se] – Ishtar

等待和线性化是正交的概念。 –

@DavidEisenstat：同意他们是正交的概念。我的问题是，证明两个是否足以证明正确性。 – grillSandwich

要正式证明一些东西，你需要以下条件：

的你要证明的东西准确定义。就你而言，这可能是某种总是正确的谓词。我将举一个例子：

对于BlockingQueue用大小为N封端的，元件的队列的数目应始终为[0，N]。

如果BlockingQueue为空，项目添加的次数等于它从那里删除的次数。

好的，我们有定义或/和确切的描述。现在有几种方法来证明它：

Proof by contradiction方法。考虑一下陈述是不正确的，并最终得出一些不可能的结论。例如，我们想证明点Integer numbers can be negative。让我指出：

所有整数都是正数。

这让我们看到-1是一个错误的正数，所以这个陈述是不正确的，并且原始陈述被证明了。

证明：对所有可能的情况下，该语句是通过检查所有的人（有限套），通过使用Mathematical induction（用于Сountable套），或使用一些更复杂的逻辑语句和方法是正确的。更具体的例子取决于我们要证明的定理。

我还想补充一点，根据我的经验，Proof by contradiction方法我上面写的是经常使用，适合在许多情况下，所以也许你应该首先考虑它。

来源

2014-04-18 14:14:16

“无等待”意味着只要进程调用共享对象上的操作，调用就会在该进程的有限多个步骤*中完成。，当进程需要无限多的步骤但操作从未结束时，不存在无限的执行）。 “可线性化”意味着，对于每次执行，都存在操作的顺序重新排序，以使得（i）对象具有正确的顺序行为并且（ii）遵守执行中的部分操作顺序。随意写一个更具体的答案。 –

谢谢@Alexey。但是我不能在像顺序程序这样的并发程序中使用不变量。线性化被用来代替，如http://cs.brown.edu/~mph/HerlihyW90/p463-herlihy.pdf。同样，IMO，生成所有可能的状态对于并发程序来说不是一个可伸缩的解决方案。 – grillSandwich

等待免费算法正确性证明的一般方法

回答

相关问题