Why does data_at_conflict require identical shares?

Question

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?

Answer 1

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.

Answer 2

To add to the above answer, yes disjoint shares to the same pointer of memory are considered separated. For example, one can split a readable share into two disjoint shares using slice.split_readable_share, and use the result with data_at_share_join to split a pointer with the original share into two separated pointers to the same block of memory with two disjoint readable shares.

As suggested in the question, one way to ensure two pointers with readable shares cannot alias is to require that the two shares have identical shares. However, a somewhat more general condition is instead to add a precondition nonempty_share (Share.glb sh1 sh2). Then you can use the data_at_conflict_glb lemma in the answer above to get a contradiction if the pointers do alias.

Note: nonempty_share sh and sepalg.nonidentity sh are (definitionally) the same.