這個TLA +規範是否正確？

到目前爲止，我已經爲我的項目做了一些代碼，但不知道它是真是假。你們能看到我的代碼嗎？首先，我應該提出更好的理解要求。這個TLA +規範是否正確？

在計算機科學中，互斥是指確保兩個進程或線程同時處於關鍵部分的要求。關鍵部分是指進程訪問共享資源（例如共享內存）的時間段。互斥問題最早由Edsger W. Dijkstra在1965年的題爲「解決併發編程控制問題的文章」中找到並解決。

有關問題的直觀描述，請參見圖。在鏈表中，通過改變前一節點的「下一個」指針指向後續節點來完成節點的移除（例如，如果移除節點i，則節點i-1的「下一個」指針將是改爲指向節點i + 1）。在多個進程之間共享這樣的鏈表的執行中，兩個進程可能試圖同時移除兩個不同的節點，導致以下問題：讓節點i和i + 1成爲要移除的節點;此外，既不是頭部也不是尾巴;節點i-1的下一個指針將改變爲指向節點i + 1，並且節點i的下一個指針將改變爲指向節點i + 2。儘管兩個刪除操作都成功完成，但是由於i-1指向i + 1跳過節點i（這是通過將下一個指針設置爲i來反映刪除i + 1的節點），節點i + 1仍然保留在列表中I + 2）。使用互斥可以避免此問題，以確保不會同時更新列表的同一部分。

enter image description here

這是我的代碼：

EXTENDS Naturals 
CONSTANT Unlocked, Locked 
VARIABLE P1,P2 

TypeInvariant == /\ P1 \in {Unlocked,Locked} 
      /\ P2 \in {Unlocked,Locked} 


Init == /\ TypeInvariant 
     /\ P1 = Unlocked 


Remove1 == P2' = Locked 
Remove2 == P1' = Locked 

Next == Remove1 \/ Remove2 

Spec == Init /\ [][Next]_<<P1,P2>> 
THEOREM Spec => []TypeInvariant

來源

2013-12-18 Norlihazmey Ghazali

你想實現什麼？互斥體如何與刪除鏈表中的元素相關？我認爲你可以改善這個問題。順便說一句，你有沒有試過閱讀Lamport的並行系統原理和規範第7章：http：//research.microsoft.com/en-us/um/people/lamport/tla/hyperbook.html – marcmagransdeabril

首先，你有什麼模型？看起來你感興趣的唯一證明是定理的是類型不變式。我原以爲你想證明一些關於互斥的東西，而不僅僅是P1和P2的可能值。例如，你是否想證明P1和P2永遠都不會同時被鎖定？

MutualExclusion == ~(P1 = Locked /\ P2 = Locked) 
THEOREM MutualExclusionTheorem == Spec => []MutualExclusion

而且，我不會把TypeInvariant在Init定義。您的Init應包含變量P1和P2的起始值。那麼你有一個定理，

THEOREM InitTypeInvariant == Init => TypeInvariant

並證明它。這個定理將用於定理Spec的證明。

來源

2017-08-01 16:47:50

並提出了問題的道歉從死者回來：D –

這個TLA +規範是否正確？

回答

相關問題