How to join processes in Promela?

I'm making a model with Promela and I need to wait 2 processes to end in order to continue. How can I achieve that with Promela?

First: theory recap.

In Promela, a process ends when it reaches the end of its code, i.e.

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

    /* here it ends */
}

When a process ends, it is ready for being terminated by the system. Being terminated means the following things:

• the _pid used by the process is freed and can now be re-used by any other new process being instantiated later on.
• any resource used by the process is freed and released

However, notice that there exist some constraints on processes termination:

• a process p_i is terminated only when it is in its end state and there exists no other process p_j whose _pid value is larger than that of p_i and that it is still alive.

In other words, processes can only be terminated in reverse order of their creation, as indicated in the docs.

This limitation is important because in Spin there can be only up to 255 processes that are concurrently alive at any given moment. Any attempt to spawn a larger amount of processes with run will block, unless some of the existing processes have been correctly terminated in the meanwhile to make room for new processes.

---

Second: join.

Now, to implement the join operation, we first have to decide what it means for us to do that:

1. the join should catch when another process reaches a certain end state in its execution
2. the join should catch when another process is effectively terminated and its resources are freed by the system

---

Impl: case 1)

The first situation is definitively easy to design and implement. We merely need some synchronization mechanism among processes so as to notify that the given end state has been reached.

This can be done in several ways, depending on the kind of behavioural flavour you want to model. Here is a possible implementation:

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: case 2)

The second situation is a bit more complicated to model and, to the extent of my knowledge, it might have some limitations and not being entirely feasible under certain designs.

This approach relies on the value of the variable _nr_pr, which is a predefined, global, read-only variable recording the number of processes that are currently running.

One can either:

A. join one by one all processes we have spawned in reverse order of creation

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. join all processes we have spawned at once

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");
}