1

我正在构建一个 Promela 模型，其中一个进程向 N 个其他进程发送请求，等待回复，然后计算一个值。基本上是典型的 map-reduce 风格的执行流程。目前我的模型以固定的顺序发送请求。我想将其概括为发送不确定的订单。我已经查看了该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();
  }
}
4

1 回答 1

2

从您的问题中，我了解到您希望以随机顺序将任务分配给给定进程，而不是简单地将随机任务分配给有序的进程序列。

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

#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分配了自己的任务，因此他们都可以或多或少地同时开始。

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

  • 对象被随机分配任务
  • 对象可以以不同的随机顺序完成任务
~$ 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应该先初始化一些有意义的内容。

于 2017-11-14T09:16:03.500 回答