Commit 8d499eb4 authored by Dan Frumin's avatar Dan Frumin

Logically atomic triples for spin lock.

+ deriving sequential specification from log. atomic one
parent 9a3c6fd7
Pipeline #6531 failed with stage
in 0 seconds
-Q theories iris_atomic
-arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
theories/atomic.v
theories/lock.v
theories/sync.v
theories/atomic_incr.v
theories/simple_sync.v
......
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang proofmode notation.
From iris_atomic Require Import atomic.
From iris.proofmode Require Import tactics.
From iris.heap_lang.lib Require Import spin_lock.
Section lock.
Context `{!heapG Σ, !lockG Σ} (N : namespace).
(* Some observations here. It is crucial that we prove those triples
for an _arbitrary_ E, not just for E = . *)
Definition release_triple E (l: loc) :=
atomic_triple (fun (v: bool) => l #v)%I
(fun v ret => ret = #() l #false)%I
E
(release #l).
Lemma release_atomic_spec E : (l: loc), release_triple E l.
Proof.
iIntros (l).
rewrite /release_triple /atomic_triple.
iIntros (P Q) "#Hvs".
iIntros "!# HP".
iSpecialize ("Hvs" with "HP").
unfold release.
wp_rec.
iMod "Hvs" as (x) "[Hl Hvs']".
wp_store.
iDestruct "Hvs'" as "[_ Hvs']".
iMod ("Hvs'" with "[Hl]") as "HQ"; by iFrame.
Qed.
(* The parameter `b` in a way controlls interference from other
threads. The environment is allowed to change the value of b. One
can think of `b` as "what is the value of the lock according to
the environment". *)
Definition acquire_triple E (l: loc) :=
atomic_triple (fun (b: bool) => l #b)%I
(fun b ret => ret = #() b = false l #true)%I
E
(acquire #l).
Lemma acquire_atomic_spec E : (l: loc), acquire_triple E l.
Proof.
iIntros (l).
rewrite /acquire_triple /atomic_triple.
iIntros (P Q) "#Hvs".
iLöb as "IH".
iIntros "!# HP".
wp_rec. unfold try_acquire.
wp_rec. wp_bind (CAS _ _ _).
iMod ("Hvs" with "HP") as (b) "[Hl Hvs']".
destruct b.
- (* Lock is in use *)
wp_cas_fail.
iDestruct "Hvs'" as "[Hvs' _]".
iMod ("Hvs'" with "Hl") as "HP".
iModIntro. wp_if.
by iApply "IH".
- (* Lock is available *)
wp_cas_suc.
iDestruct "Hvs'" as "[_ Hvs']".
iMod ("Hvs'" with "[Hl]") as "HQ"; first by iFrame.
iModIntro. wp_if. done.
Qed.
Lemma release_spec_from_atomic γ (lk: loc) R :
{{ is_lock N γ (#lk) R locked γ R }} release #lk @ {{ v, v = #() }}.
Proof.
iApply (release_atomic_spec _ lk).
iAlways.
iIntros "(His & Hlok & HR)".
unfold is_lock.
iDestruct "His" as (l) "[% #Hinv]"; simplify_eq/=.
unfold lock_inv.
iInv N as (b) "(>Hl & Htok)" "Hcl".
iModIntro. iExists _. iFrame "Hl".
iSplit.
- iIntros "Hl". iFrame.
iMod ("Hcl" with "[-]") as "_".
{ iNext. iExists _; iFrame. }
iModIntro. iExists _; iSplit; eauto.
- iIntros (v) "[% Hl]"; subst.
unfold locked.
iMod ("Hcl" with "[-]").
{ iNext. iExists _; iFrame. }
iModIntro; eauto.
Qed.
(* Why do we need `R` to be timeless here? *)
Lemma acquire_spec_from_atomic γ (lk: loc) (R : iProp Σ)
`{Timeless _ R} :
{{ is_lock N γ (#lk) R }} acquire #lk @ {{ v, v = #() locked γ R }}.
Proof.
iApply (acquire_atomic_spec _ lk).
iAlways.
iIntros "His".
unfold is_lock.
iDestruct "His" as (l) "[% #Hinv]"; simplify_eq/=.
iInv N as (b) "(>Hl & Htok)" "Hcl".
iModIntro. iExists _. iFrame "Hl".
iSplit.
- iIntros "Hl". iFrame.
iMod ("Hcl" with "[-]") as "_".
{ iNext. iExists _; iFrame. }
iModIntro. iExists _; iSplit; eauto.
- iIntros (v) "[% [% Hl]]"; subst.
iMod ("Hcl" with "[-Htok]") as "_".
{ iNext. iExists _; iFrame. }
iDestruct "Htok" as "[>Htok >HR]".
unfold locked. by iFrame.
Qed.
End lock.
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