Skip to content

GitLab

Commit b74dbd7d authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

Right-to-left evaluation order.

parent 50b77084
Hide whitespace changes
Inline Side-by-side
tests/heap_lang.v
View file @ b74dbd7d
......@@ -65,12 +65,12 @@ Section tests.
Qed.
Definition heap_e5 : expr :=
let: "x" := ref (ref #1) in FAA (!"x") (#10 + #1) + ! !"x".
let: "x" := ref (ref #1) in ! ! "x" + FAA (!"x") (#10 + #1).
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.
wp_op. wp_load. wp_faa. do 2 wp_load. wp_op. done.
Qed.
Definition heap_e6 : val := λ: "v", "v" = "v".
......
theories/heap_lang/lang.v
View file @ b74dbd7d
......@@ -271,14 +271,14 @@ Canonical Structure exprC := leibnizC expr.
(** Evaluation contexts *)
Inductive ectx_item :=
| AppLCtx (e2 : expr)
| AppRCtx (v1 : val)
| AppLCtx (v2 : val)
| AppRCtx (e1 : expr)
| UnOpCtx (op : un_op)
| BinOpLCtx (op : bin_op) (e2 : expr)
| BinOpRCtx (op : bin_op) (v1 : val)
| BinOpLCtx (op : bin_op) (v2 : val)
| BinOpRCtx (op : bin_op) (e1 : expr)
| IfCtx (e1 e2 : expr)
| PairLCtx (e2 : expr)
| PairRCtx (v1 : val)
| PairLCtx (v2 : val)
| PairRCtx (e1 : expr)
| FstCtx
| SndCtx
| InjLCtx
......@@ -286,24 +286,24 @@ Inductive ectx_item :=
| CaseCtx (e1 : expr) (e2 : expr)
| AllocCtx
| LoadCtx
| StoreLCtx (e2 : expr)
| StoreRCtx (v1 : val)
| CasLCtx (e1 : expr) (e2 : expr)
| CasMCtx (v0 : val) (e2 : expr)
| CasRCtx (v0 : val) (v1 : val)
| FaaLCtx (e2 : expr)
| FaaRCtx (v1 : val).
| StoreLCtx (v2 : val)
| StoreRCtx (e1 : expr)
| CasLCtx (v1 : val) (v2 : val)
| CasMCtx (e0 : expr) (v2 : val)
| CasRCtx (e0 : expr) (e1 : expr)
| FaaLCtx (v2 : val)
| FaaRCtx (e1 : expr).
Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
match Ki with
| AppLCtx e2 => App e e2
| AppRCtx v1 => App (of_val v1) e
| AppLCtx v2 => App e (of_val v2)
| AppRCtx e1 => App e1 e
| UnOpCtx op => UnOp op e
| BinOpLCtx op e2 => BinOp op e e2
| BinOpRCtx op v1 => BinOp op (of_val v1) e
| BinOpLCtx op v2 => BinOp op e (of_val v2)
| BinOpRCtx op e1 => BinOp op e1 e
| IfCtx e1 e2 => If e e1 e2
| PairLCtx e2 => Pair e e2
| PairRCtx v1 => Pair (of_val v1) e
| PairLCtx v2 => Pair e (of_val v2)
| PairRCtx e1 => Pair e1 e
| FstCtx => Fst e
| SndCtx => Snd e
| InjLCtx => InjL e
......@@ -311,13 +311,13 @@ Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
| CaseCtx e1 e2 => Case e e1 e2
| AllocCtx => Alloc e
| LoadCtx => Load e
| StoreLCtx e2 => Store e e2
| StoreRCtx v1 => Store (of_val v1) e
| 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
| StoreLCtx v2 => Store e (of_val v2)
| StoreRCtx e1 => Store e1 e
| CasLCtx v1 v2 => CAS e (of_val v1) (of_val v2)
| CasMCtx e0 v2 => CAS e0 e (of_val v2)
| CasRCtx e0 e1 => CAS e0 e1 e
| FaaLCtx v2 => FAA e (of_val v2)
| FaaRCtx e1 => FAA e1 e
end.
(** Substitution *)
......
theories/heap_lang/lib/atomic_heap.v
View file @ b74dbd7d
......@@ -27,7 +27,7 @@ Class atomic_heap {Σ} `{!heapG Σ} := AtomicHeap {
<<< ∀ (v : val) q, mapsto l q v >>> load #l @ ⊤ <<< mapsto l q v, RET v >>>;
store_spec (l : loc) (e : expr) (w : val) :
IntoVal e w →
<<< ∀ v, mapsto l 1 v >>> store (#l, e) @ ⊤
<<< ∀ v, mapsto l 1 v >>> store #l e @ ⊤
<<< mapsto l 1 w, RET #() >>>;
(* This spec is slightly weaker than it could be: It is sufficient for [w1]
*or* [v] to be unboxed. However, by writing it this way the [val_is_unboxed]
......@@ -35,7 +35,7 @@ Class atomic_heap {Σ} `{!heapG Σ} := AtomicHeap {
spec is still good enough for all our applications. *)
cas_spec (l : loc) (e1 e2 : expr) (w1 w2 : val) :
IntoVal e1 w1 → IntoVal e2 w2 → val_is_unboxed w1 →
<<< ∀ v, mapsto l 1 v >>> cas (#l, e1, e2) @ ⊤
<<< ∀ v, mapsto l 1 v >>> cas #l e1 e2 @ ⊤
<<< if decide (v = w1) then mapsto l 1 w2 else mapsto l 1 v,
RET #(if decide (v = w1) then true else false) >>>;
}.
......@@ -53,9 +53,9 @@ Notation "l ↦ -" := (l ↦{1} -)%I (at level 20) : bi_scope.
Notation "'ref' e" := (alloc e) : expr_scope.
Notation "! e" := (load e) : expr_scope.
Notation "e1 <- e2" := (store (e1, e2)%E) : expr_scope.
Notation "e1 <- e2" := (store e1 e2) : expr_scope.
Notation CAS e1 e2 e3 := (cas (e1, e2, e3)%E).
Notation CAS e1 e2 e3 := (cas e1 e2 e3).
End notation.
......@@ -65,9 +65,9 @@ Definition primitive_alloc : val :=
Definition primitive_load : val :=
λ: "l", !"l".
Definition primitive_store : val :=
λ: "p", (Fst "p") <- (Snd "p").
λ: "l" "x", "l" <- "x".
Definition primitive_cas : val :=
λ: "p", CAS (Fst (Fst "p")) (Snd (Fst "p")) (Snd "p").
λ: "l" "e1" "e2", CAS "l" "e1" "e2".
Section proof.
Context `{!heapG Σ}.
......@@ -89,10 +89,10 @@ Section proof.
Lemma primitive_store_spec (l : loc) (e : expr) (w : val) :
IntoVal e w →
<<< ∀ v, l ↦ v >>> primitive_store (#l, e) @ ⊤
<<< ∀ v, l ↦ v >>> primitive_store #l e @ ⊤
<<< l ↦ w, RET #() >>>.
Proof.
iIntros (<- Q Φ) "? AU". wp_let. wp_proj. wp_proj.
iIntros (<- Q Φ) "? AU". wp_lam. wp_let.
iMod "AU" as (v) "[H↦ [_ Hclose]]".
wp_store. iMod ("Hclose" with "H↦") as "HΦ". by iApply "HΦ".
Qed.
......@@ -100,11 +100,11 @@ Section proof.
Lemma primitive_cas_spec (l : loc) e1 e2 (w1 w2 : val) :
IntoVal e1 w1 → IntoVal e2 w2 → val_is_unboxed w1 →
<<< ∀ (v : val), l ↦ v >>>
primitive_cas (#l, e1, e2) @ ⊤
primitive_cas #l e1 e2 @ ⊤
<<< if decide (v = w1) then l ↦ w2 else l ↦ v,
RET #(if decide (v = w1) then true else false) >>>.
Proof.
iIntros (<- <- ? Q Φ) "? AU". wp_let. repeat wp_proj.
iIntros (<- <- ? Q Φ) "? AU". wp_lam. wp_let. wp_let.
iMod "AU" as (v) "[H↦ [_ Hclose]]".
destruct (decide (v = w1)) as [<-|Hv]; [wp_cas_suc|wp_cas_fail];
iMod ("Hclose" with "H↦") as "HΦ"; by iApply "HΦ".
......
theories/heap_lang/lib/ticket_lock.v
View file @ b74dbd7d
......@@ -74,7 +74,7 @@ Section proof.
{{{ R }}} newlock #() {{{ lk γ, RET lk; is_lock γ lk R }}}.
Proof.
iIntros (Φ) "HR HΦ". rewrite -wp_fupd /newlock /=.
wp_seq. wp_alloc lo as "Hlo". wp_alloc ln as "Hln".
wp_seq. wp_alloc ln as "Hln". wp_alloc lo as "Hlo".
iMod (own_alloc (● (Excl' 0%nat, GSet ∅) ⋅ ◯ (Excl' 0%nat, GSet ∅))) as (γ) "[Hγ Hγ']".
{ by rewrite -auth_both_op. }
iMod (inv_alloc _ _ (lock_inv γ lo ln R) with "[-HΦ]").
......@@ -111,7 +111,7 @@ Section proof.
iInv N as (o n) "[Hlo [Hln Ha]]".
wp_load. iModIntro. iSplitL "Hlo Hln Ha".
{ iNext. iExists o, n. by iFrame. }
wp_let. wp_proj. wp_op. wp_bind (CAS _ _ _).
wp_let. wp_op. wp_proj. wp_bind (CAS _ _ _).
iInv N as (o' n') "(>Hlo' & >Hln' & >Hauth & Haown)".
destruct (decide (#n' = #n))%V as [[= ->%Nat2Z.inj] | Hneq].
- iMod (own_update with "Hauth") as "[Hauth Hofull]".
......@@ -137,14 +137,14 @@ Section proof.
Proof.
iIntros (Φ) "(Hl & Hγ & HR) HΦ". iDestruct "Hl" as (lo ln ->) "#Hinv".
iDestruct "Hγ" as (o) "Hγo".
wp_let. wp_proj. wp_proj. wp_bind (! _)%E.
wp_let. wp_proj. wp_bind (! _)%E.
iInv N as (o' n) "(>Hlo & >Hln & >Hauth & Haown)".
wp_load.
iDestruct (own_valid_2 with "Hauth Hγo") as
%[[<-%Excl_included%leibniz_equiv _]%prod_included _]%auth_valid_discrete_2.
iModIntro. iSplitL "Hlo Hln Hauth Haown".
{ iNext. iExists o, n. by iFrame. }
wp_op.
wp_op. wp_proj.
iInv N as (o' n') "(>Hlo & >Hln & >Hauth & Haown)".
iApply wp_fupd. wp_store.
iDestruct (own_valid_2 with "Hauth Hγo") as
......
theories/heap_lang/tactics.v
View file @ b74dbd7d
......@@ -269,15 +269,15 @@ Ltac reshape_expr e tac :=
let rec go K e :=
match e with
| _ => tac K e
| App ?e1 ?e2 => reshape_val e1 ltac:(fun v1 => go (AppRCtx v1 :: K) e2)
| App ?e1 ?e2 => go (AppLCtx e2 :: K) e1
| App ?e1 ?e2 => reshape_val e2 ltac:(fun v2 => go (AppLCtx v2 :: K) e1)
| App ?e1 ?e2 => go (AppRCtx e1 :: K) e2
| UnOp ?op ?e => go (UnOpCtx op :: K) e
| BinOp ?op ?e1 ?e2 =>
reshape_val e1 ltac:(fun v1 => go (BinOpRCtx op v1 :: K) e2)
| BinOp ?op ?e1 ?e2 => go (BinOpLCtx op e2 :: K) e1
reshape_val e2 ltac:(fun v2 => go (BinOpLCtx op v2 :: K) e1)
| BinOp ?op ?e1 ?e2 => go (BinOpRCtx op e1 :: K) e2
| If ?e0 ?e1 ?e2 => go (IfCtx e1 e2 :: K) e0
| Pair ?e1 ?e2 => reshape_val e1 ltac:(fun v1 => go (PairRCtx v1 :: K) e2)
| Pair ?e1 ?e2 => go (PairLCtx e2 :: K) e1
| Pair ?e1 ?e2 => reshape_val e2 ltac:(fun v2 => go (PairLCtx v2 :: K) e1)
| Pair ?e1 ?e2 => go (PairRCtx e1 :: K) e2
| Fst ?e => go (FstCtx :: K) e
| Snd ?e => go (SndCtx :: K) e
| InjL ?e => go (InjLCtx :: K) e
......@@ -285,12 +285,12 @@ Ltac reshape_expr e tac :=
| Case ?e0 ?e1 ?e2 => go (CaseCtx e1 e2 :: K) e0
| Alloc ?e => go (AllocCtx :: K) e
| Load ?e => go (LoadCtx :: K) e
| Store ?e1 ?e2 => reshape_val e1 ltac:(fun v1 => go (StoreRCtx v1 :: K) e2)
| Store ?e1 ?e2 => go (StoreLCtx e2 :: K) e1
| CAS ?e0 ?e1 ?e2 => reshape_val e0 ltac:(fun v0 => first
[ 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
| Store ?e1 ?e2 => reshape_val e2 ltac:(fun v2 => go (StoreLCtx v2 :: K) e1)
| Store ?e1 ?e2 => go (StoreRCtx e1 :: K) e2
| CAS ?e0 ?e1 ?e2 => reshape_val e2 ltac:(fun v2 => first
[ reshape_val e1 ltac:(fun v1 => go (CasLCtx v1 v2 :: K) e0)
| go (CasMCtx e0 v2 :: K) e1 ])
| CAS ?e0 ?e1 ?e2 => go (CasRCtx e0 e1 :: K) e2
| FAA ?e1 ?e2 => reshape_val e2 ltac:(fun v2 => go (FaaLCtx v2 :: K) e1)
| FAA ?e1 ?e2 => go (FaaRCtx e1 :: K) e2
end in go (@nil ectx_item) e.
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