Как изменить порядок сообщений в канале? - PullRequest
Новая
       34

Как изменить порядок сообщений в канале?

0 голосов
/ 16 января 2019

Мне нужно изменить этот код, чтобы каналы могли переупорядочивать сообщения, и мне нужно добавить механизм, чтобы справиться с этим 

chan linkA = [10] of {byte};
chan linkB = [10] of {byte};
proctype sender ()
{ byte n;
do
:: n<10 -> linkA!n*n; n++;
linkB!n*n; n++
:: else -> break
od
}
proctype receiver (chan link)
{ byte m,i; byte result[5];
do
:: i<5 -> link?m -> result[i]=m; i++
:: else -> break
od
}
init
{
run sender ();
run receiver (linkA);
run receiver (linkB)
}

Я создал новый процесс, у которого есть параметр канала (linkC) В процессе переупорядочения канал получит две переменные (байт x), которые представляют байт данных и (байт s) индекс результата. Как следствие, объявление каналов получателю было изменено на получение {байт, байт}

Также я изменил процесс получения 

1   chan linkA = [10] of {byte , byte};
2   chan linkB = [10] of {byte, byte};
3   
4   proctype sender ()
5   { byte n;
6   do
7   :: n<10 -> linkA!!n*n; n++;
8              linkB!!n*n; n++
9   :: else -> break
10  od
11  }
12  proctype reorder (chan linkC)
13  {
14  byte x;
15  byte s;
16  end1:
17  do
18  :: linkC ? x,s -> linkC !x,s
19  od
20  }
21  proctype receiver (chan link)
22  { byte m,i; 
23  byte result[5];
24  byte from_proc;
25  do
26  :: i<5 -> link?from_proc,m -> result[i]=from_proc; i++
27  :: else -> break
28  od
29  }
30  init
31  {
32  run sender ();
33  run reorder (linkA);
34  run reorder (linkB);
35  run receiver (linkA);
36  run receiver (linkB)
37  }

чтобы справиться с повторным заказом, я добавил !! (сортированная операция отправки)

но код не работает так, как я хочу, и я не знаю, в чем проблема.

1 Ответ

0 голосов
/ 16 января 2019

В вашем решении проблема в том, что сообщения изначально сортируются по sender в точном порядке их создания, что также соответствует возрастающему порядку значений. Процесс reorder в вашем образце модели, на самом деле, мало что дает. Он берет первое сообщение из очереди и помещает его в конец очереди. Если очередь содержит k сообщений, после шагов k сообщения снова сортируются в соответствии с первоначальным порядком.

Я вижу три возможных подхода к решению этой проблемы:

  • напрямую генерирует сообщения в случайном порядке, так что нет необходимости переупорядочивать их позже

  • помещает случайно сгенерированное начальное число в первое поле каждого сообщения и откладывает выполнение receiver до тех пор, пока все сообщения не окажутся в очереди, чтобы при использовании случайным образом сообщения помещались в очередь сообщений. отсортировано отправить

  • использует случайный прием вместе с eval(idx), чтобы receiver читал сообщения в случайном порядке, даже если сообщения в очереди идеально отсортированы. Это устраняет проблему синхронизации receiver с sender, но требует receiver, чтобы узнать что-то больше о содержании сообщения, например, idx каждого сообщения.

Решение, следующее за вторым подходом, описанным выше: 

chan linkA = [10] of {byte, byte};
chan linkB = [10] of {byte, byte};
bool synch = false;

proctype sender ()
{
    byte i;
    byte idx;

    for (i : 0 .. 5) {
        int n = 2*i;
        select(idx:0..255);
        printf("Sender: <%d, %d> to linkA\n", idx, n*n);
        linkA!!idx,n*n;
        n = n + 1;
        select(idx:0..255);
        printf("Sender: <%d, %d> to linkB\n", idx, n*n);
        linkB!!idx,n*n;
    }
    synch = true;
}

proctype receiver (chan link)
{
    byte i, idx;
    byte result[6];

    /* wait until all messages in the queue */
    synch;

    for (i : 0 .. 5) {
        link?idx,result[i];
        printf("Receiver(%d): <%d, %d>\n", _pid, idx, result[i]);
    }
}

init
{
    run sender ();
    run receiver (linkA);
    run receiver (linkB)
}

Вывод: 

~$ spin test.pml 
          Sender: <0, 0> to linkA
          Sender: <3, 1> to linkB
          Sender: <2, 4> to linkA
          Sender: <1, 9> to linkB
          Sender: <1, 16> to linkA
          Sender: <0, 25> to linkB
          Sender: <0, 36> to linkA
          Sender: <0, 49> to linkB
          Sender: <4, 64> to linkA
          Sender: <2, 81> to linkB
          Sender: <0, 100> to linkA
          Sender: <0, 121> to linkB
                  Receiver(3): <0, 25>
                  Receiver(3): <0, 49>
              Receiver(2): <0, 0>
                  Receiver(3): <0, 121>
              Receiver(2): <0, 36>
                  Receiver(3): <1, 9>
                  Receiver(3): <2, 81>
              Receiver(2): <0, 100>
                  Receiver(3): <3, 1>
              Receiver(2): <1, 16>
              Receiver(2): <2, 4>
              Receiver(2): <4, 64>
4 processes created

Обратите внимание, что idx генерируется случайным образом и что модель допускает выполнения, в которых каждое сообщение имеет различное значение idx.

...