max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
15787 commits 1 branch 0 tags 5.3 GiB
Commit graph

156 commits

Author SHA1 Message Date
Leonardo de Moura
2a0f5186e8 fix(runtime/object): bug at array_push 
Small object allocator was masking this bug.
 2019-02-26 14:19:37 -08:00
Leonardo de Moura
5635057549 feat(runtime/object): improve m_queue 2019-02-26 09:15:00 -08:00
Leonardo de Moura
f2ef0eb597 fix(runtime/alloc): bug at import_objs 2019-02-26 07:34:26 -08:00
Leonardo de Moura
a9458fdcb3 chore(runtime/alloc): remove incorrect assertion 2019-02-26 07:33:53 -08:00
Leonardo de Moura
1f3de14f9c fix(runtime/object): embarrassing bug at del_core 2019-02-25 17:42:56 -08:00
Leonardo de Moura
3a252f5b55 chore(runtime/object): avoid overhead when SMALL_ALLOCATOR is disabled 2019-02-25 15:32:59 -08:00
Leonardo de Moura
66b55d9d12 chore(CMakeLists.txt): add options for enabling/disabling LAZY_RC and SMALL_ALLOCATOR 2019-02-24 15:11:48 -08:00
Leonardo de Moura
67d197a2e0 fix(runtime/object): correct support for objects without RC 
Lean was not crashing because we do not have region objects yet, and
the persistent objects still have a RC.
 2019-02-24 09:29:20 -08:00
