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:
When
waitingFood[id]is released by theServer, theCustomerdoes not immediately turnwaiting[id]tofalse, so it is possible that theServerhandles the sameCustomer's request more than once (actually, it is very likely to happen).In fact, by adding the following ltl property to the model:
and then checking the property, it is confirmed that the variable
waitingFoodcan be assigned an "incorrect" value:The problematic trace is:
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.