如何在没有超时/死锁的情况下在 PROMELA 进程中发送和接收？

Question

我无法解决这个 PROMELA 问题：我有 N 个进程 ("pc")，它们可以通过通道 ("to_pc") 发送和接收消息。每个进程都有自己的接收消息的通道。对于能够接收的进程，我必须将它保持在一个循环中，该循环检查传入消息的通道。作为第二个循环选项，进程向所有其他通道发送消息。

然而，在模拟模式下，这总是导致超时，根本没有发送任何东西。到目前为止，我的理论是我创建了一个死锁，所有进程都想立即发送，导致它们都无法接收（因为它们卡在代码的 "send" 部分）。

到目前为止，我一直无法解决这个问题。我尝试使用一个全局变量作为 "forbid" 发送的信号量，这样只有一个通道可以发送。然而，这并没有改变结果。我唯一的另一个想法是使用超时作为发送的触发器，但这对我来说似乎根本不正确。

有什么想法吗？提前致谢！

#define N 4

mtype={request,reply}

typedef message {
    mtype type;
    byte target;
    byte sender;
};

chan to_pc[N] = [0] of {message}

inline send() {
    byte j = 0;
    for (j : 0 .. N-1) {
        if
        :: j != address ->
            to_pc[j]!msg;
        :: else;
        fi
    }
}

active [N] proctype pc(){
    byte address = _pid;
    message msg;

    do
    :: to_pc[address]?msg -> /* Here I am receiving a message. */
        if
        ::msg.type == request->
            if
            :: msg.target == address ->
                d_step {
                    msg.target = msg.sender
                    msg.sender = address;
                    msg.type = reply;
                }
                send();
            :: else
            fi
        :: msg.type == reply;
        :: else;
        fi
    :: /* Here I want to send a message! */
        d_step {
            msg.target = (address + 1) % N;
            msg.sender = address;
            msg.type = request;
        }
        send();
    od
};

Answer 1

如果你愿意，我可以为你的源代码写一个full-fledged工作版本，但也许这就足够了突出显示您正在处理的问题的根源，让您享受解决它的乐趣。

分支规则

任何具有可执行条件的分支都可以采用，non-deterministically
如果 no 分支具有 可执行 条件，则采用 else 分支
如果 no 分支具有 可执行 条件且 no 分支，则进程挂起，直到其中一个条件变为真

考虑一下

1: if
2:    :: in?stuff -> ...
3:    :: out!stuff -> ...
4: fi

其中in和out都是同步通道（大小为0）。

然后

如果有人在in的另一端发送那么in?stuff是可执行的，否则不是
如果有人在out的另一端接收那么out!stuff是可执行的，否则不是
第 1: 行阻塞进程，直到两个条件中的至少一个 可执行 。

将该代码与此代码进行比较

1: if
2:    :: true -> in?stuff; ...
3:    :: true -> out!stuff; ...
4: fi

其中 in 和 out 又是 同步通道 （大小为 0）。

然后

两个分支都有一个可执行条件（true）
进程立即将自己提交给发送或接收某事，通过non-deterministically 选择在 2: 行或 3:
如果进程选择 2: 那么它阻塞如果 in?stuff 不可执行，即使 out!stuff 将是可执行的
如果进程选择 3: 那么它阻塞如果 out!stuff 不可执行，即使 in!stuff 将是可执行的

您的代码属于后一种情况，因为 d_step { } 中的所有指令都是 executable 并且您的进程过早提交 send。

总结：为了修复您的模型，您应该重构您的代码，以便始终可以从发送跳转到接收模式，反之亦然。 提示：摆脱内联代码，将发送决定与实际发送分开。

如何在没有超时/死锁的情况下在 PROMELA 进程中发送和接收？

How to send and receive in a PROMELA process without timeout / deadlock?

deadlock

timeout

send

promela