以不确定的顺序向一组通道发送消息

Question

我正在构建一个 Promela 模型，其中一个进程向 N 个其他进程发送请求，等待回复，然后计算一个值。基本上是一个典型的 map-reduce 风格的执行流程。目前我的模型以固定顺序发送请求。我想将其概括为发送一个不确定的订单。我查看了 select 语句，但 select 似乎是一个不确定的单个元素。

是否有实现此目的的良好模式？这是我正在使用的基本结构：

#define NUM_OBJECTS 2
chan obj_req[NUM_OBJECTS] = [0] of { mtype, chan };

这是对象进程，它使用它计算出的某个值来响应 msgtype 消息。

proctype Object(chan request) {
  chan reply;

end:
  do
  :: request ? msgtype(reply) ->
    int value = 23
    reply ! value
  od;
}

这是客户。它按顺序 0, 1, 2, ... 向每个对象发送请求，并收集所有响应并减少值。

proctype Client() {
  chan obj_reply = [0] of { int };
  int value

  // WOULD LIKE NON-DETERMINISM HERE
  for (i in obj_req) {
    obj_req[i] ! msgtype(obj_reply)
    obj_reply ? value
    // do something with value
  }
}

然后我这样启动系统

init {
  atomic {
    run Object(obj_req[0]);
    run Object(obj_req[1]);
    run Client();
  }
}

Answer 1

根据你的问题，我了解到你想分配一个任务给一个随机顺序的给定进程，而不是简单地分配一个随机任务 到有序的流程序列。

总而言之，两种方法的解决方案非常相似。不过，我不知道我要提出的方法是否是最优雅的方法。

#define NUM_OBJECTS 10

mtype = { ASSIGN_TASK };
chan obj_req[NUM_OBJECTS] = [0] of { mtype, chan, int };

init
{
    byte i;
    for (i in obj_req) {
        run Object(i, obj_req[i]);
    }
    run Client();
};

proctype Client ()
{
    byte i, id;
    int value;
    byte map[NUM_OBJECTS];
    int data[NUM_OBJECTS];
    chan obj_reply = [NUM_OBJECTS] of { byte, int };

    d_step {
        for (i in obj_req) {
            map[i] = i;
        }
    }

    // scramble task assignment map
    for (i in obj_req) {
        byte j;
        select(j : 0 .. (NUM_OBJECTS - 1));
        byte tmp = map[i];
        map[i] = map[j];
        map[j] = tmp;
    }

    // assign tasks
    for (i in obj_req) {
        obj_req[map[i]] ! ASSIGN_TASK(obj_reply, data[i]);
    }

    // out-of-order wait of data
    for (i in obj_req) {
        obj_reply ? id(value);
        printf("Object[%d]: end!\n", id, value);
    }

    printf("client ends\n");
};


proctype Object(byte id; chan request)
{
  chan reply;
  int in_data;

end:
  do
    :: request ? ASSIGN_TASK(reply, in_data) ->
        printf("Object[%d]: start!\n", id)
        reply ! id(id)
  od;
};

这个想法是有一个 array，它的作用类似于从索引集到起始位置（或者，等同于分配的任务）的 map。然后 map 通过有限次数的 swap 操作被加扰。之后，每个 object 都被分配了并行自己的任务，因此他们可以同时开始 more-or-less时间。

在下面的输出示例中，您可以看到：

正在以随机顺序
对象可以以不同的随机顺序

~$ spin test.pml
              Object[1]: start!
                                              Object[9]: start!
          Object[0]: start!
                                  Object[6]: start!
                  Object[2]: start!
                                          Object[8]: start!
                          Object[4]: start!
                              Object[5]: start!
                      Object[3]: start!
                                      Object[7]: start!
                                                  Object[1]: end!
                                                  Object[9]: end!
                                                  Object[0]: end!
                                                  Object[6]: end!
                                                  Object[2]: end!
                                                  Object[4]: end!
                                                  Object[8]: end!
                                                  Object[5]: end!
                                                  Object[3]: end!
                                                  Object[7]: end!
                                                  client ends
      timeout
#processes: 11
...

如果想给每个object分配一个随机任务而不是随机开始它们，那么它就足够了变化：

        obj_req[map[i]] ! ASSIGN_TASK(obj_reply, data[i]);

进入：

        obj_req[i] ! ASSIGN_TASK(obj_reply, data[map[i]]);

显然，data应该先初始化一些有意义的内容。

以不确定的顺序向一组通道发送消息

send message to set of channels in non-deterministic order

promela

spin