Commit b7a6d2b0 authored by Ike Mulder's avatar Ike Mulder
Browse files

Added AtomicFreezer, removed state from AtomicLock. I don't think these can be unified.

parent e00f1161
Pipeline #60382 passed with stage
in 12 minutes and 12 seconds
......@@ -12,7 +12,7 @@ Section problems.
iExists #42; iStepsS.
Qed.
Hint Mode ReshapeExprAnd + ! - - ! : typeclass_instances.
Hint Mode defs.ReshapeExprAnd + ! - - ! : typeclass_instances.
Lemma exist_wand_autom : |==> ( (v : val), WP (ref v) {{ λ v, (l : loc), v = #l l #42 }})%I.
Proof.
......@@ -22,13 +22,13 @@ Section problems.
search_abd.find_abd_step.
search_abd.find_abd_step.
eapply search_abd.abd_unfoldgoal_from_base.
eapply abduct_from_execution. iSolveTC. split.
eapply weakestpre.abduct_from_execution. iSolveTC. split.
match goal with
| |- ?el = ?K ?er =>
idtac el; idtac K; idtac er;
unify K (fill (Λ := heap_ectxi_lang) []); by simpl
end.
notypeclasses refine (as_template_step).
notypeclasses refine (defs.as_template_step).
eapply class_instances_heaplang.alloc_step_wp.
all: iSolveTC || simpl.
Fail iStepS. (* cannot step since there is an update on the RHS.. but even if that were gone, there would be a ▷ and a forall *)
......@@ -47,9 +47,128 @@ Section problems.
namely, the a is instantiated with an evar, while it should be an existential *)
Fail solve [iStepsS; match goal with | |- ?P => idtac P end].
iStepS.
(* iStepDebug.
solveStep with "H1".
split.
assert (∀ A, A ∧ A → A) by (move => ?; case; done).
apply H. split.
- eapply lemmas_abd.abd_witness_postpone.
intros. cbn.
eapply lemmas_abd.abd_forall_one; [ iSolveTC | cbn ].
eapply lemmas_abd.abduct_wand; [iSolveTC | cbn | ].
iSolveTC. cbn. iSolveTC. iSolveTC.
- admit. (* eapply lemmas_abd.abd_forall_postpone; [ iSolveTC | ].
intros. cbn.
eapply lemmas_abd.abduct_wand; [iSolveTC | cbn | ].
eapply lemmas_abd.abd_witness_postpone; [ | ].
intros. cbn. all: admit. *)
- iSolveTC.
- reduction.pm_reduce. cbn.
iStepS.
iStepS.
iStepS.
iStepS. *)
iMod "H2"; iRevert "H2". iStepsS.
Qed.
Lemma advanced_existentials3 {A : Type} (f g : A A) (G R : A A iProp Σ) :
(( a b, R a b - G (f a) b) |==> a y, R a (g y))%I @{iPropI Σ} |==> x y, G x (g y).
Proof.
Fail solve [iStepsS]. (* current system cannot handle this *)
iStepS.
iMod "H2". iReIntro "H2".
iStepsS. (* even though it is provable *)
Restart.
iStepS.
iStepDebug.
solveStep with "H1".
split.
eapply abd_forall_both; [ iSolveTC | intros; eexists; eexists; split ].
eapply abd_witness_both; [ intros; eexists; eexists; split | ].
eapply abd_witness_both; [ intros; eexists; eexists; split | ].
eapply abd_forall_both; [ iSolveTC | intros; eexists; eexists; split ].
eapply lemmas_abd.abduct_wand; [iSolveTC | cbn | ]. iSolveTC.
all: try iSolveTC || simpl.
(* if we get more clever with rewrites this would be an appropriate goal *)
Restart.
iStepS.
iAssert (|==> x y, G x (g y) emp)%I with "[H1 H2]" as ">H"; last (iReIntro "H"; iStepsS).
iStepDebug.
solveStep.
solveStep with "H1".
split.
eapply biabd_forall_both; [ iSolveTC | intros; eexists; eexists; eexists; eexists; split | ].
eapply biabd_witness_both; [ intros; eexists; eexists; eexists; eexists; split | | | ].
eapply biabd_witness_both; [ intros; eexists; eexists; eexists; eexists; split | | | ].
eapply biabd_forall_both; [ iSolveTC | intros; eexists; eexists; eexists; eexists; split | ].
eapply lemmas.biabd_wand; [iSolveTC | ].
iSolveTC.
all: try iSolveTC || simpl.
simple notypeclasses refine (ex_intro _ _ _); last cbn beta; iSolveTC.
simple notypeclasses refine (ex_intro _ _ _); last cbn beta; iSolveTC.
all: try iSolveTC || simpl.
iSolveTC.
simple notypeclasses refine (ex_intro _ _ _); last cbn beta; iSolveTC.
all: try iSolveTC || simpl.
iSolveTC.
simple notypeclasses refine (ex_intro _ _ _); last cbn beta; iSolveTC.
solveStep. (* as before: if we get more clever with rewrites this will be okay *)
Restart. iStepS. iMod "H2". iReIntro "H2". iStepsS.
Qed.
Lemma advanced_existentials4 {A : Type} (f g : A A) (G R : A A iProp Σ) :
(( b a, R a b - G (f a) b) |==> a y, R a (g y))%I @{iPropI Σ} |==> x y, G x (g y).
Proof.
Fail solve [iStepsS]. (* current system cannot handle this *)
iStepS.
iMod "H2". iReIntro "H2".
iStepsS. (* even though it is provable *)
Restart.
iStepS.
iStepDebug.
solveStep with "H1".
split.
eapply abd_witness_both; [ intros; eexists; eexists; split | ].
eapply abd_witness_both; [ intros; eexists; eexists; split | ].
eapply abd_forall_both; [ iSolveTC | intros; eexists; eexists; split ].
eapply abd_forall_both; [ iSolveTC | intros; eexists; eexists; split ].
eapply lemmas_abd.abduct_wand; [iSolveTC | cbn | ]. iSolveTC.
all: try iSolveTC || simpl.
(* if we get more clever with rewrites this would be an appropriate goal *)
Restart.
iStepS.
iAssert (|==> x y, G x (g y) emp)%I with "[H1 H2]" as ">H"; last (iReIntro "H"; iStepsS).
iStepDebug.
solveStep.
solveStep with "H1".
split.
eapply biabd_forall_both; [ iSolveTC | intros; eexists; eexists; eexists; eexists; split | ].
eapply biabd_witness_both; [ intros; eexists; eexists; eexists; eexists; split | | | ].
eapply biabd_witness_both; [ intros; eexists; eexists; eexists; eexists; split | | | ].
eapply biabd_forall_both; [ iSolveTC | intros; eexists; eexists; eexists; eexists; split | ].
eapply lemmas.biabd_wand; [iSolveTC | ].
iSolveTC.
all: try iSolveTC || simpl.
simple notypeclasses refine (ex_intro _ _ _); last cbn beta; iSolveTC.
simple notypeclasses refine (ex_intro _ _ _); last cbn beta; iSolveTC.
all: try iSolveTC || simpl.
iSolveTC.
simple notypeclasses refine (ex_intro _ _ _); last cbn beta; iSolveTC.
all: try iSolveTC || simpl.
iSolveTC.
simple notypeclasses refine (ex_intro _ _ _); last cbn beta; iSolveTC.
solveStep. (* as before: if we get more clever with rewrites this will be okay *)
Restart. iStepS. iMod "H2". iReIntro "H2". iStepsS.
Qed.
Context `{!Fractional (PROP := iPropI Σ) P}.
Context `{!inG Σ $ authUR $ optionUR $ exclR $ leibnizO Qp}.
......
......@@ -80,7 +80,7 @@ Section spec.
(l' : loc), l #l' P l'.
Definition queued_loc γe l γ : iProp Σ :=
own γ (to_agree l, 1%Qp) ( (b : bool), l {#1/2} #b (b = true (b = false own γe ( Excl' l) own γ (to_agree l, 1/2)%Qp l {#1/2} #b))).
own γ (to_agree l, 1%Qp) ( (b : bool), l {#1/2} #b (b = true (b = false own γe ( (Excl' l)) own γ (to_agree l, 1/2)%Qp l {#1/2} #b))).
Global Program Instance own_frac_or_as_forall l γ R :
IntoForallCareful (own γ (to_agree l, 1%Qp) R)%I (λ (q : Qp), own γ (to_agree l, q) - (own γ (to_agree l, q) R))%I.
......@@ -90,6 +90,11 @@ Section spec.
Definition is_queue_head γe (p : loc) : iProp Σ := own γe ( (Excl' p)).
Global Instance update_lock_holder_biabd γe l1 l2 E :
BiAbd (TTl := [tele_pair loc]) (TTr := [tele]) false (own γe ( (Excl' l1))) (own γe ( (Excl' l2))) (fupd E E)
(λ p, own γe ( (Excl' p)))%I (λ p, own γe ( (Excl' l2)) p = l1)%I | 99.
Proof. rewrite /BiAbd /=. iStepS. iStepS. rewrite comm. iStepsS. Qed.
Definition acquired_node γe n (p : loc) : iProp Σ :=
(n + 1) #p own γe ( (Excl' p)) p #false (l' : loc), n #l' is_queued_loc γe l' l' {#1/2} #true.
......@@ -98,39 +103,7 @@ Section spec.
acquire_with #l #n
<< RET #(); holds_at_loc l (is_queued_loc γe) is_queue_head γe p acquired_node γe n p >>.
Proof.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS. iLeft.
iStepsS. iLeft.
iStepS. iRight.
iStepS.
iStepS.
......@@ -156,7 +129,8 @@ Section spec.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS. (* need to manually open invs, otherwise the AU will and can no longer be be opened.
I think this could be fixed by instead using |={⊤,E}=> masks instead of |={⊤ ∖ E, ∅}=> masks.. *)
iMod (inv_acc with "H7") as "[HN HNcl]"; first done.
iMod "H5" as (p) "[[Hl >Hp] Hcl]".
iReIntro "HN".
......@@ -203,33 +177,7 @@ Section spec.
SPEC ⟨↑N_node (p : loc), << acquired_node γe n p' ¦ holds_at_loc l (is_queued_loc γe) is_queue_head γe p >>
release_with #l #n
<< (p'' : loc), RET #(); free_node n ¦ holds_at_loc l (is_queued_loc γe) is_queue_head γe p'' >>.
Proof.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS. iRight.
iStepS.
iMod "H8" as (p) "[[Hl Hp] [_ Hcl]]".
iReIntro "Hp".
iAssert (|==> is_queue_head γe x0 own γe ( Excl' x0))%I with "[H8 H3]" as ">[H8 H3]"; first iStepsS.
iMod ("Hcl" with "[Hl H8]") as "HΦ"; first iFrame.
iStepS.
iStepsS.
Qed.
Proof. iSmash. Qed.
Global Program Instance new_node_spec :
SPEC {{ True }}
......@@ -256,19 +204,17 @@ Section spec.
Definition lock_state (γe : gname) (l p : loc) : iProp Σ :=
holds_at_loc l (is_queued_loc γe) is_queue_head γe p.
Definition locked_at (γe : gname) (v : val) : iProp Σ
:= (n : loc) (p : loc), v = #n acquired_node γe n p.
Definition locked_at (γe : gname) (p : loc) (v : val) : iProp Σ
:= (n : loc), v = #n acquired_node γe n p.
Obligation Tactic := idtac.
Global Program Instance clh_lock_atomic_lock : atomic_lock.atomic_lock Σ :=
atomic_lock.AtomicLock new_lock acquire release gname loc loc (nroot.@ "free") (λ l, #l) lock_state locked_at _ _ _ _ _.
Next Obligation. iStepsS. Qed.
(* Next Obligation. iStepsS. Qed.*)
Next Obligation. intros. iSmash. Qed.
Next Obligation. intros. iSmash. Qed.
(* nice! :) *)
Global Program Instance clh_lock_atomic_lock : atomic_state_freezer.atomic_freezer Σ :=
atomic_state_freezer.AtomicFreezer _ _ new_lock acquire release gname loc loc ( N_node) (nroot.@ "free") (λ l, #l) lock_state locked_at _ _ _ _ _ _ _.
Next Obligation. verify_tac. Qed.
Next Obligation. verify_tac. Qed.
Next Obligation. verify_tac. Qed.
Next Obligation. intros; iSmash. Qed. (* verify_tac fails since it does induction, then gets conflicted on a ▷ ⌜_⌝ which is not used because of the later *)
Next Obligation. intros; iSmash. Qed.
End spec.
......
......@@ -17,41 +17,37 @@ Module atomic_lock.
(** * Predicates *)
(** [name] is used to associate locked with [is_lock] *)
name : Type;
state : Type;
raw_lock : Type;
lock_mask : coPset;
client_namespace : namespace;
as_lock : raw_lock val;
lock_state (γ : name) (lock : raw_lock) (s : state) : iProp Σ;
lock_inv (γ : name) (lock : raw_lock) : iProp Σ;
locked_at (γ : name) (v : val) : iProp Σ;
can_have_clients : client_namespace lock_mask;
(* usually, locked_at is slightly more than just an exclusive proposition: it contains knowledge on the exact state of
the lock. In previous versions, we used 'locked_at γ s v' where 'locked_at γ s1 v ∗ lock_state γ lock s2 ⊢ ⌜s1 = s2⌝'.
This information is not required to prove that one can implement an iCap lock, so we currently do not expose it in the
atomic_lock interface *)
state_inhabited :> Inhabited state ;
(* lock_state_timeless γ lk s :> Laterable (lock_state γ lk s);*)
(* lock_state_exclusize γ lk b1 b2 : lock_state γ lk b1 -∗ lock_state γ lk b2 -∗ False; -> not included since atomic_heap does not expose that q ≤ 1 *)
(* locked_timeless γ s v :> Laterable (locked_at γ s v);*)
locked_at_exclusive γ v1 v2 : locked_at γ v1 - locked_at γ v2 - False;
(* locked_state_at_agree γ lk s1 s2 v : ▷ lock_state γ lk s1 -∗ ▷ locked_at γ s2 v -∗ ◇ ⌜s1 = s2⌝;*)
locked_at_exclusive γ v1 v2 lk : lock_inv γ lk - locked_at γ v1 - locked_at γ v2 - False;
(** * Program specs *)
newlock_spec :>
SPEC {{ True }} newlock #() {{ (lk : raw_lock) (s : state) γ, RET (as_lock lk); lock_state γ lk s }} ;
SPEC {{ True }} newlock #() {{ (lk : raw_lock) γ, RET (as_lock lk); lock_inv γ lk }} ;
acquire_spec γ (lk : raw_lock) :>
SPEC client_namespace s, << lock_state γ lk s >> acquire (as_lock lk) << s' (v : val), RET v; lock_state γ lk s' locked_at γ v >>;
SPEC lock_mask << lock_inv γ lk >> acquire (as_lock lk) << (v : val), RET v; lock_inv γ lk locked_at γ v >>;
release_spec γ (lk : raw_lock) (v : val) :>
SPEC client_namespace s, << locked_at γ v ¦ lock_state γ lk s >> release (as_lock lk) v << s', RET #(); lock_state γ lk s' >>;
SPEC lock_mask << locked_at γ v ¦ lock_inv γ lk >> release (as_lock lk) v << RET #(); lock_inv γ lk >>;
}.
Global Arguments newlock {_ _} _.
Global Arguments acquire {_ _} _.
Global Arguments release {_ _} _.
Global Arguments name {_ _} _.
Global Arguments state {_ _} _.
Global Arguments client_namespace {_ _} _.
Global Arguments lock_mask {_ _} _.
Global Arguments raw_lock {_ _} _.
Global Arguments lock_state {_ _} _ _ _ _.
Global Arguments locked_at {_ _} _ _.
Global Arguments AtomicLock {_ _} _ _ _ _ _ _ _ _ _ _ _ _ _.
Global Arguments lock_inv {_ _} _ _ _.
Global Arguments locked_at {_ _} _ _ _.
Global Arguments AtomicLock {_ _} _ _ _ _ _ _ _ _ _ _ _.
Local Obligation Tactic := program_smash_verify.
......@@ -64,72 +60,48 @@ Module atomic_lock.
Section as_icap_lock.
Context `{!heapGS Σ, iCapLockG Σ} {L : atomic_lock Σ}.
Let N := client_namespace L.
Global Instance locked_at_exclusive_merge1 γ v1 v2 :
MergableConsume ( locked_at L γ v1) (λ p Pin Pout,
TCAnd (TCEq Pin (locked_at L γ v2)) $
TCEq Pout ( False)%I).
Proof.
rewrite /MergableConsume => p Pin Pout [-> ->].
rewrite bi.intuitionistically_if_elim comm locked_at_exclusive.
apply bi.wand_elim_l.
Qed.
Global Instance locked_at_exclusive_merge2 γ v1 v2 :
MergableConsume (locked_at L γ v1) (λ p Pin Pout,
TCAnd (TCEq Pin ( locked_at L γ v2)%I) $
TCEq Pout ( False)%I).
Proof.
rewrite /MergableConsume => p Pin Pout [-> ->].
rewrite bi.intuitionistically_if_elim. by iStepS.
Qed.
Global Instance locked_at_exclusive_merge3 γ v1 v2 :
MergableConsume (locked_at L γ v1) (λ p Pin Pout,
TCAnd (TCEq Pin (locked_at L γ v2)%I) $
TCEq Pout ( False)%I).
Proof.
rewrite /MergableConsume => p Pin Pout [-> ->].
rewrite bi.intuitionistically_if_elim. rewrite (bi.later_intro (locked_at _ _ _)). by iStepS.
Qed.
(* Global Instance locked_at_state_agree1 γ s1 lk s2 v :
MergablePersist (▷ lock_state L γ lk s2) (λ p Pin Pout,
TCAnd (TCEq Pin (▷ locked_at L γ s1 v)%I) $
TCEq Pout (◇ ⌜s2 = s1⌝)%I).
Proof.
rewrite /MergableConsume => p Pin Pout [-> ->].
rewrite bi.intuitionistically_if_elim comm locked_state_at_agree.
erewrite bi.wand_elim_r. eauto.
Qed.
Global Instance locked_at_state_agree2 γ s1 lk s2 v :
MergablePersist (▷ locked_at L γ s1 v) (λ p Pin Pout,
TCAnd (TCEq Pin (▷ lock_state L γ lk s2)%I) $
TCEq Pout (◇ ⌜s2 = s1⌝)%I).
Proof.
rewrite /MergableConsume => p Pin Pout [-> ->].
rewrite bi.intuitionistically_if_elim. by iStepS.
Qed. *)
Let HL := can_have_clients.
Definition locked (γ' : gname) (v : val) : iProp Σ := own γ' ( (Excl' v)).
Definition lock_inv (γ : name L) (γ' : gname) (l : raw_lock L) (R : iProp Σ) : iProp Σ :=
(s : state L) (v : val), lock_state L γ l s
Definition icap_lock_inv (γ : name L) (γ' : gname) (l : raw_lock L) (R : iProp Σ) : iProp Σ :=
lock_inv L γ l (v : val),
((locked_at L γ v own γ' ( (Excl' v))) (R v = NONEV own γ' ( None) own γ' ( None))).
Definition is_lock (γ : name L) (γ' : gname) (lk : val) (R : iProp Σ) : iProp Σ :=
(l : raw_lock L), lk = as_lock l inv N (lock_inv γ γ' l R).
(l : raw_lock L), lk = as_lock l inv N (icap_lock_inv γ γ' l R).
Global Program Instance newlock_spec' :
SPEC {{ True }}
newlock L #()
{{ lk, RET (lk : val); R E, R ={E}= γ γ', is_lock γ γ' lk R }}.
Global Program Instance acquire_spec' γ γ' (lk : val) R :
Global Instance acquire_spec' γ γ' (lk : val) R :
SPEC {{ is_lock γ γ' lk R }}
acquire L lk
{{ (v : val), RET v; locked γ' v R }}.
Proof.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
iStepS.
- iStepS.
iStepS.
* iStepS.
iStepS.
iStepS.
rewrite locked_at_exclusive.
iDestruct ("H5" with "H6 H3") as ">[]".
* iSmash.
- iStepS.
iStepS.
* iSmash.
* iSmash.
Qed.
Global Instance release_spec' γ γ' (lk v : val) R :
SPEC {{ is_lock γ γ' lk R locked γ' v R }}
......@@ -146,8 +118,8 @@ Module atomic_lock.
End as_icap_lock.
End atomic_lock.
Module atomic_lock_stateless.
Class atomic_lock_stateless Σ `{!heapGS Σ} := AtomicLockStateless {
Module atomic_state_freezer.
Class atomic_freezer Σ `{!heapGS Σ} := AtomicFreezer {
(** * Operations *)
newlock : val;
acquire : val;
......@@ -157,47 +129,94 @@ Module atomic_lock_stateless.
name : Type;
state : Type;
raw_lock : Type;
lock_mask : coPset;
client_namespace : namespace;
as_lock : raw_lock val;
lock_state (γ : name) (lock : raw_lock) (s : state) : iProp Σ;
locked_at (γ : name) : iProp Σ;
state_inhabited :> Inhabited (state) ;
(* lock_state_timeless γ lk s :> Laterable (lock_state γ lk s);
(* lock_state_exclusize γ lk b1 b2 : lock_state γ lk b1 -∗ lock_state γ lk b2 -∗ False; -> not included since atomic_heap does not expose that q ≤ 1 *)
locked_timeless γ s :> Laterable (locked_at γ s); *)
locked_at_exclusive γ : locked_at γ - locked_at γ - False;
(* locked_state_at_agree γ lk s1 s2 : ▷ lock_state γ lk s1 -∗ ▷ locked_at γ s2 -∗ ◇ ⌜s1 = s2⌝;*)
locked_at (γ : name) (s : state) (v : val) : iProp Σ;
(* usually, locked_at is slightly more than just an exclusive proposition: it contains knowledge on the exact state of
the lock. In previous versions, we used 'locked_at γ s v' where 'locked_at γ s1 v ∗ lock_state γ lock s2 ⊢ ⌜s1 = s2⌝'.
This information is not required to prove that one can implement an iCap lock, so we currently do not expose it in the
atomic_lock interface *)
state_inhabited :> Inhabited state ;
(* needed to commute laters with ∃. could probably be dropped, but would require manual proofs to use bi.later_exist_except_0 *)
can_have_clients : client_namespace lock_mask;
locked_at_state_neq γ s1 s2 v1 v2 : locked_at γ s1 v1 - locked_at γ s2 v2 - s1 s2;
locked_state_at_agree γ lk s1 s2 v : lock_state γ lk s1 - locked_at γ s2 v - s1 = s2;
(** * Program specs *)
newlock_spec :>
SPEC {{ True }} newlock #() {{ (lk : raw_lock) (s : state) γ, RET (as_lock lk); lock_state γ lk s }} ;
acquire_spec γ (lk : raw_lock) :>
SPEC client_namespace s, << lock_state γ lk s >> acquire (as_lock lk) << s', RET #(); lock_state γ lk s' locked_at γ >>;
SPEC lock_mask s, << lock_state γ lk s >> acquire (as_lock lk) << s' (v : val), RET v; lock_state γ lk s' locked_at γ s' v >>;
release_spec γ (lk : raw_lock) (v : val) s' :>
SPEC lock_mask s, << locked_at γ s' v ¦ lock_state γ lk s >> release (as_lock lk) v << s'', RET #(); lock_state γ lk s'' (* ∗ ⌜s'' ≠ s⌝ *) >>;
}. (* the s'' ≠ s condition is required for liveness. but since our logic is not able to prove liveness conditions, we can omit it: proofs will still go through *)
Program Definition lock_from_freezer `{heapGS Σ} (af : atomic_freezer Σ) : atomic_lock.atomic_lock Σ :=
atomic_lock.AtomicLock newlock acquire release name raw_lock lock_mask client_namespace as_lock (λ γ l, s, lock_state γ l s)%I (λ γ v, s, locked_at γ s v)%I _ _ _ _ _.
Next Obligation. intros. apply can_have_clients. Qed.
Next Obligation.
intros. do 3 iStepS.
iDestruct (locked_state_at_agree with "H1 H3") as "#>->".
iDestruct (locked_state_at_agree with "H1 [H2]") as "#>->"; first iFrame.
iDestruct (locked_at_state_neq with "H2 H3") as ">%". contradiction.
Qed.
Next Obligation. intros. iSmash. Qed.
Next Obligation. intros. cbn. iSmash. Qed.
Next Obligation. intros. cbn. iSmash. Qed.
(* My hypothesis is that every real lock can be seen as a freezer in some way. but this is hard to show, I'm not sure how.
One problem is that in fact it is fine for a lock to change some part of its state, as long as some part remains fixed.
this fixed part is the one witnessed to be frozen *)
End atomic_state_freezer.
Module atomic_lock_stateless.
Class atomic_lock_stateless Σ `{!heapGS Σ} := AtomicLockStateless {
(** * Operations *)
newlock : val;
acquire : val;
release : val;
(** * Predicates *)
(** [name] is used to associate locked with [is_lock] *)
name : Type;
raw_lock : Type;
lock_mask : coPset;
client_namespace : namespace;
as_lock : raw_lock val;
lock_inv (γ : name) (lock : raw_lock) : iProp Σ;
locked_at (γ : name) : iProp Σ;
can_have_clients : client_namespace lock_mask;
locked_at_exclusive γ lk : lock_inv γ lk - locked_at γ - locked_at γ - False;
(** * Program specs *)
newlock_spec :>
SPEC {{ True }} newlock #() {{ (lk : raw_lock) γ, RET (as_lock lk); lock_inv γ lk }} ;
acquire_spec γ (lk : raw_lock) :>
SPEC lock_mask << lock_inv γ lk >> acquire (as_lock lk) << RET #(); lock_inv γ lk locked_at γ >>;
release_spec γ (lk : raw_lock) :>
SPEC client_namespace s, << locked_at γ ¦ lock_state γ lk s >> release (as_lock lk) << s', RET #(); lock_state γ lk s' >>;