This project is read-only.

Back reference

Apr 12, 2011 at 6:18 PM

We're trying to implement a version of semaphores which has a "back reference", as outlined in the Local Verification of Global Invariants. The back reference did indeed solve an admissibility problem we were having, but created a new one that I don't understand.

Here is the code

#include<vcc.h>

_(claimable) _(volatile_owns) typedef struct _ConditionSemaphore {
	volatile int s;
	_(ghost \object protected_obj;)
	_(invariant s==0 || s==1 )
	_(invariant s == 1 <==> \mine(protected_obj))
	// The next two lines ensure that any time the semaphore is
	// given ownership of the object, the associated condition
	// object's invariant is true.
	_(ghost \object condition)
	_(invariant \old(s)!=s && s==1 ==> \inv(condition))
	// Not sure I need the following, but they seem harmless
	_(invariant protected_obj != condition )
	_(invariant protected_obj != \this )
	_(invariant condition != \this )
} ConditionSemaphore;

void ReleaseToConditionSemaphore(struct ConditionSemaphore *l _(ghost \claim c))
  _(always c, l->\consistent)
  _(requires l->protected_obj != c)
  _(requires \wrapped(l->protected_obj))
  _(requires l->condition \in l->protected_obj->\owns)
  _(writes l->protected_obj)
{
  _(atomic c, l) { //Line 27
    _(assert l->condition \in l->protected_obj->\owns) 
    l->s = 1;
    _(ghost l->\owns += l->protected_obj;)
  }

The error messages are

Z:\tsn-2011-04-11c.c(28,28) : error VC9500: Assertion 'l->condition \in l->protected_obj->\owns' did not verify.
Z:\tsn-2011-04-11c.c(27,29) : error VC8524: Assertion 'chunk \old(s)!=s && s==1 ==> \inv(condition) of invariant of l holds after atomic' did not verify.

My reasoning for the quoted "chunk" holding is that since (by the preconditions) the thread owns l->protected_obj and l->protected_obj owns l->condition, the invariant of l->condition must hold to start. Since nothing happens in the subroutine to change these facts, the invariant should also hold at the end.

I think the failure of the assertion on line 28 to verify may give a hint as to the problem. That is, even though it is a precondition that l->condition is owned by the l->protected_obj, this precondition might get falsified by some concurrent process.

Any suggestions about how to get this to verify (e.g. a stronger precondition or invariant) would be greatly appreciated.

Cheers,
Theo

Apr 12, 2011 at 9:54 PM

Hi Theo,

  the problem here is that the protected object may have a volatile owns set, i.e., after the beginning of the atomic it is not known whether l->condition is still in the owns set of the protected object and there's no way to derive that the condition is closed / its invariant still holds. So, somewhere you have to strengthen your assumptions / invariants. Unfortunately, at this time you can't currently specify in the semaphore invariant, that the protected object has a nonvolatile owns set.

  HTH, Mark

Apr 15, 2011 at 8:09 PM

Mark: Thanks for your reply. I thought that might be the problem and it almost certainly is a problem.

So I tried replacing the uses of \object with pointer types to definite struct types that are definitely not declared as volatile_owns.

Here is the revised code

#include<vcc.h>

typedef struct _MonitoredBuffer {
	int x ;
} MonitoredBuffer ;

typedef struct _Condition {
	int y ;
} Condition ;

_(claimable) _(volatile_owns) typedef struct _ConditionSemaphore {
	volatile int s;
	_(ghost MonitoredBuffer* protected_obj;)
	_(invariant s==0 || s==1 )
	_(invariant s == 1 <==> \mine(protected_obj))
	// The next two lines ensure that any time the semaphore is
	// given ownership of the object, the associated condition
	// object's invariant is true.
	_(ghost Condition* condition)
	_(invariant \old(s)!=s && s==1 ==> \inv(condition))
} ConditionSemaphore;

void ReleaseToConditionSemaphore(struct ConditionSemaphore *l _(ghost \claim c))
  _(always c, l->\consistent)
  _(requires \wrapped(l->protected_obj))
  _(requires l->condition->\owner == l->protected_obj)
  _(writes l->protected_obj)
{
  _(assert l->condition->\owner == l->protected_obj)

  _(atomic c, l) { /*Line 31*/

    _(assert l->condition->\owner == l->protected_obj) /* Line 33*/

    l->s = 1;
    _(ghost l->\owns += l->protected_obj;)
  }
}

The errors are

   Z:> vcc /2 /it /smoke tsn-2011-04-11c.c
  Verification of _ConditionSemaphore#adm succeeded.
  Verification of ReleaseToConditionSemaphore failed.
  Z:\tsn-2011-04-11c.c(33,28) : error VC9500: Assertion 'l->condition->\owner == l->protected_obj' did not verify.
  Z:\tsn-2011-04-11c.c(31,29) : error VC8524: Assertion 'chunk \old(s)!=s && s==1 ==> \inv(condition) of invariant of l holds after atomic' did not verify.
  Exiting with 3 (1 error(s).)

I don't see why the ownership precondition that appears holds on line 29 does not hold on line 33.

 

Cheers,
Theo