进程未终止导致 "too many processes" 错误

Question

我是第一次使用spin，遇到了一个我不明白的错误。我知道进程终止的顺序与它们创建的顺序相同，因此我不明白为什么我在循环中调用的函数的进程没有终止。这是我的代码的一个非常简化的版本：

int limit;

proctype f() {
    limit--;
    printm(limit)
    run g();
}

proctype g() {
    limit++;
}

init {
    limit = 5;
    do
        :: (limit > 0) -> run f();
    od
}

限制变量已创建，因此同时存在的进程不超过 5 个 f 运行。进程 g 会终止，但 f 不会。所以我得到错误：too many processes 我想知道为什么 f 没有终止，是否有其他方法可以做到这一点？

Answer 1

你的问题是基于一个错误的前提：你的系统中进程永远不会超过 5 个是不正确的。

事实上，f()类型的进程可以有任意多个，因为绝对不能保证指令：

limit--;

在使用

创建进程后立即执行

run f();

进程调度程序可能让 init() 在抢占它之前执行几个（数十、数百、更多..）循环迭代并给一些 f() 执行任何东西的机会.

如果创建了一个进程g()，那么这显然可以终止。

如果创建了一个进程 f()，只有当系统中还没有 255 个进程并且进程 f() 最高 pid，这样就不用等待其他进程了。

init() 进程永远不会终止。

作为可能的解决方法，您可能想尝试查看 _nr_pr:

int limit = 5;

proctype f() {
    printm(limit)
}

init {
    do
        :: (_nr_pr <= (limit + 1)) ->
                run f();
    od
}

进程未终止导致 "too many processes" 错误

Process not terminated causing a "too many processes" error

spin

promela