Skip to content

GitLab

Commit ed371062 authored by Zhen Zhang's avatar Zhen Zhang
Browse files

improve proofs

parent 49861aa5
Expand all Hide whitespace changes
Inline Side-by-side
Makefile.coq
View file @ ed371062
......@@ -99,11 +99,7 @@ endif
VFILES:=sync.v\
pair_cas.v\
flat.v\
sync_stack.v\
protocol.v\
misc.v\
atomic_pair.v\
srv.v
atomic_pair.v
ifneq ($(filter-out archclean clean cleanall printenv,$(MAKECMDGOALS)),)
-include $(addsuffix .d,$(VFILES))
......
_CoqProject
View file @ ed371062
......@@ -2,8 +2,4 @@
sync.v
pair_cas.v
flat.v
sync_stack.v
protocol.v
misc.v
atomic_pair.v
srv.v
flat.v
View file @ ed371062
This diff is collapsed.
incr.v deleted 100644 → 0
View file @ 49861aa5
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
From iris.proofmode Require Import invariants tactics.
From iris.heap_lang Require Import proofmode notation.
From iris.tests Require Import atomic.
From iris.heap_lang Require Import spin_lock.
From flatcomb Require Import sync.
Section sync_incr.
Context `{!heapG Σ, !lockG Σ} (N : namespace).
Definition α (l: val) (v: Z) := (∃ l': loc, l = #l' ∧ l' ↦ #v)%I.
Definition β (l: val) (v: Z) ret := (∃ l': loc, l = #l' ∧ ret = #v ★ l' ↦ #(v + 1))%I.
Variable R: val → iProp Σ.
Definition incr_seq: val :=
λ: "l",
let: "v" := !"l" in
"l" <- "v" + #1;;
"v".
Lemma incr_seq_spec:
∀ (l: val) (x: Z) (Φ: val → iProp Σ),
heapN ⊥ N →
heap_ctx ★ α l x ★ (∀ v, β l x v -★ Φ v)
⊢ WP incr_seq l {{ Φ }}.
Proof.
rewrite /α /β.
iIntros (l x Φ HN) "(#Hh & Hl & HΦ)".
wp_let. iDestruct "Hl" as (l') "[% Hl]". subst.
wp_load. wp_let. wp_op. wp_store.
iSpecialize ("HΦ" $! #x with "[Hl]"); first by eauto.
by iApply "HΦ".
Qed.
Local Opaque incr_seq.
Definition cons: val := λ: <>, ref #0.
Definition cons_spec :=
∀ (Φ: val → iProp Σ),
heapN ⊥ N →
heap_ctx ★ (∀ v, R v -★ Φ v)%I
⊢ WP cons #() {{ Φ }}.
Lemma mk_increr_spec:
∀ (Φ: val → iProp Σ),
heapN ⊥ N →
cons_spec →
heap_ctx ★
(∀ obj: val, conc_obj_triple α β (nclose heapN) ⊤ (obj #()) -★ Φ obj)
⊢ WP mk_whatever cons incr_seq #() {{ Φ }}.
Proof.
iIntros (Φ HN Hcons) "[#Hh HΦ]".
iApply mk_whatever_spec=>//.
- rewrite /whatever_seq_spec. apply incr_seq_spec.
- by iFrame.
Qed.
End sync_incr.
pair_cas.v
View file @ ed371062
......@@ -90,9 +90,9 @@ Section proof.
Definition is_plock (fs: val) (R1 R2 : iProp Σ) : iProp Σ :=
(∃ (l1 l2: loc) (f1 f2 f3: val) (γ1 γ2: gname),
heapN ⊥ N ∧ heap_ctx ∧ fs = (f1, f2, f3)%V ∧
refines f1 (casp_seq' l1 l2) (plock_inv γ1 γ2 R1 R2 l1 l2) ∧
refines f2 (loadp_seq' l1 l2) (plock_inv γ1 γ2 R1 R2 l1 l2) ∧
refines f3 (storep_seq' l1 l2) (plock_inv γ1 γ2 R1 R2 l1 l2))%I.
synced f1 (casp_seq' l1 l2) (plock_inv γ1 γ2 R1 R2 l1 l2) ∧
synced f2 (loadp_seq' l1 l2) (plock_inv γ1 γ2 R1 R2 l1 l2) ∧
synced f3 (storep_seq' l1 l2) (plock_inv γ1 γ2 R1 R2 l1 l2))%I.
Global Instance is_plock_persistent p R1 R2: PersistentP (is_plock p R1 R2).
Proof. apply _. Qed.
......@@ -150,7 +150,7 @@ Section proof.
iIntros "(#Hp & HΦ)".
iLöb as "Hl".
wp_rec. wp_let.
rewrite /is_plock /refines.
rewrite /is_plock /synced.
iDestruct "Hp" as (l1 l2 casp loadp storep γ1 γ2) "(#? & #? & % & #HRcas & _ & #HRstore)".
subst. wp_proj. wp_proj. wp_bind (casp _).
iAssert ({{ True }} casp (#false%V, #true%V)%E {{ z, z = #false ∨ (z =#true ★ plocked ★ R1 ★ R2)}})%I as "#HP".
......
protocol.v deleted 100644 → 0
View file @ 49861aa5
From iris.algebra Require Export sts.
From iris.program_logic Require Import ghost_ownership.
From iris.prelude Require Export gmap.
Inductive state :=
| Init
| Req
| Exec
| Resp
| Ack.
Inductive token := White | Black | Lock.
Global Instance stateT_inhabited: Inhabited state := populate Init.
Inductive prim_step : relation state :=
| Initialize: prim_step Init Req
| Execute: prim_step Req Exec
| Respond: prim_step Exec Resp
| Acknowledge: prim_step Resp Ack.
Definition tok (s : state) : set token :=
match s with
| Init | Ack => {[ Black; White ]}
| Req | Resp => {[ White ]}
| Exec => {[ Lock ]}
end.
Global Arguments tok !_ /.
Canonical Structure sts := sts.STS prim_step tok.
srv.v deleted 100644 → 0
View file @ 49861aa5
This diff is collapsed.
sync.v
View file @ ed371062
......@@ -24,20 +24,20 @@ Global Opaque mk_sync.
Section syncer.
Context `{!heapG Σ, !lockG Σ} (N: namespace).
(* f' refines f *)
Definition refines (f' f: val) (R: iProp Σ): iProp Σ :=
(* R synced f w.r.t f' *)
Definition synced (f' f: val) (R: iProp Σ): iProp Σ :=
(□ ∀ (x: expr) (v: val) (P: iProp Σ) (Q: val -> iProp Σ),
to_val x = Some v -★
{{ R ★ P }} f x {{ z, R ★ Q z }} -★
{{ P }} f' x {{ z, Q z }})%I.
Global Instance refines_persistent f f' R: PersistentP (refines f f' R).
Global Instance synced_persistent f f' R: PersistentP (synced f f' R).
Proof. apply _. Qed.
Global Opaque refines.
Global Opaque synced.
Definition is_syncer (R: iProp Σ) (s: val) : iProp Σ :=
(∀ (f : val), WP s f {{ f', refines f' f R }})%I.
(∀ (f : val), WP s f {{ f', synced f' f R }})%I.
Lemma mk_sync_spec_wp:
∀ (R: iProp Σ) (Φ: val -> iProp Σ),
......@@ -51,7 +51,7 @@ Section syncer.
iFrame "HR".
iIntros (lk γ) "#Hl". wp_let. iApply "HΦ". iIntros "!#".
rewrite /is_syncer. iIntros (f).
wp_let. iVsIntro. rewrite /refines. iIntros "!#".
wp_let. iVsIntro. rewrite /synced. iIntros "!#".
iIntros (x v P Q <-%of_to_val) "#Hf !# HP".
wp_let.
wp_bind (acquire _).
......@@ -143,23 +143,23 @@ Section atomic_sync.
iIntros (s) "#Hsyncer".
wp_let. rewrite /is_syncer /seq_spec.
wp_bind (f_seq _). iApply wp_wand_r. iSplitR; first by iApply (Hseq with "[]")=>//.
iIntros (f) "%". (* FIXME: name *)
iIntros (f Hf).
iApply wp_wand_r. iSplitR; first by iApply "Hsyncer".
iIntros (v) "#Hrefines".
iIntros (v) "#Hsynced".
iExists γ. iFrame. iIntros (x).
iAlways. rewrite /atomic_triple'.
iIntros (P Q) "#Hvss".
rewrite /refines.
iDestruct "Hrefines" as "#Hrefines".
iSpecialize ("Hrefines" $! (of_val x) x P Q).
iApply ("Hrefines" with "[]"); first by rewrite to_of_val.
rewrite /synced.
iDestruct "Hsynced" as "#Hsynced".
iSpecialize ("Hsynced" $! (of_val x) x P Q).
iApply ("Hsynced" with "[]"); first by rewrite to_of_val.
iAlways. iIntros "[HR HP]". iDestruct "HR" as (g) "[Hϕ HgFull]".
(* we should view shift at this point *)
iDestruct ("Hvss" $! g) as "[Hvs1 [Hvs2 Hvs3]]".
iApply pvs_wp.
iVs ("Hvs1" with "HP") as "[HgFrag #Hα]".
iVs ("Hvs2" with "[HgFrag]") as "HP"; first by iFrame.
iVsIntro. iApply H=>//. (* FIXME: name *)
iVsIntro. iApply Hf=>//.
iFrame "Hh Hϕ". iSplitR; first done. iIntros (ret g') "Hϕ' Hβ".
iVs ("Hvs1" with "HP") as "[HgFrag _]".
iCombine "HgFull" "HgFrag" as "Hg".
......
sync_stack.v deleted 100644 → 0
View file @ 49861aa5
From iris.program_logic Require Export weakestpre hoare.
From iris.proofmode Require Import invariants ghost_ownership.
From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import proofmode notation.
From iris.heap_lang.lib Require Import spin_lock.
From iris.algebra Require Import excl.
From flatcomb Require Import sync.
Import uPred.
Definition mk_stack: val :=
λ: <>,
let: "s" := mk_sync #() in
let: "lhd" := ref NONE in
("s" (* push *)
(λ: "x",
let: "hd" := !"lhd" in
"lhd" <- SOME (ref("x", "hd"))),
"s" (* pop *)
(λ: <>,
let: "hd" := !"lhd" in
match: "hd" with
NONE => NONE
| SOME "l" =>
let: "x" := Fst !"l" in
let: "xs" := Snd !"l" in
"lhd" <- "xs";;
SOME "x"
end),
"s" (* "iter" *)
(rec: "iter" "f" :=
let: "hd" := Fst !"lhd" in
match: "hd" with
NONE => #()
| SOME "l" =>
let: "x" := Fst !"l" in
let: "xs" := Snd !"l" in
"f" "x";;
"iter" "xs"
end)).
Definition push: val := λ: "s", Fst (Fst "s").
Definition pop: val := λ: "s", Snd (Fst "s").
Definition iter: val := λ: "s", Snd "s".
Section proof.
Context `{!heapG Σ} (N: namespace).
Implicit Types l : loc.
(* copied from /tests/list_reverse.v *)
Fixpoint is_stack (hd : val) (xs : list val) :=
match xs with
| [] => hd = NONEV
| x :: xs => ∃ l hd', hd = SOMEV #l ★ l ↦ (x,hd') ★ is_stack hd' xs
end%I.
End proof.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment