Блокировка между N процессами в Promela

Я пытаюсь смоделировать один из моих проектов в promela для проверки модели. При этом у меня есть N узлов в сети. Итак, для каждого узла я делаю процесс. Что-то вроде этого:

init {
byte proc;
atomic {
    proc = 0;
    do
    :: proc < N ->
        run node (q[proc],proc);
        proc++
    :: proc >= N ->
        break
    od
}
}

Итак, в основном здесь каждый «узел» — это процесс, который будет имитировать каждый узел в моей сети. Теперь Node Process имеет 3 потока, которые выполняются параллельно в моей исходной реализации, и в этих трех потоках у меня есть блокировка в какой-то части, чтобы три потока не обращались к критическому разделу одновременно. Итак, для этого в промеле я сделал что-то вроде этого:

proctype node (chan inp;byte ppid)
{
   run recv_A()
   run send_B()
   run do_C()
}

Итак, здесь recv_A, send_B и do_C — это три потока, работающих параллельно на каждом узле в сети. Теперь проблема в том, что если я поставлю блокировку в recv_A, send_B, do_C с помощью atomic, тогда она поставит блокировку на все 3 * N процессов, тогда как я хочу такую ​​блокировку, чтобы блокировка применялась к группам из трех. То есть, если recv_A процесса 1 (процесса основного узла, из которого выполняется recv_A) находится в его CS, тогда только send_B и do_C процесса 1 должны быть запрещены для входа в CS, а не recv_A, send_B, do_C процесса 2. Есть ли способ сделать это?


verification promela spin model-checking
person Carol    schedule 01.11.2017    source источник

Ответы (1)


arrow_upward
0
arrow_downward

У вас есть несколько вариантов, и все они связаны с реализацией некоего алгоритма взаимного исключения среди N процессов:

Реализация алгоритма Black & White Bakery доступна здесь. Обратите внимание, однако, что эти алгоритмы — возможно, за исключением алгоритма Петерсона — имеют тенденцию быть сложными и могут сделать проверку вашей системы непрактичной.

Несколько простой подход заключается в использовании Алгоритма проверки и установки, который, однако, по-прежнему использует atomic в разделе тестирования. Вот пример реализации, взятый из здесь.

bool lock = false;
int counter = 0;

active [3] proctype mutex()
{
  bool tmp = false;

trying:
  do
    :: atomic {
       tmp = lock;
       lock = true;
       } ->
       if
          :: tmp;
          :: else -> break;
       fi;
  od;

critical:
    printf("Process %d entered critical section.\n", _pid);
    counter++;
    assert(counter == 1);
    counter--;

exit:
    lock = false;
    printf("Process %d exited critical section.\n", _pid);

goto trying;
}

#define c0 (mutex[0]@critical)
#define c1 (mutex[1]@critical)
#define c2 (mutex[2]@critical)
#define t0 (mutex[0]@trying)
#define t1 (mutex[1]@trying)
#define t2 (mutex[2]@trying)
#define l0 (_last == 0)
#define l1 (_last == 1)
#define l2 (_last == 2)
#define f0 ([] <> l0)
#define f1 ([] <> l1)
#define f2 ([] <> l2)

ltl p1 { []   !(c0  &&  c1)  && !(c0 && c2) && !(c1 && c2)}
ltl p2 { []((t0 || t1 || t2) -> <> (c0 || c1 || c2)) }
ltl p3 {
        (f0 -> [](t0 -> <> c0))
        &&
        (f1 -> [](t1 -> <> c1))
        &&
        (f2 -> [](t2 -> <> c2))
        };

В своем коде вы должны использовать разные переменные lock для каждой группы потоков, связанных 3. Конфликт за блокировку по-прежнему будет происходить на глобальном уровне, но какой-либо процесс, работающий внутри критического раздела, не будет заставлять другие процессы ждать, кроме тех, которые принадлежат к той же группе потоков.

Другая идея состоит в том, чтобы использовать каналы для достижения взаимного исключения: каждая группа потоков использует общий асинхронный канал, который изначально содержит одно сообщение token. Всякий раз, когда один из этих потоков хочет получить доступ к критической секции, он читает из канала. Если token не находится внутри канала, он ждет, пока не станет доступным. В противном случае он может продолжить работу в критической секции, а когда он завершится, он поместит token обратно в общий канал.

proctype node (chan inp; byte ppid)
{
   chan lock = [1] of { bool };
   lock!true;

   run recv_A(lock);
   run send_B(lock);
   run do_C(lock);
};

proctype recv_A(chan lock)
{
    bool token;
    do
        :: true ->

            // non-critical section code
            // ...

            // acquire lock
            lock?token ->

            // critical section
            // ...

            // release lock
            lock!token

            // non-critical section code
            // ...
    od;
};

...

Этот подход может быть самым простым для начала, поэтому я бы выбрал его первым. Однако обратите внимание, что я понятия не имею, как это влияет на производительность во время проверки, и это вполне может зависеть от того, как каналы обрабатываются внутри Spin. Полный пример кода этого решения можно найти здесь в файл channel_mutex.pml.

В заключение обратите внимание, что вы можете добавить в свою модель свойства взаимное исключение, прогресс и свобода от блокировки LTL, чтобы убедиться, что она работает правильно. . Пример определения этих свойств доступен здесь, а код Пример доступен здесь.

person Patrick Trentin    schedule 02.11.2017