Skip to content
Snippets Groups Projects
Commit e795b65a authored by Daniël Louwrink's avatar Daniël Louwrink
Browse files

add SB to lang semantics

parent b9151c61
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 46 additions and 32 deletions
theories/lang/lang.v
+ 46
− 32
View file @ e795b65a
...@@ -241,27 +241,30 @@ Inductive head_step : expr → state → list Empty_set → expr → state → l ...@@ -241,27 +241,30 @@ Inductive head_step : expr → state → list Empty_set → expr → state → l
Closed (f :b: xl +b+ []) e → Closed (f :b: xl +b+ []) e →
subst_l (f::xl) (Rec f xl e :: el) e = Some e' → subst_l (f::xl) (Rec f xl e :: el) e = Some e' →
head_step (App (Rec f xl e) el) σ [] e' σ [] head_step (App (Rec f xl e) el) σ [] e' σ []
| ReadScS l tg n v σ stbor: | ReadScS l tg n v σ stbor1 stbor2:
σ !! l = Some (RSt n, v) → σ !! l = Some (RSt n, v) →
head_step (Read ScOrd (Lit $ LitLoc l tg)) (MkSt σ stbor) [] (of_val v) (MkSt σ stbor) [] stbor_step stbor1 (StborReadEv l tg 1) stbor2 →
head_step (Read ScOrd (Lit $ LitLoc l tg)) (MkSt σ stbor1) [] (of_val v) (MkSt σ stbor2) []
| ReadNa1S l tg n v σ stbor: | ReadNa1S l tg n v σ stbor:
σ !! l = Some (RSt n, v) → σ !! l = Some (RSt n, v) →
head_step (Read Na1Ord (Lit $ LitLoc l tg)) (MkSt σ stbor) head_step (Read Na1Ord (Lit $ LitLoc l tg)) (MkSt σ stbor)
[] []
(Read Na2Ord (Lit $ LitLoc l tg)) (MkSt (<[l:=(RSt $ S n, v)]>σ) stbor) (Read Na2Ord (Lit $ LitLoc l tg)) (MkSt (<[l:=(RSt $ S n, v)]>σ) stbor)
[] []
| ReadNa2S l tg n v σ stbor: | ReadNa2S l tg n v σ stbor1 stbor2:
σ !! l = Some (RSt $ S n, v) → σ !! l = Some (RSt $ S n, v) →
head_step (Read Na2Ord (Lit $ LitLoc l tg)) (MkSt σ stbor) stbor_step stbor1 (StborReadEv l tg 1) stbor2 →
head_step (Read Na2Ord (Lit $ LitLoc l tg)) (MkSt σ stbor1)
[] []
(of_val v) (MkSt (<[l:=(RSt n, v)]>σ) stbor) (of_val v) (MkSt (<[l:=(RSt n, v)]>σ) stbor2)
[] []
| WriteScS l tg e v v' σ stbor: | WriteScS l tg e v v' σ stbor1 stbor2:
to_val e = Some v → to_val e = Some v →
σ !! l = Some (RSt 0, v') → σ !! l = Some (RSt 0, v') →
head_step (Write ScOrd (Lit $ LitLoc l tg) e) (MkSt σ stbor) stbor_step stbor1 (StborWriteEv l tg 1) stbor2 →
head_step (Write ScOrd (Lit $ LitLoc l tg) e) (MkSt σ stbor1)
[] []
(Lit LitPoison) (MkSt (<[l:=(RSt 0, v)]>σ) stbor) (Lit LitPoison) (MkSt (<[l:=(RSt 0, v)]>σ) stbor2)
[] []
| WriteNa1S l tg e v v' σ stbor: | WriteNa1S l tg e v v' σ stbor:
to_val e = Some v → to_val e = Some v →
...@@ -270,25 +273,28 @@ Inductive head_step : expr → state → list Empty_set → expr → state → l ...@@ -270,25 +273,28 @@ Inductive head_step : expr → state → list Empty_set → expr → state → l
[] []
(Write Na2Ord (Lit $ LitLoc l tg) e) (MkSt (<[l:=(WSt, v')]>σ) stbor) (Write Na2Ord (Lit $ LitLoc l tg) e) (MkSt (<[l:=(WSt, v')]>σ) stbor)
[] []
| WriteNa2S l tg e v v' σ stbor: | WriteNa2S l tg e v v' σ stbor1 stbor2 :
to_val e = Some v → to_val e = Some v →
σ !! l = Some (WSt, v') → σ !! l = Some (WSt, v') →
head_step (Write Na2Ord (Lit $ LitLoc l tg) e) (MkSt σ stbor) stbor_step stbor1 (StborWriteEv l tg 1) stbor2 →
head_step (Write Na2Ord (Lit $ LitLoc l tg) e) (MkSt σ stbor1)
[] []
(Lit LitPoison) (MkSt (<[l:=(RSt 0, v)]>σ) stbor) (Lit LitPoison) (MkSt (<[l:=(RSt 0, v)]>σ) stbor2)
[] []
| CasFailS l tg n e1 lit1 e2 lit2 litl σ stbor : | CasFailS l tg n e1 lit1 e2 lit2 litl σ stbor1 stbor2 :
to_val e1 = Some $ LitV lit1 → to_val e2 = Some $ LitV lit2 → to_val e1 = Some $ LitV lit1 → to_val e2 = Some $ LitV lit2 →
σ !! l = Some (RSt n, LitV litl) → σ !! l = Some (RSt n, LitV litl) →
lit_neq lit1 litl → lit_neq lit1 litl →
head_step (CAS (Lit $ LitLoc l tg) e1 e2) (MkSt σ stbor) [] (Lit $ lit_of_bool false) (MkSt σ stbor) [] stbor_step stbor1 (StborReadEv l tg 1) stbor2 →
| CasSucS l tg e1 lit1 e2 lit2 litl σ stbor : head_step (CAS (Lit $ LitLoc l tg) e1 e2) (MkSt σ stbor1) [] (Lit $ lit_of_bool false) (MkSt σ stbor2) []
| CasSucS l tg e1 lit1 e2 lit2 litl σ stbor1 stbor2 :
to_val e1 = Some $ LitV lit1 → to_val e2 = Some $ LitV lit2 → to_val e1 = Some $ LitV lit1 → to_val e2 = Some $ LitV lit2 →
σ !! l = Some (RSt 0, LitV litl) → σ !! l = Some (RSt 0, LitV litl) →
lit_eq σ lit1 litl → lit_eq σ lit1 litl →
head_step (CAS (Lit $ LitLoc l tg) e1 e2) (MkSt σ stbor) stbor_step stbor1 (StborWriteEv l tg 1) stbor2 →
head_step (CAS (Lit $ LitLoc l tg) e1 e2) (MkSt σ stbor1)
[] []
(Lit $ lit_of_bool true) (MkSt (<[l:=(RSt 0, LitV lit2)]>σ) stbor) (Lit $ lit_of_bool true) (MkSt (<[l:=(RSt 0, LitV lit2)]>σ) stbor2)
[] []
(* A succeeding CAS has to detect concurrent non-atomic read accesses, and (* A succeeding CAS has to detect concurrent non-atomic read accesses, and
trigger UB if there is one. In lambdaRust, succeeding and failing CAS are trigger UB if there is one. In lambdaRust, succeeding and failing CAS are
...@@ -312,20 +318,27 @@ Inductive head_step : expr → state → list Empty_set → expr → state → l ...@@ -312,20 +318,27 @@ Inductive head_step : expr → state → list Empty_set → expr → state → l
[] []
stuck_term (MkSt σ stbor) stuck_term (MkSt σ stbor)
[] []
(* TODO: Right now the tag is always zero! *) | AllocS n l tgnew σ stbor1 stbor2 :
| AllocS n l σ stbor :
0 < n → 0 < n →
(∀ m, σ !! (l +ₗ m) = None) → (∀ m, σ !! (l +ₗ m) = None) →
head_step (Alloc $ Lit $ LitInt n) (MkSt σ stbor) stbor_step stbor1 (StborAllocEv l (Z.to_nat n) tgnew) stbor2 →
head_step (Alloc $ Lit $ LitInt n) (MkSt σ stbor1)
[]
(Lit $ LitLoc l tgnew) (MkSt (init_mem l (Z.to_nat n) σ) stbor2)
[]
| RetagS interior pkind rkind l tgold σ stbor1 stbor2 tgnew :
stbor_step stbor1 (StborRetagEv l tgold interior pkind rkind tgnew) stbor2 →
head_step (Retag interior pkind rkind $ Lit $ LitLoc l tgold) (MkSt σ stbor1)
[] []
(Lit $ LitLoc l (Tagged 0%nat)) (MkSt (init_mem l (Z.to_nat n) σ) stbor) (Lit $ LitLoc l tgnew) (MkSt σ stbor2)
[] []
| FreeS n l tg σ stbor : | FreeS n l tg σ stbor1 stbor2 :
0 < n → 0 < n →
(∀ m, is_Some (σ !! (l +ₗ m)) ↔ 0 ≤ m < n) → (∀ m, is_Some (σ !! (l +ₗ m)) ↔ 0 ≤ m < n) →
head_step (Free (Lit $ LitInt n) (Lit $ LitLoc l tg)) (MkSt σ stbor) stbor_step stbor1 (StborDeallocEv l tg (Z.to_nat n)) stbor2 →
head_step (Free (Lit $ LitInt n) (Lit $ LitLoc l tg)) (MkSt σ stbor1)
[] []
(Lit LitPoison) (MkSt (free_mem l (Z.to_nat n) σ) stbor) (Lit LitPoison) (MkSt (free_mem l (Z.to_nat n) σ) stbor2)
[] []
| CaseS i el e σ : | CaseS i el e σ :
0 ≤ i → 0 ≤ i →
...@@ -442,15 +455,16 @@ Proof. ...@@ -442,15 +455,16 @@ Proof.
move=> /(help _ _ ∅) /=. apply is_fresh. move=> /(help _ _ ∅) /=. apply is_fresh.
Qed. Qed.
Lemma alloc_fresh n σ stbor : (* TODO: FIXME *)
let l := (fresh_block σ, 0) in (* Lemma alloc_fresh n σ stbor : *)
let init := repeat (LitV $ LitInt 0) (Z.to_nat n) in (* let l := (fresh_block σ, 0) in *)
0 < n → (* let init := repeat (LitV $ LitInt 0) (Z.to_nat n) in *)
head_step (Alloc $ Lit $ LitInt n) (MkSt σ stbor) [] (Lit $ LitLoc l (Tagged 0%nat)) (MkSt (init_mem l (Z.to_nat n) σ) stbor) []. (* 0 < n → *)
Proof. (* head_step (Alloc $ Lit $ LitInt n) (MkSt σ stbor) [] (Lit $ LitLoc l (Tagged 0%nat)) (MkSt (init_mem l (Z.to_nat n) σ) stbor) []. *)
intros l init Hn. apply AllocS. auto. (* Proof. *)
- intros i. apply (is_fresh_block _ i). (* intros l init Hn. apply AllocS. auto. *)
Qed. (* - intros i. apply (is_fresh_block _ i). *)
(* Qed. *)
Lemma lookup_free_mem_ne σ l l' n : l.1 ≠ l'.1 → free_mem l n σ !! l' = σ !! l'. Lemma lookup_free_mem_ne σ l l' n : l.1 ≠ l'.1 → free_mem l n σ !! l' = σ !! l'.
Proof. Proof.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment