specification.v 1.26 KB
Newer Older
1
From iris.program_logic Require Export hoare.
Ralf Jung's avatar
Ralf Jung committed
2
3
From iris.heap_lang.lib.barrier Require Export barrier.
From iris.heap_lang.lib.barrier Require Import proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
4
From iris.heap_lang Require Import proofmode.
5
6
7
Import uPred.

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

Local Notation iProp := (iPropG heap_lang Σ).

Lemma barrier_spec (heapN N : namespace) :
  heapN  N 
14
   recv send : loc  iProp -n> iProp,
15
    ( P, heap_ctx heapN  {{ True }} newbarrier #() {{ v,
16
17
18
                              l : loc, v = #l  recv l P  send l P }}) 
    ( l P, {{ send l P  P }} signal #l {{ _, True }}) 
    ( l P, {{ recv l P }} wait #l {{ _, P }}) 
19
    ( l P Q, recv l (P  Q) ={N}=> recv l P  recv l Q) 
20
    ( l P Q, (P - Q)  (recv l P - recv l Q)).
21
22
23
24
Proof.
  intros HN.
  exists (λ l, CofeMor (recv heapN N l)), (λ l, CofeMor (send heapN N l)).
  split_and?; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
25
26
27
28
  - iIntros {P} "#? ! _". iApply (newbarrier_spec _ _ P); first done.
    iSplit; [done|]; iIntros {l} "?"; iExists l; by iSplit.
  - iIntros {l P} "! [Hl HP]". by iApply signal_spec; iFrame "Hl HP".
  - iIntros {l P} "! Hl". iApply wait_spec; iFrame "Hl". by iIntros "?".
29
  - intros; by apply recv_split.
Robbert Krebbers's avatar
Robbert Krebbers committed
30
  - apply recv_weaken.
31
32
Qed.
End spec.