Spinroot

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

Hi,

From the command line, I built my model and attempted to compile the verifier and it gives me "Access Denied":

      C:\Data\ProtocolAnalysis>spin -a RA_Scheduling.pml

      C:\Data\ProtocolAnalysis>cc -o pan pan.c
      Access is denied.

      C:\Data\ProtocolAnalysis>

Does anyone know why I'm getting access denied? I am running on Windows 7 and I know some things require you to run as administrator but I have administrator privileges on my machine. Additionally, I can generate/run the verifier from within the GUI so...

Thanks,
Robin