Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Do not rely on accumulators having tag 0 in native compilation. #14048

Closed
wants to merge 1 commit into from
Closed

Do not rely on accumulators having tag 0 in native compilation. #14048

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
23 changes: 23 additions & 0 deletions kernel/byterun/coq_values.c
View file
Open in desktop
Expand Up @@ -96,3 +96,26 @@ value coq_tcode_array(value tcodes) {
}
CAMLreturn(res);
}

/* Low-level representation of accumulators for native compilation */

static code_t coq_accumulator_code;
static int coq_accumulator_init = 0;

value coq_native_register_accu(value v) {
if (coq_accumulator_init == 0) {
coq_accumulator_init = 1;
coq_accumulator_code = Code_val(v);
}
return Val_unit;
}

value coq_native_is_clos(value v) {
if (Is_block(v) && Tag_val(v) == Closure_tag) return Val_true;
return Val_false;
}

value coq_native_is_accu(value v) {
if (Is_block(v) && Tag_val(v) == Closure_tag && Code_val(v) == coq_accumulator_code) return Val_true;
return Val_false;
}
20 changes: 14 additions & 6 deletions kernel/nativecode.ml
View file
Open in desktop
Expand Up @@ -1668,13 +1668,22 @@ let pp_mllam fmt l =
| MLif(t,l1,l2) ->
Format.fprintf fmt "@[(if %a then@\n %a@\nelse@\n %a)@]"
pp_mllam t pp_mllam l1 pp_mllam l2
| MLmatch (_annot, c, accu_br, [||]) ->
(* special case for empty types *)
Format.fprintf fmt
"@[begin match Obj.magic (%a) with@\n| _ ->@\n %a@\nend@]"
pp_mllam c pp_mllam accu_br
| MLmatch (annot, c, accu_br, br) ->
let ind = annot.asw_ind in
let prefix = annot.asw_prefix in
let accu = string_of_accu_construct prefix ind in
let na = fresh_lname Anonymous in
Format.fprintf fmt
"@[begin match Obj.magic (%a) with@\n| %s _ ->@\n %a@\n%aend@]"
pp_mllam c accu pp_mllam accu_br (pp_branches prefix ind) br
"@[begin match Obj.magic (%a) with@\n\
| %a when Nativevalues.is_closure (%a) ->@\n %a@\n\
| %s _ -> assert false@\n\
%aend@]"
pp_mllam c pp_lname na pp_lname na pp_mllam accu_br accu (pp_branches prefix ind) br

| MLconstruct(prefix,ind,tag,args) ->
Format.fprintf fmt "@[(Obj.magic (%s%a) : Nativevalues.t)@]"
Expand All @@ -1696,11 +1705,10 @@ let pp_mllam fmt l =
pp_mllam fmt arr.(len-1)
end;
Format.fprintf fmt "|]@]"
| MLisaccu (prefix, ind, c) ->
let accu = string_of_accu_construct prefix ind in
| MLisaccu (_prefix, _ind, c) ->
(* Only applied to inductive accumulators, it cannot be confused with an arbitrary closure *)
Format.fprintf fmt
"@[begin match Obj.magic (%a) with@\n| %s _ ->@\n true@\n| _ ->@\n false@\nend@]"
pp_mllam c accu
"@[(Nativevalues.is_closure (%a))@]" pp_mllam c

and pp_letrec fmt defs =
let len = Array.length defs in
Expand Down
43 changes: 24 additions & 19 deletions kernel/nativevalues.ml
View file
Open in desktop
Expand Up @@ -82,29 +82,33 @@ type symbols = symbol array

let empty_symbols = [| |]


let accumulate_tag = 0

(** Unique pointer used to drive the accumulator function *)
let ret_accu = Obj.repr (ref ())

type accu_val = { mutable acc_atm : atom; acc_arg : Obj.t list }

external register_accu : t -> unit = "coq_native_register_accu" [@@noalloc]
external is_accu : t -> bool = "coq_native_is_accu" [@@noalloc]
external is_closure : 'a -> bool = "coq_native_is_clos" [@@noalloc]

(** TODO: do this more efficiently in C? *)
(* Dummy wrapper to ensure the closure is not inlined by the compiler *)
Copy link
Contributor

