Commit c90f27aa authored by Gaurav Parthasarathy's avatar Gaurav Parthasarathy

some cleanup

parent 1bff8148
......@@ -106,3 +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
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"
else
(* CAS failed, hence we could linearize at the CAS *)
"n"
|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"
end.
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"
.
......@@ -3,12 +3,13 @@ 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.conditional_increment*) Require Import spec.
From iris_examples.logatom.rdcss_minor Require Import spec.
Import uPred bi List Decidable.
Set Default Proof Using "Type".
(** Using prophecy variables with helping: generalizing the conditional counter from
"Logical Relations for Fine-Grained Concurrency" by Turon et al. (POPL 2013) *)
(** Using prophecy variables with helping: implementing a simplified version of
the restricted double-compare single-swap from "A Practical Multi-Word Compare-and-Swap Operation" by Harris et al. (DISC 2002)
*)
(** * Implementation of the functions. *)
......
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