Search code examples
verifiable-c

Why does data_at_conflict require identical shares?

I'm trying to prove a contradiction from two aliased pointers

...
  * data_at sha (tarray tulong 5) (map (fun x : Z => Vlong (Int64.repr x)) arra) a
  * data_at shb (tarray tulong 5) (map (fun x : Z => Vlong (Int64.repr x)) arrb) b
|-- !! (a <> b)

I've tried

destruct (Val.eq a b) as [->|Hneq];[|entailer!].
data_at_conflict b.

However, the data_at_conflict b tactic doesn't work, yielding the error

Unable to unify "shb" with "sha".

Why do the shares need to be unified to prove that alaised pointer to separated blocks is a contradiction?

Or am I misunderstanding how shares work? Normally I just assign each read-only pointer its own individual readable_share. Are disjoint shares to the same memory block considered separated?

As to why I'm doing this, the function I'm using has a const and restrict parameter and I was trying to capture that notion in its specification. Should I be using identical shares when writing the specification of functions that use restrict?

Solution

  • Perhaps these lemmas will be useful. In fact, perhaps useful enough we should add them to VST.

    Lemma data_at_conflict_glb: forall {cs: compspecs} sh1 sh2 t v v' p,
  sepalg.nonidentity (Share.glb sh1 sh2) ->
  0 < sizeof t ->
  data_at sh1 t v p * data_at sh2 t v' p |-- FF.
Proof.
  intros.
  pose (sh := Share.glb sh1 sh2).
  assert (sepalg.join sh (Share.glb sh1 (Share.comp sh)) sh1). {
    hnf. 
    rewrite (Share.glb_commute sh1), <- Share.glb_assoc, Share.comp2.
     rewrite Share.glb_commute, Share.glb_bot.
     split; auto. 
     rewrite Share.distrib2, Share.comp1.
      rewrite Share.glb_commute, Share.glb_top.
      unfold sh. rewrite Share.lub_commute, Share.lub_absorb. auto.
   }
  assert (sepalg.join sh (Share.glb sh2 (Share.comp sh)) sh2). {
    hnf. rewrite (Share.glb_commute sh2), <- Share.glb_assoc, Share.comp2.
     rewrite Share.glb_commute, Share.glb_bot.
     split; auto. 
     rewrite Share.distrib2, Share.comp1.
      rewrite Share.glb_commute, Share.glb_top.
      unfold sh. rewrite Share.glb_commute.
     rewrite Share.lub_commute, Share.lub_absorb. auto.
   }
   rewrite <- (data_at_share_join _ _ _ _ _ _ H1).
   rewrite <- (data_at_share_join _ _ _ _ _ _ H2).
    sep_apply data_at_conflict; auto.
   entailer!.
Qed.

Lemma glb_Ews_Ers: sepalg.nonidentity (Share.glb Ews Ers).
Proof.
  unfold Ews, Ers.
  rewrite <- Share.distrib2.
  intro. apply identity_share_bot in H.
  apply lub_bot_e in H. destruct H as [? _].
  apply nonidentity_extern_retainer.
  rewrite H; apply bot_identity.
Qed.


Goal forall {cs: compspecs} v v' p,
   data_at Ews tint v p * data_at Ers tint v' p |-- FF.
Proof.
  intros.
  apply data_at_conflict_glb.
  apply glb_Ews_Ers.
  reflexivity.
Qed.