等待免費算法正確性證明的一般方法

我已經使用通用構造來設計等待免費二分查找樹的算法。每個方法都有線性化點。但我不確定我如何正式證明這種算法的正確性。等待免費算法正確性證明的一般方法

在搜索類似的論文時，我發現他們已經證明算法是無等待的，只能生成可線性執行。這種情況是必要的還是充足的？

是否有任何其他正式的方法來證明等待自由算法的正確性？

來源

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

等待免費算法正確性證明的一般方法

回答

相關問題