Commit dadcdd18 authored by Gaurav Parthasarathy's avatar Gaurav Parthasarathy

changed name rdcss_minor to rdcss

parent 307d1cae
......@@ -106,5 +106,5 @@ theories/logatom/snapshot/spec.v
theories/logatom/snapshot/atomic_snapshot.v
theories/logatom/conditional_increment/spec.v
theories/logatom/conditional_increment/cinc.v
theories/logatom/rdcss_minor/rdcss_minor.v
theories/logatom/rdcss_minor/spec.v
theories/logatom/rdcss/rdcss.v
theories/logatom/rdcss/spec.v
......@@ -3,7 +3,7 @@ From iris.base_logic.lib Require Export invariants.
From iris.program_logic Require Export atomic.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation.
From iris_examples.logatom.rdcss_minor Require Import spec.
From iris_examples.logatom.rdcss Require Import spec.
Import uPred bi List Decidable.
Set Default Proof Using "Type".
......@@ -88,7 +88,7 @@ Definition get : val :=
end.
(*
rdcss_minor(rdcss_data, m1, n1, n2) :=
rdcss(rdcss_data, m1, n1, n2) :=
let lm = rdcss_data.1 in
let lln = rdcss_data.2 in
let ln = !lln in
......@@ -99,15 +99,15 @@ rdcss_minor(rdcss_data, m1, n1, n2) :=
let lnew = ref (injR ((m1, (n1, n2)), p)) in
if CAS(lln, ln, lnew) = ln then
complete(lln, lm, lnew, m1, n1, n2, p); #true
else rdcss_minor(data, m1, n1, n2)
else rdcss(data, m1, n1, n2)
else #false
| injR ( (m1', (n1', n2')), p') =>
complete(lln, lm, ln, m1', n1', n2', p');
rdcss_minor(data, m1, n1, n2)
rdcss(data, m1, n1, n2)
end.
*)
Definition rdcss_minor : val :=
rec: "rdcss_minor" "rdcss_data" "m1" "n1" "n2" :=
Definition rdcss: val :=
rec: "rdcss" "rdcss_data" "m1" "n1" "n2" :=
let: "lm" := Fst "rdcss_data" in
let: "lln" := Snd "rdcss_data" in
let: "ln" := !"lln" in
......@@ -118,7 +118,7 @@ Definition rdcss_minor : val :=
let: "lnew" := ref (InjR (("m1", ("n1", "n2")), "p")) in
if: (CAS "lln" "ln" "lnew") = "ln" then
complete "lln" "lm" "lnew" "m1" "n1" "n2" "p" ;; #true
else "rdcss_minor" "rdcss_data" "m1" "n1" "n2"
else "rdcss" "rdcss_data" "m1" "n1" "n2"
else #false
| InjR "args'" =>
(* args' = ( (m1', (n1', n2')) , p') *)
......@@ -127,7 +127,7 @@ Definition rdcss_minor : val :=
let: "n2'" := (Snd (Snd (Fst "args'"))) in
let: "p'" := (Snd "args'") in
complete "lln" "lm" "ln" "m1'" "n1'" "n2'" "p'" ;;
"rdcss_minor" "rdcss_data" "m1" "n1" "n2"
"rdcss" "rdcss_data" "m1" "n1" "n2"
end.
(** ** Proof setup *)
......@@ -136,20 +136,20 @@ Definition numUR := authR $ optionUR $ exclR ZC.
Definition tokenUR := exclR unitC.
Definition one_shotUR := csumR (exclR unitC) (agreeR unitC).
Class rdcssminorG Σ := RDCSSMinorG {
rdcssminor_numG :> inG Σ numUR;
rdcssminor_tokenG :> inG Σ tokenUR;
rdcssminor_one_shotG :> inG Σ one_shotUR;
Class rdcssG Σ := RDCSSG {
rdcss_numG :> inG Σ numUR;
rdcss_tokenG :> inG Σ tokenUR;
rdcss_one_shotG :> inG Σ one_shotUR;
}.
Definition rdcssminorΣ : gFunctors :=
Definition rdcssΣ : gFunctors :=
#[GFunctor numUR; GFunctor tokenUR; GFunctor one_shotUR].
Instance subG_rdcssminorΣ {Σ} : subG rdcssminorΣ Σ rdcssminorG Σ.
Instance subG_rdcssΣ {Σ} : subG rdcssΣ Σ rdcssG Σ.
Proof. solve_inG. Qed.
Section rdcss_minor.
Context {Σ} `{!heapG Σ, !rdcssminorG Σ}.
Section rdcss.
Context {Σ} `{!heapG Σ, !rdcssG Σ}.
Context (N : namespace).
Local Definition stateN := N .@ "state".
......@@ -477,11 +477,11 @@ Section rdcss_minor.
with "InvC InvS PAU HQ Hl_new"); done.
Qed.
(** ** Proof of [rdcss_minor] *)
Lemma rdcss_minor_spec γs v (m1 n1 n2: Z) :
(** ** Proof of [rdcss] *)
Lemma rdcss_spec γs v (m1 n1 n2: Z) :
is_rdcss γs v -
<<< (m n: Z), rdcss_content γs m n >>>
rdcss_minor v #m1 #n1 #n2 @∖↑N
rdcss v #m1 #n1 #n2 @∖↑N
<<< rdcss_content γs m (if decide (m = m1 n = n1) then n2 else n), RET #(bool_decide (n = n1)) >>>.
Proof.
iIntros "#InvC". iDestruct "InvC" as (γ_m γ_n lm lln) "[Heq InvC]".
......@@ -623,12 +623,12 @@ Section rdcss_minor.
iIntros "Ht". wp_seq. iApply "IH". iApply "AU".
Qed.
End rdcss_minor.
End rdcss.
Definition atomic_rdcss_minor `{!heapG Σ, rdcssminorG Σ} :
spec.atomic_rdcss_minor Σ :=
Definition atomic_rdcss `{!heapG Σ, rdcssG Σ} :
spec.atomic_rdcss Σ :=
{| spec.new_rdcss_spec := new_rdcss_spec;
spec.rdcss_minor_spec := rdcss_minor_spec;
spec.rdcss_spec := rdcss_spec;
spec.set_value_spec := set_value_spec;
spec.get_spec := get_spec;
spec.rdcss_content_exclusive := rdcss_content_exclusive |}.
......
......@@ -4,10 +4,10 @@ From iris.program_logic Require Export atomic.
Set Default Proof Using "Type".
(** A general logically atomic interface for conditional increment. *)
Record atomic_rdcss_minor {Σ} `{!heapG Σ} := AtomicRdcss {
Record atomic_rdcss {Σ} `{!heapG Σ} := AtomicRdcss {
(* -- operations -- *)
new_rdcss : val;
rdcss_minor: val;
rdcss: val;
set_value: val;
get : val;
(* -- other data -- *)
......@@ -27,10 +27,10 @@ Record atomic_rdcss_minor {Σ} `{!heapG Σ} := AtomicRdcss {
{{{ True }}}
new_rdcss #()
{{{ ctr γs, RET ctr ; is_rdcss N γs ctr rdcss_content γs 0 0 }}};
rdcss_minor_spec N γs v (m1 n1 n2 : Z):
rdcss_spec N γs v (m1 n1 n2 : Z):
is_rdcss N γs v -
<<< (m n: Z), rdcss_content γs m n >>>
rdcss_minor v #m1 #n1 #n2 @∖↑N
rdcss v #m1 #n1 #n2 @∖↑N
<<< rdcss_content γs m (if decide (m = m1 n = n1) then n2 else n), RET #(bool_decide (n = n1)) >>>;
set_value_spec N γs v (new_m: Z) :
is_rdcss N γs v -
......@@ -43,7 +43,7 @@ Record atomic_rdcss_minor {Σ} `{!heapG Σ} := AtomicRdcss {
get v @∖↑N
<<< rdcss_content γs m n, RET #n >>>;
}.
Arguments atomic_rdcss_minor _ {_}.
Arguments atomic_rdcss _ {_}.
Existing Instances
is_rdcss_persistent rdcss_content_timeless
......
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