Pull in the implementation source

_CoqProject

@@ -2,3 +2,6 @@
 incr.v
 sync.v
 pair_cas.v
+flat.v
+sync_stack.v
+treiber_stack.v

flat.v

+From iris.program_logic Require Export weakestpre.
+From iris.proofmode Require Import invariants ghost_ownership.
+From iris.heap_lang Require Export lang.
+From iris.heap_lang Require Import proofmode notation.
+From iris.heap_lang.lib Require Import spin_lock.
+From flatcomb Require Import sync_stack.
+Import uPred.
+
+Section flat_combiner.
+  Context `{!heapG Σ, !lockG Σ} (N: namespace).
+  Implicit Types l : loc.
+
+  Definition install: val :=
+    λ: "lcl" "req" "push",
+       match: !"lcl" with
+         SOME "o" => "o" <- InjL "req";; "o"
+       | NONE => let: "o" := ref (InjL "req") in
+                 "lcl" <- "o";;
+                 "push" "o";;
+                 "o"
+       end.
+
+  Definition doOp: val :=
+    λ: "f" "o",
+       match: !"o" with
+         InjL "req" => "o" <- InjR ("f" "o")
+       | InjR "_" => #()
+       end.
+
+  Definition loop: val :=
+    rec: "loop" "o" "f" "lock" "iter" :=
+      match: !"o" with
+        InjL "_" =>
+          if: CAS "lock" #false #true
+            then "iter" (doOp "f") ;; "lock" <- #false;; "loop" "o" "f" "lock" "iter"
+            else "loop" "o" "f" "lock" "iter"
+      | InjR "res" => "res"
+      end.
+
+  Definition flat: val :=
+    λ: "f",
+       let: "lock" := ref (#false) in
+       let: "lcl" := ref #0 in
+       let: "s" := mk_stack #() in
+       λ: "x",
+          let: "o" := install "x" (push "s") in
+          loop "o" "f" "lock" (iter "s").
+
+End flat_combiner.

sync_stack.v

+From iris.program_logic Require Export weakestpre hoare.
+From iris.proofmode Require Import invariants ghost_ownership.
+From iris.heap_lang Require Export lang.
+From iris.heap_lang Require Import proofmode notation.
+From iris.heap_lang.lib Require Import spin_lock.
+From iris.algebra Require Import excl.
+From flatcomb Require Import sync.
+Import uPred.
+
+Definition mk_stack: val :=
+  λ: <>,
+       let: "s" := mk_sync #() in
+       let: "lhd" := ref NONE in
+       ("s" (* push *)
+          (λ: "x",
+              let: "hd" := !"lhd" in
+              "lhd" <- SOME (ref("x", "hd"))),
+        "s" (* pop *)
+          (λ: <>,
+                let: "hd" := !"lhd" in
+                match: "hd" with
+                  NONE => NONE
+                | SOME "l" =>
+                      let: "x" := Fst !"l" in
+                      let: "xs" := Snd !"l" in
+                      "lhd" <- "xs";;
+                      SOME "x"
+                end),
+        "s" (* "iter" *)
+          (rec: "iter" "f" :=
+             let: "hd" := Fst !"lhd" in
+             match: "hd" with
+               NONE => #()
+             | SOME "l" =>
+                 let: "x" := Fst !"l" in
+                 let: "xs" := Snd !"l" in
+                 "f" "x";;
+                 "iter" "xs"
+             end)).
+
+Definition push: val := λ: "s", Fst (Fst "s").
+Definition pop: val := λ: "s",  Snd (Fst "s").
+Definition iter: val := λ: "s", Snd "s".
+                    
+
+Section proof.
+  Context `{!heapG Σ} (N: namespace).
+  Implicit Types l : loc.
+
+  (* copied from /tests/list_reverse.v *)
+  Fixpoint is_stack (hd : val) (xs : list val) :=
+    match xs with
+    | [] => hd = NONEV
+    | x :: xs => ∃ l hd', hd = SOMEV #l ★ l ↦ (x,hd') ★ is_stack hd' xs
+    end%I.
+
+End proof.
+

treiber_stack.v

+From iris.program_logic Require Export weakestpre.
+From iris.proofmode Require Import invariants ghost_ownership.
+From iris.heap_lang Require Export lang.
+From iris.heap_lang Require Import proofmode notation.
+
+Section treiber_stack.
+  Context `{!heapG Σ} (N: namespace).
+
+  Definition push_treiber: val :=
+    rec: "push_treiber" "lhd" "x" :=
+      let: "hd" := !"lhd" in
+      let: "hd'" := ("x", SOME "lhd") in
+      if: CAS "lhd" "hd" "hd'"
+        then #()
+        else "push_treiber" "lhd" "x".
+
+  Definition pop_treiber: val :=
+    rec: "pop_treiber" "lhd" :=
+      let: "hd" := !"lhd" in
+      match: "hd" with
+        SOME "pair" =>
+        if: CAS "lhd" "hd" (Snd "pair")
+          then SOME (Fst "pair")
+          else "pop_treiber" "lhd"
+      | NONE => NONE
+      end.
+
+End treiber_stack.