Spinroot
A forum for Spin users
You are not logged in.
- Topics: Active | Unanswered
#1 2012-08-10 21:37:46
- rileyrob
- Member
- Registered: 2012-07-31
- Posts: 7
Confusion over atomicity and send/receive operation
Hi,
I know that for a rendezvous, when the message is passed (handshake takes place), the recipient immediately begins running. But I thought for an asynchronous send wrapped in atomicity, the sent message would simply be stored in the recipient's buffer (so long as channel wasn't full) and the sender would continue executing to the closing brace of its atomic clause before the receive got to do anything. For example, given the following:
/* Asynchronous, NOT rondezvous */
chan chInbound = [5] of { mtype };
chan chOutbound = [5] of { mtype, bool};
active proctype ProcA()
{
do
:: chOutbound?EID_PKT, oppAvail -> chInbound!RES_REQ
:: timeout -> skip;
od;
}
active proctype ProcB()
{
show int cnt;
do
:: atomic { chOutbound!EID_PKT, oppAvail -> cnt++; }
:: timeout -> skip;
od;
}
Assuming chOutbound is NOT full, I would have thought that if ProcB ran and sent the EID_PKT msg to ProcA, it would then continue on to increment the cnt variable. However, instead what I'm seeing is that, upon receipt of the EID_PKT, ProcA immediately starts running and sends the RES_REQ msg. Am I totally misunderstanding how atomicity works? How do I prevent the receiver from acting on the message until the sender is finished doing what it needed to do?
Any guidance would be greatly appreciated!
Thanks,
Robin
Offline
#2 2012-08-11 01:03:05
Re: Confusion over atomicity and send/receive operation
you are right that what you say should happen, should in fact happen
and it does when I try it:
$ spin -u10 -p tryme.pml
0: proc - (:root:) creates proc 0 (ProcA)
0: proc - (:root:) creates proc 1 (ProcB)
1: proc 1 (ProcB) tryme.pml:19 (state 6) [chOutbound!EID_PKT,oppAvail]
2: proc 1 (ProcB) tryme.pml:20 (state 2) [cnt = (cnt+1)]
3: proc 0 (ProcA) tryme.pml:8 (state 5) [chOutbound?EID_PKT,oppAvail]
4: proc 1 (ProcB) tryme.pml:23 (state 7) [.(goto)]
5: proc 0 (ProcA) tryme.pml:9 (state 2) [chInbound!RES_REQ]
6: proc 1 (ProcB) tryme.pml:19 (state 6) [chOutbound!EID_PKT,oppAvail]
7: proc 1 (ProcB) tryme.pml:20 (state 2) [cnt = (cnt+1)]
8: proc 1 (ProcB) tryme.pml:23 (state 7) [.(goto)]
9: proc 0 (ProcA) tryme.pml:12 (state 6) [.(goto)]
10: proc 0 (ProcA) tryme.pml:8 (state 5) [chOutbound?EID_PKT,oppAvail]
-------------
depth-limit (-u10 steps) reached
#processes: 2
queue 2 (chInbound): [RES_REQ]
queue 1 (chOutbound):
10: proc 1 (ProcB) tryme.pml:19 (state 6)
10: proc 0 (ProcA) tryme.pml:9 (state 2)
2 processes created
Offline
#3 2012-08-13 13:31:27
- rileyrob
- Member
- Registered: 2012-07-31
- Posts: 7
Re: Confusion over atomicity and send/receive operation
Ok, thanks. back to the drawing board then because in my actual model (much more complicated) it doesn't do that so.... obviously I'm missing something. thanks!
Offline
