Merge branch 'robbert/faa' into 'master'

Add atomic fetch-and-add operation to heap_lang

Closes #120

See merge request FP/iris-coq!96

CHANGELOG.md

@@ -90,7 +90,9 @@ sed 's/\bPersistentP\b/Persistent/g; s/\bTimelessP\b/Timeless/g; s/\bCMRADiscret
   + The version of big operations over lists was redefined so that it enjoys
     more definitional equalities.
 * Various improvements to `solve_ndisj`.
-* Improve handling of pure (non-state-dependent) reductions in heap_lang.
+* Some extensions/improvements of heap_lang:
+  - Improve handling of pure (non-state-dependent) reductions.
+  - Add fetch-and-add (`FAA`) operation.
 * Use `Hint Mode` to prevent Coq from making arbitrary guesses in the presence
   of evars, which often led to divergence. There are a few places where type
   annotations are now needed.

theories/heap_lang/lang.v

@@ -57,7 +57,8 @@ Inductive expr :=
   | Alloc (e : expr)
   | Load (e : expr)
   | Store (e1 : expr) (e2 : expr)
-  | CAS (e0 : expr) (e1 : expr) (e2 : expr).
+  | CAS (e0 : expr) (e1 : expr) (e2 : expr)
+  | FAA (e1 : expr) (e2 : expr).
 
 Bind Scope expr_scope with expr.
 
@@ -68,7 +69,7 @@ Fixpoint is_closed (X : list string) (e : expr) : bool :=
   | Lit _ => true
   | UnOp _ e | Fst e | Snd e | InjL e | InjR e | Fork e | Alloc e | Load e =>
      is_closed X e
-  | App e1 e2 | BinOp _ e1 e2 | Pair e1 e2 | Store e1 e2 =>
+  | App e1 e2 | BinOp _ e1 e2 | Pair e1 e2 | Store e1 e2 | FAA e1 e2 =>
      is_closed X e1 && is_closed X e2
   | If e0 e1 e2 | Case e0 e1 e2 | CAS e0 e1 e2 =>
      is_closed X e0 && is_closed X e1 && is_closed X e2
@@ -189,6 +190,7 @@ Proof.
   | Load e => GenNode 13 [go e]
   | Store e1 e2 => GenNode 14 [go e1; go e2]
   | CAS e0 e1 e2 => GenNode 15 [go e0; go e1; go e2]
+  | FAA e1 e2 => GenNode 16 [go e1; go e2]
   end).
  set (dec := fix go e :=
   match e with
@@ -210,6 +212,7 @@ Proof.
   | GenNode 13 [e] => Load (go e)
   | GenNode 14 [e1; e2] => Store (go e1) (go e2)
   | GenNode 15 [e0; e1; e2] => CAS (go e0) (go e1) (go e2)
+  | GenNode 16 [e1; e2] => FAA (go e1) (go e2)
   | _ => Lit LitUnit (* dummy *)
   end).
  refine (inj_countable' enc dec _). intros e. induction e; f_equal/=; auto.
@@ -245,7 +248,9 @@ Inductive ectx_item :=
   | StoreRCtx (v1 : val)
   | CasLCtx (e1 : expr) (e2 : expr)
   | CasMCtx (v0 : val) (e2 : expr)
-  | CasRCtx (v0 : val) (v1 : val).
+  | CasRCtx (v0 : val) (v1 : val)
+  | FaaLCtx (e2 : expr)
+  | FaaRCtx (v1 : val).
 
 Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
   match Ki with
@@ -269,6 +274,8 @@ Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
   | CasLCtx e1 e2 => CAS e e1 e2
   | CasMCtx v0 e2 => CAS (of_val v0) e e2
   | CasRCtx v0 v1 => CAS (of_val v0) (of_val v1) e
+  | FaaLCtx e2 => FAA e e2
+  | FaaRCtx v1 => FAA (of_val v1) e
   end.
 
 (** Substitution *)
@@ -293,6 +300,7 @@ Fixpoint subst (x : string) (es : expr) (e : expr)  : expr :=
   | Load e => Load (subst x es e)
   | Store e1 e2 => Store (subst x es e1) (subst x es e2)
   | CAS e0 e1 e2 => CAS (subst x es e0) (subst x es e1) (subst x es e2)
+  | FAA e1 e2 => FAA (subst x es e1) (subst x es e2)
   end.
 
 Definition subst' (mx : binder) (es : expr) : expr → expr :=
@@ -364,7 +372,12 @@ Inductive head_step : expr → state → expr → state → list (expr) → Prop
   | CasSucS l e1 v1 e2 v2 σ :
      to_val e1 = Some v1 → to_val e2 = Some v2 →
      σ !! l = Some v1 →
-     head_step (CAS (Lit $ LitLoc l) e1 e2) σ (Lit $ LitBool true) (<[l:=v2]>σ) [].
+     head_step (CAS (Lit $ LitLoc l) e1 e2) σ (Lit $ LitBool true) (<[l:=v2]>σ) []
+   | FaaS l i1 e2 i2 σ :
+     to_val e2 = Some (LitV (LitInt i2)) →
+     σ !! l = Some (LitV (LitInt i1)) →
+     head_step (FAA (Lit $ LitLoc l) e2) σ (Lit $ LitInt i1) (<[l:=LitV (LitInt (i1 + i2))]>σ) [].
+
 
 (** Basic properties about the language *)
 Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki).

