2

到目前为止，我已经为我的项目做了一点代码，但不知道它是真是假。你们能看到我的代码吗？首先，我应该发布要求以更好地理解..

在计算机科学中，互斥是指确保没有两个进程或线程同时处于其临界区的要求。临界区是指进程访问共享资源（如共享内存）的一段时间。互斥问题由 Edsger W. Dijkstra 于 1965 年在他的论文《并发编程控制问题的解决方案》中首次发现并解决。

有关问题的直观描述，请参见图。在链表中，节点的删除是通过将前一个节点的“下一个”指针更改为指向后续节点来完成的（例如，如果节点 i 正在被删除，那么节点 i-1 的“下一个”指针将是改为指向节点 i+1)。在多个进程之间共享这样一个链表的执行中，两个进程可能会尝试同时删除两个不同的节点，从而导致以下问题：设节点 i 和 i+1 为要删除的节点；此外，不要让他们成为头或尾；节点 i-1 的 next 指针将更改为指向节点 i+1，节点 i 的 next 指针将更改为指向节点 i+2。尽管两个删除操作都成功完成，节点 i+1 保留在列表中，因为 i-1 指向 i+1 跳过节点 i（该节点通过将下一个指针设置为 i+2 来反映 i+1 的删除）。可以使用互斥来避免此问题，以确保不会同时更新列表的同一部分。

在此处输入图像描述

这是我的代码：

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
4

1 回答 1

2

首先，您要建模什么？看来您唯一有兴趣证明作为定理的是类型不变量。我原以为您想证明一些关于互斥的事情，而不仅仅是 and 的可能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-01T16:47:50.273 回答