Module Permissions

Require Import Coqlib Utf8.
Require Import Ast Mem Pointers Integers Utils.

Require Import Utils Emem INJECT.

Notation thread_id:= positive (only parsing).


Section permission.

  Inductive permission : Type :=
  | HiddenBy (t:thread_id)

  | FrozenBy (s:Rset.t).

  Definition empty_perm : permission := FrozenBy Rset.empty.

  Definition perm_map := pointer -> permission.
  Definition upd_perm (d:perm_map) (p0:pointer) (perm:permission) : perm_map :=
    fun p => if Ptr.eq_dec p p0 then perm else d p.

  Lemma perm_gss:
    forall (d : perm_map) (perm : permission) (p : pointer),
    upd_perm d p perm p = perm.

  Lemma perm_gso:
    forall (d : perm_map) (p0 : pointer) (perm : permission) (p : pointer),
      p<>p0 ->
      upd_perm d p0 perm p = d p.

  Inductive is_perm_set : permission -> Prop :=
  | is_perm_set_def: forall s, is_perm_set (FrozenBy s).

  Inductive readable_perm (d:perm_map) (p:pointer) (t:thread_id) : Prop :=
  | readable_perm_case1: forall s
    (RP1: d p = FrozenBy s)
    (RP2: Rset.mem t s = true),
    readable_perm d p t.

  Inductive upd_read_perm_set d p t d' : Prop :=
  | upd_read_perm_set_def: forall s
    (URP1: d p = FrozenBy s)
    (URP2: d' = upd_perm d p (FrozenBy (Rset.add t s))),
    upd_read_perm_set d p t d'.

  Inductive release_perm (t:thread_id) : permission -> permission -> Prop :=
  | release_perm_hiden_by_other : forall t',
    t<> t' ->
    release_perm t (HiddenBy t') (HiddenBy t')
  | release_perm_hiden_by_me :
    release_perm t (HiddenBy t) empty_perm
  | release_perm_frozen_by : forall s,
    release_perm t (FrozenBy s) (FrozenBy (Rset.remove t s)).

  Definition release (t:thread_id) (perm perm':perm_map) : Prop :=
    forall p, release_perm t (perm p) (perm' p).


  Definition is_free t (perm:permission) : Prop :=
    match perm with
      | HiddenBy t' => t<>t'
      | FrozenBy s => Rset.mem t s = false
    end.

End permission.

Definition has_store_perm t (d: perm_map) (p: pointer) : Prop :=
    match d p with
      | HiddenBy t' => t = t'
      | FrozenBy s => Rset.subset s (Rset.singleton t)
    end.

Inductive check_perm_store t : perm_map -> annot_perm -> pointer -> Prop :=
  | check_perm_localstore: forall p d
    (ESD:d p = HiddenBy t),
    check_perm_store t d Local p
  | check_perm_gobalstore: forall p d s
    (ALONE: Rset.subset s (Rset.singleton t))
    (ESD:d p = FrozenBy s),
    check_perm_store t d Global p.

Inductive check_perm_load t : perm_map → annot_perm → pointer → Prop :=
  | check_perm_localload d p
      (RP: readable_perm d p t)
    : check_perm_load t d Local p
  | check_perm_globalload d p
      (RP: match d p with HiddenBy t' => t' = t | FrozenBy _ => True end)
    : check_perm_load t d Global p
.

Inductive perm_step t : perm_map -> perm_event -> perm_map -> Prop :=
  | perm_step_check_store ap p d
    (ESD: check_perm_store t d ap p)
    : perm_step t d (PEcheck_store ap p) d
  | perm_step_check_load ap p d
    (ESD: check_perm_load t d ap p)
    : perm_step t d (PEcheck_load ap p) d
  | perm_step_requeststore: forall p d
    (ESD: has_store_perm t d p)
    (ESWF2: wf_ptr p),
    perm_step t d (PErequest RPwrite p) (upd_perm d p (HiddenBy t))
  | perm_step_requestload: forall p d d'
    (ESD:upd_read_perm_set d p t d')
    (ESWF2: wf_ptr p),
    perm_step t d (PErequest RPread p) d'
  | perm_step_release: forall d d'
    (ESP: release t d d'),
    perm_step t d PErelease d'
  | perm_step_is_free: forall d
    (ESP: forall p, is_free t (d p)),
    perm_step t d PEfreeperm d.


Definition range_has_store_perm t (d: perm_map) (r: arange) : Prop :=
  wf_range r /\
  forall p,
    range_inside (range_of_chunk p Mint32) r ->
    has_store_perm t d p.

Lemma not_free_ranges_disjoint t d p r:
  wf_ptr p -> range_has_store_perm t d r ->
  (match d p with FrozenBy s => ¬ Rset.subset s (Rset.singleton t) | HiddenBy t' => t <> t' end) ->
  ranges_disjoint (range_of_chunk p Mint32) r.

Lemma release_perm_o {t t' s s'} :
  t <> t' -> release_perm t (FrozenBy s) (FrozenBy s') ->
  Rset.mem t' s = Rset.mem t' s'.

Lemma release_perm_empty t : release_perm t empty_perm empty_perm.

Lemma release_func : forall t d d',
  release t d d' <->
  d' = (fun p => match d p with
                               | FrozenBy s => FrozenBy (Rset.remove t s)
                               | HiddenBy t' =>
                                 if peq t t' then empty_perm
                                 else HiddenBy t'
                             end).

Lemma release_deterministe : forall t d d1 d2,
  release t d d1 -> release t d d2 -> d1 = d2.

Lemma perm_step_empty_perm : forall t d1 ap a d p,
  perm_step t d1 (PErequest ap a) d ->
  d p = empty_perm ->
  d1 p = empty_perm.

Require Import Maps.

Lemma rset_mem_remove: forall tid s,
  ~ Rset.mem tid (Rset.remove tid s).
Hint Resolve rset_mem_remove.

Lemma release_frozen: forall tid s1 s2,
  s2 = Rset.remove tid s1 ->
  release_perm tid (FrozenBy s1) (FrozenBy s2).

Lemma release_diamond: forall d' d'' t tid d,
  release tid d d' ->
  release t d d'' ->
  exists d0, release t d' d0 /\ release tid d'' d0.

Ltac perm :=
  unfold has_store_perm in *;
  repeat (repeat (rewrite perm_gso in *;[|congruence]); repeat rewrite perm_gss in *);
  auto.

Lemma has_store_perm_excl t t' d p :
  has_store_perm t d p →
  has_store_perm t' d p →
  t = t' ∨ d p = FrozenBy Rset.empty.