diff options
| author | Guillaume Melquiond | 2020-08-26 13:37:20 +0200 |
|---|---|---|
| committer | Guillaume Melquiond | 2020-11-13 15:13:23 +0100 |
| commit | 930e51c23f5a8778af02f7a971a404860d713346 (patch) | |
| tree | c82395fe93c70dd2e088b09958d27c7c42beb30c /kernel | |
| parent | 51e759fb2ff92dd89ab4823ddea3ea81be7f8046 (diff) | |
Optimize handling of the VM stack with respect to the GC.
1. There is no point in marking plain integers as GC roots.
2. There is no need to restore the stack pointer, as the stack is not
allocated on the OCaml heap (contrarily to coq_env).
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/byterun/coq_interp.c | 2 | ||||
| -rw-r--r-- | kernel/byterun/coq_memory.c | 3 |
2 files changed, 3 insertions, 2 deletions
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 1b6da7dd6f..3bee36b667 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -113,7 +113,7 @@ if (sp - num_args < coq_stack_threshold) { \ #define Setup_for_gc { sp -= 2; sp[0] = accu; sp[1] = coq_env; coq_sp = sp; } #define Restore_after_gc { accu = sp[0]; coq_env = sp[1]; sp += 2; } #define Setup_for_caml_call { *--sp = coq_env; coq_sp = sp; } -#define Restore_after_caml_call { sp = coq_sp; coq_env = *sp++; } +#define Restore_after_caml_call coq_env = *sp++; /* Register optimization. Some compilers underestimate the use of the local variables representing diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c index ae5251c252..fe076f8f04 100644 --- a/kernel/byterun/coq_memory.c +++ b/kernel/byterun/coq_memory.c @@ -65,9 +65,10 @@ static void coq_scan_roots(scanning_action action) register value * i; /* Scan the stack */ for (i = coq_sp; i < coq_stack_high; i++) { + if (!Is_block(*i)) continue; #ifdef NO_NAKED_POINTERS /* The VM stack may contain C-allocated bytecode */ - if (Is_block(*i) && !Is_in_heap_or_young(*i)) continue; + if (!Is_in_heap_or_young(*i)) continue; #endif (*action) (*i, i); }; |