mcs_lock.v

From iris.heap_lang Require Import proofmode.
From iris_automation.heap_lang Require Import stepping_tacs.
From iris_automation.biabd Require Import biabd_local_updates.
From iris.algebra Require Import agree frac excl auth.
From iris_automation.lib Require Import loc_map.

Definition new_lock : val :=
  λ: "_", ref NONE.

Definition new_node : val :=
  λ: "_", 
    let: "ret" := AllocN #2 NONE in
    "ret".

Definition enqueue_node : val :=
  rec: "enqueue" "lk" "node" :=
    let: "pred" := ! "lk" in
    if: CAS "lk" "pred" (SOME "node") then 
      "pred"
    else 
      "enqueue" "lk" "node".

Definition wait_on : val :=
  rec: "wait_on" "l" :=
    if: ! "l" then 
      "wait_on" "l"
    else 
      #().

Definition acquire : val :=
  λ: "lk" "node",
    ("node" +ₗ #1) <- NONE;;
    let: "pred" := enqueue_node "lk" "node" in (* this transfers ownership of "node" +ₗ 1 to "lk" *)
    match: "pred" with
      NONE => #()
    | SOME "l" => (* in this case, we have received of "l" +ₗ 1 ↦{1/2} NONEV from enqueue_node "lk" *)
      "node" <- #true ;;
      ("l" +ₗ #1) <- SOME "node";; (* this transfers ownership of "node" +ₗ 0 to "l" *)
      wait_on "node"
    end.

Definition wait_for_succ : val :=
  rec: "wait_for" "node" :=
    match: !("node" +ₗ #1) with
      NONE => "wait_for" "node" (* after reading SOME, we gain ownership of the location *)
    | SOME "l" => #()
    end.

Definition release : val :=
  λ: "lk" "node",
    let: "free" := 
      if: !("node" +ₗ #1) = NONE then (* after reading SOME, we gain ownership of the location *)
        if: CAS "lk" (SOME "node") NONE then (* This CAS, if succesful gives us almost the ownership back *)
          #true
        else (* someone is in the process of claiming the lock, wait until it has made itself our tail *)
          wait_for_succ "node";;
          #false
      else
        #false
      in
    if: "free" then
      #()
    else
      match: !("node" +ₗ #1) with (* here we should have gained ownership and knowledge that it points to SOME *)
        NONE => #() #() (* unsafe *)
      | SOME "l" =>
        "l" <- #false (* returns ownership to "l", and relinquishes lock resource R *)
      end.

Definition mcs_lockR := prodR (agreeR $ prodO (leibnizO loc) (leibnizO bool)) fracR.
Class mcs_lockG Σ := MCSLockG { 
  mcs_lock_tok1G :> inG Σ mcs_lockR; 
  mcs_lock_locmapG :> loc_mapG Σ (option gname);
  mcs_lock_exclG :> inG Σ $ exclR unitO 
}.
Definition mcs_lockΣ : gFunctors := #[GFunctor mcs_lockR; GFunctor $ exclR unitO; loc_mapΣ (option gname)].

Local Obligation Tactic := program_smash_verify.

Program Instance subG_mcs_lockΣ {Σ} : subG mcs_lockΣ Σ → mcs_lockG Σ.

Section spec.
  Context `{!heapGS Σ, mcs_lockG Σ}.

  Let N := nroot .@ "mcslock".
  Definition N_signal := N .@ "signal".
  Definition N_node := N .@ "node".
  (* l, false is about the boolean, l, true is about the next location *)

  Definition signal_loc γm γe l n γb R : iProp Σ :=
    own γb (to_agree (l, false), 1%Qp) ∨ (∃ (b : bool), l ↦ #b ∗ (⌜b = true⌝ ∗ (∃ γ, loc_map_elem γm n (DfracOwn $ 1/2)%Qp (Some γ)) ∨ ⌜b = false⌝ ∗ R ∗ own γe (Excl ()) ∗ own γb (to_agree (l, false), (1/2)%Qp))).

  Definition waiting_loc_inv γm γn γe (n : loc) R : iProp Σ :=
    own γn (to_agree (n, true), 1%Qp) ∨ (∃ v, (n +ₗ 1) ↦{# 1/2} v ∗ ⌜val_is_unboxed v⌝ ∗
        (⌜v = NONEV⌝ ∨ (∃ (n' : loc) γ, ⌜v = SOMEV #n'⌝ ∗ (n +ₗ 1) ↦{# 1/2} v ∗ own γn (to_agree (n, true), (1/2)%Qp) ∗ own γ (to_agree (n', false), (1/2)%Qp) ∗ inv N_signal (signal_loc γm γe n' n γ R)))).

  Definition free_node γm n : iProp Σ :=
    ∃ v1 v2, n ↦ v1 ∗ (n +ₗ 1) ↦ v2 ∗ loc_map_elem γm n (DfracOwn 1) None.

  Definition lock_inv γm γe lk R : iProp Σ :=
    ∃ (v : val), lk ↦ v ∗ ⌜val_is_unboxed v⌝ ∗ (
      ⌜v = NONEV⌝ ∗ own γe (Excl ()) ∗ R
        ∨
      ∃ (l : loc) γn, ⌜v = SOMEV #l⌝ ∗ (l +ₗ 1) ↦{# 1/2} NONEV ∗ own γn (to_agree (l, true), (1/2)%Qp) ∗ loc_map_elem γm l (DfracOwn $ 1/2)%Qp (Some γn) ∗ inv N_node (waiting_loc_inv γm γn γe l R)
    ).

  Definition is_lock γm γe R v : iProp Σ :=
    ∃ (lk : loc), ⌜v = #lk⌝ ∗ global_reg γm ∗ inv N (lock_inv γm γe lk R).

  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.

  Global Program Instance new_lock_spec :
    SPEC {{ True }} 
      new_lock #()          (* note that global_reg is not a difficult premise, since one has ⊢ |={E}=> ∃ γm, global_reg γm *)
    {{ (lk : val), RET lk; (∀ R γm, R ∗ global_reg γm ={⊤}=∗ ∃ γe, is_lock γm γe R lk) }}.
    (* having global_reg γm on the left side of the fupd means multiple mcs_locks can share the same global_reg γm,
       which means free_nodes can be used in any of these locks, as desired. *)

  Global Program Instance new_node_spec :
    SPEC {{ True }} 
      new_node #() (* global_reg or is_lock? *)
    {{ (n : loc), RET #n; ∀ γm, global_reg γm ={⊤}=∗ free_node γm n }}.

  Program Instance enqueue_node_spec (lk n : loc) γm γe R :
    SPEC {{ inv N (lock_inv γm γe lk R) ∗ (n +ₗ 1) ↦ NONEV ∗ loc_map_elem γm n (DfracOwn 1) None }}
      enqueue_node #lk #n
    {{ (p : val) γn, RET p; inv N_node (waiting_loc_inv γm γn γe n R) ∗ own γn (to_agree (n, true), (1/2))%Qp ∗ loc_map_elem γm n (DfracOwn $ 1/2)%Qp (Some γn) ∗ (
      ⌜p = NONEV⌝ ∗ own γe (Excl ()) ∗ R
          ∨
      ∃ (l : loc) γl, ⌜p = SOMEV #l⌝ ∗ (l +ₗ 1) ↦{# 1/2} NONEV ∗ loc_map_elem γm l (DfracOwn $ 1/2)%Qp (Some γl) ∗ own γl (to_agree (l, true), (1/2)%Qp) ∗ inv N_node (waiting_loc_inv γm γl γe l R)) }}.

  Program Instance wait_on_spec (n l : loc) γm γe γ R :
    SPEC {{ inv N_signal (signal_loc γm γe n l γ R) ∗ own γ (to_agree (n, false), 1/2)%Qp }}
      wait_on #n
    {{ RET #(); R ∗ own γe (Excl ()) ∗ n ↦ #false }}.

  Definition acquired_node γm γn γe n R : iProp Σ :=
    ∃ v, n ↦ v ∗ inv N_node (waiting_loc_inv γm γn γe n R) ∗ own γe (Excl ()) ∗ own γn (to_agree (n, true), (1/2))%Qp ∗ loc_map_elem γm n (DfracOwn $ 1/2)%Qp (Some γn).

  Global Program Instance acquire_spec R (n : loc) (lk : val) γm γe :
    SPEC {{ is_lock γm γe R lk ∗ free_node γm n }}
      acquire lk #n
    {{ γn, RET #(); R ∗ acquired_node γm γn γe n R }}.

  Program Instance wait_for_succ_spec γm γn γe (n : loc) R :
    SPEC {{ inv N_node (waiting_loc_inv γm γn γe n R) ∗ own γn (to_agree (n, true), (1/2))%Qp }}
      wait_for_succ #n
    {{ (l : loc) γ, RET #(); (n +ₗ 1) ↦ SOMEV #l ∗ own γ (to_agree (l, false), (1/2)%Qp) ∗ inv N_signal (signal_loc γm γe l n γ R) }}.

  Global Instance release_spec R (n : loc) γm γn γe (v : val) :
    SPEC {{ R ∗ acquired_node γm γn γe n R ∗ is_lock γm γe R v }}
      release v #n
    {{ RET #(); free_node γm n }}.
  Proof.
    iStepsS; last iSmash.
    iRight.
    iStepsS; last iSmash.
    (* need a revert since a detected equality rewrites the context, causing a Mergable instance to be missed *)
    iRevert "H6". iSmash.
  Qed.

  Definition acquired_mutual_exclusion γm γn1 γn2 γe n m R : acquired_node γm γn1 γe n R ∗ acquired_node γm γn2 γe m R ⊢ False
    := verify. (* Cannot do Lemma _ : _ := verify unfortunately. If proper reuse is wanted this should be a Mergable instance *)
End spec.