Admissibility of invariants of dependent types

Oct 5, 2015 at 12:00 PM
I am not getting, in the following type definitions, why invariants are not admissible ?
struct counter{
    volatile unsigned int m;
    _(invariant (m == \old(m)) || (m == \old(m) + 2))

struct low{
    struct counter *cnt;
    unsigned int floor;
    _(invariant floor <= cnt->m)  // not admissible

struct low2{
    struct counter cnt;
    unsigned int floor;
    _(invariant floor <= cnt.m) // not admissible

struct high{
    struct counter cnt;
    unsigned int ceilval;
    _(invariant cnt.m <= ceilval) // not admissible
I am referring following research paper :
Cohen, Ernie, et al. "Local verification of global invariants in concurrent programs." Computer Aided Verification. Springer Berlin Heidelberg, 2010.

As given in the paper, we can reason about invariant of type 'high', but can anyone please explain, why invariant of 'low' or 'low2' is not admissible ? How this invariant is broken in stability ?
Thanking you.
Oct 5, 2015 at 11:24 PM
There is nothing in the invariant that forces cnt to be closed. (Recall that nested structs are treated as separate objects unless they are explicitly inlined.) If cnt isn't closed, its invariants needn't hold.

This issue didn't show up in the CAV example because it was talking about simpler objects whose invariants always hold.
Oct 12, 2015 at 3:21 PM
Thank you for your reply. It was helpful.
Can you please, tell specifically which example are you referring by CAV example ?
How checking of stability of invariant works in VCC, in the scenarios as above ?