Nachricht an Kanalgruppe in nichtdeterministischer Reihenfolge senden

Question

Ich baue ein Promela-Modell, in dem ein Prozess eine Anforderung an N andere Prozesse sendet, auf die Antworten wartet und dann einen Wert berechnet. Im Wesentlichen ein typischer Map-Reduct-Style-Ausführungsfluss. Derzeit sendet mein Modell Anfragen in einer festen Reihenfolge. Ich möchte das verallgemeinern, um eine nicht-deterministische Ordnung zu senden. Ich habe die select Anweisung angeschaut, aber das scheint ein einzelnes Element nicht-deterministisch auszuwählen.

Gibt es ein gutes Muster, um dies zu erreichen? Hier ist die Grundstruktur von dem, was ich arbeite mit:

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

Dies ist das Objekt Prozess, der mit einem gewissen Wert zu msgtype Nachrichten antwortet, dass es berechnet.

proctype Object(chan request) { 
    chan reply; 

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

Dies ist der Client. Er sendet eine Anforderung an jedes der Objekte in der Reihenfolge 0, 1, 2, ... und sammelt alle Antworten und reduziert die Werte.

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 
    } 
} 

Und ich starten Sie das System wie dieses

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

Answer 1

Aus Ihrer Frage entnehme ich, dass Sie eine Aufgabe zu einem bestimmten Prozess in einer randomisierten, um zuweisen möchten, im Gegensatz zu einfach zuweisen eine zufällige Aufgabe zu einer geordneten Folge von Prozessen.

Alles in allem ist die Lösung für beide Ansätze sehr ähnlich. Ich weiß nicht, ob der, den ich vorschlagen werde, der eleganteste Ansatz ist.

#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; 
}; 

Die Idee ist es, ein array haben, die wie ein map aus dem Satz von Indizes in die Ausgangsposition wirkt (oder, in äquivalenter Weise, auf die zugeordnete Aufgabe). Die map ist dann verschlüsselt durch eine endliche Anzahl von swap Operationen. Danach erhält jede object ihre eigene Aufgabe in parallel, so dass sie alle mehr oder weniger zur gleichen Zeit starten können.

---

Im folgenden Ausgabebeispiel, können Sie sehen, dass:

• Objekte werden eine Aufgabe in einer Reihenfolge Zufalls zugewiesen
• Objekte kann führen Sie die Aufgabe in ein verschieden zufällig bestellen

~$ 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 
... 

---

Wenn man eine zufällige Aufgabe zu jeder object zuweisen will, anstatt sie zu starten zufällig, dann genügt es, zu ändern:

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

in:

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

Offensichtlich sollte data initialisiert werden zu einem sinnvollen Inhalt zuerst.