如何在 Promela 中加入流程？

Question

我正在使用 Promela 制作模型，我需要等待 2 个进程结束才能继续。我如何使用 Promela 实现这一目标？

Answer 1

第一：理论回顾

在 Promela 中，进程在到达其代码末尾时结束，即

active proctype example() 
{
    /* some code */

    /* here it ends */
}

当进程结束时，它已准备好被系统终止。被终止意味着以下事情：

• 进程使用的 _pid 被释放，现在可以被稍后实例化的任何其他 new 进程重新使用。
• 进程使用的任何资源都被释放并释放

但是，请注意进程终止存在一些约束：

• 一个进程p_i只有在它处于结束状态并且不存在其他_pid值大于p_i的进程p_j时才会终止而且它还活着。

换句话说，进程只能按照创建顺序的相反顺序终止，如 docs.

中所示

此限制很重要，因为在 Spin 中，在任何给定时刻最多只能有 255 个进程同时处于活动状态。任何使用 run 生成大量进程的尝试都将被阻止，除非某些现有进程已同时正确终止以为新进程腾出空间。

---

第二：加入。

现在，要实施 join 操作，我们首先必须确定这样做对我们意味着什么：

1. 当另一个进程在其执行中达到某个 end state 时，join 应该捕获
2. 当另一个进程有效终止并且其资源被系统释放时，join 应该捕获

---

实施：案例 1)

第一种情况绝对容易设计和实现。我们只需要进程之间的一些 同步 机制，以便通知给定的 end state 已经达到。

这可以通过多种方式完成，具体取决于您想要建模的行为风格。这是一个可能的实现：

mtype = { END };

proctype do_something(chan out)
{
    printf("proc[%d]: doing something ...\n", _pid);

end:
    out!_pid, END;
}

init {
    chan in = [5] of { mtype };
    pid pids[5];
    byte idx;

    /* atomic{} is optional here */
    atomic {
        for (idx: 0 .. 4) {
            pids[idx] = run do_something(in);
        }

        printf("init: initialized all processes ...\n");
    }

    /* join section */

    for (idx: 0 .. 4) {
        in??eval(pids[idx]), END;

        printf("init: joined process %d ... \n", pids[idx]);
    }
}

---

实现：案例 2)

第二种情况的建模有点复杂，据我所知，它可能有一些局限性，在某些设计下并不完全可行。

此方法依赖于变量 _nr_pr 的值，这是一个预定义的全局只读变量，记录当前 运行.

的进程数

一个可以：

A. 将我们以相反的创建顺序生成的所有进程一一加入

proctype do_something()
{
    printf("proc[%d]: doing something ...\n", _pid);

end:
    /* nothing to do */
}

init {
    pid pids[5];
    byte idx;

    /* atomic{} is optional here */
    atomic {
        for (idx: 0 .. 4) {
            pids[idx] = run do_something();
        }

        printf("init: initialized all processes ...\n");
    }

    /* join section */

    for (idx: 0 .. 4) {
        (_nr_pr <= pids[4 - idx]);

        printf("init: joined process %d ... \n", pids[4 - idx]);
    }
}

B. 立即加入我们生成的所有进程

proctype do_something()
{
    printf("proc[%d]: doing something ...\n", _pid);

end:
    /* nothing to do */
}

init {
    pid pids[5];
    byte idx;

    /* atomic{} is optional here */
    atomic {
        for (idx: 0 .. 4) {
            pids[idx] = run do_something();
        }

        printf("init: initialized all processes ...\n");
    }

    /* join section */

    (_nr_pr <= pids[0]);

    printf("init: all children terminated ... \n");
}