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.mli | 1 -
 1 file changed, 1 deletion(-)

(limited to 'kernel/vmvalues.mli')

diff --git a/kernel/vmvalues.mli b/kernel/vmvalues.mli
index f6efd49cfc..ee3e2bd5fc 100644
--- a/kernel/vmvalues.mli
+++ b/kernel/vmvalues.mli
@@ -181,7 +181,6 @@ val rec_args : vfix -> int array
 val first_fix : vfix -> vfix
 val fix_types : vfix -> tcode array
 val cofix_types : vcofix -> tcode array
-external offset_closure_fix : vfix -> int -> vm_env = "coq_offset_closure"
 val mk_fix_body : int -> int -> vfix -> vfun array
 
 (** CoFix *)
-- 
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.mli | 2 --
 1 file changed, 2 deletions(-)

(limited to 'kernel/vmvalues.mli')

diff --git a/kernel/vmvalues.mli b/kernel/vmvalues.mli
index ee3e2bd5fc..6632dc46b2 100644
--- a/kernel/vmvalues.mli
+++ b/kernel/vmvalues.mli
@@ -27,8 +27,6 @@ type to_update
 
 type tag = int
 
-val accu_tag : tag
-
 val type_atom_tag : tag
 val max_atom_tag : tag
 val proj_tag : tag
-- 
cgit v1.2.3