concurrencypromelaspin

When to use semaphore locks / unlocks vs. wait / notify?


I'm learning Promela and using SPIN to model some examples I found. This model involves a food ordering simulation. So the customer orders, cashier takes order, sends to server, back to customer etc.

Here is a flow of the program.

The specific processes are as followed.

Here is the code I have written so far:

#define NCUSTS 3    /* number of customers */
#define NCASHIERS 1 /* number of cashiers */
#define NSERVERS 1  /* number of servers */
#define NOBODY 255

#define semaphore byte   /* define a sempahore */

/*
 * lock (down) and unlock (up) functions for mutex semaphores
 */
inline unlock(s) {s++;}
inline lock(s) {atomic{ s>0 ; s--}}

/*
 * wait (down) and notify (up) functions for signaling semaphores
 */
inline notify(s) {s++;}
inline wait(s) {atomic{ s>0 ; s--}}

mtype = {CHILI, SANDWICH, PIZZA, NULL} ; // the types of foods (added null for resets)
mtype favorites[NCUSTS];
mtype orders[NCUSTS] = NULL;

byte ordering = NOBODY;

semaphore waitingFood[NCUSTS] = 1;
semaphore cashierOpen = 1;
semaphore serverOpen = 1;

bool waiting[NCUSTS] = false;


/*
 * Process representing a customer.
 * Takes in their favorite food and an integer id
 * to represent them
 */
proctype Customer(mtype favorite; byte id)
{
    /* customer cycle */
    do
    ::

        //Enter
        printf("Customer %d Entered\n", id);

        //Record
        favorites[id] = favorite;

        //Wait for cashier
        cashierOpen > 0;
        atomic{
            lock(cashierOpen);
            printf("Cashier selects customer %d\n", id);
            ordering = id;
        }
        //Order
        orders[id] = favorite;
        printf("Customer orders %e\n", favorite);
        unlock(cashierOpen);
        ordering = NOBODY;


        printf("Customer %d is waiting for %e\n", id, favorite);
        waiting[id] = true;
        wait(waitingFood[id]);
        waitingFood[id] > 0;

        printf("Customer %d recieves food and leaves\n", id);
        favorites[id] = NULL;
        orders[id] = NULL;

    od ;
}

/*
 * Process representing a cashier
 */
proctype Cashier()
{
    do
    ::
        printf("Cashier is waiting for a customer\n");
        cashierOpen < 1;
        printf("Cashier takes the order of Customer %d\n", ordering);
        serverOpen > 0;
        printf("Cashier passes order to server\n");
    od ;
}

/*
 * Process representing a server 
 */
proctype Server()
{

    byte id;
    do
    ::
        printf("Server is waiting for order\n");
        for(id : 0..2){
            if
            ::  waiting[id] ->
                lock(serverOpen);
                printf("Server creates order of %e for %d\n", orders[id], id);
                printf("Server delivers order of %e to %d\n", orders[id], id);
                notify(waitingFood[id]);
                unlock(serverOpen);
            ::  else ->
                    skip;
            fi;
        }
    od ;

}

/*
 * Sets up processes. This model creates two
 * customers with the favorite foods PIZZA & CHILI.
 */
init{

    atomic{
        run Customer(PIZZA, 0) ;
        run Customer(CHILI, 1) ;
        run Cashier();
        run Server();       
    }
}

Clearly, the program does not work as I expected. Could someone help me understand how to use semaphores and when to use locks unlocks waits and notifies here?


