Commit 4b577aed authored by Robbert Krebbers's avatar Robbert Krebbers

Move stack definitions to top of file.

parent 4b017ac0
......@@ -3,17 +3,63 @@ From iris_logrel.F_mu_ref_par Require Import lang examples.lock typing
rules_binary rules.
Import uPred.
Definition CG_StackType τ :=
TRec (TSum TUnit (TProd τ.[ren (+1)] (TVar 0))).
(* Coarse-grained push *)
Definition CG_push (st : expr) : expr :=
Lam (Store
(st.[ren (+2)]) (Fold (InjR (Pair (Var 1) (Load st.[ren (+ 2)]))))).
Definition CG_locked_push (st l : expr) := with_lock (CG_push st) l.
Definition CG_locked_pushV (st l : expr) : val := with_lockV (CG_push st) l.
Definition CG_pop (st : expr) : expr :=
Lam (Case (Unfold (Load st.[ren (+ 2)]))
(InjL Unit)
(
App (Lam (InjR (Fst (Var 2))))
(Store st.[ren (+ 3)] (Snd (Var 0)))
)
).
Definition CG_locked_pop (st l : expr) := with_lock (CG_pop st) l.
Definition CG_locked_popV (st l : expr) : val := with_lockV (CG_pop st) l.
Definition CG_snap (st l : expr) := with_lock (Lam (Load st.[ren (+2)])) l.
Definition CG_snapV (st l : expr) : val := with_lockV (Lam (Load st.[ren (+2)])) l.
Definition CG_iter (f : expr) : expr :=
Lam (Case (Unfold (Var 1))
Unit
(
App (Lam (App (Var 3) (Snd (Var 2))))
(App f.[ren (+3)] (Fst (Var 0)))
)
).
Definition CG_iterV (f : expr) : val :=
LamV (Case (Unfold (Var 1))
Unit
(
App (Lam (App (Var 3) (Snd (Var 2))))
(App f.[ren (+3)] (Fst (Var 0)))
)
).
Definition CG_snap_iter (st l : expr) : expr :=
Lam (App (CG_iter (Var 1)) (App (CG_snap st.[ren (+2)] l.[ren (+2)]) Unit)).
Definition CG_stack_body (st l : expr) : expr :=
Pair (Pair (CG_locked_push st l) (CG_locked_pop st l))
(CG_snap_iter st l).
Definition CG_stack : expr :=
TLam (App (Lam (App (Lam (CG_stack_body (Var 1) (Var 3)))
(Alloc (Fold (InjL Unit))))) newlock).
Section CG_Stack.
Context {Σ : gFunctors} {iS : cfgSG Σ}.
Definition CG_StackType τ :=
(TRec (TSum TUnit (TProd τ.[ren (+1)] (TVar 0)))).
(* Coarse-grained push *)
Definition CG_push (st : expr) : expr :=
Lam (Store
(st.[ren (+2)]) (Fold (InjR (Pair (Var 1) (Load st.[ren (+ 2)]))))).
Lemma CG_push_type st Γ τ :
typed Γ st (Tref (CG_StackType τ))
typed Γ (CG_push st) (TArrow τ TUnit).
......@@ -55,11 +101,6 @@ Section CG_Stack.
Global Opaque CG_push.
Definition CG_locked_push (st l : expr) :=
with_lock (CG_push st) l.
Definition CG_locked_pushV (st l : expr) : val :=
with_lockV (CG_push st) l.
Lemma CG_locked_push_to_val st l :
to_val (CG_locked_push st l) = Some (CG_locked_pushV st l).
Proof. trivial. Qed.
......@@ -109,15 +150,6 @@ Section CG_Stack.
Global Opaque CG_locked_push.
(* Coarse-grained pop *)
Definition CG_pop (st : expr) : expr :=
Lam (Case (Unfold (Load st.[ren (+ 2)]))
(InjL Unit)
(
App (Lam (InjR (Fst (Var 2))))
(Store st.[ren (+ 3)] (Snd (Var 0)))
)
).
Lemma CG_pop_type st Γ τ :
typed Γ st (Tref (CG_StackType τ))
typed Γ (CG_pop st) (TArrow TUnit (TSum TUnit τ)).
......@@ -213,11 +245,6 @@ Section CG_Stack.
Global Opaque CG_pop.
Definition CG_locked_pop (st l : expr) :=
with_lock (CG_pop st) l.
Definition CG_locked_popV (st l : expr) : val :=
with_lockV (CG_pop st) l.
Lemma CG_locked_pop_to_val st l :
to_val (CG_locked_pop st l) = Some (CG_locked_popV st l).
Proof. trivial. Qed.
......@@ -281,11 +308,6 @@ Section CG_Stack.
Global Opaque CG_locked_pop.
Definition CG_snap (st l : expr) :=
with_lock (Lam (Load st.[ren (+2)])) l.
Definition CG_snapV (st l : expr) : val :=
with_lockV (Lam (Load st.[ren (+2)])) l.
Lemma CG_snap_to_val st l : to_val (CG_snap st l) = Some (CG_snapV st l).
Proof. trivial. Qed.
......@@ -341,15 +363,6 @@ Section CG_Stack.
Global Opaque CG_snap.
(* Coarse-grained iter *)
Definition CG_iter (f : expr) : expr :=
Lam (Case (Unfold (Var 1))
Unit
(
App (Lam (App (Var 3) (Snd (Var 2))))
(App f.[ren (+3)] (Fst (Var 0)))
)
).
Lemma CG_iter_folding (f : expr) :
CG_iter f =
Lam (Case (Unfold (Var 1))
......@@ -376,15 +389,6 @@ Section CG_Stack.
repeat econstructor.
Qed.
Definition CG_iterV (f : expr) : val :=
LamV (Case (Unfold (Var 1))
Unit
(
App (Lam (App (Var 3) (Snd (Var 2))))
(App f.[ren (+3)] (Fst (Var 0)))
)
).
Lemma CG_iter_to_val f : to_val (CG_iter f) = Some (CG_iterV f).
Proof. trivial. Qed.
......@@ -479,10 +483,6 @@ Section CG_Stack.
rewrite CG_snap_subst CG_iter_subst. by asimpl.
Qed.
Definition CG_stack_body (st l : expr) : expr :=
Pair (Pair (CG_locked_push st l) (CG_locked_pop st l))
(CG_snap_iter st l).
Lemma CG_stack_body_type st l Γ τ :
typed Γ st (Tref (CG_StackType τ))
typed Γ l LockType
......@@ -509,10 +509,6 @@ Section CG_Stack.
by rewrite CG_snap_iter_closed.
Qed.
Definition CG_stack : expr :=
TLam (App (Lam (App (Lam (CG_stack_body (Var 1) (Var 3)))
(Alloc (Fold (InjL Unit))))) newlock).
Lemma CG_stack_type Γ :
typed Γ (CG_stack)
(TForall
......
From iris.program_logic Require Import language.
From iris_logrel.F_mu_ref_par Require Import lang typing rules.
Definition FG_StackType τ :=
TRec (Tref (TSum TUnit (TProd τ.[ren (+1)] (TVar 0)))).
Definition FG_push (st : expr) : expr :=
Lam (App (Lam
(* try push *)
(If (CAS (st.[ren (+4)]) (Var 1)
(Fold (Alloc (InjR (Pair (Var 3) (Var 1)))))
)
Unit (* push succeeds we return unit *)
(App (Var 2) (Var 3)) (* push fails, we try again *)
)
)
(Load st.[ren (+2)]) (* read the stack pointer *)
).
Definition FG_pushV (st : expr) : val :=
LamV (App (Lam
(* try push *)
(If (CAS (st.[ren (+4)]) (Var 1)
(Fold (Alloc (InjR (Pair (Var 3) (Var 1)))))
)
Unit (* push succeeds we return unit *)
(App (Var 2) (Var 3)) (* push fails, we try again *)
)
)
(Load st.[ren (+2)]) (* read the stack pointer *)
).
Definition FG_pop (st : expr) : expr :=
Lam (App (Lam
(App
(Lam
(
Case (Var 1)
(InjL Unit)
( (* try popping *)
If
(CAS
(st.[ren (+7)])
(Fold (Var 4))
(Snd (Var 0))
)
(InjR (Fst (Var 0))) (* pop succeeds *)
(App (Var 5) (Var 6)) (* pop fails, we retry*)
)
)
)
(
(Load (Var 1))
)
)
)
(Unfold (Load st.[ren (+ 2)]))
).
Definition FG_popV (st : expr) : val :=
LamV
(App
(Lam
( App
(Lam
(
Case (Var 1)
(InjL Unit)
( (* try popping *)
If
(CAS
(st.[ren (+7)])
(Fold (Var 4))
(Snd (Var 0))
)
(InjR (Fst (Var 0))) (* pop succeeds *)
(App (Var 5) (Var 6)) (* pop fails, we retry*)
)
)
)
(
(Load (Var 1))
)
)
)
(Unfold (Load st.[ren (+ 2)]))
).
Definition FG_iter (f : expr) : expr :=
Lam
(Case (Load (Unfold (Var 1)))
Unit
(App (Lam (App (Var 3) (Snd (Var 2)))) (* recursive_call *)
(App f.[ren (+3)] (Fst (Var 0)))
)
).
Definition FG_iterV (f : expr) : val :=
LamV
(Case (Load (Unfold (Var 1)))
Unit
(App (Lam (App (Var 3) (Snd (Var 2)))) (* recursive_call *)
(App f.[ren (+3)] (Fst (Var 0)))
)
).
Definition FG_read_iter (st : expr) : expr :=
Lam (App (FG_iter (Var 1)) (Load st.[ren (+2)])).
Definition FG_stack_body (st : expr) : expr :=
Pair (Pair (FG_push st) (FG_pop st)) (FG_read_iter st).
Definition FG_stack : expr :=
TLam (App (Lam (FG_stack_body (Var 1)))
(Alloc (Fold (Alloc (InjL Unit))))).
Section FG_stack.
Context {Σ : gFunctors} {iI : heapIG Σ}.
Definition FG_StackType τ :=
TRec (Tref (TSum TUnit (TProd τ.[ren (+1)] (TVar 0)))).
(* Fine-grained push *)
Definition FG_push (st : expr) : expr :=
Lam (App (Lam
(* try push *)
(If (CAS (st.[ren (+4)]) (Var 1)
(Fold (Alloc (InjR (Pair (Var 3) (Var 1)))))
)
Unit (* push succeeds we return unit *)
(App (Var 2) (Var 3)) (* push fails, we try again *)
)
)
(Load st.[ren (+2)]) (* read the stack pointer *)
).
Lemma FG_push_folding (st : expr) :
FG_push st =
Lam (App (Lam
......@@ -51,22 +144,8 @@ Section FG_stack.
- by asimpl.
- eapply (context_weakening [_; _]); eauto.
Qed.
End FG_push_type.
Definition FG_pushV (st : expr) : val :=
LamV (App (Lam
(* try push *)
(If (CAS (st.[ren (+4)]) (Var 1)
(Fold (Alloc (InjR (Pair (Var 3) (Var 1)))))
)
Unit (* push succeeds we return unit *)
(App (Var 2) (Var 3)) (* push fails, we try again *)
)
)
(Load st.[ren (+2)]) (* read the stack pointer *)
).
Lemma FG_push_to_val st : to_val (FG_push st) = Some (FG_pushV st).
Proof. trivial. Qed.
......@@ -85,33 +164,6 @@ Section FG_stack.
Global Opaque FG_push.
(* Fine-grained push *)
Definition FG_pop (st : expr) : expr :=
Lam (App (Lam
(App
(Lam
(
Case (Var 1)
(InjL Unit)
( (* try popping *)
If
(CAS
(st.[ren (+7)])
(Fold (Var 4))
(Snd (Var 0))
)
(InjR (Fst (Var 0))) (* pop succeeds *)
(App (Var 5) (Var 6)) (* pop fails, we retry*)
)
)
)
(
(Load (Var 1))
)
)
)
(Unfold (Load st.[ren (+ 2)]))
).
Lemma FG_pop_folding (st : expr) :
FG_pop st =
Lam (App (Lam
......@@ -156,38 +208,8 @@ Section FG_stack.
- asimpl; trivial.
- eapply (context_weakening [_; _]); eauto.
Qed.
End FG_pop_type.
Definition FG_popV (st : expr) : val :=
LamV
(App
(Lam
( App
(Lam
(
Case (Var 1)
(InjL Unit)
( (* try popping *)
If
(CAS
(st.[ren (+7)])
(Fold (Var 4))
(Snd (Var 0))
)
(InjR (Fst (Var 0))) (* pop succeeds *)
(App (Var 5) (Var 6)) (* pop fails, we retry*)
)
)
)
(
(Load (Var 1))
)
)
)
(Unfold (Load st.[ren (+ 2)]))
).
Lemma FG_pop_to_val st : to_val (FG_pop st) = Some (FG_popV st).
Proof. trivial. Qed.
......@@ -206,15 +228,6 @@ Section FG_stack.
Global Opaque FG_pop.
(* Fine-grained iter *)
Definition FG_iter (f : expr) : expr :=
Lam
(Case (Load (Unfold (Var 1)))
Unit
(App (Lam (App (Var 3) (Snd (Var 2)))) (* recursive_call *)
(App f.[ren (+3)] (Fst (Var 0)))
)
).
Lemma FG_iter_folding (f : expr) :
FG_iter f =
Lam
......@@ -242,15 +255,6 @@ Section FG_stack.
repeat econstructor.
Qed.
Definition FG_iterV (f : expr) : val :=
LamV
(Case (Load (Unfold (Var 1)))
Unit
(App (Lam (App (Var 3) (Snd (Var 2)))) (* recursive_call *)
(App f.[ren (+3)] (Fst (Var 0)))
)
).
Lemma FG_iter_to_val st : to_val (FG_iter st) = Some (FG_iterV st).
Proof. trivial. Qed.
......@@ -268,9 +272,6 @@ Section FG_stack.
Global Opaque FG_iter.
Definition FG_read_iter (st : expr) : expr :=
Lam (App (FG_iter (Var 1)) (Load st.[ren (+2)])).
Lemma FG_read_iter_type st Γ τ :
typed Γ st (Tref (FG_StackType τ))
typed Γ (FG_read_iter st)
......@@ -297,9 +298,6 @@ Section FG_stack.
Global Opaque FG_iter.
Definition FG_stack_body (st : expr) : expr :=
Pair (Pair (FG_push st) (FG_pop st)) (FG_read_iter st).
Section FG_stack_body_type.
(* The following assumption is simply ** WRONG ** *)
(* We assume it though to just be able to prove that the
......@@ -318,7 +316,6 @@ Section FG_stack.
repeat (econstructor; eauto using FG_push_type,
FG_pop_type, FG_read_iter_type).
Qed.
End FG_stack_body_type.
Opaque FG_read_iter.
......@@ -333,10 +330,6 @@ Section FG_stack.
by rewrite FG_read_iter_closed.
Qed.
Definition FG_stack : expr :=
TLam (App (Lam (FG_stack_body (Var 1)))
(Alloc (Fold (Alloc (InjL Unit))))).
Section FG_stack_type.
(* The following assumption is simply ** WRONG ** *)
(* We assume it though to just be able to prove that the
......
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