Process not terminated causing a "too many processes" error

Question

It is my first time using spin and I am encountering an error that I do not understand. I am aware that the processes terminates in the same order they are created thus I don't understand why the process of the function I call in a loop does not terminate. Here is a very simplified version of my code :

int limit;

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

proctype g() {
    limit++;
}

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

The limit variable is created so there is not more than 5 processes f running at the same time. The processes g does terminate but f don't. So I get the error : too many processes I would like to know why f does not terminate and if there is another way to do that?

Answer 1

Your question is based on a false premise: it isn't true that there are never more than 5 processes in your system.

In fact, there can be any number of processes of type f(), because there is absolutely no guarantee that the instruction:

limit--;

is executed right after the process is created with

run f();

It is possible that the process scheduler lets init() execute for several (tens, hundreds, more..) loop iterations before it preempts it and gives a chance to some f() to execute anything.

If a process g() is created, then this can clearly terminate.

If a process f() is created, this can terminate only if there aren't already 255 processes in the system and it is the process f() with the highest pid, so that it does not have to wait for other processes.

The init() process can never terminate.

---

As a possible fix, you might want to try to look into _nr_pr:

int limit = 5;

proctype f() {
    printm(limit)
}

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