I'm learning Promela and using SPIN to model some examples I found. This model involves a food ordering simulation. So the customer orders, cashier takes order, sends to server, back to customer etc.
Here is a flow of the program.
The specific processes are as followed.
Here is the code I have written so far:
#define NCUSTS 3 /* number of customers */
#define NCASHIERS 1 /* number of cashiers */
#define NSERVERS 1 /* number of servers */
#define NOBODY 255
#define semaphore byte /* define a sempahore */
/*
* lock (down) and unlock (up) functions for mutex semaphores
*/
inline unlock(s) {s++;}
inline lock(s) {atomic{ s>0 ; s--}}
/*
* wait (down) and notify (up) functions for signaling semaphores
*/
inline notify(s) {s++;}
inline wait(s) {atomic{ s>0 ; s--}}
mtype = {CHILI, SANDWICH, PIZZA, NULL} ; // the types of foods (added null for resets)
mtype favorites[NCUSTS];
mtype orders[NCUSTS] = NULL;
byte ordering = NOBODY;
semaphore waitingFood[NCUSTS] = 1;
semaphore cashierOpen = 1;
semaphore serverOpen = 1;
bool waiting[NCUSTS] = false;
/*
* Process representing a customer.
* Takes in their favorite food and an integer id
* to represent them
*/
proctype Customer(mtype favorite; byte id)
{
/* customer cycle */
do
::
//Enter
printf("Customer %d Entered\n", id);
//Record
favorites[id] = favorite;
//Wait for cashier
cashierOpen > 0;
atomic{
lock(cashierOpen);
printf("Cashier selects customer %d\n", id);
ordering = id;
}
//Order
orders[id] = favorite;
printf("Customer orders %e\n", favorite);
unlock(cashierOpen);
ordering = NOBODY;
printf("Customer %d is waiting for %e\n", id, favorite);
waiting[id] = true;
wait(waitingFood[id]);
waitingFood[id] > 0;
printf("Customer %d recieves food and leaves\n", id);
favorites[id] = NULL;
orders[id] = NULL;
od ;
}
/*
* Process representing a cashier
*/
proctype Cashier()
{
do
::
printf("Cashier is waiting for a customer\n");
cashierOpen < 1;
printf("Cashier takes the order of Customer %d\n", ordering);
serverOpen > 0;
printf("Cashier passes order to server\n");
od ;
}
/*
* Process representing a server
*/
proctype Server()
{
byte id;
do
::
printf("Server is waiting for order\n");
for(id : 0..2){
if
:: waiting[id] ->
lock(serverOpen);
printf("Server creates order of %e for %d\n", orders[id], id);
printf("Server delivers order of %e to %d\n", orders[id], id);
notify(waitingFood[id]);
unlock(serverOpen);
:: else ->
skip;
fi;
}
od ;
}
/*
* Sets up processes. This model creates two
* customers with the favorite foods PIZZA & CHILI.
*/
init{
atomic{
run Customer(PIZZA, 0) ;
run Customer(CHILI, 1) ;
run Cashier();
run Server();
}
}
Clearly, the program does not work as I expected. Could someone help me understand how to use semaphores and when to use locks unlocks waits and notifies here?
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.