Commit 1bff8148 authored by Gaurav Parthasarathy's avatar Gaurav Parthasarathy

Merge rdcss_minor from other repository

parents 2deb5e0d 146dc789
From iris.algebra Require Import excl auth agree frac list cmra csum.
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.
Import uPred bi List Decidable.
Set Default Proof Using "Type".
Using prophecy variables with helping: implementing the restricted double compare-and-swap
from "A Practical Multi-Word Compare-and-Swap Operation" by Harris et al. (DISC 2002).
The following simplifications are made:
1) The values which are used for the comparisons are always integers.
2) To distinguish if a value is a descriptor or not we use injections.
In the original implementation the two least significant bits are used to identify the kind of value.
(** * Implementation of the functions. *)
(* cas1 is the same as a heap_lang CAS except that it returns the value read
instead of a boolean *)
Definition cas1 : val. Admitted.
Definition complete : val :=
λ: "l_d" "p",
let: "l_ghost" := ref #() in
let: "d_data" := !"l_d" in (* d_data = ((l_m, l_n), (m1, (n1, n2))) *)
let: "l_m" := Fst (Fst ("d_data")) in
let: "l_n" := Snd (Fst ("d_data")) in
let: "m1" := Fst (Snd ("d_data")) in
let: "n1_n2" := (Snd (Snd ("d_data"))) in
let: "n_new" := (if: !"l_m" = "m1" then Fst("n1_n2") else Snd("n1_n2")) in
Resolve (cas1 "l_n" "l_d" (InjL "n_new")) "p" "l_ghost".
Definition rdcss_aux : val :=
rec: "rdcss_aux" "l_d" "l_m" "l_n" "m1" "n1" "n2" :=
let: "p" := NewProph in
let: "r" := cas1 "l_n" (InjL ("n1")) (InjR ("l_d", "p")) in
match: "r" with
InjL "n" => (* an integer was read, check if CAS was successful *)
if: "n" = "n1" then
(* CAS was successful, finish operation *)
complete "l_d" "p";; "n"
(* CAS failed, hence we could linearize at the CAS *)
|InjR "args" =>
(* a descriptor from a different operation was read, try to help and then restart*)
let: "l_d'" := Fst ("args") in
let: "p'" := Snd ("args") in
complete "l_d'" "p'" ;; "rdcss_aux" "l_d" "l_m" "l_n" "m1" "n1" "n2"
Definition rdcss : val :=
λ: "rdcss" "l_d",
let: "d_data" := !"l_d" in (* d_data = ((l_m, l_n), (m1, (n1, n2))) *)
let: "l_m" := Fst (Fst ("d_data")) in
let: "l_n" := Snd (Fst ("d_data")) in
let: "m1" := Fst (Snd ("d_data")) in
let: "n1" := Fst (Snd (Snd ("d_data"))) in
let: "n2" := Snd (Snd (Snd ("d_data"))) in
rdcss_aux "l_d" "l_m" "l_n" "m1" "n1" "n2"
This diff is collapsed.
From stdpp Require Import namespaces.
From iris.heap_lang Require Export lifting notation.
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 {
(* -- operations -- *)
new_data: val;
rdcss_minor: val;
set_value: val;
get : val;
(* -- other data -- *)
name : Type;
name_eqdec : EqDecision name;
name_countable : Countable name;
(* -- predicates -- *)
is_data (N : namespace) (γs : name) (v : val) : iProp Σ;
data_content (γs : name) (m n : Z) : iProp Σ;
(* -- predicate properties -- *)
is_data_persistent N γs v : Persistent (is_data N γs v);
data_content_timeless γs f c : Timeless (data_content γs f c);
data_content_exclusive γs f1 c1 f2 c2 :
data_content γs f1 c1 - data_content γs f2 c2 - False;
(* -- operation specs -- *)
new_data_spec N :
{{{ True }}}
new_data #()
{{{ ctr γs, RET ctr ; is_data N γs ctr data_content γs 0 0 }}};
rdcss_minor_spec N γs v (m1 n1 n2 : Z):
is_data N γs v -
<<< (m n: Z), data_content γs m n >>>
rdcss_minor v #m1 #n1 #n2 @∖↑N
<<< data_content γs m (if decide (m = m1 n = n1) then n2 else n), RET if decide (n = n1) then #true else #false >>>;
set_value_spec N γs v (new_m: Z) :
is_data N γs v -
<<< (m n : Z), data_content γs m n >>>
set_value v #new_m @∖↑N
<<< data_content γs new_m n, RET #() >>>;
get_spec N γs v:
is_data N γs v -
<<< (m n : Z), data_content γs m n >>>
get v @∖↑N
<<< data_content γs m n, RET #n >>>;
Arguments atomic_rdcss_minor _ {_}.
Existing Instances
is_data_persistent data_content_timeless
name_countable name_eqdec.
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