Commit e3046298 authored by Glen Mével's avatar Glen Mével
Browse files

add mult/div/mod to the programming language

parent 77e3e90e
......@@ -6,10 +6,6 @@ From cosmo.program_logic Require Export proofmode atomic.
Set Default Proof Using "Type".
Open Scope Z.
(* TODO:
- add multiplication, division, modulo to the core language
*)
(** Implementation **)
Section bounded_queue.
......@@ -25,10 +21,6 @@ Definition init_array (α : atomicity) : val := λ: "n" "f",
)
) #0.
Axiom modulo : val.
Axiom modulo_spec : `{cosmoG Σ} (n m : Z),
(Φ : val vProp Σ), Φ #(n mod m) - WP modulo #n #m {{ Φ }}.
(*
ICFP21: Below follows the implementation, in our toy deep-embedded language,
of the bounded queue with a circular buffer. It corresponds to Figure 8 of
......@@ -50,7 +42,7 @@ Axiom modulo_spec : ∀ `{cosmoG Σ} (n m : Z),
Definition make : val := λ: <>,
let: "elements" := Alloc NonAtomic #capacity #() in
let: "statuses" := init_array Atomic #capacity (λ: "i", "i"+"i") in
let: "statuses" := init_array Atomic #capacity (λ: "i", #2*"i") in
let: "tail" := ref_at #0 in
let: "head" := ref_at #0 in
("tail", "head", "statuses", "elements").
......@@ -58,11 +50,11 @@ Definition make : val := λ: <>,
Definition try_enqueue : val := λ: "q" "x",
let: ("tail", "head", "statuses", "elements") := "q" in
let: "h" := !at "head" in
let: "hmod" := modulo "h" #capacity in
let: "hmod" := "h" `mod` #capacity in
let: "s" := Read Atomic "statuses" "hmod" in
if: ("s" = "h"+"h") && CAS_ref "head" "h" ("h" + #1) then (
if: ("s" = #2*"h") && CAS_ref "head" "h" ("h" + #1) then (
Write NonAtomic "elements" "hmod" "x" ;;
Write Atomic "statuses" "hmod" ("s" + #1) ;;
Write Atomic "statuses" "hmod" (#2*"h" + #1) ;;
#true
)
else
......@@ -77,12 +69,12 @@ Definition enqueue : val := rec: "enqueue" "q" "x" :=
Definition try_dequeue : val := λ: "q",
let: ("tail", "head", "statuses", "elements") := "q" in
let: "t" := !at "tail" in
let: "tmod" := modulo "t" #capacity in
let: "tmod" := "t" `mod` #capacity in
let: "s" := Read Atomic "statuses" "tmod" in
if: ("s" = "t"+"t" + #1) && CAS_ref "tail" "t" ("t" + #1) then (
if: ("s" = #2*"t" + #1) && CAS_ref "tail" "t" ("t" + #1) then (
let: "x" := Read NonAtomic "elements" "tmod" in
Write NonAtomic "elements" "tmod" #() ;; (* optional, useful for GC *)
Write Atomic "statuses" "tmod" ("t"+"t" + #capacity+#capacity) ;;
Write Atomic "statuses" "tmod" (#2*("t" + #capacity)) ;;
SOME "x"
)
else
......@@ -607,7 +599,7 @@ Section Spec.
apply list_lookup_valid => ?. destruct (_ !! _) eqn:Hlookup ; last done.
apply lookup_replicate in Hlookup as [[=->] _]. done. }
epose (monos := (λ sV, to_latT (Some (StatusPair sV.1 sV.2))) <$> (
(λ i, (i+i, Ve)) <$> seqZ 0 capacity ) ).
(λ i, (2*i, Ve)) <$> seqZ 0 capacity ) ).
iMod (own_alloc monos) as (γmonos) "Hγmonos●".
{ apply list_lookup_valid => ?. rewrite list_lookup_fmap.
destruct (_ !! _) => //=. by apply Some_valid, auth_auth_valid. }
......@@ -690,7 +682,7 @@ Section Spec.
clear dependent t0 Vt0 Vh0 xVs0 sVs0.
(* pure steps *)
iModIntro. wp_let. wp_apply modulo_spec. wp_let.
iModIntro. wp_let. wp_op. wp_let.
(* (2) atomic read statuses.[h % capacity] *)
(* --- open invariant *)
......@@ -836,7 +828,6 @@ Section Spec.
(* --- perform write *)
wp_write_block at (V Ve) as s3 V3 _ "_" ; last clear s3 V3.
{ rewrite fmap_length Hlens. apply Z_mod_lt. lia. }
rewrite (_ : h0+h0 = 2*h0) ; last lia.
(* --- close invariant *)
iSplitR "HΦ".
......@@ -984,7 +975,7 @@ Section Spec.
clear dependent h0 Vt0 Vh0 xVs0 sVs0.
(* pure steps *)
iModIntro. wp_let. wp_apply modulo_spec. wp_let.
iModIntro. wp_let. wp_op. wp_let.
(* (2) atomic read statuses.[h % capacity] *)
(* --- open invariant *)
......@@ -1135,7 +1126,6 @@ Section Spec.
(* --- perform write *)
wp_write_block at (V Ve) as s3 V3 HsV3 "HV3".
{ rewrite fmap_length Hlens. apply Z_mod_lt. lia. }
rewrite (_ : t0+t0+capacity+capacity = 2*(t0+capacity)) ; last lia.
(* --- close invariant *)
iSplitR "HΦ".
......
......@@ -31,13 +31,12 @@ Implicit Types l : lit.
Inductive un_op := | MinusUnOp | NotOp.
Inductive bin_op := | PlusOp | MinusOp | LeOp | EqOp | AndOp | OrOp.
Inductive bin_op := | PlusOp | MinusOp | MultOp | DivOp | ModOp | LeOp | EqOp | AndOp | OrOp.
Module base.
(** Base expression language without views **)
(* TODO: Add pairs and sums, or at least an if-then-else on booleans. *)
Inductive expr :=
(* Values *)
| Val (v : val)
......@@ -225,6 +224,9 @@ Module base.
match op, l1, l2 with
| PlusOp, LitInt z1, LitInt z2 => Some $ LitInt (z1 + z2)
| MinusOp, LitInt z1, LitInt z2 => Some $ LitInt (z1 - z2)
| MultOp, LitInt z1, LitInt z2 => Some $ LitInt (z1 * z2)
| DivOp, LitInt z1, LitInt z2 => Some $ LitInt (z1 / z2)
| ModOp, LitInt z1, LitInt z2 => Some $ LitInt (z1 `mod` z2)
| LeOp, LitInt z1, LitInt z2 => Some $ LitBool $ bool_decide (z1 z2)
| EqOp, _, _ =>
match lit_eq l1 l2, lit_neq l1 l2 with
......@@ -448,9 +450,11 @@ Module base.
Instance bin_op_countable : Countable bin_op.
Proof.
refine (inj_countable' (λ op, match op with
| PlusOp => 0 | MinusOp => 1 | LeOp => 2 | EqOp => 3 | AndOp => 4 | OrOp => 5
| PlusOp => 0 | MinusOp => 1 | MultOp => 2 | DivOp => 3 | ModOp => 4
| LeOp => 5 | EqOp => 6 | AndOp => 7 | OrOp => 8
end) (λ n, match n with
| 0 => PlusOp | 1 => MinusOp | 2 => LeOp | 3 => EqOp | 4 => AndOp | _ => OrOp
| 0 => PlusOp | 1 => MinusOp | 2 => MultOp | 3 => DivOp | 4 => ModOp
| 5 => LeOp | 6 => EqOp | 7 => AndOp | _ => OrOp
end) _); by intros [].
Qed.
Instance expr_countable : Countable expr.
......
......@@ -35,8 +35,8 @@ Notation Skip := (App (Val $ LamV BAnon (Val $ LitV LitUnit)) (Val $ LitV LitUni
properly. *)
Notation "# l" := (LitV l%Z%V%stdpp) (at level 8, format "# l").
(** Syntax inspired by Coq/Ocaml. Constructions with higher precedence come
first. *)
(** Syntax inspired by Coq/Ocaml. *)
Notation "( e1 , e2 , .. , en )" := (Pair .. (Pair e1 e2) .. en) : expr_scope.
Notation "( e1 , e2 , .. , en )" := (PairV .. (PairV e1 e2) .. en) : val_scope.
Notation "'let:' ( x , y1 , .. , yn ) := e1 'in' e2" :=
......@@ -118,6 +118,9 @@ Notation "¬ e" := (UnOp NotOp e%E)%E : expr_scope.
Notation "e1 + e2" := (BinOp PlusOp e1%E e2%E) : expr_scope.
Notation "e1 - e2" := (BinOp MinusOp e1%E e2%E) : expr_scope.
Notation "e1 * e2" := (BinOp MultOp e1%E e2%E) : expr_scope.
Notation "e1 / e2" := (BinOp DivOp e1%E e2%E) : expr_scope.
Notation "e1 `mod` e2" := (BinOp ModOp e1%E e2%E) : expr_scope.
Notation "e1 ≤ e2" := (BinOp LeOp e1%E e2%E) : expr_scope.
Notation "e1 = e2" := (BinOp EqOp e1%E e2%E) : expr_scope.
Notation "e1 ≠ e2" := (¬ (e1%E = e2%E))%E : expr_scope.
......
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