@silene silene Apr 2, 2021 •
edited

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I do not understand why this would prevent any inlining. It seems better to use the old code and put the attribute [@inline never] on it:

let [@inline never] rec accumulate data x =
  if x == ret_accu then Obj.repr data
  else Obj.repr (accumulate { data with acc_arg = x :: data.acc_arg })

Another way to prevent inlining (if you do not trust the attribute) is to simply store the accumulator in a public mutable reference.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This doesn't work because we will get partially applied functions, which have not the accumulator code. I need to have a function of arity one that is exactly the one performing accumulation for my trick to work.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Indeed, my mistake. Still, I do not see how your code guarantees the uniqueness of the inner function. Perhaps something like the following would help, but I am not even sure OCaml guarantees that the [@inline] attribute is respected for inner functions.

let rec accumulate data =
  let [@inline never] accfun x =
    if x == ret_accu then Obj.repr data
    else
      let data = { data with acc_arg = x :: data.acc_arg } in
      Obj.repr (accumulate data).accfun in
  { accfun }

Here is another possibility, which is documented (or at least folklore enough to not be broken that easily):

let [@inline never] rec accumulate data = (); fun x ->
  if x == ret_accu then Obj.repr data
  else Obj.repr (accumulate { data with acc_arg = x :: data.acc_arg })

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I believe flambda explicitly breaks the second kind of trick. I witnessed that when observing the code generated by the proof monad with flambda.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

At least, with 4.12.0+flambda, it is compiled as expected, that is, ();fun forces an explicit closure creation.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Quoting Vincent Laviron:

Flambda doesn’t try to coalesce a function returning a function into a function taking more arguments. Some transformations earlier in the compiler do that, but at that point (); will not have been simplified yet so you should be fine.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Other suggestion by Vincent:

let [@inline never] rec accumulate data = Sys.opaque_identity (fun x ->
  if x == ret_accu then Obj.repr data
  else Obj.repr (accumulate { data with acc_arg = x :: data.acc_arg }))

type accfun = { accfun : Obj.t -> Obj.t }

let rec accumulate data = { accfun = fun x ->
if x == ret_accu then Obj.repr data
else
let data = { data with acc_arg = x :: data.acc_arg } in
Obj.repr (accumulate data).accfun
}

let mk_accu (a : atom) : t =
let rec accumulate data x =
if x == ret_accu then Obj.repr data
else
let data = { data with acc_arg = x :: data.acc_arg } in
let ans = Obj.repr (accumulate data) in
let () = Obj.set_tag ans accumulate_tag [@ocaml.warning "-3"] in
ans
in
let acc = { acc_atm = a; acc_arg = [] } in
let ans = Obj.repr (accumulate acc) in
(** FIXME: use another representation for accumulators, this causes naked
pointers. *)
let () = Obj.set_tag ans accumulate_tag [@ocaml.warning "-3"] in
(Obj.obj ans : t)
let ans : t = Obj.magic (accumulate acc).accfun in
(* This will only have an effect if accumulators are not registered yet *)
let () = register_accu ans in
let () = assert (is_accu ans) in
ans

let get_accu (k : accumulator) =
(Obj.magic k : Obj.t -> accu_val) ret_accu
Expand Down Expand Up @@ -247,15 +251,16 @@ type kind_of_value =
| Varray of t Parray.t
| Vblock of block

let array_tag = 0

let kind_of_value (v:t) =
let o = Obj.repr v in
if Obj.is_int o then Vconst (Obj.magic v)
else if Obj.tag o == Obj.double_tag then Vfloat64 (Obj.magic v)
else
let tag = Obj.tag o in
if Int.equal tag accumulate_tag then
if Int.equal (Obj.size o) 1 then Varray (Obj.magic v)
else Vaccu (Obj.magic v)
if is_accu v then Vaccu (Obj.magic v)
else if Int.equal tag array_tag then Varray (Obj.magic v)
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 if (tag < Obj.lazy_tag) then Vblock (Obj.magic v)
Expand Down
2 changes: 2 additions & 0 deletions kernel/nativevalues.mli
View file
Open in desktop
Expand Up @@ -116,6 +116,8 @@ val accu_nargs : accumulator -> int
val cast_accu : t -> accumulator
[@@ocaml.inline always]

val is_closure : 'a -> bool

(* Functions over block: i.e constructors *)

type block
Expand Down