theories/heap_lang/lifting.v

@@ -179,4 +179,17 @@ Proof.
   iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
   iModIntro. iSplit=>//. by iApply "HΦ".
 Qed.
+
+Lemma wp_faa E l i1 e2 i2 :
+  IntoVal e2 (LitV (LitInt i2)) →
+  {{{ ▷ l ↦ LitV (LitInt i1) }}} FAA (Lit (LitLoc l)) e2 @ E
+  {{{ RET LitV (LitInt i1); l ↦ LitV (LitInt (i1 + i2)) }}}.
+Proof.
+  iIntros (<-%of_to_val Φ) ">Hl HΦ".
+  iApply wp_lift_atomic_head_step_no_fork; auto.
+  iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
+  iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
+  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
+  iModIntro. iSplit=>//. by iApply "HΦ".
+Qed.
 End lifting.

theories/heap_lang/proofmode.v

@@ -161,6 +161,20 @@ Proof.
   rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
   rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
 Qed.
+
+Lemma tac_wp_faa Δ Δ' Δ'' E i K l i1 e2 i2 Φ :
+  IntoVal e2 (LitV (LitInt i2)) →
+  IntoLaterNEnvs 1 Δ Δ' →
+  envs_lookup i Δ' = Some (false, l ↦ LitV (LitInt i1))%I →
+  envs_simple_replace i false (Esnoc Enil i (l ↦ LitV (LitInt (i1 + i2)))) Δ' = Some Δ'' →
+  envs_entails Δ'' (WP fill K (Lit (LitInt i1)) @ E {{ Φ }}) →
+  envs_entails Δ (WP fill K (FAA (Lit (LitLoc l)) e2) @ E {{ Φ }}).
+Proof.
+  rewrite /envs_entails=> ?????; subst.
+  rewrite -wp_bind. eapply wand_apply; first exact: (wp_faa _ _ i1 _ i2).
+  rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
+  rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
+Qed.
 End heap.
 
 Tactic Notation "wp_apply" open_constr(lem) :=
@@ -256,3 +270,19 @@ Tactic Notation "wp_cas_suc" :=
     |wp_expr_simpl; try wp_value_head]
   | _ => fail "wp_cas_suc: not a 'wp'"
   end.
+
+Tactic Notation "wp_faa" :=
+  iStartProof;
+  lazymatch goal with
+  | |- envs_entails _ (wp ?E ?e ?Q) =>
+    first
+      [reshape_expr e ltac:(fun K e' =>
+         eapply (tac_wp_faa _ _ _ _ _ K); [apply _|..])
+      |fail 1 "wp_faa: cannot find 'CAS' in" e];
+    [apply _
+    |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
+     iAssumptionCore || fail "wp_cas_suc: cannot find" l "↦ ?"
+    |env_cbv; reflexivity
+    |wp_expr_simpl; try wp_value_head]
+  | _ => fail "wp_faa: not a 'wp'"
+  end.

theories/heap_lang/tactics.v

@@ -34,7 +34,8 @@ Inductive expr :=
   | Alloc (e : expr)
   | Load (e : expr)
   | Store (e1 : expr) (e2 : expr)
-  | CAS (e0 : expr) (e1 : expr) (e2 : expr).
+  | CAS (e0 : expr) (e1 : expr) (e2 : expr)
+  | FAA (e1 : expr) (e2 : expr).
 
 Fixpoint to_expr (e : expr) : heap_lang.expr :=
   match e with
@@ -58,6 +59,7 @@ Fixpoint to_expr (e : expr) : heap_lang.expr :=
   | Load e => heap_lang.Load (to_expr e)
   | Store e1 e2 => heap_lang.Store (to_expr e1) (to_expr e2)
   | CAS e0 e1 e2 => heap_lang.CAS (to_expr e0) (to_expr e1) (to_expr e2)
