# Back reference

 TheodoreNorvell Apr 12, 2011 at 5: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 _(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 MarkHillebrand Coordinator Apr 12, 2011 at 8: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 TheodoreNorvell Apr 15, 2011 at 7: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 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