Leonardo de Moura
935d90e77c chore(runtime/object): disable lazy RC to collect data at speedcenter 2019-02-23 17:37:11 -08:00
Leonardo de Moura
abd0f89820 feat(runtime): avoid extra switch 2019-02-23 17:35:21 -08:00
Leonardo de Moura
4b44c5ce36 feat(runtime/object): small object allocator 2019-02-23 17:17:56 -08:00
Leonardo de Moura
a9276c8834 fix(runtime/object): incorrect { 2019-02-23 17:16:49 -08:00
Leonardo de Moura
feea8ecccd feat(library/compiler/llnf): avoid inc/dec operations on persistent objects 
inc/dec operations are noop's for persistent objects.
 2019-02-18 20:22:18 -08:00
Leonardo de Moura
b752dd1984 fix(library/compiler/emit_cpp): mark global objects as persistent 
They may be used by tasks, but they are not directly reachable from
task starting point.
 2019-02-17 11:45:51 -08:00
Leonardo de Moura
8ac1a1969d fix(runtime/object): task.bind and task.map should also invoke to_mt 2019-02-17 11:11:41 -08:00
Leonardo de Moura
827021a6c5 feat(runtime/object): given mk_task(o), mark objects reachable from o as MTHeap 2019-02-17 10:29:41 -08:00
Leonardo de Moura
d100f95469 feat(runtime/object): make dbg_trace thread safe 2019-02-17 09:50:55 -08:00
Leonardo de Moura
7623f64b5e feat(runtime,library/init/util): add some debugging helper function 2019-02-17 09:22:37 -08:00
Leonardo de Moura
9e0b28d8ce feat(library/init/data/array/basic): improve 2019-02-16 16:08:10 -08:00
Leonardo de Moura
3c73c43ab2 feat(runtime,library/init/data/array/basic): add builtin support for arrays 2019-02-16 15:27:23 -08:00
Leonardo de Moura
00b177ad54 chore(runtime/object): enable Lazy RC by default 
@kha I tried a compiling a few .lean examples using Lazy RC, and I did
not observe any significant increase in memory consumption.
 2019-02-15 12:10:57 -08:00
Leonardo de Moura
06f1a2b1a0 feat(runtime/object): lazy RC 
In this commit, we replace the option `LEAN_DEFERRED_FREE` with
`LEAN_LAZY_RC`. The idea is to match the nomenclature used in the
literature. See paper:
https://dl.acm.org/citation.cfm?id=964019
The following slide deck summarizes the paper:
http://www.hboehm.info/popl04/refcnt.pdf

We also implement the very simple approach described on this paper
where a `del(o)` just puts `o` in the "to free" list, and each
allocation frees at most one object. As pointed out in the paper
above lazy RC may prevent a lot of memory from being reclaimed.
For now, I am keeping the new option disabled.

That being said, the test `arith_eval_nat.lean` is 29% faster when
using lazy RC, and beats the OCaml version.

In the following paper
https://www.microsoft.com/en-us/research/wp-content/uploads/2017/01/tm567-1.pdf
a separate thread keeps processing the "to free" list. However, I
think this approach is not compatible with our
`object_memory_kind::STHeap` trick.

Tomorrow, I will measure the space overhead when compiling the Lean
corelib using Lazy RC using my linux desktop

cc @kha
 2019-02-14 17:41:11 -08:00
Sebastian Ullrich
956a047d1e chore(library/compiler/extern_attribute): style 2019-02-14 14:07:05 -08:00
Sebastian Ullrich
7cffe6935e feat(frontends/lean/vm_elaborator): port to new runtime 2019-02-14 14:07:05 -08:00
Leonardo de Moura
03d5ac2a3c feat(runtime): add LEAN_DEFERRED_FREE compilation option 
It prevents the runtime from performing arbitrarily long pauses when
invoking `del`.
 2019-02-14 10:40:10 -08:00
Leonardo de Moura
b722885137 feat(library/init/io): add unsafe_io and timeit 2019-02-13 16:59:24 -08:00
Leonardo de Moura
e10240fe5c refactor(runtime/io): use extern "C" for io primitives 2019-02-13 11:21:29 -08:00
Leonardo de Moura
4627929a83 refactor(boot,runtime,util): move name runtime implementation to util/name, and use "extern C" ABI 2019-02-13 08:27:23 -08:00
Leonardo de Moura
425a4b70d1 feat(library/init/data/int/basic): use extern attribute, and fix div/mod mess 
Now, int.div and int.mod behave like C++ `/` and `%` for int,
moreover, they satisfy

          (a/b)*b + (a%b) = a
 2019-02-12 11:41:46 -08:00
Leonardo de Moura
6be47dfb97 feat(library/init/data/string/basic): use extern attribute 2019-02-11 17:54:24 -08:00
Sebastian Ullrich
ece423300b fix(runtime/object): avoid implicit string allocation in string.iterator.curr/next/remove 2019-02-09 14:18:04 +01:00
Leonardo de Moura
434627ee8e chore(runtime/io): implement io.prim.put_str just to be able to test 2019-02-06 14:35:13 -08:00
Leonardo de Moura
fbc6c47094 chore(boot): update 2019-02-06 09:59:22 -08:00
Sebastian Ullrich
83e0c35204 chore(runtime/object): closure double-free assert 2019-02-06 09:38:35 -08:00
Leonardo de Moura
c4e8770342 feat(runtime,boot): second part of the previous commit 2019-02-05 16:28:18 -08:00
Leonardo de Moura
2058d33d07 feat(runtime,library/compiler): add name.dec_eq builtin 2019-02-05 14:36:02 -08:00
Leonardo de Moura
eb57a904af chore(runtime): avoid overloads 2019-02-05 14:04:29 -08:00
Leonardo de Moura
3444a295e7 feat(library/compiler,runtime): builtin support for lean.name 2019-02-05 12:57:46 -08:00
Leonardo de Moura
579ac58b62 chore(runtime/object): expose thunk_map and thunk_bind 2019-02-04 13:11:37 -08:00
Leonardo de Moura
98edae152a fix(runtime): replace lean::alloca with macro 
Functions using `alloca` are not inlined even when marked with
`inline` in some compilers.

Remark: GCC will _not_ inline a function calling alloca unless it is
annotated with always_inline.
 2019-02-04 09:36:53 -08:00
Leonardo de Moura
0918a599ae feat(*): builtin support for uint functions 
@kha The VM versions just throw exceptions. They are just stubs to
make sure we can compile Lean.
I implemented the uint functions in the new runtime, but there are a
few missing cases marked with TODO.
I needed these builtins to be able to compile the C++ generated code for
corelib.
 2019-02-01 17:04:24 -08:00
Sebastian Ullrich
a8f668a3d2 feat(runtime/object): add LEAN_FAKE_FREE option to disable freeing runtime objects while debugging 2019-02-01 16:33:18 +01:00
Sebastian Ullrich
c162ec9583 fix(runtime/object): mk_option_some 2019-02-01 16:33:13 +01:00
Sebastian Ullrich
e3afa47c9e fix(runtime/object): fix some string primitives 2019-02-01 16:33:11 +01:00
Sebastian Ullrich
e0fc2a7812 feat(runtime/object): string_to_std 2019-02-01 16:32:52 +01:00
Leonardo de Moura
4166851574 feat(library/compiler/emit_cpp): emit_box and emit_unbox 2019-01-31 16:16:30 -08:00
Leonardo de Moura
7c3354f15f feat(library/compiler/emit_cpp): emit_reset 2019-01-31 12:33:17 -08:00
Leonardo de Moura
d2cbf9584f feat(library/compiler/emit_cpp): emit _apply instruction 2019-01-30 14:37:21 -08:00
Leonardo de Moura
bb43567273 fix(runtime/object): typos 2019-01-29 16:03:40 -08:00
Sebastian Ullrich
ead4e8998d feat(library/init/lean/elaborator): elaborate constants 2018-12-19 15:04:48 +01:00