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












1















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 Enteredn", id);



        //Record

        favorites[id] = favorite;



        //Wait for cashier

        cashierOpen > 0;

        atomic{

            lock(cashierOpen);

            printf("Cashier selects customer %dn", id);

            ordering = id;

        }

        //Order

        orders[id] = favorite;

        printf("Customer orders %en", favorite);

        unlock(cashierOpen);

        ordering = NOBODY;





        printf("Customer %d is waiting for %en", id, favorite);

        waiting[id] = true;

        wait(waitingFood[id]);

        waitingFood[id] > 0;



        printf("Customer %d recieves food and leavesn", id);

        favorites[id] = NULL;

        orders[id] = NULL;



    od ;

}



/*

 * Process representing a cashier

 */

proctype Cashier()

{

    do

    ::

        printf("Cashier is waiting for a customern");

        cashierOpen < 1;

        printf("Cashier takes the order of Customer %dn", ordering);

        serverOpen > 0;

        printf("Cashier passes order to servern");

    od ;

}



/*

 * Process representing a server 

 */

proctype Server()

{



    byte id;

    do

    ::

        printf("Server is waiting for ordern");

        for(id : 0..2){

            if

            ::  waiting[id] ->

                lock(serverOpen);

                printf("Server creates order of %e for %dn", orders[id], id);

                printf("Server delivers order of %e to %dn", 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?






concurrency promela spin







share|improve this question

























  • Well, if you could explain why "Clearly, the program does not work as I expected." that would really speed-up the entire process of helping you..

    – Patrick Trentin
    Nov 29 '18 at 4:52
















1















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 Enteredn", id);



        //Record

        favorites[id] = favorite;



        //Wait for cashier

        cashierOpen > 0;

        atomic{

            lock(cashierOpen);

            printf("Cashier selects customer %dn", id);

            ordering = id;

        }

        //Order

        orders[id] = favorite;

        printf("Customer orders %en", favorite);

        unlock(cashierOpen);

        ordering = NOBODY;





        printf("Customer %d is waiting for %en", id, favorite);

        waiting[id] = true;

        wait(waitingFood[id]);

        waitingFood[id] > 0;



        printf("Customer %d recieves food and leavesn", id);

        favorites[id] = NULL;

        orders[id] = NULL;



    od ;

}



/*

 * Process representing a cashier

 */

proctype Cashier()

{

    do

    ::

        printf("Cashier is waiting for a customern");

        cashierOpen < 1;

        printf("Cashier takes the order of Customer %dn", ordering);

        serverOpen > 0;

        printf("Cashier passes order to servern");

    od ;

}



/*

 * Process representing a server 

 */

proctype Server()

{



    byte id;

    do

    ::

        printf("Server is waiting for ordern");

        for(id : 0..2){

            if

            ::  waiting[id] ->

                lock(serverOpen);

                printf("Server creates order of %e for %dn", orders[id], id);

                printf("Server delivers order of %e to %dn", 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?






concurrency promela spin







share|improve this question

























  • Well, if you could explain why "Clearly, the program does not work as I expected." that would really speed-up the entire process of helping you..

    – Patrick Trentin
    Nov 29 '18 at 4:52














1












1








1


0






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 Enteredn", id);



        //Record

        favorites[id] = favorite;



        //Wait for cashier

        cashierOpen > 0;

        atomic{

            lock(cashierOpen);

            printf("Cashier selects customer %dn", id);

            ordering = id;

        }

        //Order

        orders[id] = favorite;

        printf("Customer orders %en", favorite);

        unlock(cashierOpen);

        ordering = NOBODY;





        printf("Customer %d is waiting for %en", id, favorite);

        waiting[id] = true;

        wait(waitingFood[id]);

        waitingFood[id] > 0;



        printf("Customer %d recieves food and leavesn", id);

        favorites[id] = NULL;

        orders[id] = NULL;



    od ;

}



/*

 * Process representing a cashier

 */

proctype Cashier()

{

    do

    ::

        printf("Cashier is waiting for a customern");

        cashierOpen < 1;

        printf("Cashier takes the order of Customer %dn", ordering);

        serverOpen > 0;

        printf("Cashier passes order to servern");

    od ;

}



/*

 * Process representing a server 

 */

proctype Server()

{



    byte id;

    do

    ::

        printf("Server is waiting for ordern");

        for(id : 0..2){

            if

            ::  waiting[id] ->

                lock(serverOpen);

                printf("Server creates order of %e for %dn", orders[id], id);

                printf("Server delivers order of %e to %dn", 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?






concurrency promela spin







share|improve this question
















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 Enteredn", id);



        //Record

        favorites[id] = favorite;



        //Wait for cashier

        cashierOpen > 0;

        atomic{

            lock(cashierOpen);

            printf("Cashier selects customer %dn", id);

            ordering = id;

        }

        //Order

        orders[id] = favorite;

        printf("Customer orders %en", favorite);

        unlock(cashierOpen);

        ordering = NOBODY;





        printf("Customer %d is waiting for %en", id, favorite);

        waiting[id] = true;

        wait(waitingFood[id]);

        waitingFood[id] > 0;



        printf("Customer %d recieves food and leavesn", id);

        favorites[id] = NULL;

        orders[id] = NULL;



    od ;

}



/*

 * Process representing a cashier

 */

proctype Cashier()

{

    do

    ::

        printf("Cashier is waiting for a customern");

        cashierOpen < 1;

        printf("Cashier takes the order of Customer %dn", ordering);

        serverOpen > 0;

        printf("Cashier passes order to servern");

    od ;

}



/*

 * Process representing a server 

 */

proctype Server()

{



    byte id;

    do

    ::

        printf("Server is waiting for ordern");

        for(id : 0..2){

            if

            ::  waiting[id] ->

                lock(serverOpen);

                printf("Server creates order of %e for %dn", orders[id], id);

                printf("Server delivers order of %e to %dn", 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?






concurrency promela spin




concurrency promela spin






share|improve this question















share|improve this question













share|improve this question




share|improve this question








edited Nov 29 '18 at 5:31









Patrick Trentin

4,64631635




4,64631635










asked Nov 28 '18 at 3:33









ritterritter

64




64













  • Well, if you could explain why "Clearly, the program does not work as I expected." that would really speed-up the entire process of helping you..

    – Patrick Trentin
    Nov 29 '18 at 4:52



















  • Well, if you could explain why "Clearly, the program does not work as I expected." that would really speed-up the entire process of helping you..

    – Patrick Trentin
    Nov 29 '18 at 4:52

















Well, if you could explain why "Clearly, the program does not work as I expected." that would really speed-up the entire process of helping you..

– Patrick Trentin
Nov 29 '18 at 4:52





Well, if you could explain why "Clearly, the program does not work as I expected." that would really speed-up the entire process of helping you..

– Patrick Trentin
Nov 29 '18 at 4:52












1 Answer
1






active

oldest

votes


















0














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:




  • For the Customer, it is pointless to wait over cashierOpen > 0, because it is already done inside lock(cashierOpen);


  • The fact that there is only one ordering variable means that your model may display incorrect information as soon as cashierOpen is initialized to a value > 1


  • The Customer should release cashierOpen with unlock(cashierOpen) and set ordering to NOBODY within an atomic { } statement. Otherwise some other Customer could write inside ordering in-between the two instructions and then the former Customer would incorrectly overwrite such variable with NOBODY.


  • The array waitingFood[NCUSTS] is initialized to 1. It is unclear to me what you expect to happen when you write wait(waitingFood[id]), as the memory location should already contain 1 and thus the Customer does not have to wait. Instead, I think that the array should be initialized to 0, and perhaps it is also worth updating its name to mirror this change.


  • Again, writing waitingFood[id] > 0 after wait(waitingFood[id]) seems to be not only pointless, but in this case also incorrect. The semaphore should contain 0/1 values at this stage! When wait(waitingFood[id]) is able to acquire the semaphore, the memory location waitingFood[id] is set to 0, so the line waitingFood[id] > 0 would block the Customer forever. The only reason why right now this does not happen is because of the bug I underlined at the beginning of this answer, which allows the Server to serve the same Customer multiple times.







share|improve this answer

























    Your Answer






    StackExchange.ifUsing("editor", function () {
    StackExchange.using("externalEditor", function () {
    StackExchange.using("snippets", function () {
    StackExchange.snippets.init();
    });
    });
    }, "code-snippets");

    StackExchange.ready(function() {
    var channelOptions = {
    tags: "".split(" "),
    id: "1"
    };
    initTagRenderer("".split(" "), "".split(" "), channelOptions);

    StackExchange.using("externalEditor", function() {
    // Have to fire editor after snippets, if snippets enabled
    if (StackExchange.settings.snippets.snippetsEnabled) {
    StackExchange.using("snippets", function() {
    createEditor();
    });
    }
    else {
    createEditor();
    }
    });

    function createEditor() {
    StackExchange.prepareEditor({
    heartbeatType: 'answer',
    autoActivateHeartbeat: false,
    convertImagesToLinks: true,
    noModals: true,
    showLowRepImageUploadWarning: true,
    reputationToPostImages: 10,
    bindNavPrevention: true,
    postfix: "",
    imageUploader: {
    brandingHtml: "Powered by u003ca class="icon-imgur-white" href="https://imgur.com/"u003eu003c/au003e",
    contentPolicyHtml: "User contributions licensed under u003ca href="https://creativecommons.org/licenses/by-sa/3.0/"u003ecc by-sa 3.0 with attribution requiredu003c/au003e u003ca href="https://stackoverflow.com/legal/content-policy"u003e(content policy)u003c/au003e",
    allowUrls: true
    },
    onDemand: true,
    discardSelector: ".discard-answer"
    ,immediatelyShowMarkdownHelp:true
    });


    }
    });














    draft saved

    draft discarded


















    StackExchange.ready(
    function () {
    StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fstackoverflow.com%2fquestions%2f53511713%2fwhen-to-use-semaphore-locks-unlocks-vs-wait-notify%23new-answer', 'question_page');
    }
    );

    Post as a guest















    Required, but never shown

























    1 Answer
    1






    active

    oldest

    votes








    1 Answer
    1






    active

    oldest

    votes









    active

    oldest

    votes






    active

    oldest

    votes









    0














    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:




    • For the Customer, it is pointless to wait over cashierOpen > 0, because it is already done inside lock(cashierOpen);


    • The fact that there is only one ordering variable means that your model may display incorrect information as soon as cashierOpen is initialized to a value > 1


    • The Customer should release cashierOpen with unlock(cashierOpen) and set ordering to NOBODY within an atomic { } statement. Otherwise some other Customer could write inside ordering in-between the two instructions and then the former Customer would incorrectly overwrite such variable with NOBODY.


    • The array waitingFood[NCUSTS] is initialized to 1. It is unclear to me what you expect to happen when you write wait(waitingFood[id]), as the memory location should already contain 1 and thus the Customer does not have to wait. Instead, I think that the array should be initialized to 0, and perhaps it is also worth updating its name to mirror this change.


    • Again, writing waitingFood[id] > 0 after wait(waitingFood[id]) seems to be not only pointless, but in this case also incorrect. The semaphore should contain 0/1 values at this stage! When wait(waitingFood[id]) is able to acquire the semaphore, the memory location waitingFood[id] is set to 0, so the line waitingFood[id] > 0 would block the Customer forever. The only reason why right now this does not happen is because of the bug I underlined at the beginning of this answer, which allows the Server to serve the same Customer multiple times.







    share|improve this answer






























      0














      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:




      • For the Customer, it is pointless to wait over cashierOpen > 0, because it is already done inside lock(cashierOpen);


      • The fact that there is only one ordering variable means that your model may display incorrect information as soon as cashierOpen is initialized to a value > 1


      • The Customer should release cashierOpen with unlock(cashierOpen) and set ordering to NOBODY within an atomic { } statement. Otherwise some other Customer could write inside ordering in-between the two instructions and then the former Customer would incorrectly overwrite such variable with NOBODY.


      • The array waitingFood[NCUSTS] is initialized to 1. It is unclear to me what you expect to happen when you write wait(waitingFood[id]), as the memory location should already contain 1 and thus the Customer does not have to wait. Instead, I think that the array should be initialized to 0, and perhaps it is also worth updating its name to mirror this change.


      • Again, writing waitingFood[id] > 0 after wait(waitingFood[id]) seems to be not only pointless, but in this case also incorrect. The semaphore should contain 0/1 values at this stage! When wait(waitingFood[id]) is able to acquire the semaphore, the memory location waitingFood[id] is set to 0, so the line waitingFood[id] > 0 would block the Customer forever. The only reason why right now this does not happen is because of the bug I underlined at the beginning of this answer, which allows the Server to serve the same Customer multiple times.







      share|improve this answer




























        0












        0








        0







        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:




        • For the Customer, it is pointless to wait over cashierOpen > 0, because it is already done inside lock(cashierOpen);


        • The fact that there is only one ordering variable means that your model may display incorrect information as soon as cashierOpen is initialized to a value > 1


        • The Customer should release cashierOpen with unlock(cashierOpen) and set ordering to NOBODY within an atomic { } statement. Otherwise some other Customer could write inside ordering in-between the two instructions and then the former Customer would incorrectly overwrite such variable with NOBODY.


        • The array waitingFood[NCUSTS] is initialized to 1. It is unclear to me what you expect to happen when you write wait(waitingFood[id]), as the memory location should already contain 1 and thus the Customer does not have to wait. Instead, I think that the array should be initialized to 0, and perhaps it is also worth updating its name to mirror this change.


        • Again, writing waitingFood[id] > 0 after wait(waitingFood[id]) seems to be not only pointless, but in this case also incorrect. The semaphore should contain 0/1 values at this stage! When wait(waitingFood[id]) is able to acquire the semaphore, the memory location waitingFood[id] is set to 0, so the line waitingFood[id] > 0 would block the Customer forever. The only reason why right now this does not happen is because of the bug I underlined at the beginning of this answer, which allows the Server to serve the same Customer multiple times.







        share|improve this answer















        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:




        • For the Customer, it is pointless to wait over cashierOpen > 0, because it is already done inside lock(cashierOpen);


        • The fact that there is only one ordering variable means that your model may display incorrect information as soon as cashierOpen is initialized to a value > 1


        • The Customer should release cashierOpen with unlock(cashierOpen) and set ordering to NOBODY within an atomic { } statement. Otherwise some other Customer could write inside ordering in-between the two instructions and then the former Customer would incorrectly overwrite such variable with NOBODY.


        • The array waitingFood[NCUSTS] is initialized to 1. It is unclear to me what you expect to happen when you write wait(waitingFood[id]), as the memory location should already contain 1 and thus the Customer does not have to wait. Instead, I think that the array should be initialized to 0, and perhaps it is also worth updating its name to mirror this change.


        • Again, writing waitingFood[id] > 0 after wait(waitingFood[id]) seems to be not only pointless, but in this case also incorrect. The semaphore should contain 0/1 values at this stage! When wait(waitingFood[id]) is able to acquire the semaphore, the memory location waitingFood[id] is set to 0, so the line waitingFood[id] > 0 would block the Customer forever. The only reason why right now this does not happen is because of the bug I underlined at the beginning of this answer, which allows the Server to serve the same Customer multiple times.








        share|improve this answer














        share|improve this answer



        share|improve this answer








        edited Nov 29 '18 at 9:22

























        answered Nov 29 '18 at 5:31









        Patrick TrentinPatrick Trentin

        4,64631635




        4,64631635
































            draft saved

            draft discarded




















































            Thanks for contributing an answer to Stack Overflow!


            • Please be sure to answer the question. Provide details and share your research!

            But avoid …



            • Asking for help, clarification, or responding to other answers.

            • Making statements based on opinion; back them up with references or personal experience.


            To learn more, see our tips on writing great answers.




            draft saved


            draft discarded














            StackExchange.ready(
            function () {
            StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fstackoverflow.com%2fquestions%2f53511713%2fwhen-to-use-semaphore-locks-unlocks-vs-wait-notify%23new-answer', 'question_page');
            }
            );

            Post as a guest















            Required, but never shown





















































            Required, but never shown














            Required, but never shown












            Required, but never shown







            Required, but never shown

































            Required, but never shown














            Required, but never shown












            Required, but never shown







            Required, but never shown







            -

            Popular posts from this blog

            A CLEAN and SIMPLE way to add appendices to Table of Contents and bookmarks

            Image
            0 I found a lot of questions abount appendices and ToC. Many users want appendices to be grouped in an Appendix part, however some problems arise with ToC, hyperref, PDF viewer bookmarks, and so on. There are different solutions which require extra packages, command patching and other extra code, however none of them satisfies me. I almost found an easy way to accomplish a good result, where appendices are added to bookmarks in the right way and hyperref links point to the right page. However, the number of the "Appendix" part page is wrong (it's the number of appendix A). Is there any EASY way to fix that? This is a MWE: documentclass{book} usepackage[nottoc,notlot,notlof]{tocbibind} usepackage{hyperref} begin{document} frontmatter tableofcontents mainmatter part{First} chapter{...
            Read more

            Calculate evaluation metrics using cross_val_predict sklearn

            Image
            1 In the sklearn.model_selection.cross_val_predict page it is stated: Generate cross-validated estimates for each input data point. It is not appropriate to pass these predictions into an evaluation metric. Can someone explain what does it mean? If this gives estimate of Y (y prediction) for every Y (true Y), why can't I calculate metrics such as RMSE or coefficient of determination using these results? python scikit-learn cross-validation share | improve this question edited Nov 28 '18 at 17:52 desertnaut 20.3k 7 43 79 ...
            Read more

            Insert data from modal to MySQL (multiple modal on website)

            Image
            0 I have problem with inserting data to MySQL from modal. My modal: <a href="#" class="badge badge-pill badge-success">6 komentarzy</a> <a href="#" class="badge badge-pill badge-danger">brak komentarzy</a> <a data-toggle="modal" href="#add_desk_comm_{$desk_['desk_id']}" data-target="#add_desk_comm_{$desk_['desk_id']}" class="ediiit">(dodaj)</a> <div class="modal fade" id="add_desk_comm_{$desk_['desk_id']}" tabindex="-1" role="dialog" aria-labelledby="edit_printer" aria-hidden="true"> <div class="modal-dialog" role="document"> ...
            Read more