Qcert.Translation.NNRCtoNNRCMR

Section NNRCtoNNRCMR.

  Context {fruntime:foreign_runtime}.
  Context {fredop:foreign_reduce_op}.
  Context {ftoredop:foreign_to_reduce_op}.

  Definition fresh_mr_var (prefix: string) (loc: dlocalization) (vars_loc: list (var × dlocalization)) :=
    let x := fresh_var prefix (domain vars_loc) in
    (x , (x , loc )::vars_loc ).

load_env unit_var vars env takes the environment env used to evaluate an NNRC expression and return the environment to use to execute the translation of this expression as a map-reduce chain. vars is the list of variables that have to be stored in the map-reduce with their dlocalization kind.

This function also add to the map-reduce environment and entry init that contains the unit value.

  Definition load_init_env' (initunit: var) (vars_loc: list (var × dlocalization)) (env: bindings) : option nrcmr_env :=
    let mr_env :=
        List.fold_left
          (fun acc (x_loc: var × dlocalization) ⇒
             let (x, loc) := x_loc in
             match lookup equiv_dec env x with
             | Some d ⇒
               match loc with
               | Vlocal ⇒ lift (fun env' ⇒ (x , Dlocal d) :: env') acc
               | Vdistr ⇒
                 match d with
                 | dcoll coll ⇒ lift (fun env' ⇒ (x , Ddistr coll) :: env') acc
                 | _ ⇒ None
                 end
               end
             | None ⇒ None
             end)
          vars_loc
          (Some nil)
    in
    match mr_env with
    | Some env ⇒ Some ((initunit , Dlocal dunit ) :: env)
    | None ⇒ None
    end.

  Definition load_init_env (initunit: var) (vars_loc: list (var × dlocalization)) (env: list (string ×data)) : option (list (string ×ddata)) :=
    let add_initunit (initunit:var) (env:list (string ×ddata)) :=
        (initunit , Dlocal dunit ) :: env
    in
    let mr_env := mkDistConstants vars_loc env in
    lift (add_initunit initunit) mr_env.

  Definition load_init_env_success initunit vars_loc nnrc_env mr_env :=
    load_init_env initunit vars_loc nnrc_env = Some mr_env ∧
    (∀ x,
       lookup equiv_dec vars_loc x = Some Vlocal →
       lift Dlocal (lookup equiv_dec nnrc_env x) = lookup equiv_dec mr_env x ) ∧
    (∀ x,
       lookup equiv_dec vars_loc x = Some Vdistr →
       ∃ coll,
         lookup equiv_dec nnrc_env x = Some (dcoll coll) ∧
         lookup equiv_dec mr_env x = Some (Ddistr coll)).

  Lemma load_env_lookup_initunit initunit vars_loc nnrc_env mr_env:
    load_init_env_success initunit vars_loc nnrc_env mr_env →
    lookup equiv_dec mr_env initunit = Some (Dlocal dunit).

  Definition mr_chain_of_nnrc_with_no_free_var (n: nnrc) (initunit: var) (output: var) :=
    let coll_n :=
        let var := "x"%string in
        (var , NNRCUnop AColl n )
    in
    let mr :=
        mkMR
          initunit
          output
          (MapScalar coll_n)
          RedSingleton
    in
    (mr ::nil).

  Definition nnrcmr_of_nnrc_with_no_free_var (n: nnrc) (free_vars_loc: vdbindings) (initunit: var) (output: var) :=
    mkMRChain
      free_vars_loc
      (mr_chain_of_nnrc_with_no_free_var n initunit output)
      ((output ::nil , (NNRCVar output )), (output , Vlocal )::nil ).

  Lemma nnrcmr_of_nnrc_with_no_free_var_wf (n: nnrc) (free_vars_loc: vdbindings) (initunit: var) (output: var):
    nnrc_free_vars n = nil →
    nnrcmr_well_formed (nnrcmr_of_nnrc_with_no_free_var n free_vars_loc initunit output).

  Lemma nnrcmr_of_nnrc_with_no_free_var_correct h mr_env n:
    ∀ free_vars_loc initunit output,
    ∀ (Hfv: nnrc_free_vars n = nil),
    ∀ (Hinitunit: lookup equiv_dec mr_env initunit = Some (Dlocal dunit)),
    ∀ (Houtput: lookup equiv_dec mr_env output = None),
      nnrc_core_eval h nil n =
      nnrcmr_eval h mr_env (nnrcmr_of_nnrc_with_no_free_var n free_vars_loc initunit output).

  Definition mr_chain_of_nnrc_with_one_free_var (n: nnrc) (x_loc: var × dlocalization) (output:var) :=
    match x_loc with
    | (x, Vlocal ) ⇒
      let mr :=
          mkMR
            x
            output
            (MapScalar (x, NNRCUnop AColl n ))
            RedSingleton
      in
      (mr ::nil)
    | (x, Vdistr ) ⇒
      let values := x in
      let mr :=
          mkMR
            x
            output
            (MapDist id_function)
            (RedCollect (values , n ))
      in
      (mr ::nil)
    end.

  Definition nnrcmr_of_nnrc_with_one_free_var (n: nnrc) (x_loc: var × dlocalization) (free_vars_loc: vdbindings) (output:var) :=
    mkMRChain
      free_vars_loc
      (mr_chain_of_nnrc_with_one_free_var n x_loc output)
      ((output ::nil , (NNRCVar output )), (output , Vlocal )::nil ).

  Lemma nnrcmr_of_nnrc_with_one_free_var_wf (free_vars_loc: vdbindings) (n: nnrc) (x_loc: var × dlocalization) (output:var):
    function_with_no_free_vars (fst x_loc , n ) →
    nnrcmr_well_formed (nnrcmr_of_nnrc_with_one_free_var n x_loc free_vars_loc output).

  Lemma nnrcmr_of_nnrc_with_one_free_var_correct h nnrc_env mr_env n x_loc:
    ∀ free_vars_loc output initunit,
    ∀ (Hnnrc_env: ∃ d, lookup equiv_dec nnrc_env (fst x_loc) = Some d),
    ∀ (Hmr_env: load_init_env_success initunit (x_loc ::nil) nnrc_env mr_env),
    ∀ (Hfv: function_with_no_free_vars (fst x_loc , n )),
    ∀ (Houtput: lookup equiv_dec mr_env output = None),
      nnrc_core_eval h nnrc_env n =
      nnrcmr_eval h mr_env (nnrcmr_of_nnrc_with_one_free_var n x_loc free_vars_loc output).

  Definition brand_of_var (x: var) := String.append "__Env."%string (x).

