何时使用信号量锁/解锁与等待/通知？
When to use semaphore locks / unlocks vs. wait / notify?
我正在学习 Promela 并使用 SPIN 对我发现的一些示例进行建模。该模型涉及食品订购模拟。所以客户下单，收银员接受订单，发送到服务器，返回给客户等。
Here is a flow of the program.
The specific processes are as followed.
这是我到目前为止编写的代码：
#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();
}
}
很明显，程序没有像我预期的那样工作。有人可以帮助我了解如何使用信号量以及何时使用锁解锁等待和通知吗？
您的模型的这一部分必须更改：
:: waiting[id] ->
...
notify(waitingFood[id]);
...
当waitingFood[id]被Server释放时，Customer不会立即将waiting[id]变为false，所以有可能是Server 多次处理同一个 Customer 的请求（实际上，很可能发生）。
实际上，通过在模型中添加以下ltl 属性：
ltl p0 { [] (waitingFood[0] < 2) };
然后查看属性，确认变量waitingFood可以赋"incorrect"值：
~$ 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
有问题的轨迹是：
~$ 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
以下是基于阅读您的模型的一些补充评论：
对于Customer，等待cashierOpen > 0没有意义，因为lock(cashierOpen);
[=85=里面已经完成了]
只有一个 ordering 变量这一事实意味着一旦 cashierOpen 被初始化为一个值 > 1[，您的模型可能会显示不正确的信息=53=]
Customer 应该用 unlock(cashierOpen) 释放 cashierOpen 并在 atomic { } 语句中将 ordering 设置为 NOBODY .否则其他一些 Customer 可能会在两条指令之间写入 ordering，然后前者 Customer 会错误地用 NOBODY.
[= 覆盖此类变量85=]
数组waitingFood[NCUSTS]初始化为1。我不清楚您在写 wait(waitingFood[id]) 时期望发生什么，因为内存位置应该已经包含 1，因此客户不必等待。相反，我认为该数组应该初始化为 0，也许还值得更新它的名称以反映此更改。
同样，在 wait(waitingFood[id]) 之后写 waitingFood[id] > 0 似乎不仅没有意义，而且在这种情况下也是不正确的。信号量在此阶段应包含 0/1 值！当 wait(waitingFood[id]) 能够获取信号量时，内存位置 waitingFood[id] 被设置为 0，因此行 waitingFood[id] > 0 将永远阻塞 Customer。现在没有发生这种情况的唯一原因是因为 bug 我在这个答案的开头强调了这一点，它允许 Server 提供相同的 Customer多次
我正在学习 Promela 并使用 SPIN 对我发现的一些示例进行建模。该模型涉及食品订购模拟。所以客户下单，收银员接受订单，发送到服务器，返回给客户等。
Here is a flow of the program.
The specific processes are as followed.
这是我到目前为止编写的代码：
#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();
}
}
很明显，程序没有像我预期的那样工作。有人可以帮助我了解如何使用信号量以及何时使用锁解锁等待和通知吗？
您的模型的这一部分必须更改：
:: waiting[id] ->
...
notify(waitingFood[id]);
...
当waitingFood[id]被Server释放时，Customer不会立即将waiting[id]变为false，所以有可能是Server 多次处理同一个 Customer 的请求（实际上，很可能发生）。
实际上，通过在模型中添加以下ltl 属性：
ltl p0 { [] (waitingFood[0] < 2) };
然后查看属性，确认变量waitingFood可以赋"incorrect"值：
~$ 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
有问题的轨迹是：
~$ 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
以下是基于阅读您的模型的一些补充评论：
对于
[=85=里面已经完成了]Customer，等待cashierOpen > 0没有意义，因为lock(cashierOpen);只有一个
ordering变量这一事实意味着一旦cashierOpen被初始化为一个值> 1[，您的模型可能会显示不正确的信息=53=]
[= 覆盖此类变量85=]Customer应该用unlock(cashierOpen)释放cashierOpen并在atomic { }语句中将ordering设置为NOBODY.否则其他一些Customer可能会在两条指令之间写入ordering，然后前者Customer会错误地用NOBODY.数组
waitingFood[NCUSTS]初始化为1。我不清楚您在写wait(waitingFood[id])时期望发生什么，因为内存位置应该已经包含1，因此客户不必等待。相反，我认为该数组应该初始化为0，也许还值得更新它的名称以反映此更改。同样，在
wait(waitingFood[id])之后写waitingFood[id] > 0似乎不仅没有意义，而且在这种情况下也是不正确的。信号量在此阶段应包含0/1值！当wait(waitingFood[id])能够获取信号量时，内存位置waitingFood[id]被设置为0，因此行waitingFood[id] > 0将永远阻塞Customer。现在没有发生这种情况的唯一原因是因为 bug 我在这个答案的开头强调了这一点，它允许Server提供相同的Customer多次