Как объединить процессы в Promela?

Я создаю модель с помощью Promela, и мне нужно дождаться завершения 2 процессов, чтобы продолжить. Как я могу добиться этого с помощью Promela?


multithreading promela spin
person Rafael Marinho    schedule 19.07.2018    source источник

Ответы (1)


arrow_upward
3
arrow_downward

Во-первых: краткое изложение теории.

В 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 должен поймать, когда другой процесс эффективно завершается и его ресурсы освобождаются системой

Использование: случай 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");
}
person Patrick Trentin    schedule 19.07.2018