+  | FAA e1 e2 => heap_lang.FAA (to_expr e1) (to_expr e2)
   end.
 
 Ltac of_expr e :=
@@ -90,6 +92,8 @@ Ltac of_expr e :=
   | heap_lang.CAS ?e0 ?e1 ?e2 =>
      let e0 := of_expr e0 in let e1 := of_expr e1 in let e2 := of_expr e2 in
      constr:(CAS e0 e1 e2)
+  | heap_lang.FAA ?e1 ?e2 =>
+     let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(FAA e1 e2)
   | to_expr ?e => e
   | of_val ?v => constr:(Val v (of_val v) (to_of_val v))
   | _ => match goal with
@@ -106,7 +110,7 @@ Fixpoint is_closed (X : list string) (e : expr) : bool :=
   | Lit _ => true
   | UnOp _ e | Fst e | Snd e | InjL e | InjR e | Fork e | Alloc e | Load e =>
      is_closed X e
-  | App e1 e2 | BinOp _ e1 e2 | Pair e1 e2 | Store e1 e2 =>
+  | App e1 e2 | BinOp _ e1 e2 | Pair e1 e2 | Store e1 e2 | FAA e1 e2 =>
      is_closed X e1 && is_closed X e2
   | If e0 e1 e2 | Case e0 e1 e2 | CAS e0 e1 e2 =>
      is_closed X e0 && is_closed X e1 && is_closed X e2
@@ -167,6 +171,7 @@ Fixpoint subst (x : string) (es : expr) (e : expr)  : expr :=
   | Load e => Load (subst x es e)
   | Store e1 e2 => Store (subst x es e1) (subst x es e2)
   | CAS e0 e1 e2 => CAS (subst x es e0) (subst x es e1) (subst x es e2)
+  | FAA e1 e2 => FAA (subst x es e1) (subst x es e2)
   end.
 Lemma to_expr_subst x er e :
   to_expr (subst x er e) = heap_lang.subst x (to_expr er) (to_expr e).
@@ -182,6 +187,7 @@ Definition is_atomic (e : expr) :=
   | Store e1 e2 => bool_decide (is_Some (to_val e1) ∧ is_Some (to_val e2))
   | CAS e0 e1 e2 =>
      bool_decide (is_Some (to_val e0) ∧ is_Some (to_val e1) ∧ is_Some (to_val e2))
+  | FAA e1 e2 => bool_decide (is_Some (to_val e1) ∧ is_Some (to_val e2))
   | Fork _ => true
   (* Make "skip" atomic *)
   | App (Rec _ _ (Lit _)) (Lit _) => true
@@ -287,4 +293,6 @@ Ltac reshape_expr e tac :=
      [ reshape_val e1 ltac:(fun v1 => go (CasRCtx v0 v1 :: K) e2)
      | go (CasMCtx v0 e2 :: K) e1 ])
   | CAS ?e0 ?e1 ?e2 => go (CasLCtx e1 e2 :: K) e0
+  | FAA ?e1 ?e2 => reshape_val e1 ltac:(fun v1 => go (FaaRCtx v1 :: K) e2)
+  | FAA ?e1 ?e2 => go (FaaLCtx e2 :: K) e1
   end in go (@nil ectx_item) e.

theories/tests/heap_lang.v

@@ -20,7 +20,7 @@ Section LiftingTests.
     end.
   Qed.
 
-  Definition heap_e  : expr :=
+  Definition heap_e : expr :=
     let: "x" := ref #1 in "x" <- !"x" + #1 ;; !"x".
 
   Lemma heap_e_spec E : WP heap_e @ E {{ v, ⌜v = #2⌝ }}%I.
@@ -62,6 +62,15 @@ Section LiftingTests.
     wp_alloc l''. wp_let. by repeat wp_load.
   Qed.
 
+  Definition heap_e5 : expr :=
+    let: "x" := ref (ref #1) in FAA (!"x") (#10 + #1) + ! !"x".
+
+  Lemma heap_e5_spec E : WP heap_e5 @ E {{ v, ⌜v = #13⌝ }}%I.
+  Proof.
+    rewrite /heap_e5. wp_alloc l. wp_alloc l'. wp_let.
+    wp_load. wp_op. wp_faa. do 2 wp_load. wp_op. done.
+  Qed.
+
   Definition FindPred : val :=
     rec: "pred" "x" "y" :=
       let: "yp" := "y" + #1 in