specification.v 1.16 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 `{!heapG Σ} `{!barrierG Σ}.
9

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