Protected object equivalence could not be inferenced

Apr 19, 2011 at 6:35 AM

Getting an idea from Reader-Writer problem, I was trying my hand on Dining philosopher problem. Like in Reader-Writer, a data object has been assumed for testing. I assumed 3 data objects (chopstick[3]) with 3 locks (ChopLock[3]). But I am having some problem in initializing locks due to multiple locks. The part of code is:-

#include "Lock.c"

typedef struct _DATA semaphore;

#define NUM_PHILOSOPHERS    3
semaphore chopstick[NUM_PHILOSOPHERS];

LOCK ChopLock[5];

spec(
struct vcc(claimable) _DATA_CONTAINER {
  int dummy;
  invariant(keeps(&ChopLock[0]))
  invariant(keeps(&ChopLock[1]))
  invariant(keeps(&ChopLock[2]))
  invariant(ChopLock[0].protected_obj == &chopstick[0])
  invariant(ChopLock[1].protected_obj == &chopstick[1])
  invariant(ChopLock[2].protected_obj == &chopstick[2])
 
} ChopContainer;
)


void initialize()
  writes(set_universe())
  requires(program_entry_point())
  requires( (&chopstick[0]!=&chopstick[1])&&(&chopstick[0]!=&chopstick[2]) &&     
            (&chopstick[1]!=&chopstick[2])&&(&chopstick[1]!=&chopstick[3]) &&
            (&chopstick[2]!=&chopstick[3]))
{
    int i=0;
    // Initializing chopsticks
    spec(claim_t c, c1;)

   
    {
        chopstick[0].state=0;
        wrap(&chopstick[0]);
        chopstick[1].state=0;
        wrap(&chopstick[1]);
        chopstick[2].state=0;
        wrap(&chopstick[2]);       
    }        
         

        InitializeLock(&ChopLock[0] spec(&chopstick[0]));   
         set_owner(&ChopLock[0], &ChopContainer);
         assert(ChopLock[0].protected_obj==&chopstick[0]);   //proved
        InitializeLock(&ChopLock[1] spec(&chopstick[1]));

           assert(ChopLock[0].protected_obj==&chopstick[0]);   //could not assert why?

        set_owner(&ChopLock[1], &ChopContainer);
       
        InitializeLock(&ChopLock[2] spec(&chopstick[2]));   
         set_owner(&ChopLock[2], &ChopContainer);       
    wrap(&ChopContainer);
   spec(c = claim(&ChopContainer, closed(&ChopContainer)); )   
  
}

 

/*


C:\Users\manpreet\Desktop\philosopher problem>vcc philosopher.c /f:initialize
Verification of initialize failed.
C:\Users\manpreet\Desktop\philosopher problem\philosopher.c(126,12) : error VC8014:

invariant(ChopLock[0].protected_obj == &chopstick[0]) of _DATA_CONTAINER fails on wrap
.
C:\Users\manpreet\Desktop\philosopher problem\philosopher.c(55,15) : error VC9599: (r
elated information) location of the invariant.
C:\Users\manpreet\Desktop\philosopher problem\philosopher.c(126,12) : error VC8014:

invariant(ChopLock[1].protected_obj == &chopstick[1]) of _DATA_CONTAINER fails on wrap
.
C:\Users\manpreet\Desktop\philosopher problem\philosopher.c(56,15) : error VC9599: (r
elated information) location of the invariant.
Exiting with 3 (1 error(s).)

*/

 

How did the protected_obj changed and only for the first 2 chopsticks and not for the third one?

Coordinator
May 12, 2011 at 8:34 PM

Hi,

  VCC sometimes needs to be explicitly reminded (in the form of assertions) to preserve sequential state across function calls, in this case across the InitializeLock() calls. The third chopstick is constructed by the third calls, and the postcondition of this calls if sufficient to show the invariant; in contrast to that, VCC thinks the the first chopstick might be modified in call 2 and 3, and the second chopstick might be modified in the third call. This is explained in Section 6.4 of the tutorial (http://research.microsoft.com/en-us/um/people/moskal/pdf/vcc-tutorial-col1.pdf). Adding appropriate assertions "a \in \domain(a)" (or "set_in(a, owns(a))" in the old syntax) solves the problem above. Code is shown below (new syntax, working with the checked in version of Lock.c).

  Best, Mark

#include "Lock.c"

typedef struct _DATA semaphore;

#define NUM_PHILOSOPHERS    3
semaphore chopstick[NUM_PHILOSOPHERS];

LOCK ChopLock[5];

_(ghost _(claimable) struct _CHOP_CONTAINER {
  int dummy;
  _(invariant \mine(&ChopLock[0]))
  _(invariant \mine(&ChopLock[1]))
  _(invariant \mine(&ChopLock[2]))
  _(invariant ChopLock[0].protected_obj == &chopstick[0])
  _(invariant ChopLock[1].protected_obj == &chopstick[1])
  _(invariant ChopLock[2].protected_obj == &chopstick[2])

} ChopContainer;)

void initialize()
  _(writes \universe())
  _(requires \program_entry_point())
  _(requires (&chopstick[0]!=&chopstick[1])&&(&chopstick[0]!=&chopstick[2]) &&
	    (&chopstick[1]!=&chopstick[2])&&(&chopstick[1]!=&chopstick[3]) &&
	    (&chopstick[2]!=&chopstick[3]))
{
    int i=0;

    _(ghost \claim c, c1)

    {
	chopstick[0].a = chopstick[0].b = 1;
	_(wrap &chopstick[0])
	chopstick[1].a = chopstick[1].b = 1;
	_(wrap &chopstick[1])
	chopstick[2].a = chopstick[2].b = 1;
	_(wrap &chopstick[2])
    }


    InitializeLock(&ChopLock[0] _(ghost &chopstick[0]));
    _(ghost (&ChopContainer)->\owns += &ChopLock[0]);
    _(assert ChopLock[0].protected_obj==&chopstick[0])   //proved
    
    _(assert &ChopLock[0] \in \domain(&ChopLock[0])) // (*)
    
    InitializeLock(&ChopLock[1] _(ghost &chopstick[1]));
    
    _(assert &ChopLock[1] \in \domain(&ChopLock[1])) // (*)
    
    _(assert ChopLock[0].protected_obj==&chopstick[0]) 
    
    
    _(ghost (&ChopContainer)->\owns += &ChopLock[1]);
    
    InitializeLock(&ChopLock[2] _(ghost &chopstick[2]));
    _(ghost (&ChopContainer)->\owns += &ChopLock[2]);
    _(wrap &ChopContainer)
    _(ghost c = \make_claim({&ChopContainer}, (&ChopContainer)->\closed);)
    
}