This project is read-only.

How did bv_lemma help here?

Mar 28, 2011 at 12:20 AM

Code of Reader-Writer Lock implementation verification:

How did bv_lemma (1) helped in verification? Or what made us to come up to this bv_lemma?

void AcquireShared(LOCK *lock
  claimp(lock_access_claim) claimp(out read_access_claim))
  always(lock_access_claim, closed(lock) && lock->initialized)
  ensures(wrapped0(read_access_claim) && is_fresh(read_access_claim))
  ensures(claims(read_access_claim, closed(lock) &&
    lock->initialized && !lock->writing &&
    claims_obj(read_access_claim, lock->self_claim) &&
    claims_obj(read_access_claim, lock->protected_obj) &&
    closed(lock->protected_obj)))
{
  long old_state, new_state;

  // TODO this looks too complicated
  bv_lemma(forall(long i; Write(i) <==> i < 0));                                      //         (1)
  bv_lemma(forall(long i; 0 <= i && i < 0x7FFFFFFF;                                //         (2)
    Readers(i + 1) == Readers(i) + 1 && Write(i) == Write(i + 1)));

  do
  {
    do
      atomic (lock, lock_access_claim) {
        old_state  = lock->state;
      }
    while (Write(old_state));
    assume(old_state < 0x7FFFFFFF);
    new_state = old_state + 1;
    assert(new_state == unchecked(old_state + 1)); // cf. issue 5883
  } while (old_state != atomic_op(
    _InterlockedCompareExchange(&lock->state, new_state, old_state),
    lock, lock_access_claim,
    old_state != result ||
      CreateReadAccessClaim(lock spec(out read_access_claim))));
}

spec(vcc(atomic_inline)
bool CreateReadAccessClaim(LOCK *lock, claimp(out read_access_claim)) {
  read_access_claim = claim(lock->self_claim, lock->protected_obj,
    lock->initialized && !lock->writing
    &&   stays_unchanged(lock->protected_obj)
    && stays_unchanged(lock->self_claim) //Doubt?? why these 2 req.
    );
  return true;
})

Mar 28, 2011 at 7:35 AM

Hi,

  the first bitvector lemma relates the value of the Write bit (defined via bit masking), to an arithmetic property; the Write bit is the sign bit / MSB of the lock's state field. Similarly, the second bit vector lemma characterizes the Readers() and Write() results after incrementing the state variable. Both lemmas are meant to help prove the reader-write lock invariant after a successful atomic update via _InterlockedCompareExchange(). We didn't come up with these lemmas up front, but while "debugging" verification attempts of the function. You can watch the verification break by commenting one or the other. As the comment before the bitvector lemma says, there might be a simpler form to expressed the needed bitvector properties.

  Hope this helps,

  Mark