Commit 892b1802 authored by Dan Frumin's avatar Dan Frumin

Add the ticket lock example

The specification for ticket lock is proven using the atomic
specification for the increment operation.
parent 8d499eb4
Pipeline #7394 failed with stage
in 0 seconds
...@@ -4,6 +4,7 @@ theories/atomic.v ...@@ -4,6 +4,7 @@ theories/atomic.v
theories/lock.v theories/lock.v
theories/sync.v theories/sync.v
theories/atomic_incr.v theories/atomic_incr.v
theories/ticket_lock.v
theories/simple_sync.v theories/simple_sync.v
theories/flat.v theories/flat.v
theories/atomic_sync.v theories/atomic_sync.v
......
(* Ticket lock as a user of the atomic increment *)
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang proofmode notation.
From iris.algebra Require Import auth gset.
From iris_atomic Require Import atomic atomic_incr.
From iris.proofmode Require Import tactics.
From iris.heap_lang.lib Require Import ticket_lock.
(* we only change the definition of "acquire" *)
Definition acquire : val :=
rec: "acquire" "lk" :=
let: "n" := incr (Snd "lk") in
wait_loop "n" "lk".
Section contents.
Context `{!heapG Σ, !tlockG Σ} (N : namespace).
Transparent is_lock.
Lemma acquire_spec γ lk R :
{{{ is_lock N γ lk R }}} acquire lk {{{ RET #(); locked γ R }}}.
Proof.
iIntros (ϕ) "Hl HΦ". unfold is_lock.
iDestruct "Hl" as (lo ln ->) "#Hinv".
unfold acquire. do 2 (wp_pure _). wp_bind (incr _).
iDestruct (incr_atomic_spec ln) as "Hincr".
iApply "Hincr"; last by iExact "HΦ".
iAlways. iIntros "HΦ".
iInv N as (o n) "[>Hlo [>Hln [>Hauth Ha]]]" "Hclose".
iMod (fupd_intro_mask' _ ) as "Hvs"; first set_solver.
(* ^ this would be easier if we would have generalized the incr_atomic_spec to an aribtrary mask *)
iModIntro. iExists _; iFrame "Hln". iSplit.
- iIntros "Hln". iFrame "HΦ".
iMod "Hvs" as "_". iApply "Hclose".
iNext. iExists _,_; iFrame.
- iIntros (?) "[% Hln]"; simplify_eq.
iMod (own_update with "Hauth") as "[Hauth Hofull]".
{ eapply auth_update_alloc, prod_local_update_2.
eapply (gset_disj_alloc_empty_local_update _ {[ n ]}).
apply (seq_set_S_disjoint 0). }
rewrite -(seq_set_S_union_L 0).
iMod "Hvs" as "_". iMod ("Hclose" with "[-HΦ Hofull]") as "_".
{ iNext. iExists _,_; iFrame.
rewrite Nat2Z.inj_succ -Z.add_1_r. by iFrame. }
iModIntro. wp_let.
iApply (wait_loop_spec N γ (#lo, #ln) with "[-HΦ]").
+ iFrame. rewrite /issued /is_lock; eauto 10.
+ by iNext.
Qed.
End contents.
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