Commit 7281dcca authored by Hai Dang's avatar Hai Dang
Browse files

fix notations, WIP: adding optmizations

parent f5a44b4e
......@@ -23,3 +23,5 @@ theories/sim/program.v
theories/sim/sflib.v
theories/sim/one_step.v
theories/opt/foo.v
theories/opt/ex1_2.v
theories/opt/ex2_2.v
......@@ -17,7 +17,7 @@ Definition demo0 : expr :=
(* let y = &mut *x; *)
(* mut reference y created by dereferencing mut reference x *)
let: "y" := new_place (&mut int) & *{int} (Copy1 "x") in
let: "y" := new_place (&mut int) & *{int} "x" in
(* Check read x with Uniq(x): OK! *)
(* Check deref int with Uniq(0): OK! *)
(* stack of y : [Uniq(y)], not frozen *)
......@@ -28,21 +28,21 @@ Definition demo0 : expr :=
(* y now uses Uniq(1) for i *)
(* *y = 5; *)
*{int} (Copy1 "y") <- #[5] ;;
*{int} "y" <- #[5] ;;
(* Check read y with Uniq(y): OK! *)
(* Check deref i with Uniq(1): OK! because Uniq(1) in on the stack *)
(* Check write i with Uniq(1): OK! *)
(* stack of int: [Uniq(1); Uniq(0); Uniq(?)], not frozen *)
(* *x = 3; *)
*{int} (Copy1 "x") <- #[3] ;;
*{int} "x" <- #[3] ;;
(* Check read x with Uniq(x): OK! *)
(* Check deref i with Uniq(0): OK! because Uniq(0) in on the stack *)
(* Check write i with Uniq(0): OK! but pop Uniq(1) to reactivate Uniq(0) *)
(* stack of i: [Uniq(0); Uniq(?)], not frozen *)
(* let _val = *y; *)
Copy *{int} (Copy1 "y") ;;
Copy *{int} "y" ;;
(* Check read y with Uniq(y): OK! *)
(* Check deref i with Uniq(1): UB! Uniq(1) not on stack of i! *)
(* Check read i with Uniq(1): UNREACHABLE *)
......@@ -69,7 +69,7 @@ Definition demo1 : expr :=
(* let y1 = & *x; *)
(* immut reference y1 created by dereferencing mut reference x *)
let: "y1" := new_place (& int) & *{int} (Copy1 "x") in
let: "y1" := new_place (& int) & *{int} "x" in
(* Check read x with Uniq(x): OK! *)
(* Check deref i with Uniq(0): OK! *)
(* stack of y1 : [Uniq(y1)], not frozen *)
......@@ -80,7 +80,7 @@ Definition demo1 : expr :=
(* y1 now uses Alias(1) for i *)
(* let _val = *x; *)
Copy *{int} (Copy1 "x") ;;
Copy *{int} "x" ;;
(* Check read x with Uniq(x): OK! *)
(* Check deref i with Uniq(0): OK! because Uniq(0) is on the stack *)
(* Check read i with Uniq(0): OK! because the stack is frozen *)
......@@ -88,7 +88,7 @@ Definition demo1 : expr :=
(* immut reference y2 created by dereferencing mut reference x *)
(* let y2 = & *x; *)
let: "y2" := new_place (& int) & *{int} (Copy1 "x") in
let: "y2" := new_place (& int) & *{int} "x" in
(* Check read x with Uniq(x): OK! *)
(* Check deref i with Uniq(0): OK! *)
(* stack of y2 : [Uniq(y2)], not frozen *)
......@@ -99,13 +99,13 @@ Definition demo1 : expr :=
(* y2 now uses Alias(2) for i *)
(* let _val = *y1; *)
Copy *{int} (Copy1 "y1") ;;
Copy *{int} "y1" ;;
(* Check read y1 with Uniq(y1): OK! *)
(* Check deref y1 with Alias(1): OK! because the stack is frozen_since(1) *)
(* Check read i with Alias(1): OK! because the stack is frozen *)
(* let _val = *y2; *)
Copy *{int} (Copy1 "y2") ;;
Copy *{int} "y2" ;;
(* Check read y2 with Uniq(y2): OK! *)
(* Check deref y2 with Alias(2): OK! because the stack is frozen_since(1) *)
(* Check read i with Alias(2): OK! because the stack is frozen *)
......@@ -132,7 +132,7 @@ Definition demo2 : expr :=
(* immut reference y created by dereferencing mut reference x *)
(* let y = & *x; *)
let: "y" := new_place (& int) & *{int} (Copy1 "x") in
let: "y" := new_place (& int) & *{int} "x" in
(* Check read x with Uniq(x): OK! *)
(* Check deref i with Uniq(0): OK! *)
(* stack of y : [Uniq(y)], not frozen *)
......@@ -145,7 +145,7 @@ Definition demo2 : expr :=
(* raw pointer z created by dereferencing x as raw pointer immutably then
mutably. *)
(* let z = x as *const u8 as *mut u8; *)
let: "z" := new_place ( *mut int ) & *{int} & *{int} (Copy1 "x") in
let: "z" := new_place ( *mut int ) & *{int} & *{int} "x" in
(* Check read x with Uniq(x): OK! *)
(* Check deref i with Uniq(0): OK! because Uniq(0) is on the stack and
raw derefs are not checked. *)
......@@ -156,14 +156,14 @@ Definition demo2 : expr :=
(* stack of i: [Raw; Uniq(0); Uniq(?)], frozen_since(1) *)
(* z now uses Alias(None) for the int *)
*{int} (Copy1 "z") <- #[3] ;;
*{int} "z" <- #[3] ;;
(* Check read z with Uniq(z) : OK! *)
(* Check deref int with Alias(None): OK! because raw derefs are not checked. *)
(* Check write int with Alias(None): OK! because there matches a Raw.
Furthermore, the stack is unfrozen. *)
(* stack of int: [Raw; Uniq(0); Uniq(?)], not frozen *)
Copy *{int} (Copy1 "y") ;;
Copy *{int} "y" ;;
(* Check read y with Uniq(y) : OK! *)
(* Check deref i with Alias(1): UB! because the stack is not frozen with a
timestamp less than or equal to the tag.
......@@ -193,7 +193,7 @@ Definition demo4 : expr :=
(* raw pointer y1 created from x *)
(* let y1 = x as *mut u8; *)
let: "y1" := new_place ( *mut int) & *{int} (Copy1 "x") in
let: "y1" := new_place ( *mut int) & *{int} "x" in
(* Check read x with Uniq(x): OK! *)
(* Check deref i with Uniq(0): OK! *)
(* stack of y1 : [Uniq(y1)], not frozen *)
......@@ -205,7 +205,7 @@ Definition demo4 : expr :=
(* raw pointer y2 created from y1. *)
(* let y2 = y1; *)
let: "y2" := new_place ( *mut int) & *{int} (Copy1 "y1") in
let: "y2" := new_place ( *mut int) & *{int} "y1" in
(* Check read y1 with Uniq(y1) : OK! *)
(* Check deref i with Alias(None): OK! because Raw is on the stack. *)
(* stack of y2 : [Uniq(y2)], not frozen *)
......@@ -218,23 +218,23 @@ Definition demo4 : expr :=
(* *y1 = 3;
*y2 = 5;
*y2 = *y1; *)
*{int} (Copy1 "y1") <- #[3] ;;
*{int} (Copy1 "y2") <- #[5];;
*{int} (Copy1 "y2") <- Copy *{int} (Copy1 "y1") ;;
*{int} "y1" <- #[3] ;;
*{int} "y2" <- #[5];;
*{int} "y2" <- Copy *{int} "y1" ;;
(* Checks for deref/read/write of y1 and y2 all pass because:
* raw derefs are not checked
* read/write are ok because Raw is on top of the stack, and nothing changes. *)
(* stack of i: [Raw; Uniq(0); Uniq(?)], not frozen *)
(* *x = 7; *)
*{int} (Copy1 "x") <- #[7] ;;
*{int} "x" <- #[7] ;;
(* Check read x with Uniq(x): OK! *)
(* Check deref int with Uniq(0): OK! because Uniq(0) is on the stack *)
(* Check write int with Uniq(0): OK! because Uniq(0) is on the stack *)
(* stack of i: [Uniq(0); Uniq(?)], not frozen *)
(* let _val = unsafe { *y1 }; *)
Copy *{int} (Copy1 "y1") ;;
Copy *{int} "y1" ;;
(* Check read y1 with Uniq(y1) : OK! *)
(* Check deref int with Alias(None): UB! because Raw is not on the unfrozen stack *)
(* Check read int with Alias(None): UNREACHABLE *)
......
......@@ -291,7 +291,7 @@ Inductive pure_expr_step (FNs: fn_env) (h: mem) : expr → event → expr → Pr
pure_expr_step FNs h (Ref (Place l lbor T)) SilentEvt #[ScPtr l lbor]
| DerefBS l lbor T
(DEFINED: (i: nat), (i < tsize T)%nat l + i dom (gset loc) h) :
pure_expr_step FNs h ( *{T} #[ScPtr l lbor]) SilentEvt (Place l lbor T)
pure_expr_step FNs h (Deref #[ScPtr l lbor] T) SilentEvt (Place l lbor T)
| FieldBS l lbor T path off T'
(FIELD: field_access T path = Some (off, T')) :
pure_expr_step FNs h (Field (Place l lbor T) path)
......
......@@ -54,11 +54,9 @@ Notation "'Box<' T '>'" := (Reference RawPtr T%T)
(** Pointer operations *)
Notation "& e" := (Ref e%E) (at level 8, format "& e") : expr_scope.
Notation "*{ T } e" := (Deref e%E T%T)
Notation "*{ T } e" := (Deref (Proj (Copy e%E) #[0]) T%T)
(at level 9, format "*{ T } e") : expr_scope.
Notation "'Copy1' e" := (Proj (Copy e%E) #[0]) (at level 10) : expr_scope.
(** Syntax inspired by Coq/Ocaml. Constructions with higher precedence come
first. *)
......
......@@ -345,8 +345,8 @@ Qed.
(** Deref *)
Lemma fill_deref_decompose K e e' T :
fill K e = ( *{T} e')%E
K = [] e = ( *{T} e')%E ( K', K = K' ++ [DerefCtx T] fill K' e = e').
fill K e = (Deref e' T)%E
K = [] e = (Deref e' T)%E ( K', K = K' ++ [DerefCtx T] fill K' e = e').
Proof.
revert e. induction K as [|Ki K IH]; [naive_solver|].
intros e EqK. right.
......@@ -356,7 +356,7 @@ Proof.
Qed.
Lemma tstep_deref_inv l tg T e' σ σ'
(STEP: (( *{T} #[ScPtr l tg])%E, σ) ~{fns}~> (e', σ')) :
(STEP: ((Deref #[ScPtr l tg] T)%E, σ) ~{fns}~> (e', σ')) :
e' = Place l tg T σ' = σ
( (i: nat), (i < tsize T)%nat l + i dom (gset loc) σ.(shp)).
Proof.
......
From stbor.sim Require Import local invariant one_step.
Set Default Proof Using "Type".
Definition ex1_2 : function :=
fun: ["x"],
Retag "x" FnEntry ;;
*{int} (Copy1 "x") <- #[42] ;;
Call #[ScFnPtr "f"] [] ;;
*{int} (Copy1 "x") <- #[13]
.
Definition ex1_2_opt_1 : function :=
fun: ["x"],
Retag "x" FnEntry ;;
Call #[ScFnPtr "f"] [] ;;
*{int} (Copy1 "x") <- #[42] ;;
*{int} (Copy1 "x") <- #[13]
.
Definition ex1_2_opt_2 : function :=
fun: ["x"],
Retag "x" FnEntry ;;
Call #[ScFnPtr "f"] [] ;;
*{int} (Copy1 "x") <- #[13]
.
Lemma ex1_2_sim_fun fs ft : {fs,ft} ex1_2 ≥ᶠ ex1_2_opt_1.
Proof.
intros [r1 r2] es et els elt σs σt FAs FAt FREL SUBSTs SUBSTt.
destruct els as [|efs []]; [done| |done]. simpl in SUBSTs.
destruct elt as [|eft []]; [done| |done]. simpl in SUBSTt. simplify_eq.
(* InitCall *)
exists 1%nat.
apply sim_body_init_call. rewrite pair_op.
Abort.
\ No newline at end of file
From stbor.sim Require Import local invariant one_step.
Set Default Proof Using "Type".
Definition ex2_2 : function :=
fun: ["x"],
Retag "x" FnEntry ;;
let: "v" := Copy *{int} "x" in
Call #[ScFnPtr "f"] ["x"] ;;
"v"
.
Definition ex2_2_opt : function :=
fun: ["x"],
Retag "x" FnEntry ;;
Call #[ScFnPtr "f"] ["x"] ;;
Copy *{int} "x"
.
From stbor.sim Require Import local invariant one_step.
Set Default Proof Using "Type".
Definition foo_s : function :=
fun: [],
let: "i" := new_place int #[1] in
let: "x" := new_place (&mut int) &"i" in
Retag "x" Default ;;
let: "j" := new_place int #[1] in
let: "y" := new_place (&mut int) &"j" in
Retag "y" Default ;;
*{int} (Copy1 "y") <- #[5] ;;
*{int} (Copy1 "x") <- #[3] ;;
Free "i" ;;
Free "x" ;;
Free "j" ;;
Free "y"
.
Definition foo_t : function :=
fun: [],
let: "i" := new_place int #[1] in
let: "x" := new_place (&mut int) &"i" in
Retag "x" Default ;;
let: "j" := new_place int #[1] in
let: "y" := new_place (&mut int) &"j" in
Retag "y" Default ;;
(* reordering x and y *)
*{int} (Copy1 "x") <- #[3] ;;
*{int} (Copy1 "y") <- #[5] ;;
Free "i" ;;
Free "x" ;;
Free "j" ;;
Free "y"
.
Lemma foo_sim_fun fs ft : {fs,ft} foo_s ≥ᶠ foo_t.
Proof.
move => r es et els elt σs σt _ _ _
/subst_l_nil_is_Some ? /subst_l_nil_is_Some ?.
subst es et. clear els elt.
(* InitCall *)
exists 1%nat.
Abort.
......@@ -1165,12 +1165,12 @@ Qed.
Lemma sim_body_deref fs ft r n l tgs tgt Ts Tt σs σt Φ
(EQS: tsize Ts = tsize Tt) :
r {n,fs,ft} (Place l tgs Ts, σs) (Place l tgt Tt, σt) : Φ
r {n,fs,ft} (( *{Ts} #[ScPtr l tgs])%E, σs) (( *{Tt} #[ScPtr l tgt])%E, σt) : Φ.
r {n,fs,ft} (Deref #[ScPtr l tgs] Ts, σs) (Deref #[ScPtr l tgt] Tt, σt) : Φ.
Proof.
intros SIM. pfold.
intros NT r_f WSAT. split; [|done|].
{ right.
destruct (NT ( *{Ts} #[ScPtr l tgs])%E σs) as [[]|[es' [σs' STEPS]]]; [done..|].
destruct (NT (Deref #[ScPtr l tgs] Ts) σs) as [[]|[es' [σs' STEPS]]]; [done..|].
destruct (tstep_deref_inv _ _ _ _ _ _ _ STEPS) as [? [? IS]]. subst es' σs'.
have ?: ( (i: nat), (i < tsize Tt)%nat l + i dom (gset loc) σt.(shp)).
{ clear -WSAT IS EQS. rewrite -EQS. move => i /IS. by rewrite -wsat_heap_dom. }
......
Supports Markdown
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