Skip to content
GitLab
Commit e3064586 authored by Ike Mulder's avatar Ike Mulder
Browse files

Barrier can work, if we get abddisj working and maybe an extended, backtracking version?

parent 0fc71aac
Hide whitespace changes
Inline Side-by-side
theories/examples/comparison/barrier.v
View file @ e3064586
......@@ -84,25 +84,49 @@ Section proof.
Definition barrier_inv (threads : positive) γp1 γp2 γt γb (l : loc) : iProp Σ :=
∃ (z : Z), l ↦ #z ∗ own γt (CoPset $ tickets_geq (S (Z.abs_nat z))) ∗ own γb (● Excl' z) ∗ (
(⌜0 ≤ z⌝%Z ∗ (
(⌜z < Zpos threads⌝%Z ∗ token_counter P1 γp1 (Z.to_pos (Zpos threads - z)) ∗ no_tokens P2 γp2 1%Qp ∗ own γt (CoPset $ ticket (Z.abs_nat z)) ∗ own γb (◯ Excl' z))
(⌜0 < z⌝%Z ∗ (
(⌜z < Zpos threads⌝%Z ∗
((own γt (CoPset $ ticket (Z.abs_nat z))
∗ ((no_tokens P1 γp1 1%Qp ∗ own γt (CoPset $ ticket 0) ∗ token_counter P2 γp2 (Z.to_pos (Zpos threads - z)))
∨
(own γb (◯ Excl' z) ∗ token_counter P1 γp1 (Z.to_pos (Zpos threads - z)) ∗ no_tokens P2 γp2 1%Qp)
))
∨
(⌜z < Zpos threads⌝%Z ∗ no_tokens P1 γp1 1%Qp ∗ token_counter P2 γp2 (Z.to_pos (Zpos threads - z)) ∗ (own γb (◯ Excl' z) ∨ own γt (CoPset $ ticket (Z.abs_nat z))) ∗ own γt (CoPset $ ticket 0))
((own γb (◯ Excl' z)) ∗ own γt (CoPset $ ticket 0) ∗ no_tokens P1 γp1 1%Qp ∗ token_counter P2 γp2 (Z.to_pos (Zpos threads - z))))
)
∨
(⌜z = Zpos threads⌝ ∗ no_tokens P1 γp1 1%Qp ∗ no_tokens P2 γp2 1%Qp ∗ P1 1 ∗ (own γt (CoPset $ ticket 0) ∨ own γb (◯ Excl' z)) ∗ own γt (CoPset $ ticket $ Pos.to_nat threads))))
∨
(⌜z ≤ 0⌝%Z ∗ (
(⌜Zneg threads < z⌝%Z ∗ token_counter P2 γp2 (Z.to_pos (Zpos threads + z)) ∗ no_tokens P1 γp1 1%Qp ∗ own γt (CoPset $ ticket (Z.abs_nat z)) ∗ own γb (◯ Excl' z))
(⌜z < 0⌝%Z ∗ (
(⌜Zneg threads < z⌝%Z ∗
((own γt (CoPset $ ticket (Z.abs_nat z))
∗ ((no_tokens P2 γp2 1%Qp ∗ own γt (CoPset $ ticket 0) ∗ token_counter P1 γp1 (Z.to_pos (Zpos threads + z)))
∨
(own γb (◯ Excl' z) ∗ token_counter P2 γp2 (Z.to_pos (Zpos threads + z)) ∗ no_tokens P1 γp1 1%Qp)
))
∨
(⌜Zneg threads < z⌝%Z ∗ no_tokens P2 γp2 1%Qp ∗ token_counter P1 γp1 (Z.to_pos (Zpos threads + z)) ∗ (own γb (◯ Excl' z) ∨ own γt (CoPset $ ticket (Z.abs_nat z))) ∗ own γt (CoPset $ ticket 0))
((own γb (◯ Excl' z)) ∗ own γt (CoPset $ ticket 0) ∗ no_tokens P2 γp2 1%Qp ∗ token_counter P1 γp1 (Z.to_pos (Zpos threads + z))))
)
∨
(⌜z = Zneg threads⌝ ∗ no_tokens P1 γp1 1%Qp ∗ no_tokens P2 γp2 1%Qp ∗ P1 1 ∗ (own γt (CoPset $ ticket 0) ∨ own γb (◯ Excl' z)) ∗ own γt (CoPset $ ticket (Pos.to_nat threads)))))).
(⌜z = Zneg threads⌝ ∗ no_tokens P1 γp1 1%Qp ∗ no_tokens P2 γp2 1%Qp ∗ P1 1 ∗ (own γt (CoPset $ ticket 0) ∨ own γb (◯ Excl' z)) ∗ own γt (CoPset $ ticket (Pos.to_nat threads)))))
∨
(⌜z = 0⌝%Z ∗ (
own γt (CoPset $ ticket 0) ∗ own γb (◯ Excl' z) ∗ (
(token_counter P1 γp1 threads ∗ no_tokens P2 γp2 1%Qp)
∨
(no_tokens P1 γp1 1%Qp ∗ token_counter P2 γp2 threads)
)
))
).
(*
token_counter P1 γp1 (Z.to_pos (Zpos threads - z)) ∗ no_tokens P2 γp2 1%Qp ∗ own γt (CoPset $ ticket (Z.abs_nat z)) ∗ own γb (◯ Excl' z))
∨s
no_tokens P1 γp1 1%Qp ∗ token_counter P2 γp2 (Z.to_pos (Zpos threads - z)) ∗ (own γt (CoPset $ ticket (Z.abs_nat z)) ∨ own γb (◯ Excl' z)) ∗ own γt (CoPset $ ticket 0))
(own γt (CoPset $ ticket (Z.abs_nat z)) ∨ ((own γb (◯ Excl' z)) ∗ own γt (CoPset $ ticket 0) ∗ no_tokens P1 γp1 1%Qp ∗ token_counter P2 γp2 (Z.to_pos (Zpos threads - z))) *)
((own γt (CoPset $ ticket (Z.abs_nat z))
∗ ((own γt (CoPset $ ticket 0) ∗ no_tokens P1 γp1 1%Qp ∗ token_counter P2 γp2 (Z.to_pos (Zpos threads - z)))
∨
(own γb (◯ Excl' z) ∗ token_counter P1 γp1 (Z.to_pos (Zpos threads - z)) ∗ no_tokens P2 γp2 1%Qp)
)
)
∨
((own γb (◯ Excl' z)) ∗ own γt (CoPset $ ticket 0) ∗ no_tokens P1 γp1 1%Qp ∗ token_counter P2 γp2 (Z.to_pos (Zpos threads - z)))) *)
Definition is_barrier (threads : positive) γp1 γp2 γt γb (v : val) : iProp Σ :=
∃ (l : loc), ⌜v = #l⌝ ∗ □ (P1 1 ={⊤∖↑N}=∗ P2 1) ∗ □ (P2 1 ={⊤∖↑N}=∗ P1 1) ∗ inv N (barrier_inv threads γp1 γp2 γt γb l).
......@@ -131,15 +155,227 @@ Section proof.
{{ (z : Z), RET #z; ⌜Zneg threads ≤ z ≤ Zpos threads⌝%Z }}.
Proof. iStepsS. Qed.
Program Instance sync_up_enter_spec threads γp1 γp2 γt γb (v : val) :
Lemma extract_ticket threads γt γb γp1 γp2 z1 n2 l :
SolveSepSideCondition (n2 = Z.abs_nat z1)%Z →
SolveSepSideCondition (Z.abs_nat z1 < Zpos threads)%Z →
BiAbd (TTl := [tele]) (TTr := [tele]) false (own γb (◯ Excl' z1)) (own γt (CoPset $ ticket n2)) (fupd ⊤ ⊤)
(inv N (barrier_inv threads γp1 γp2 γt γb l)) emp%I.
Proof.
rewrite /BiAbd /SolveSepSideCondition /= => -> Hz.
iStepS. iInv N as "HN". iRevert "HN". iStepS.
- iStepDebug.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj. iRight.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj. iStepS. iStepS.
all: repeat solveStepDisj.
- iStepDebug.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj. iRight.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj. iStepS. iStepS.
all: repeat solveStepDisj.
Qed.
Instance sync_up_enter_spec threads γp1 γp2 γt γb (v : val) :
SPEC {{ is_barrier threads γp1 γp2 γt γb v ∗ token P1 γp1 }}
sync_up_enter v
{{ (z : Z), RET #z; ⌜0 ≤ z⌝%Z ∗ own γt (CoPset $ ticket (Z.to_nat z)) }}.
Proof.
iStepsS. iLöb as "IH".
wp_lam.
iStepsS.
iAssert (|={⊤}=> own γt (CoPset (ticket (Z.to_nat 0))) ∗ emp)%I with "[-]" as ">[$ _]"; last done.
iStepS.
iStepS. iIntros "!>". iStepsS.
Qed. (*
Program Instance sync_down_enter_spec threads γp1 γp2 γt γb (v : val) :
SPEC {{ is_barrier threads γp1 γp2 γt γb v ∗ token P2 γp2 }}
sync_down_enter v
{{ (z : Z), RET #z; ⌜0 ≤ z⌝%Z ∗ own γt (CoPset $ ticket (Z.to_nat z)) }}.
{{ (z : Z), RET #z; ⌜0 ≤ z⌝%Z ∗ own γt (CoPset $ ticket (Z.to_nat z)) }}. *)
Instance sync_up_exit_spec threads γp1 γp2 γb γt (z : Z) (v : val) :
SPEC {{ is_barrier threads γp1 γp2 γt γb v ∗ ⌜0 ≤ z⌝%Z ∗ own γt (CoPset $ ticket $ Z.to_nat z) }}
......@@ -172,239 +408,64 @@ Section proof.
iStepS.
- iStepsS.
- iStepsS.
- iStepS.
iStepDebug.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj. iRight.
solveStepDisj.
solveStepDisj.
all: repeat solveStepDisj.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
- iStepsS.
iInv N as "HN". iRevert "HN". iStepS.
iStepDebug. solveSteps. iRight. (* bloody later *) admit.
- iStepsS.
- iStepsS.
- iStepsS.
iAssert (|={⊤}=> own γt (CoPset (ticket (0))) ∗ emp)%I with "[-]" as ">[$ _]"; last done.
iStepS.
iStepS. iIntros "!>". iStepsS.
- iStepS.
iStepS.
iStepDebug.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj. iRight.
iStepDebug.
repeat solveStepDisj. iStepsS.
all: repeat
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepsS; try iSmash.
- destruct (decide (z = x3)) as [-> | Hneq]; iSmash.
- iRevert "H4"; iSmash.
Qed.
* iStepS. iStepS. iStepS. iStepsS.
* iStepS. iStepsS.
* iStepS. iStepDebug.
solveSteps. solveStepDisj.
solveStepDisj.
Set Nested Proofs Allowed.
Instance issued_hint x1 x2 γ :
TCIf (SolveSepSideCondition (x1 ≠ x2)) False TCTrue →
BiAbdDisjHypAtom (TTm := [tele]) (TTr := [tele]) false (own γ (CoPset $ ticket x1)) false (own γ (CoPset $ ticket x1) ∗ ⌜x1 = x2⌝%I) (own γ (CoPset $ ticket x2))
id emp%I ⌜x1 = x2⌝%I (⌜x1 ≠ x2⌝ ∗ own γ (CoPset $ ticket x1))%I.
Proof.
move => /= _.
split.
- iStepS.
destruct (decide (x1 = x2)) as [-> | Hneq]; iStepsS.
- rewrite /BiAbd /=.
iStepsS.
Qed.
solveStepDisj.
solveStepDisj.
solveStepDisj.
solveStepDisj.
repeat solveStepDisj. iStepS. iStepsS. iStepsS.
* iStepS. iRevert "H4". iStepS. iStepsS.
* iStepS. iStepsS.
iAssert (|={⊤}=> own γt (CoPset (ticket (Z.to_nat z))) ∗ emp)%I with "[-]" as ">[$ _]"; last done.
iStepS. iStepS. iIntros "!>". iStepsS.
* iStepS. iStepsS.
* iStepS. iStepsS.
* iStepS. iStepsS.
iAssert (|={⊤}=> own γt (CoPset (ticket (Z.to_nat z))) ∗ emp)%I with "[-]" as ">[$ _]"; last done.
iStepS. iStepsS.
* iStepS. iRevert "H4". iStepS. iStepsS.
* iStepS. iRevert "H4". iStepS. iStepsS.
iAssert (|={⊤}=> own γt (CoPset (ticket (Z.to_nat z))) ∗ emp)%I with "[-]" as ">[$ _]"; last done.
iStepS. iStepsS.
Unshelve. apply inhabitant.
Admitted.
(* we need reverts in some places to detect extra inequalities: at some places we have 3 tickets and mergablepersist does not get all currently *)
Global Program Instance sync_up_spec threads γp1 γp2 γt γb (v : val) :
......
theories/steps/solve_sep.v
View file @ e3064586
......@@ -777,8 +777,6 @@ Ltac solveSepStepDisj namer_tac :=