如何加入Promela的进程？

Question

我正在用Promela制作一个模型，我需要等待两个过程才能结束，这样才能继续。我怎么能用Promela来达到这个目的呢？

Answer 1

First:理论概述.

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

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

    /* here it ends */
}

当进程结束时，它已经准备好由系统以终止。终止意味着以下几点：

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

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

• 进程p_i只有在处于其结束状态时才被终止，并且没有任何其他进程p_j的_pid值大于p_i的值，并且它仍然活着。

换句话说，进程只能按照创建过程的相反顺序终止，如文档中所示。

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

第二:加入.

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

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

Impl:案例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]);
    }
}

Impl:案例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");
}