Spinroot

A forum for Spin users

You are not logged in.

#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

spinroot
forum
Registered: 2010-11-18
Posts: 694
Website

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

#4 2012-11-12 06:19:21

TRiXGype
Member
Registered: 2012-08-30
Posts: 1
Website

Re: Confusion over atomicity and send/receive operation

Absolutely with you it agree. In it something is and it is good idea. I support you.

smile

Offline

Board footer

Powered by FluxBB