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 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
edited Nov 29 '18 at 5:31
Patrick Trentin
4,64631635
asked Nov 28 '18 at 3:33
ritterritter
64
add a comment |
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
edited Nov 29 '18 at 5:31
Patrick Trentin
4,64631635
asked Nov 28 '18 at 3:33
ritterritter
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
add a comment |
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
edited Nov 29 '18 at 5:31
Patrick Trentin
4,64631635
asked Nov 28 '18 at 3:33
ritterritter
64
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
edited Nov 29 '18 at 5:31
Patrick Trentin
4,64631635
asked Nov 28 '18 at 3:33
ritterritter
64
edited Nov 29 '18 at 5:31
Patrick Trentin
4,64631635
asked Nov 28 '18 at 3:33
ritterritter
64
edited Nov 29 '18 at 5:31
Patrick Trentin
4,64631635
edited Nov 29 '18 at 5:31
Patrick Trentin
4,64631635
edited Nov 29 '18 at 5:31
Patrick Trentin
4,64631635
4,64631635
asked Nov 28 '18 at 3:33
ritterritter
64
asked Nov 28 '18 at 3:33
ritterritter
64
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
add a comment |
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
add a comment |
1 Answer
1
active
oldest
votes
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 overcashierOpen > 0, because it is already done insidelock(cashierOpen);The fact that there is only one
orderingvariable means that your model may display incorrect information as soon ascashierOpenis initialized to a value> 1The
Customershould releasecashierOpenwithunlock(cashierOpen)and setorderingtoNOBODYwithin anatomic { }statement. Otherwise some otherCustomercould write insideorderingin-between the two instructions and then the formerCustomerwould incorrectly overwrite such variable withNOBODY.The array
waitingFood[NCUSTS]is initialized to1. It is unclear to me what you expect to happen when you writewait(waitingFood[id]), as the memory location should already contain1and thus the Customer does not have to wait. Instead, I think that the array should be initialized to0, and perhaps it is also worth updating its name to mirror this change.Again, writing
waitingFood[id] > 0afterwait(waitingFood[id])seems to be not only pointless, but in this case also incorrect. The semaphore should contain0/1values at this stage! Whenwait(waitingFood[id])is able to acquire the semaphore, the memory locationwaitingFood[id]is set to0, so the linewaitingFood[id] > 0would block theCustomerforever. 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 theServerto serve the sameCustomermultiple times.
answered Nov 29 '18 at 5:31
Patrick TrentinPatrick Trentin
4,64631635
add a comment |
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
});
}
});
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
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
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 overcashierOpen > 0, because it is already done insidelock(cashierOpen);The fact that there is only one
orderingvariable means that your model may display incorrect information as soon ascashierOpenis initialized to a value> 1The
Customershould releasecashierOpenwithunlock(cashierOpen)and setorderingtoNOBODYwithin anatomic { }statement. Otherwise some otherCustomercould write insideorderingin-between the two instructions and then the formerCustomerwould incorrectly overwrite such variable withNOBODY.The array
waitingFood[NCUSTS]is initialized to1. It is unclear to me what you expect to happen when you writewait(waitingFood[id]), as the memory location should already contain1and thus the Customer does not have to wait. Instead, I think that the array should be initialized to0, and perhaps it is also worth updating its name to mirror this change.Again, writing
waitingFood[id] > 0afterwait(waitingFood[id])seems to be not only pointless, but in this case also incorrect. The semaphore should contain0/1values at this stage! Whenwait(waitingFood[id])is able to acquire the semaphore, the memory locationwaitingFood[id]is set to0, so the linewaitingFood[id] > 0would block theCustomerforever. 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 theServerto serve the sameCustomermultiple times.
answered Nov 29 '18 at 5:31
Patrick TrentinPatrick Trentin
4,64631635
add a comment |
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 overcashierOpen > 0, because it is already done insidelock(cashierOpen);The fact that there is only one
orderingvariable means that your model may display incorrect information as soon ascashierOpenis initialized to a value> 1The
Customershould releasecashierOpenwithunlock(cashierOpen)and setorderingtoNOBODYwithin anatomic { }statement. Otherwise some otherCustomercould write insideorderingin-between the two instructions and then the formerCustomerwould incorrectly overwrite such variable withNOBODY.The array
waitingFood[NCUSTS]is initialized to1. It is unclear to me what you expect to happen when you writewait(waitingFood[id]), as the memory location should already contain1and thus the Customer does not have to wait. Instead, I think that the array should be initialized to0, and perhaps it is also worth updating its name to mirror this change.Again, writing
waitingFood[id] > 0afterwait(waitingFood[id])seems to be not only pointless, but in this case also incorrect. The semaphore should contain0/1values at this stage! Whenwait(waitingFood[id])is able to acquire the semaphore, the memory locationwaitingFood[id]is set to0, so the linewaitingFood[id] > 0would block theCustomerforever. 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 theServerto serve the sameCustomermultiple times.
answered Nov 29 '18 at 5:31
Patrick TrentinPatrick Trentin
4,64631635
add a comment |
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 overcashierOpen > 0, because it is already done insidelock(cashierOpen);The fact that there is only one
orderingvariable means that your model may display incorrect information as soon ascashierOpenis initialized to a value> 1The
Customershould releasecashierOpenwithunlock(cashierOpen)and setorderingtoNOBODYwithin anatomic { }statement. Otherwise some otherCustomercould write insideorderingin-between the two instructions and then the formerCustomerwould incorrectly overwrite such variable withNOBODY.The array
waitingFood[NCUSTS]is initialized to1. It is unclear to me what you expect to happen when you writewait(waitingFood[id]), as the memory location should already contain1and thus the Customer does not have to wait. Instead, I think that the array should be initialized to0, and perhaps it is also worth updating its name to mirror this change.Again, writing
waitingFood[id] > 0afterwait(waitingFood[id])seems to be not only pointless, but in this case also incorrect. The semaphore should contain0/1values at this stage! Whenwait(waitingFood[id])is able to acquire the semaphore, the memory locationwaitingFood[id]is set to0, so the linewaitingFood[id] > 0would block theCustomerforever. 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 theServerto serve the sameCustomermultiple times.
answered Nov 29 '18 at 5:31
Patrick TrentinPatrick Trentin
4,64631635
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 overcashierOpen > 0, because it is already done insidelock(cashierOpen);The fact that there is only one
orderingvariable means that your model may display incorrect information as soon ascashierOpenis initialized to a value> 1The
Customershould releasecashierOpenwithunlock(cashierOpen)and setorderingtoNOBODYwithin anatomic { }statement. Otherwise some otherCustomercould write insideorderingin-between the two instructions and then the formerCustomerwould incorrectly overwrite such variable withNOBODY.The array
waitingFood[NCUSTS]is initialized to1. It is unclear to me what you expect to happen when you writewait(waitingFood[id]), as the memory location should already contain1and thus the Customer does not have to wait. Instead, I think that the array should be initialized to0, and perhaps it is also worth updating its name to mirror this change.Again, writing
waitingFood[id] > 0afterwait(waitingFood[id])seems to be not only pointless, but in this case also incorrect. The semaphore should contain0/1values at this stage! Whenwait(waitingFood[id])is able to acquire the semaphore, the memory locationwaitingFood[id]is set to0, so the linewaitingFood[id] > 0would block theCustomerforever. 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 theServerto serve the sameCustomermultiple times.
answered Nov 29 '18 at 5:31
Patrick TrentinPatrick Trentin
4,64631635
edited Nov 29 '18 at 9:22
answered Nov 29 '18 at 5:31
Patrick TrentinPatrick Trentin
4,64631635
answered Nov 29 '18 at 5:31
Patrick TrentinPatrick Trentin
4,64631635
answered Nov 29 '18 at 5:31
Patrick TrentinPatrick Trentin
4,64631635
4,64631635
add a comment |
add a comment |
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.
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
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
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
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
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