Packing the value of a free variable fv in a closure environment named closure_env_name is done by a map-reduce job (without reduce) that looks like: (fun d => Brand "fv" d)

  Definition pack_closure_env (free_vars_loc: list (var × dlocalization)) (closure_env_name: var) : list mr :=
    List.map
      (fun (fv_loc: var × dlocalization) ⇒
         let (fv, loc) := fv_loc in
         let mr_reduce_brand :=
             RedId
         in
         match loc with
         | Vlocal ⇒
           let mr_map_brand :=
               let d:var := "x"%string in
               (d , NNRCUnop AColl
                           (NNRCUnop (ABrand (singleton (brand_of_var fv))) (NNRCVar d)))
           in
           mkMR
             fv
             closure_env_name
             (MapScalar mr_map_brand)
             mr_reduce_brand
         | Vdistr ⇒
           let mr_map_brand :=
               let d:var := "x"%string in
               (d , NNRCUnop (ABrand (singleton (brand_of_var fv))) (NNRCVar d))
           in
           mkMR
             fv
             closure_env_name
             (MapDist mr_map_brand)
             mr_reduce_brand
         end)
      free_vars_loc.

Unpacking a distributed free variable fv coming from closure_env_name with the continuation k correspond to the following NNRC code: let fv = flatten { match ("fv") d with | Some d => { Unbrand d } | None => {} end | d in closure_env_name } in k

Unpacking a scalar free variable fv coming from closure_env_name with the continuation k correspond to the following NNRC code: let fv = match singleton { match ("fv") d with | Some d => { Unbrand d } | None => {} end | d in closure_env_name } with | Some fv => fv | None => assert false in k

  Definition unpack_closure_env (closure_env_name: var) (free_vars_loc: list (var × dlocalization)) (k: nnrc) : nnrc :=
    List.fold_right
      (fun fv_loc k ⇒
         match fv_loc with
         | (fv, Vdistr ) ⇒
           let d : var := fresh_var "unpackdistributed$" (closure_env_name :: nil) in
           NNRCLet fv
                  (NNRCUnop AFlatten
                           (NNRCFor d (NNRCVar closure_env_name)
                                   (NNRCEither (NNRCUnop (ACast (singleton (brand_of_var fv))) (NNRCVar d))
                                              d (NNRCUnop AColl (NNRCUnop AUnbrand (NNRCVar d)))
                                              d (NNRCConst (dcoll nil)))))
                  k
         | (fv, Vlocal ) ⇒
           let d : var := fresh_var "unpackscalar$" (closure_env_name :: nil) in
           NNRCLet fv
                  (NNRCEither (NNRCUnop ASingleton
                                      (NNRCUnop AFlatten
                                               (NNRCFor d (NNRCVar closure_env_name)
                                                       (NNRCEither (NNRCUnop (ACast (singleton (brand_of_var fv))) (NNRCVar d))
                                                                  d (NNRCUnop AColl (NNRCUnop AUnbrand (NNRCVar d)))
                                                                  d (NNRCConst (dcoll nil))))))
                             fv (NNRCVar fv)
                             fv (NNRCConst dunit))
                  k
         end)
      k free_vars_loc.

Convert an NNRC expression n into a Map-Reduce fetching the values of the free variables from the environment. The list vars_loc give the dlocalization of each free variable of n. This list must contain all the variables that are in the map-reduce environment (it may contain variables that are not free in n).

  Definition mr_chain_of_nnrc_with_free_vars (n: nnrc) (vars_loc: list (var × dlocalization)) (output: var): list mr :=
    let free_vars := bdistinct (nnrc_free_vars n) in
    match
      List.fold_right
        (fun x oacc ⇒
           olift
             (fun loc ⇒ lift (fun acc ⇒ (x , loc )::acc) oacc)
             (lookup equiv_dec vars_loc x))
        (Some nil) free_vars
    with
    | Some free_vars_loc ⇒
      let (closure_env_name, vars_loc) := fresh_mr_var "closure$" Vdistr vars_loc in
      let pack_closure_env := pack_closure_env free_vars_loc closure_env_name in
      let final_reduce :=
          (closure_env_name , unpack_closure_env closure_env_name free_vars_loc n )
      in
      let final_mr :=
          mkMR
            closure_env_name
            output
            (MapDist id_function)
            (RedCollect final_reduce)
      in
      pack_closure_env ++ (final_mr ::nil )
    | None ⇒ nil
    end.

  Definition nnrcmr_of_nnrc_with_free_vars (n: nnrc) (vars_loc: list (var × dlocalization)) (output: var): nnrcmr :=
    mkMRChain
      vars_loc
      (mr_chain_of_nnrc_with_free_vars n vars_loc output)
      ((output ::nil , (NNRCVar output )), (output , Vlocal )::nil ).

  Lemma pack_closure_env_wf (free_vars_loc: list (var × dlocalization)) (closure_env_name: var):
    mr_chain_well_formed (pack_closure_env free_vars_loc closure_env_name).

  Lemma unpack_closure_env_free_vars (closure_env_name: var) (free_vars_loc: list (var × dlocalization)) (k: nnrc) :
    ∀ x,
      let free_vars := List.map fst free_vars_loc in
      In x (nnrc_free_vars (unpack_closure_env closure_env_name free_vars_loc k)) →
      In x (closure_env_name :: (bminus free_vars (bdistinct (nnrc_free_vars k)))).

  Lemma nnrcmr_of_nnrc_with_free_vars_wf (n: nnrc) (vars_loc: list (var × dlocalization)) (output: var):
    (∀ x, In x (nnrc_free_vars n) → In x (List.map fst vars_loc)) →
    nnrcmr_well_formed (nnrcmr_of_nnrc_with_free_vars n vars_loc output).

  Lemma nnrcmr_of_nnrc_with_free_vars_correct h nnrc_env mr_env n initunit vars_loc output:
    load_init_env_success initunit vars_loc nnrc_env mr_env →
    (∀ x, In x (domain nnrc_env) → In x (domain vars_loc)) →
    (∀ x, In x (nnrc_free_vars n) → ∃ d, lookup equiv_dec mr_env x = Some d ) →
    lookup equiv_dec mr_env output = None →
    nnrc_core_eval h nnrc_env n =
    nnrcmr_eval h mr_env (nnrcmr_of_nnrc_with_free_vars n vars_loc output).

  Definition get_mr_chain_vars nrm :=
    let vars_loc :=
        List.fold_left
          (fun acc mr ⇒
             let vinput := mr_input_localized mr in
             let voutput := mr_output_localized mr in
             vinput :: voutput :: acc)
          nrm nil
    in
    vars_loc.

Convert any NNRC expression n into a Map-Reduce fetching the values of the free variables from the environment.

The variable initunit represent a variable in the environment that contains unit.

The variable output indicates the place in the environment where the result of the evaluation must be stored. The result is a scalar.

The list vars_loc is used to represent the variables that are bind in the environment (that may not appear free in n).

The function returns the generated map-reduce and the updated version of the vars_loc list with the variables introduced by the translation.

  Definition mr_chain_of_nnrc (n: nnrc) (initunit: var) (vars_loc: list (var × dlocalization)) (output: var): list mr × list (var × dlocalization) :=
    let mr_chain :=
        match bdistinct (nnrc_free_vars n) with
        | nil ⇒
          mr_chain_of_nnrc_with_no_free_var n initunit output
        | x :: nil ⇒
          match lookup equiv_dec vars_loc x with
          | Some loc ⇒ mr_chain_of_nnrc_with_one_free_var n (x, loc) output
          | None ⇒ nil
          end
        | free_vars ⇒
          mr_chain_of_nnrc_with_free_vars n vars_loc output
        end
    in
    let nnrcmr_vars := get_mr_chain_vars mr_chain in
    (mr_chain , nnrcmr_vars ++ vars_loc ).

  Definition nnrcmr_of_nnrc (n: nnrc) (initunit: var) (inputs_loc: list (var × dlocalization)) (output: var): nnrcmr × list (var × dlocalization) :=
    let (mr_chain, vars_loc) := mr_chain_of_nnrc n initunit inputs_loc output in
    (mkMRChain
       inputs_loc
       mr_chain
       ((output ::nil , (NNRCVar output )), (output , Vlocal )::nil ),
     vars_loc ).

  Lemma nnrcmr_of_nnrc_wf (n: nnrc) (initunit: var) (vars_loc: list (var × dlocalization)) (output: var):
    nnrcmr_well_formed (fst (nnrcmr_of_nnrc n initunit vars_loc output)).

  Definition mr_chain_distributed_of_nnrc (n: nnrc) (initunit: var) (vars_loc: list (var × dlocalization)) (output: var): list mr × list (var × dlocalization) :=
    let (tmp, vars_loc) := fresh_mr_var "scalarcoll$"%string Vdistr vars_loc in
    let (mr_chain, vars_loc) := mr_chain_of_nnrc n initunit vars_loc tmp in
    (mr_chain ++ ((mr_scalar_to_distributed tmp output )::nil ), vars_loc ).

  Definition mk_loop (x: var) (n1: nnrc) (n2: nnrc) (mr_list1: list mr) (initunit: var) (vars_loc: list (var × dlocalization)) : nnrc × list mr × list (var × dlocalization) :=
    let (n1_distributed_result_var, vars_loc) := fresh_mr_var "distcoll$"%string Vdistr vars_loc in
    let (n_result_var, vars_loc) := fresh_mr_var "loop_result$"%string Vlocal vars_loc in
    let (mr_n1, vars_loc) := mr_chain_distributed_of_nnrc n1 initunit vars_loc n1_distributed_result_var in
    let mr_n2 :=
        mkMR
          n1_distributed_result_var
          n_result_var
          (MapDist (x , n2 ))
          (RedCollect id_function)
    in
    let mr_list : list mr :=
        mr_list1 ++ mr_n1 ++ (mr_n2 :: nil )
    in
    (NNRCVar n_result_var , mr_list , vars_loc ).

  Definition try_mk_loop (x: var) (n1: nnrc) (n2: nnrc) (mr_list1: list mr) (initunit: var) (vars_loc: list (var × dlocalization)) : option (nnrc × list mr × list (var × dlocalization)) :=
    match bdistinct (nnrc_free_vars n2) with
    | nil ⇒
      Some (mk_loop x n1 n2 mr_list1 initunit vars_loc)
    | x' :: nil ⇒
      if equiv_dec x x' then
        Some (mk_loop x n1 n2 mr_list1 initunit vars_loc)
      else
        None
    | _ ⇒ None
    end.

Auxiliary function for the translation from an NNRC expression into a chain of map-reduce. It take as argument:

n the expresion to translate
init a variable of the environment that contains a non-empty collection to trigger the computations of expressions without free variables.
avoid a list of names to avoid to generate fresh names.

It returns:

a NNRC expression equivalent to the input n but in which some map-reduces have been extracted
the map-reduce elements extracted from n in the order with respect to the scheduling
the updated avoid list.

  Program Fixpoint nnrc_to_nnrcmr_chain_ns_aux (n: nnrc) (initunit: var) (vars_loc: list (var × dlocalization)) { measure (nnrc_size n) }: nnrc × list mr × list (var × dlocalization) :=
    match n with
    | NNRCFor x n1 n2 ⇒
      let '(n1', mr_list1, vars_loc) := nnrc_to_nnrcmr_chain_ns_aux n1 initunit vars_loc in
      match try_mk_loop x n1' n2 mr_list1 initunit vars_loc with
      | Some (n', mr_list, vars_loc) ⇒ (n', mr_list, vars_loc)
      | None ⇒
        (NNRCFor x n1' n2, mr_list1, vars_loc)
      end
    | NNRCVar x ⇒
      (n, nil , vars_loc)
    | NNRCConst d ⇒
      (n, nil , vars_loc)
    | NNRCUnop op n1 ⇒
      let '(n1', mr_list1, vars_loc) := nnrc_to_nnrcmr_chain_ns_aux n1 initunit vars_loc in
      match foreign_to_reduce_op_of_unary_op op with
      | Some red_op ⇒
        let (n1_distributed_result_var, vars_loc) := fresh_mr_var "distcoll$"%string Vdistr vars_loc in
        let (mr_n1, vars_loc) := mr_chain_distributed_of_nnrc n1' initunit vars_loc n1_distributed_result_var in
        let (result_var, vars_loc) := fresh_mr_var "res$"%string Vlocal vars_loc in
        let mr :=
            mkMR
              n1_distributed_result_var
              result_var
              (MapDist id_function)
              (RedOp red_op)
        in
        (NNRCVar result_var , mr_list1 ++ mr_n1 ++ (mr :: nil ), vars_loc )
      | None ⇒
        match op with
        | AFlatten ⇒
          let (n1_distributed_result_var, vars_loc) := fresh_mr_var "distcoll$"%string Vdistr vars_loc in
          let (mr_n1, vars_loc) := mr_chain_distributed_of_nnrc n1' initunit vars_loc n1_distributed_result_var in
          let (flatten_result_var, vars_loc) := fresh_mr_var "flat$"%string Vdistr vars_loc in
          let mr_flatten :=
              mkMR
                n1_distributed_result_var
                flatten_result_var
                (MapDistFlatten id_function)
                RedId
          in
          (NNRCVar flatten_result_var , mr_list1 ++ mr_n1 ++ (mr_flatten :: nil ), vars_loc )
        | _ ⇒ (NNRCUnop op n1', mr_list1, vars_loc)
        end
      end
    | NNRCBinop op n1 n2 ⇒
      let '(n1', mr_list1, vars_loc) := nnrc_to_nnrcmr_chain_ns_aux n1 initunit vars_loc in
      let '(n2', mr_list2, vars_loc) := nnrc_to_nnrcmr_chain_ns_aux n2 initunit vars_loc in
      (NNRCBinop op n1' n2', mr_list1 ++ mr_list2, vars_loc)
    | NNRCLet x n1 n2 ⇒
      let '(n1', mr_list1, vars_loc) := nnrc_to_nnrcmr_chain_ns_aux n1 initunit vars_loc in
      let x_fresh := nnrc_pick_name "$" id (domain vars_loc) x n2 in
      let n2 := nnrc_rename_lazy n2 x x_fresh in
      let (mr_n1, vars_loc) := mr_chain_of_nnrc n1' initunit vars_loc x_fresh in
      let '(n2', mr_list2, vars_loc) := nnrc_to_nnrcmr_chain_ns_aux n2 initunit vars_loc in
      (n2', mr_list1 ++ mr_n1 ++ mr_list2, vars_loc )
    | NNRCIf n0 n1 n2 ⇒
      let '(n0', mr_list, vars_loc) := nnrc_to_nnrcmr_chain_ns_aux n0 initunit vars_loc in
      let '(n1', mr_list1, vars_loc) := nnrc_to_nnrcmr_chain_ns_aux n1 initunit vars_loc in
      let '(n2', mr_list2, vars_loc) := nnrc_to_nnrcmr_chain_ns_aux n2 initunit vars_loc in
      (NNRCIf n0' n1' n2', nil , vars_loc)
    | NNRCEither n0 x n1 y n2 ⇒
      (n, nil , vars_loc)
    | NNRCGroupBy g sl n1 ⇒
      (n, nil , vars_loc)
    end.

  Lemma nnrc_to_nnrcmr_chain_aux_causally_consistent (n: nnrc) (initunit: var) (vars_loc: list (var × dlocalization)) :
    shadow_free n = true →
    let '(_, mr_chain, _) := nnrc_to_nnrcmr_chain_ns_aux n initunit vars_loc in
    mr_chain_causally_consistent mr_chain = true.

  Definition nnrc_to_mr_chain_ns (n: nnrc) (initunit: var) (vars_loc: list (var × dlocalization)) (output: var) : list mr :=
    let '(n', mr_list, vars_loc) := nnrc_to_nnrcmr_chain_ns_aux n initunit vars_loc in
    let (final_mr, _) := mr_chain_of_nnrc n' initunit vars_loc output in
    mr_list ++ final_mr.

  Definition nnrc_to_nnrcmr_chain_ns (n: nnrc) (initunit: var) (inputs_loc: vdbindings) (vars_loc: vdbindings) : nnrcmr :=
    let output := fresh_var "output" (domain vars_loc) in
    mkMRChain
      inputs_loc
      (nnrc_to_mr_chain_ns n initunit vars_loc output)
      ((output ::nil , (NNRCVar output )), (output , Vlocal )::nil ).

  Definition nnrc_to_nnrcmr_chain (initunit: var) (inputs_loc: vdbindings) (n: nnrc) : nnrcmr :=
    let n_ns := n in
    let vars_loc := inputs_loc ++ List.map (fun x ⇒ (x , Vlocal )) (nnrc_bound_vars n_ns) in
    nnrc_to_nnrcmr_chain_ns n_ns initunit inputs_loc vars_loc.

  Definition nnrc_to_nnrcmr_no_chain (n: nnrc) (inputs_loc: list (var × dlocalization)) : nnrcmr :=
    mkMRChain
      inputs_loc
      nil
      ((List.map fst inputs_loc , n ), inputs_loc ).

  Lemma load_init_env_build_nnrc_env_id env initunit mr_env vars_loc :
    load_init_env initunit vars_loc env = Some mr_env →
    build_nnrc_env mr_env (map fst vars_loc) vars_loc = Some ((initunit , dunit ) :: env).

  Theorem nnrc_to_nnrcmr_no_chain_correct h env initunit mr_env (n:nnrc) (inputs_loc: list (var × dlocalization)) :
      load_init_env initunit inputs_loc env = Some mr_env →
      nnrc_core_eval h env n = nnrcmr_eval h mr_env (nnrc_to_nnrcmr_no_chain n inputs_loc).

End NNRCtoNNRCMR.