specification.v 1.42 KB
Newer Older
1 2 3 4 5 6
From program_logic Require Export hoare.
From barrier Require Export barrier.
From barrier Require Import proof.
Import uPred.

Section spec.
7
Context {Σ : gFunctors} `{!heapG Σ} `{!barrierG Σ}. 
8 9 10 11 12 13

Local Notation iProp := (iPropG heap_lang Σ).

(* TODO: Maybe notation for LocV (and Loc)? *)
Lemma barrier_spec (heapN N : namespace) :
  heapN  N 
14
   recv send : loc  iProp -n> iProp,
15 16
    ( P, heap_ctx heapN  {{ True }} newbarrier #() {{ λ v,
                              l : loc, v = LocV l  recv l P  send l P }}) 
17 18
    ( l P, {{ send l P  P }} signal (LocV l) {{ λ _, True }}) 
    ( l P, {{ recv l P }} wait (LocV l) {{ λ _, P }}) 
19
    ( l P Q, recv l (P  Q) ={N}=> recv l P  recv l Q) 
20 21 22 23 24 25
    ( l P Q, (P - Q)  (recv l P - recv l Q)).
Proof.
  intros HN.
  exists (λ l, CofeMor (recv heapN N l)), (λ l, CofeMor (send heapN N l)).
  split_and?; simpl.
  - intros P. apply: always_intro. apply impl_intro_r.
Ralf Jung's avatar
Ralf Jung committed
26
    rewrite -(newbarrier_spec heapN N P) // always_and_sep_r.
27 28 29 30 31
    apply sep_mono_r, forall_intro=>l; apply wand_intro_l.
    by rewrite right_id -(exist_intro l) const_equiv // left_id.
  - intros l P. apply ht_alt. by rewrite -signal_spec right_id.
  - intros l P. apply ht_alt.
    by rewrite -(wait_spec heapN N l P) wand_diag right_id.
32
  - intros l P Q. apply vs_alt. rewrite -(recv_split heapN N N l P Q) //.
Ralf Jung's avatar
Ralf Jung committed
33
  - intros l P Q. apply recv_weaken.
34 35
Qed.
End spec.