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

59 commits

Author SHA1 Message Date
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
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
2058d33d07 feat(runtime,library/compiler): add name.dec_eq builtin 2019-02-05 14:36:02 -08:00
Leonardo de Moura
3444a295e7 feat(library/compiler,runtime): builtin support for lean.name 2019-02-05 12:57:46 -08: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
70c4e33cf2 feat(runtime/object): missing string.iterator builtin functions 2018-11-15 13:05:29 -08:00
Leonardo de Moura
a3db4e8e09 chore(*): style 2018-11-15 10:59:17 -08:00
Leonardo de Moura
efa703d2b5 feat(runtime): implement string.iterator primitives in the new runtime 
Some of the primitives do not have optimal implementation.

@Kha Could you please check if everything we use in the parser has a
reasonable implementation?
 2018-11-15 10:42:23 -08:00
Leonardo de Moura
23202bada1 chore(runtime/object): allow shared objects at string_append and string_push 2018-11-14 16:30:23 -08:00
Leonardo de Moura
46d6f7bfb5 chore(runtime/object): store function pointer as void * inside closure 2018-09-11 14:27:45 -07:00
Leonardo de Moura
5bc9b07ab9 feat(runtime/object): split Heap into MTHeap and STHeap 2018-09-09 14:46:28 -07:00
Leonardo de Moura
0573d7e1d5 fix(runtime/object): parray RC bugs 2018-09-09 12:04:27 -07:00
Leonardo de Moura
b45ac3fcc0 chore(runtime/object): minor 2018-09-09 10:59:36 -07:00
Leonardo de Moura
36423e4389 fix(runtime): parray memory leaks 2018-09-09 10:33:15 -07:00
Leonardo de Moura
4863ca071a chore(runtime): make sure we use the same naming convention for getters and setters 2018-09-09 10:07:00 -07:00
Leonardo de Moura
8f195515a6 feat(runtime): add persistent arrays to runtime 2018-09-09 09:44:38 -07:00
Leonardo de Moura
3e528a9b67 chore(runtime): fix assertions 2018-08-28 10:33:22 -07:00
Leonardo de Moura
030669ea4d feat(runtime): do not waste space with RC for region and stack allocated objects 
The modification introduces an overhead of 1.5% on the
execution time. Here is the the time for compiling the corelib

Before: 8.61 secs (avg of 3 runs)
After:  8.74 secs (avg of 3 runs)

On the other hand, the size of the compacted region for the command
`#compact_tst 10` is smaller.

Before: 176687728
After:  153794704

The size before this change was 14.8% bigger.

For reference, using the old serializer we generate a buffer of size 105291117.

cc @kha
 2018-08-28 07:41:55 -07:00
Leonardo de Moura
fdcbf3fe9e chore(runtime/object): "section comments" 2018-08-22 17:53:11 -07:00
Leonardo de Moura
3ab1ebcb3f feat(init/core): add task 2018-08-21 16:10:07 -07:00
Leonardo de Moura
0b349f1abf chore(*): fix style 2018-08-21 09:32:01 -07:00
Leonardo de Moura
dc1f5c0aa6 feat(runtime/object): task API functions can take thunks as arguments 2018-08-20 09:13:35 -07:00
Leonardo de Moura
db98397cc0 feat(runtime): object compactor 
We need more testing and performance testing.
We also need to compare serializer and compacted_region.
 2018-08-19 17:10:18 -07:00
Leonardo de Moura
684085d93f refactor(runtime/object): delete data needed to execute task after it finishes 2018-08-18 14:33:27 -07:00
Leonardo de Moura
a0b5502821 fix(runtime/object): memory leak and simplify task_object 
We remove per task condition_variable and use m_task_finished_cv.
The same condition_variable used to implement `wait_any`.
 2018-08-18 10:29:12 -07:00
Leonardo de Moura
d0bc663f0d chore(runtime/object): avoid ugly handle_finished_rec 
Users should not rely on the order the dependencies have beed inserted.
If the order matters, priorities should be used instead.
 2018-08-17 18:15:58 -07:00
Leonardo de Moura
d52507c4b2 fix(runtime/object): memory leak 2018-08-17 18:12:17 -07:00
Leonardo de Moura
861592fe6a chore(runtime/object): cleanup 2018-08-17 15:43:01 -07:00
Leonardo de Moura
4bc8414d2b feat(runtime/object): use "weak pointers" in the task manager, and interrupt tasks at GC time 2018-08-17 15:35:00 -07:00
Leonardo de Moura
24444d65c4 refactor(runtime/object): do not use Lean runtime lists to implement the reverse dependency list in task objects 2018-08-17 14:42:43 -07:00
Leonardo de Moura
1d5411f455 feat(runtime/object): add support for io.wait_any 2018-08-17 13:04:06 -07:00
Leonardo de Moura
5f78087b08 feat(runtime/object): add support for io.has_finished 2018-08-17 12:36:48 -07:00
Leonardo de Moura
5e63e7806c chore(runtime/object): cleanup 2018-08-17 12:32:47 -07:00
Leonardo de Moura
ae9eac6781 feat(runtime/object): simplify and more tests 2018-08-17 09:41:22 -07:00
Leonardo de Moura
c863e86429 feat(runtime/object): primitives for interrupting threads 2018-08-17 09:25:40 -07:00
Leonardo de Moura
0a2e9c109f fix(runtime/object): memory leak and violation at task_bind 2018-08-17 09:03:45 -07:00
Leonardo de Moura
f5ecd8477f fix(runtime/object): memory leak 2018-08-17 08:47:29 -07:00
Leonardo de Moura
168eaefff5 fix(runtime/object): finalization and avoid leak 2018-08-17 08:32:33 -07:00
Leonardo de Moura
cc13c8ee7f refactor(runtime/object): remove unnecessary, fix malloc/delete mismatch 2018-08-17 08:10:05 -07:00
Leonardo de Moura
018542e2e1 fix(runtime/object): task bugs 2018-08-16 21:28:58 -07:00
Leonardo de Moura
066fbf2d5b refactor(runtime/object): remove state field 2018-08-16 20:46:14 -07:00
Leonardo de Moura
584eddee01 feat(runtime/object): add support for tasks 
This is just the first draft. We still need a lot of testing.
 2018-08-16 19:09:50 -07:00
Leonardo de Moura
c3be026645 chore(runtime/object): document calling convention for runtime primitives 2018-08-15 20:10:43 -07:00
Leonardo de Moura
74d94432da fix(runtime/object): make thunk_get thread safe 2018-08-15 15:34:15 -07:00
Leonardo de Moura
bcb37ef862 feat(runtime): thunk serialization 2018-08-14 15:15:12 -07:00
Leonardo de Moura
6eb598268d chore(runtime/object): naming convention 
`dec_ref` methods assume the input object is *not* a scalar
 2018-08-10 18:11:29 -07:00