git.iko.soy/Idris-dev
on master help sign in
Move documentation for the C heap to the FFI document
commite65d0fa07bdca399a4c5bf6d456aa8eeefaa16d4 authorAlex Queiroz <asandroq@gmail.com> dateThu 4 Jan 2018, 11:07 (9 years ago) parent97496b7
2 files changed+107−107
compare with master
unifiedsplit
docs/reference/ffi.rst+107 docs/reference/misc.rst−107
docs/reference/ffi.rst+107
@@ -234,6 +234,113 @@ useful to access constants that are preprocessor definitions (like ``INT_MAX``).
234234For more complicated interactions with C (such as reading and setting fields
235235of a C struct), there is a module CFFI available in the contrib package.
236236
237+C heap
238+------
239+
240+Idris has two heaps where objects can be allocated:
241+
242++--------------------------------------+---------------------------------------+
243+| FP heap | C heap |
244++======================================+=======================================+
245+| Cheney-collected | Mark-and-sweep-collected |
246++--------------------------------------+---------------------------------------+
247+| Garbage collections touches only | Garbage collection has to traverse |
248+| live objects. | all registered items. |
249++--------------------------------------+---------------------------------------+
250+| Ideal for FP-style rapid allocation | Ideal for C-style allocation of a few |
251+| of lots of small short-lived pieces | big buffers. |
252+| of memory, such as data constructors.| |
253++--------------------------------------+---------------------------------------+
254+| Finalizers are impossible to support | Items have finalizers that are called |
255+| reasonably. | on deallocation. |
256++--------------------------------------+---------------------------------------+
257+| Data is copied all the time (when | Copying does not happen. |
258+| collecting garbage, modifying data, | |
259+| registering managed pointers, etc.) | |
260++--------------------------------------+---------------------------------------+
261+| Contains objects of various types. | Contains C heap items: ``(void *)`` |
262+| | pointers with finalizers. A finalizer |
263+| | is a routine that deallocates the |
264+| | resources associated with the item. |
265++--------------------------------------+---------------------------------------+
266+| Fixed set of object types. | The data pointer may point |
267+| | to anything, as long as the finalizer |
268+| | cleans up correctly. |
269++--------------------------------------+---------------------------------------+
270+| Not suitable for C resources and | Suitable for C resources and arbitrary|
271+| arbitrary pointers. | pointers. |
272++--------------------------------------+---------------------------------------+
273+| Values form a compact memory block. | Items are kept in a linked list. |
274++--------------------------------------+---------------------------------------+
275+| Any Idris value, most notably | Items represented by the |
276+| ``ManagedPtr``. | Idris type ``CData``. |
277++--------------------------------------+---------------------------------------+
278+| Data of ``ManagedPtr`` allocated | Data allocated in C, pointer copied |
279+| in C, buffer then copied into the FP | into the C heap. |
280+| heap. | |
281++--------------------------------------+---------------------------------------+
282+| Allocation and reallocation not | Allocated and reallocate freely in C, |
283+| possible from C code (without having | registering the allocated items |
284+| a reference to the VM). Everything | in the FFI. |
285+| is copied instead. | |
286++--------------------------------------+---------------------------------------+
287+
288+The FP heap is the primary heap. It may contain values of type ``CData``,
289+which are references to items in the C heap. A C heap item contains
290+a ``(void *)`` pointer and the corresponding finalizer. Once a C heap item
291+is no longer referenced from the FP heap, it is marked as unused and
292+the next GC sweep will call its finalizer and deallocate it.
293+
294+There is no Idris interface for ``CData`` other than its type and FFI.
295+
296+Usage from C code
297+~~~~~~~~~~~~~~~~~
298+
299+* Although not enforced in code, ``CData`` is meant to be opaque
300+ and non-RTS code (such as libraries or C bindings) should
301+ access only its ``(void *)`` field called ``data``.
302+
303+* Feel free to mutate both the pointer ``data`` (eg. after calling ``realloc``)
304+ and the memory it points to. However, keep in mind
305+ that this must not break Idris's referential transparency.
306+
307+* **WARNING!** If you call ``cdata_allocate`` or ``cdata_manage``,
308+ the resulting ``CData`` object *must* be returned from your
309+ FFI function so that it is inserted in the C heap by the RTS.
310+ Otherwise the memory will be leaked.
311+
312+.. code:: idris
313+
314+ some_allocating_fun : Int -> IO CData
315+ some_allocating_fun i = foreign FFI_C "some_allocating_fun" (Int -> IO CData) i
316+
317+ other_fun : CData -> Int -> IO Int
318+ other_fun cd i = foreign FFI_C "other_fun" (CData -> Int -> IO Int) cd i
319+
320+.. code:: cpp
321+
322+ #include "idris_rts.h"
323+
324+ static void finalizer(void * data)
325+ {
326+ MyStruct * ptr = (MyStruct *) data;
327+ free_something(ptr->something);
328+ free(ptr);
329+ }
330+
331+ CData some_allocating_fun(int arg)
332+ {
333+ void * data = (void *) malloc(...);
334+ // ...
335+ return cdata_manage(data, finalizer);
336+ }
337+
338+ int other_fun(CData cd, int arg)
339+ {
340+ int result = foo(cd->data);
341+ return result;
342+ }
343+
237344FFI implementation
238345------------------
239346
docs/reference/misc.rst−107
@@ -100,113 +100,6 @@ follows:
100100 (x :: qsort (assert_smaller (x :: xs) (filter (>= x) xs))))
101101
102102
103−C heap
104−======
105−
106−Idris has two heaps where objects can be allocated:
107−
108−+--------------------------------------+---------------------------------------+
109−| FP heap | C heap |
110−+======================================+=======================================+
111−| Cheney-collected | Mark-and-sweep-collected |
112−+--------------------------------------+---------------------------------------+
113−| Garbage collections touches only | Garbage collection has to traverse |
114−| live objects. | all registered items. |
115−+--------------------------------------+---------------------------------------+
116−| Ideal for FP-style rapid allocation | Ideal for C-style allocation of a few |
117−| of lots of small short-lived pieces | big buffers. |
118−| of memory, such as data constructors.| |
119−+--------------------------------------+---------------------------------------+
120−| Finalizers are impossible to support | Items have finalizers that are called |
121−| reasonably. | on deallocation. |
122−+--------------------------------------+---------------------------------------+
123−| Data is copied all the time (when | Copying does not happen. |
124−| collecting garbage, modifying data, | |
125−| registering managed pointers, etc.) | |
126−+--------------------------------------+---------------------------------------+
127−| Contains objects of various types. | Contains C heap items: ``(void *)`` |
128−| | pointers with finalizers. A finalizer |
129−| | is a routine that deallocates the |
130−| | resources associated with the item. |
131−+--------------------------------------+---------------------------------------+
132−| Fixed set of object types. | The data pointer may point |
133−| | to anything, as long as the finalizer |
134−| | cleans up correctly. |
135−+--------------------------------------+---------------------------------------+
136−| Not suitable for C resources and | Suitable for C resources and arbitrary|
137−| arbitrary pointers. | pointers. |
138−+--------------------------------------+---------------------------------------+
139−| Values form a compact memory block. | Items are kept in a linked list. |
140−+--------------------------------------+---------------------------------------+
141−| Any Idris value, most notably | Items represented by the |
142−| ``ManagedPtr``. | Idris type ``CData``. |
143−+--------------------------------------+---------------------------------------+
144−| Data of ``ManagedPtr`` allocated | Data allocated in C, pointer copied |
145−| in C, buffer then copied into the FP | into the C heap. |
146−| heap. | |
147−+--------------------------------------+---------------------------------------+
148−| Allocation and reallocation not | Allocated and reallocate freely in C, |
149−| possible from C code (without having | registering the allocated items |
150−| a reference to the VM). Everything | in the FFI. |
151−| is copied instead. | |
152−+--------------------------------------+---------------------------------------+
153−
154−The FP heap is the primary heap. It may contain values of type ``CData``,
155−which are references to items in the C heap. A C heap item contains
156−a ``(void *)`` pointer and the corresponding finalizer. Once a C heap item
157−is no longer referenced from the FP heap, it is marked as unused and
158−the next GC sweep will call its finalizer and deallocate it.
159−
160−There is no Idris interface for ``CData`` other than its type and FFI.
161−
162−Usage from C code
163−-----------------
164−
165−* Although not enforced in code, ``CData`` is meant to be opaque
166− and non-RTS code (such as libraries or C bindings) should
167− access only its ``(void *)`` field called ``data``.
168−
169−* Feel free to mutate both the pointer ``data`` (eg. after calling ``realloc``)
170− and the memory it points to. However, keep in mind
171− that this must not break Idris's referential transparency.
172−
173−* **WARNING!** If you call ``cdata_allocate`` or ``cdata_manage``,
174− the resulting ``CData`` object *must* be returned from your
175− FFI function so that it is inserted in the C heap by the RTS.
176− Otherwise the memory will be leaked.
177−
178−.. code:: idris
179−
180− some_allocating_fun : Int -> IO CData
181− some_allocating_fun i = foreign FFI_C "some_allocating_fun" (Int -> IO CData) i
182−
183− other_fun : CData -> Int -> IO Int
184− other_fun cd i = foreign FFI_C "other_fun" (CData -> Int -> IO Int) cd i
185−
186−.. code:: cpp
187−
188− #include "idris_rts.h"
189−
190− static void finalizer(void * data)
191− {
192− MyStruct * ptr = (MyStruct *) data;
193− free_something(ptr->something);
194− free(ptr);
195− }
196−
197− CData some_allocating_fun(int arg)
198− {
199− void * data = (void *) malloc(...);
200− // ...
201− return cdata_manage(data, finalizer);
202− }
203−
204− int other_fun(CData cd, int arg)
205− {
206− int result = foo(cd->data);
207− return result;
208− }
209−
210103Preorder reasoning
211104==================
212105