Solution

  • This part of your model has to be changed:

    ::  waiting[id] ->
        ...
        notify(waitingFood[id]);
        ...
    

    When waitingFood[id] is released by the Server, the Customer does not immediately turn waiting[id] to false, so it is possible that the Server handles the same Customer's request more than once (actually, it is very likely to happen).

    In fact, by adding the following ltl property to the model:

    ltl p0 { [] (waitingFood[0] < 2) };
    

    and then checking the property, it is confirmed that the variable waitingFood can be assigned an "incorrect" value:

    ~$ spin -search -bfs t.pml
    ltl p0: [] ((waitingFood[0]<2))
    Depth=      10 States=       13 Transitions=       13 Memory=   128.195 
    Depth=      20 States=      620 Transitions=      878 Memory=   128.195 
    pan:1: assertion violated  !( !((waitingFood[0]<2))) (at depth 22)
    pan: wrote t.pml.trail
    
    (Spin Version 6.4.8 -- 2 March 2018)
    Warning: Search not completed
        + Breadth-First Search
        + Partial Order Reduction
    
    Full statespace search for:
        never claim             + (p0)
        assertion violations    + (if within scope of claim)
        cycle checks        - (disabled by -DSAFETY)
        invalid end states  - (disabled by never claim)
    
    State-vector 60 byte, depth reached 22, errors: 1
         1242 states, stored
            1239 nominal states (stored-atomic)
          684 states, matched
         1926 transitions (= stored+matched)
            3 atomic steps
    hash conflicts:         0 (resolved)
    
    Stats on memory usage (in Megabytes):
        0.104   equivalent memory usage for states (stored*(State-vector + overhead))
        0.381   actual memory usage for states
      128.000   memory used for hash table (-w24)
      128.293   total actual memory usage
    
    pan: elapsed time 0 seconds
    

    The problematic trace is:

    ~$ spin -p -g -l -t t.pml
    ltl p0: [] ((waitingFood[0]<2))
    starting claim 4
    using statement merging
    Starting Customer with pid 2
      1:    proc  0 (:init::1) t.pml:124 (state 1)  [(run Customer(PIZZA,0))]
    Starting Customer with pid 3
      2:    proc  0 (:init::1) t.pml:125 (state 2)  [(run Customer(CHILI,1))]
    Starting Cashier with pid 4
      3:    proc  0 (:init::1) t.pml:126 (state 3)  [(run Cashier())]
    Starting Server with pid 5
      4:    proc  0 (:init::1) t.pml:127 (state 4)  [(run Server())]
                              Server is waiting for order
      5:    proc  4 (Server:1) t.pml:100 (state 1)  [printf('Server is waiting for order\\n')]
      5:    proc  4 (Server:1) t.pml:101 (state 2)  [id = 0]
            Server(4):id = 0
      6:    proc  4 (Server:1) t.pml:101 (state 3)  [((id<=2))]
                          Cashier is waiting for a customer
      7:    proc  3 (Cashier:1) t.pml:83 (state 1)  [printf('Cashier is waiting for a customer\\n')]
                      Customer 1 Entered
      8:    proc  2 (Customer:1) t.pml:45 (state 1) [printf('Customer %d Entered\\n',id)]
                  Customer 0 Entered
      9:    proc  1 (Customer:1) t.pml:45 (state 1) [printf('Customer %d Entered\\n',id)]
     10:    proc  1 (Customer:1) t.pml:48 (state 2) [favorites[id] = favorite]
            favorites[0] = PIZZA
            favorites[1] = 0
            favorites[2] = 0
     11:    proc  1 (Customer:1) t.pml:51 (state 3) [((cashierOpen>0))]
     12:    proc  1 (Customer:1) t.pml:12 (state 4) [((cashierOpen>0))]
     12:    proc  1 (Customer:1) t.pml:12 (state 5) [cashierOpen = (cashierOpen-1)]
            cashierOpen = 0
                  Cashier selects customer 0
     12:    proc  1 (Customer:1) t.pml:54 (state 8) [printf('Cashier selects customer %d\\n',id)]
            cashierOpen = 0
     12:    proc  1 (Customer:1) t.pml:55 (state 9) [ordering = id]
            ordering = 0
            cashierOpen = 0
     13:    proc  1 (Customer:1) t.pml:58 (state 11)    [orders[id] = favorite]
            orders[0] = PIZZA
            orders[1] = NULL
            orders[2] = NULL
                  Customer orders PIZZA
     14:    proc  1 (Customer:1) t.pml:59 (state 12)    [printf('Customer orders %e\\n',favorite)]
     15:    proc  1 (Customer:1) t.pml:11 (state 13)    [cashierOpen = (cashierOpen+1)]
            cashierOpen = 1
     16:    proc  1 (Customer:1) t.pml:61 (state 15)    [ordering = 255]
            ordering = 255
                  Customer 0 is waiting for PIZZA
     17:    proc  1 (Customer:1) t.pml:64 (state 16)    [printf('Customer %d is waiting for %e\\n',id,favorite)]
     18:    proc  1 (Customer:1) t.pml:65 (state 17)    [waiting[id] = 1]
            waiting[0] = 1
            waiting[1] = 0
            waiting[2] = 0
     19:    proc  4 (Server:1) t.pml:103 (state 4)  [(waiting[id])]
     20:    proc  4 (Server:1) t.pml:12 (state 5)   [((serverOpen>0))]
     20:    proc  4 (Server:1) t.pml:12 (state 6)   [serverOpen = (serverOpen-1)]
            serverOpen = 0
                              Server creates order of PIZZA for 0
     21:    proc  4 (Server:1) t.pml:105 (state 9)  [printf('Server creates order of %e for %d\\n',orders[id],id)]
                              Server delivers order of PIZZA to 0
     22:    proc  4 (Server:1) t.pml:106 (state 10) [printf('Server delivers order of %e to %d\\n',orders[id],id)]
     23:    proc  4 (Server:1) t.pml:17 (state 11)  [waitingFood[id] = (waitingFood[id]+1)]
            waitingFood[0] = 2
            waitingFood[1] = 1
            waitingFood[2] = 1
    spin: trail ends after 23 steps
    #processes: 5
            favorites[0] = PIZZA
            favorites[1] = 0
            favorites[2] = 0
            orders[0] = PIZZA
            orders[1] = NULL
            orders[2] = NULL
            ordering = 255
            waitingFood[0] = 2
            waitingFood[1] = 1
            waitingFood[2] = 1
            cashierOpen = 1
            serverOpen = 0
            waiting[0] = 1
            waiting[1] = 0
            waiting[2] = 0
     23:    proc  4 (Server:1) t.pml:11 (state 14)
     23:    proc  3 (Cashier:1) t.pml:84 (state 2)
     23:    proc  2 (Customer:1) t.pml:48 (state 2)
     23:    proc  1 (Customer:1) t.pml:18 (state 21)
     23:    proc  0 (:init::1) t.pml:129 (state 6) <valid end state>
     23:    proc  - (p0:1) _spin_nvr.tmp:2 (state 6)
    5 processes created
    

    Here are a few additional comments based on reading your model: