From 5aa6d99982a9d6e2736f1eedb7fcdf6b9d05b6a0 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Mon, 24 Aug 2020 15:11:16 +0200 Subject: Modify bytecode representation of closures to please OCaml's GC (fix #12636). The second field of a closure can no longer be the value of the first free variable (or another closure of a mutually recursive block) but must be an offset to the first free variable. This commit makes the bytecode compiler and interpreter agnostic to the actual representation of closures. To do so, the execution environment (variable coq_env) no longer points to the currently executed closure but to the last one. This has the following consequences: - OFFSETCLOSURE(n) now always loads the n-th closure of a recursive block (counted from last to first); - ENVACC(n) now always loads the value of the n-th free variable. These two changes make the bytecode compiler simpler, since it no longer has to track the relative position of closures and free variables. The last change makes the interpreter a bit slower, since it has to adjust coq_env when executing GRABREC. Hopefully, cache locality will make the overhead negligible. --- kernel/vmvalues.ml | 57 +++++++++++++++++++++++++----------------------------- 1 file changed, 26 insertions(+), 31 deletions(-) (limited to 'kernel/vmvalues.ml') diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml index de604176cb..177f67210c 100644 --- a/kernel/vmvalues.ml +++ b/kernel/vmvalues.ml @@ -166,7 +166,6 @@ let cofix_upd_val v = (Obj.magic v : values) type vm_env type vm_global let fun_env v = (Obj.magic v : vm_env) -let fix_env v = (Obj.magic v : vm_env) let cofix_env v = (Obj.magic v : vm_env) let cofix_upd_env v = (Obj.magic v : vm_env) type vstack = values array @@ -207,13 +206,13 @@ type vswitch = { (* dom : values, codom : vfun *) (* *) (* + Functions have two representations : *) -(* - unapplied fun : vf = Ct_[ C | fv1 | ... | fvn] *) +(* - unapplied fun : vf = Ct_[ C | envofs=2 | fv1 | ... | fvn] *) (* C:tcode, fvi : values *) (* Remark : a function and its environment is the same value. *) -(* - partially applied fun : Ct_[Restart:C| vf | arg1 | ... argn] *) +(* - partially applied fun : Ct_[ Restart::C | envofs=2 | vf | arg1 | ... | argn] *) (* *) (* + Fixpoints : *) -(* - Ct_[C1|Infix_t|C2|...|Infix_t|Cn|fv1|...|fvn] *) +(* - Ct_[C1|envofs1=3*n-1 | Infix_t|C2|envofs2 | ... | Infix_t|Cn|envofsn=2 | fv1|...|fvn] *) (* One single block to represent all of the fixpoints, each fixpoint *) (* is the pointer to the field holding the pointer to its code, and *) (* the infix tag is used to know where the block starts. *) @@ -291,10 +290,10 @@ type whd = | Vuniv_level of Univ.Level.t (* Functions over arguments *) -let nargs : arguments -> int = fun args -> (Obj.size (Obj.repr args)) - 2 +let nargs : arguments -> int = fun args -> Obj.size (Obj.repr args) - 3 let arg args i = if 0 <= i && i < (nargs args) then - val_of_obj (Obj.field (Obj.repr args) (i+2)) + val_of_obj (Obj.field (Obj.repr args) (i + 3)) else invalid_arg ("Vm.arg size = "^(string_of_int (nargs args))^ " acces "^(string_of_int i)) @@ -356,7 +355,7 @@ let rec whd_accu a stk = | i when Int.equal i fix_app_tag -> let fa = Obj.field at 1 in let zfix = - Zfix (Obj.obj (Obj.field fa 1), Obj.obj fa) in + Zfix (Obj.obj (Obj.field fa 2), Obj.obj fa) in whd_accu (Obj.field at 0) (zfix :: stk) | i when Int.equal i switch_tag -> let zswitch = Zswitch (Obj.obj (Obj.field at 1)) in @@ -408,7 +407,7 @@ let whd_val : values -> whd = (match kind_of_closure o with | 0 -> Vfun(Obj.obj o) | 1 -> Vfix(Obj.obj o, None) - | 2 -> Vfix(Obj.obj (Obj.field o 1), Some (Obj.obj o)) + | 2 -> Vfix(Obj.obj (Obj.field o 2), Some (Obj.obj o)) | 3 -> Vatom_stk(Aid(RelKey(int_tcode (fun_code o) 1)), []) | _ -> CErrors.anomaly ~label:"Vm.whd " (Pp.str "kind_of_closure does not work.")) else if Int.equal tag Obj.custom_tag then Vint64 (Obj.magic v) @@ -516,29 +515,23 @@ external closure_arity : vfun -> int = "coq_closure_arity" (* Functions over fixpoint *) -external offset : Obj.t -> int = "coq_offset" -external offset_closure : Obj.t -> int -> Obj.t = "coq_offset_closure" -external offset_closure_fix : vfix -> int -> vm_env = "coq_offset_closure" +external current_fix : vfix -> int = "coq_current_fix" +external shift_fix : vfix -> int -> vfix = "coq_shift_fix" +external last_fix : vfix -> vfix = "coq_last_fix" external tcode_array : tcode_array -> tcode array = "coq_tcode_array" -let first o = (offset_closure o (offset o)) -let first_fix (v:vfix) = (Obj.magic (first (Obj.repr v)) : vfix) +let first_fix o = shift_fix o (- current_fix o) +let fix_env v = (Obj.magic (last_fix v) : vm_env) let last o = (Obj.field o (Obj.size o - 1)) let fix_types (v:vfix) = tcode_array (Obj.magic (last (Obj.repr v)) : tcode_array) let cofix_types (v:vcofix) = tcode_array (Obj.magic (last (Obj.repr v)) : tcode_array) -let current_fix vf = - (offset (Obj.repr vf) / 2) - -let unsafe_fb_code fb i = - let off = (2 * i) * (Sys.word_size / 8) in - Obj.obj (Obj.add_offset (Obj.repr fb) (Int32.of_int off)) - -let unsafe_rec_arg fb i = int_tcode (unsafe_fb_code fb i) 1 +let unsafe_rec_arg fb i = int_tcode (Obj.magic (shift_fix fb i)) 1 let rec_args vf = - let fb = first (Obj.repr vf) in - let size = Obj.size (last fb) in + let fb = first_fix vf in + let size = Obj.size (last (Obj.repr fb)) in Array.init size (unsafe_rec_arg fb) exception FALSE @@ -547,10 +540,10 @@ let check_fix f1 f2 = let i1, i2 = current_fix f1, current_fix f2 in (* Checking starting point *) if i1 = i2 then - let fb1,fb2 = first (Obj.repr f1), first (Obj.repr f2) in - let n = Obj.size (last fb1) in + let fb1,fb2 = first_fix f1, first_fix f2 in + let n = Obj.size (last (Obj.repr fb1)) in (* Checking number of definitions *) - if n = Obj.size (last fb2) then + if n = Obj.size (last (Obj.repr fb2)) then (* Checking recursive arguments *) try for i = 0 to n - 1 do @@ -593,21 +586,23 @@ let relaccu_code i = let mk_fix_body k ndef fb = let e = Obj.dup (Obj.repr fb) in + let env = Obj.repr (fix_env (Obj.obj e)) in for i = 0 to ndef - 1 do - set_bytecode_field e (2 * i) (relaccu_code (k + i)) + set_bytecode_field e (3 * i) (relaccu_code (k + i)) done; let fix_body i = - let c = offset_tcode (unsafe_fb_code fb i) 2 in - let res = Obj.new_block Obj.closure_tag 2 in + let c = offset_tcode (Obj.magic (shift_fix fb i)) 2 in + let res = Obj.new_block Obj.closure_tag 3 in set_bytecode_field res 0 c; - Obj.set_field res 1 (offset_closure e (2*i)); + Obj.set_field res 1 (Obj.repr 2); + Obj.set_field res 2 env; ((Obj.obj res) : vfun) in Array.init ndef fix_body (* Functions over vcofix *) let get_fcofix vcf i = - match whd_val (Obj.obj (Obj.field (Obj.repr vcf) (i+1))) with + match whd_val (Obj.obj (Obj.field (Obj.repr vcf) (i+2))) with | Vcofix(vcfi, _, _) -> vcfi | _ -> assert false @@ -628,7 +623,7 @@ let check_cofix vcf1 vcf2 = let mk_cofix_body apply_varray k ndef vcf = let e = Obj.dup (Obj.repr vcf) in for i = 0 to ndef - 1 do - Obj.set_field e (i+1) (Obj.repr (val_of_rel (k+i))) + Obj.set_field e (i+2) (Obj.repr (val_of_rel (k+i))) done; let cofix_body i = -- cgit v1.2.3 From 2d63a61a991ab42f2124775b184898d7af6725dd Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Wed, 26 Aug 2020 08:34:25 +0200 Subject: Use the same memory layout as closures for accumulators. That way, accumulators again can be used directly as execution environments by the bytecode interpreter. This fixes the issue of the first argument of accumulators being dropped when strongly normalizing. --- kernel/vmvalues.ml | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) (limited to 'kernel/vmvalues.ml') diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml index 177f67210c..98a1b13373 100644 --- a/kernel/vmvalues.ml +++ b/kernel/vmvalues.ml @@ -231,7 +231,7 @@ type vswitch = { (* + vm_env is the type of the machine environments (i.e. a function or *) (* a fixpoint) *) (* *) -(* + Accumulators : At_[accumulate| accu | arg1 | ... | argn ] *) +(* + Accumulators : At_[accumulate | envofs=2 | accu | arg1 | ... | argn ] *) (* - representation of [accu] : tag_[....] *) (* -- tag <= 3 : encoding atom type (sorts, free vars, etc.) *) (* -- 10_[accu|proj name] : a projection blocked by an accu *) @@ -328,9 +328,9 @@ let uni_lvl_val (v : values) : Univ.Level.t = let rec whd_accu a stk = let stk = - if Int.equal (Obj.size a) 2 then stk + if Int.equal (Obj.size a) 3 then stk else Zapp (Obj.obj a) :: stk in - let at = Obj.field a 1 in + let at = Obj.field a 2 in match Obj.tag at with | i when Int.equal i type_atom_tag -> begin match stk with @@ -421,9 +421,10 @@ let whd_val : values -> whd = let obj_of_atom : atom -> Obj.t = fun a -> - let res = Obj.new_block accu_tag 2 in + let res = Obj.new_block accu_tag 3 in set_bytecode_field res 0 accumulate; - Obj.set_field res 1 (Obj.repr a); + Obj.set_field res 1 (Obj.repr 2); + Obj.set_field res 2 (Obj.repr a); res (* obj_of_str_const : structured_constant -> Obj.t *) @@ -631,9 +632,10 @@ let mk_cofix_body apply_varray k ndef vcf = let c = Obj.field (Obj.repr vcfi) 0 in Obj.set_field e 0 c; let atom = Obj.new_block cofix_tag 1 in - let self = Obj.new_block accu_tag 2 in + let self = Obj.new_block accu_tag 3 in set_bytecode_field self 0 accumulate; - Obj.set_field self 1 (Obj.repr atom); + Obj.set_field self 1 (Obj.repr 2); + Obj.set_field self 2 (Obj.repr atom); apply_varray (Obj.obj e) [|Obj.obj self|] in Array.init ndef cofix_body -- cgit v1.2.3 From 27695b52413f9fd6bcb60d77e0bdba538c16201f Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Wed, 26 Aug 2020 11:40:24 +0200 Subject: Use the closure tag for accumulators. The first field of accumulators points out of the OCaml heap, so using closures instead of tag-0 objects is better for the GC. Accumulators are distinguished from closures because their code pointer necessarily is the "accumulate" address, which points to an ACCUMULATE instruction. --- kernel/vmvalues.ml | 55 ++++++++++++++++++++++++------------------------------ 1 file changed, 24 insertions(+), 31 deletions(-) (limited to 'kernel/vmvalues.ml') diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml index 98a1b13373..0678f37a0b 100644 --- a/kernel/vmvalues.ml +++ b/kernel/vmvalues.ml @@ -34,8 +34,6 @@ let crazy_val = (val_of_obj (Obj.repr 0)) type tag = int -let accu_tag = 0 - let type_atom_tag = 2 let max_atom_tag = 2 let proj_tag = 3 @@ -225,8 +223,7 @@ type vswitch = { (* + Cofixpoints : see cbytegen.ml *) (* *) (* + vblock's encode (non constant) constructors as in Ocaml, but *) -(* starting from 0 up. tag 0 ( = accu_tag) is reserved for *) -(* accumulators. *) +(* starting from 0 up. *) (* *) (* + vm_env is the type of the machine environments (i.e. a function or *) (* a fixpoint) *) @@ -391,29 +388,28 @@ external accumulate : unit -> tcode = "accumulate_code" external set_bytecode_field : Obj.t -> int -> tcode -> unit = "coq_set_bytecode_field" let accumulate = accumulate () -let whd_val : values -> whd = - fun v -> - let o = Obj.repr v in - if Obj.is_int o then Vconstr_const (Obj.obj o) +let whd_val (v: values) = + let o = Obj.repr v in + if Obj.is_int o then Vconstr_const (Obj.obj o) + else + let tag = Obj.tag o in + if Int.equal tag 0 then + if Int.equal (Obj.size o) 1 then + Varray (Obj.obj o) + else Vprod (Obj.obj o) + else if Int.equal tag Obj.closure_tag && is_accumulate (fun_code o) then + whd_accu o [] + else if Int.equal tag Obj.closure_tag || Int.equal tag Obj.infix_tag then + (match kind_of_closure o with + | 0 -> Vfun(Obj.obj o) + | 1 -> Vfix(Obj.obj o, None) + | 2 -> Vfix(Obj.obj (Obj.field o 2), Some (Obj.obj o)) + | 3 -> Vatom_stk(Aid(RelKey(int_tcode (fun_code o) 1)), []) + | _ -> CErrors.anomaly ~label:"Vm.whd " (Pp.str "kind_of_closure does not work.")) + else if Int.equal tag Obj.custom_tag then Vint64 (Obj.magic v) + else if Int.equal tag Obj.double_tag then Vfloat64 (Obj.magic v) else - let tag = Obj.tag o in - if tag = accu_tag then - if Int.equal (Obj.size o) 1 then - Varray(Obj.obj o) - else if is_accumulate (fun_code o) then whd_accu o [] - else Vprod(Obj.obj o) - else - if tag = Obj.closure_tag || tag = Obj.infix_tag then - (match kind_of_closure o with - | 0 -> Vfun(Obj.obj o) - | 1 -> Vfix(Obj.obj o, None) - | 2 -> Vfix(Obj.obj (Obj.field o 2), Some (Obj.obj o)) - | 3 -> Vatom_stk(Aid(RelKey(int_tcode (fun_code o) 1)), []) - | _ -> CErrors.anomaly ~label:"Vm.whd " (Pp.str "kind_of_closure does not work.")) - else if Int.equal tag Obj.custom_tag then Vint64 (Obj.magic v) - else if Int.equal tag Obj.double_tag then Vfloat64 (Obj.magic v) - else - Vconstr_block(Obj.obj o) + Vconstr_block (Obj.obj o) (**********************************************) (* Constructors *******************************) @@ -421,7 +417,7 @@ let whd_val : values -> whd = let obj_of_atom : atom -> Obj.t = fun a -> - let res = Obj.new_block accu_tag 3 in + let res = Obj.new_block Obj.closure_tag 3 in set_bytecode_field res 0 accumulate; Obj.set_field res 1 (Obj.repr 2); Obj.set_field res 2 (Obj.repr a); @@ -632,10 +628,7 @@ let mk_cofix_body apply_varray k ndef vcf = let c = Obj.field (Obj.repr vcfi) 0 in Obj.set_field e 0 c; let atom = Obj.new_block cofix_tag 1 in - let self = Obj.new_block accu_tag 3 in - set_bytecode_field self 0 accumulate; - Obj.set_field self 1 (Obj.repr 2); - Obj.set_field self 2 (Obj.repr atom); + let self = obj_of_atom (Obj.obj atom) in apply_varray (Obj.obj e) [|Obj.obj self|] in Array.init ndef cofix_body -- cgit v1.2.3